New tactic to rewrite decidability lemmas when one knows which side

is true. E.g. "decide (eq_nat_dec n 0) with H" on

  H: n=0 |- (if eq_nat_dec n 0 then 1 else 2) = 1

returns

  H: n=0 |- 1 = 1 .

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12291 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 29 insertions, 0 deletions

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 52b5012a9..39cd268d9 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -10,6 +10,7 @@
 
 Require Import Notations.
 Require Import Logic.
+Require Import Specif.
 
 (** * Useful tactics *)
 
@@ -173,4 +174,32 @@ Ltac easy :=
 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.