- 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

1 files changed, 38 insertions, 9 deletions

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.