Merge branch 'msammler/add_hypothesis' into 'master'

Add tactic `learn_hyp`, fixes #73

Closes #73

See merge request iris/stdpp!247

theories/gmultiset.v

@@ -254,19 +254,10 @@ Ltac multiset_instantiate :=
      let e := fresh in evar (e:A);
      let e' := eval unfold e in e in clear e;
      lazymatch constr:(P e') with
-     | context [ {[ ?y ]} ] =>
-        (* Use [unless] to avoid creating a new hypothesis [H y : P y] if [P y]
-        already exists. *)
-        unify y e'; unless (P y) by assumption; pose proof (H y)
+     | context [ {[ ?y ]} ] => unify y e'; learn_hyp (H y)
      end
-  | H : (∀ x : ?A, @?P x), _ : context [multiplicity ?y _] |- _ =>
-     (* Use [unless] to avoid creating a new hypothesis [H y : P y] if [P y]
-     already exists. *)
-     unless (P y) by assumption; pose proof (H y)
-  | H : (∀ x : ?A, @?P x) |- context [multiplicity ?y _] =>
-     (* Use [unless] to avoid creating a new hypothesis [H y : P y] if [P y]
-     already exists. *)
-     unless (P y) by assumption; pose proof (H y)
+  | H : (∀ x : ?A, _), _ : context [multiplicity ?y _] |- _ => learn_hyp (H y)
+  | H : (∀ x : ?A, _) |- context [multiplicity ?y _] => learn_hyp (H y)
   end.
 
 (** Step 4: simplify singletons *)

theories/tactics.v

@@ -525,6 +525,18 @@ Definition block {A : Type} (a : A) := a.
 Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
 Ltac unblock_goal := unfold block in *.
 
+(** [learn_hyp p as H] and [learn_hyp p], where [p] is a proof of [P],
+add [P] to the context and fail if [P] already exists in the context.
+This is a simple form of the learning pattern. These tactics are
+inspired by [Program.Tactics.add_hypothesis]. *)
+Tactic Notation "learn_hyp" constr(p) "as" ident(H') :=
+  let P := type of p in
+  match goal with
+  | H : P |- _ => fail 1
+  | _ => pose proof p as H'
+  end.
+Tactic Notation "learn_hyp" constr(p) :=
+  let H := fresh in learn_hyp p as H.
 
 (** The tactic [select pat tac] finds the last (i.e., bottommost) hypothesis
 matching [pat] and passes it to the continuation [tac]. Its main advantage over