From 56a9fc6b6f0d0e1bbdb5365cf19d42a73d59fe5e Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 15 Apr 2021 09:20:39 +0200
Subject: [PATCH] Add [learn_hyp_named] and [learn_hyp], fixes #73

---
 theories/gmultiset.v | 15 +++------------
 theories/tactics.v   | 12 ++++++++++++
 2 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 1b4a1568..a6782d0e 100644
--- a/theories/gmultiset.v
+++ b/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 *)
diff --git a/theories/tactics.v b/theories/tactics.v
index f7bd6468..39543e5f 100644
--- a/theories/tactics.v
+++ b/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
-- 
GitLab