From d6615c44439319e99615474cef465d25422a070d Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 26 Dec 2008 20:26:44 +0000 Subject: - Extracted from the tactic "now" an experimental tactic "easy" for small automation. - Permitted to use evars in the intermediate steps of "apply in" (as expected in the test file apply.v). - Back on the systematic use of eq_rect (r11697) for implementing rewriting (some proofs, especially lemma DistOoVv in Lyon/RulerCompassGeometry/C14_Angle_Droit.v and tactic compute_vcg in Sophia-Antipolis/Semantics/example2.v are explicitly refering to the name of the lemmas used for rewriting). - Fixed at the same time a bug in get_sort_of (predicativity of Set was not taken into account). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11717 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Init/Tactics.v | 47 ++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 38 insertions(+), 9 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 705fb3bdf..0e8b4ab1f 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -115,7 +115,7 @@ lazymatch T with evar (a : t); pose proof (H a) as H1; unfold a in H1; clear a; clear H; rename H1 into H; find_equiv H | ?A <-> ?B => idtac -| _ => fail "The given statement does not seem to end with an equivalence" +| _ => fail "The given statement does not seem to end with an equivalence." end. Ltac bapply lemma todo := @@ -135,14 +135,43 @@ bapply lemma ltac:(fun H => destruct H as [H _]; apply H in J). Tactic Notation "apply" "<-" constr(lemma) "in" ident(J) := bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J). -(** A tactic simpler than auto that is useful for ending proofs "in one step" *) -Tactic Notation "now" tactic(t) := -t; -match goal with -| H : _ |- _ => solve [inversion H] -| _ => solve [trivial | reflexivity | symmetry; trivial | discriminate | split] -| _ => fail 1 "Cannot solve this goal" -end. +(** An experimental tactic simpler than auto that is useful for ending + proofs "in one step" *) + +Ltac easy := +(* + let rec use_hyp H := + match type of H with + | _ /\ _ => + | _ => solve [inversion H] + end + with destruct_hyp H := + match type of H with + | _ /\ _ => case H; do_intro; do_intro + | _ => idtac + end +*) + let rec use_hyp H := + match type of H with + | _ /\ _ => exact H || destruct_hyp H + | _ => try solve [inversion H] + end + with do_intro := let H := fresh in intro H; use_hyp H + with destruct_hyp H := case H; clear H; do_intro; do_intro in + let rec use_hyps := + match goal with + | H : _ /\ _ |- _ => exact H || (destruct_hyp H; use_hyps) + | H : _ |- _ => solve [inversion H] + | _ => idtac + end in + let rec do_atom := + solve [reflexivity | symmetry; trivial] || + contradiction || + (split; do_atom) + with do_ccl := trivial; repeat do_intro; do_atom in + (use_hyps; do_ccl) || fail "Cannot solve this goal". + +Tactic Notation "now" tactic(t) := t; easy. (** A tactic to document or check what is proved at some point of a script *) Ltac now_show c := change c. -- cgit v1.2.3