### Add [learn_hyp_named] and [learn_hyp], fixes #73

parent 77cb2b8a
 ... ... @@ -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 *) ... ...
 ... ... @@ -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 ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment