Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 64 insertions, 21 deletions

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 48b4568d..3e860fd4 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -6,45 +6,52 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Tactics.v 13198 2010-06-25 22:36:20Z letouzey $ i*)
+(*i $Id$ i*)
 
 Require Import Notations.
 Require Import Logic.
+Require Import Specif.
 
 (** * Useful tactics *)
 
-(** A tactic for proof by contradiction. With contradict H, 
+(** Ex falso quodlibet : a tactic for proving False instead of the current goal.
+    This is just a nicer name for tactics such as [elimtype False]
+    and other [cut False]. *)
+
+Ltac exfalso := elimtype False.
+
+(** A tactic for proof by contradiction. With contradict H,
     -   H:~A |-  B    gives       |-  A
     -   H:~A |- ~B    gives  H: B |-  A
     -   H: A |-  B    gives       |- ~A
     -   H: A |- ~B    gives  H: B |- ~A
     -   H:False leads to a resolved subgoal.
-   Moreover, negations may be in unfolded forms, 
+   Moreover, negations may be in unfolded forms,
    and A or B may live in Type *)
 
 Ltac contradict H :=
   let save tac H := let x:=fresh in intro x; tac H; rename x into H
-  in 
-  let negpos H := case H; clear H 
-  in 
+  in
+  let negpos H := case H; clear H
+  in
   let negneg H := save negpos H
   in
-  let pospos H := 
-    let A := type of H in (elimtype False; revert H; try fold (~A))
+  let pospos H :=
+    let A := type of H in (exfalso; revert H; try fold (~A))
   in
   let posneg H := save pospos H
-  in 
-  let neg H := match goal with 
+  in
+  let neg H := match goal with
    | |- (~_) => negneg H
    | |- (_->False) => negneg H
    | |- _ => negpos H
-  end in 
-  let pos H := match goal with 
+  end in
+  let pos H := match goal with
    | |- (~_) => posneg H
    | |- (_->False) => posneg H
    | |- _ => pospos H
   end in
-  match type of H with 
+  match type of H with
    | (~_) => neg H
    | (_->False) => neg H
    | _ => (elim H;fail) || pos H
@@ -52,20 +59,20 @@ Ltac contradict H :=
 
 (* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
 
-Ltac swap H := 
+Ltac swap H :=
   idtac "swap is OBSOLETE: use contradict instead.";
   intro; apply H; clear H.
 
 (* To contradict an hypothesis without copying its type. *)
 
-Ltac absurd_hyp H := 
+Ltac absurd_hyp H :=
   idtac "absurd_hyp is OBSOLETE: use contradict instead.";
-  let T := type of H in 
+  let T := type of H in
   absurd T.
 
 (* A useful complement to contradict. Here H:A while G allows to conclude ~A *)
 
-Ltac false_hyp H G := 
+Ltac false_hyp H G :=
   let T := type of H in absurd T; [ apply G | assumption ].
 
 (* A case with no loss of information. *)
@@ -76,13 +83,21 @@ Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
 
 Tactic Notation "destruct_with_eqn" constr(x) :=
   destruct x as []_eqn.
-Tactic Notation "destruct_with_eqn" ident(n) := 
+Tactic Notation "destruct_with_eqn" ident(n) :=
   try intros until n; destruct n as []_eqn.
 Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) :=
   destruct x as []_eqn:H.
-Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) := 
+Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) :=
   try intros until n; destruct n as []_eqn:H.
 
+(** Break every hypothesis of a certain type *)
+
+Ltac destruct_all t :=
+ match goal with
+  | x : t |- _ => destruct x; destruct_all t
+  | _ => idtac
+ end.
+
 (* Rewriting in all hypothesis several times everywhere *)
 
 Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
@@ -148,7 +163,7 @@ bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
 
 (** 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
@@ -167,14 +182,42 @@ Ltac easy :=
     solve [reflexivity | symmetry; trivial] ||
     contradiction ||
     (split; do_atom)
-  with do_ccl := trivial; repeat do_intro; do_atom in
+  with do_ccl := trivial with eq_true; 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.
 
+(** Support for rewriting decidability statements *)
+
+Set Implicit Arguments.
+
+Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}),
+  C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide.
+Proof.
+intros; destruct decide. apply H0. contradiction.
+Qed.
+
+Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}),
+  ~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide.
+Proof.
+intros; destruct decide. contradiction. apply H0.
+Qed.
+
+Tactic Notation "decide" constr(lemma) "with" constr(H) :=
+  let try_to_merge_hyps H :=
+     try (clear H; intro H) ||
+     (let H' := fresh H "bis" in intro H'; try clear H') ||
+     (let H' := fresh in intro H'; try clear H') in
+  match type of H with
+  | ~ ?C => apply (decide_right lemma H); try_to_merge_hyps H
+  | ?C -> False => apply (decide_right lemma H); try_to_merge_hyps H
+  | _ => apply (decide_left lemma H); try_to_merge_hyps H
+  end.
+
 (** Clear an hypothesis and its dependencies *)
 
 Tactic Notation "clear" "dependent" hyp(h) :=