reflexive tauto

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

7 files changed, 1871 insertions, 0 deletions

diff --git a/contrib/rtauto/Bintree.v b/contrib/rtauto/Bintree.v
new file mode 100644
index 000000000..ee66f02a9
--- /dev/null
+++ b/contrib/rtauto/Bintree.v
@@ -0,0 +1,498 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+Require Export List.
+Require Export BinPos.
+
+Unset Boxed Definitions.
+
+Open Scope positive_scope.
+
+Ltac clean := try (simpl; congruence). 
+Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
+
+Functional Scheme Pcompare_ind := Induction for Pcompare.
+
+Lemma Prect : forall P : positive -> Type,
+       P 1 ->
+       (forall n : positive, P n -> P (Psucc n)) -> forall p : positive, P p.
+intros P H1 Hsucc n; induction n.
+rewrite <- plus_iter_xI; apply Hsucc; apply iterate_add; assumption.
+rewrite <- plus_iter_xO; apply iterate_add; assumption.
+assumption.
+Qed.
+
+Lemma Gt_Eq_Gt : forall p q cmp,
+       (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt.
+apply (Pcompare_ind (fun p q cmp => (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt));
+simpl;auto;congruence.
+Qed.
+
+Lemma Gt_Lt_Gt : forall p q cmp,
+       (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt.
+apply (Pcompare_ind (fun p q cmp => (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt));
+simpl;auto;congruence.
+Qed.
+
+Lemma Gt_Psucc_Eq: forall p q,
+  (p ?= Psucc q) Gt = Gt -> (p ?= q) Eq = Gt.
+intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence.
+intro;apply Gt_Eq_Gt;auto.
+apply Gt_Lt_Gt.
+Qed.
+
+Lemma Eq_Psucc_Gt: forall p q,
+  (p ?= Psucc q) Eq = Eq -> (p ?= q) Eq = Gt.
+intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence.
+intro H;elim (Pcompare_not_Eq p (Psucc q));tauto.
+intro H;apply Gt_Eq_Gt;auto.
+intro H;rewrite Pcompare_Eq_eq with p q;auto.
+generalize q;clear q IHq p H;induction q;simpl;auto.
+intro H;elim (Pcompare_not_Eq p q);tauto.
+Qed.
+
+Lemma Gt_Psucc_Gt : forall n p cmp cmp0,
+ (n?=p) cmp = Gt -> (Psucc n?=p) cmp0 = Gt.
+induction n;intros [ | p | p];simpl;try congruence.
+intros; apply IHn with cmp;trivial.
+intros; apply IHn with Gt;trivial.
+intros;apply Gt_Lt_Gt;trivial.
+intros [ | | ] _ H.
+apply Gt_Eq_Gt;trivial.
+apply Gt_Lt_Gt;trivial.
+trivial.
+Qed.
+
+Lemma Gt_Psucc: forall p q,
+       (p ?= Psucc q) Eq = Gt -> (p ?= q) Eq = Gt.
+intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence.
+apply Gt_Psucc_Eq.
+intro;apply Gt_Eq_Gt;apply IHq;auto.
+apply Gt_Eq_Gt.
+apply Gt_Lt_Gt.
+Qed.
+
+Lemma Psucc_Gt : forall p,
+       (Psucc p ?= p) Eq = Gt.
+induction p;simpl.
+apply Gt_Eq_Gt;auto.
+generalize p;clear p IHp.
+induction p;simpl;auto.
+reflexivity.
+Qed.
+
+Fixpoint pos_eq (m n:positive) {struct m} :bool :=
+match m, n with
+  xI mm, xI nn => pos_eq mm nn
+| xO mm, xO nn => pos_eq mm nn
+| xH, xH => true
+| _, _ => false
+end. 
+
+Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n.
+induction m;simpl;intro n;destruct n;congruence ||
+(intro e;apply f_equal with positive;auto).
+Defined.
+
+Theorem refl_pos_eq : forall m, pos_eq m m = true.
+induction m;simpl;auto.
+Qed.
+
+Definition pos_eq_dec (m n:positive) :{m=n}+{m<>n} .
+fix 1;intros [mm|mm|] [nn|nn|];try (right;congruence).
+case (pos_eq_dec mm nn).
+intro e;left;apply (f_equal xI e).
+intro ne;right;congruence.
+case (pos_eq_dec mm nn).
+intro e;left;apply (f_equal xO e).
+intro ne;right;congruence.
+left;reflexivity.
+Defined.
+
+Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left (m<>m) (refl_equal m) .
+fix 1;intros [mm|mm|].
+simpl; rewrite  pos_eq_dec_refl; reflexivity.
+simpl; rewrite  pos_eq_dec_refl; reflexivity.
+reflexivity.
+Qed.
+
+Theorem pos_eq_dec_ex : forall m n,
+ pos_eq m n =true -> exists h:m=n,
+ pos_eq_dec m n = left (m<>n) h.
+fix 1;intros [mm|mm|] [nn|nn|];try (simpl;congruence).
+simpl;intro e.
+elim (pos_eq_dec_ex _ _ e).
+intros x ex; rewrite ex. 
+exists (f_equal xI x).
+reflexivity.
+simpl;intro e.
+elim (pos_eq_dec_ex _ _ e).
+intros x ex; rewrite ex. 
+exists (f_equal xO x).
+reflexivity.
+simpl.
+exists (refl_equal xH).
+reflexivity.
+Qed.
+
+Fixpoint nat_eq (m n:nat) {struct m}: bool:=
+match m, n with 
+O,O => true
+| S mm,S nn => nat_eq mm nn
+| _,_ => false
+end.
+
+Theorem nat_eq_refl : forall m n, nat_eq m n = true -> m = n.
+induction m;simpl;intro n;destruct n;congruence ||
+(intro e;apply f_equal with nat;auto).
+Defined.
+
+Theorem refl_nat_eq : forall n, nat_eq n n = true.
+induction n;simpl;trivial.
+Defined.
+
+Fixpoint Lget (A:Set) (n:nat) (l:list A) {struct l}:option A :=
+match l with nil => None
+| x::q => 
+match n with O => Some x
+| S m => Lget A m q
+end end .
+
+Implicit Arguments Lget [A].
+
+Lemma map_app : forall (A B:Set) (f:A -> B) l m, 
+List.map  f (l ++ m) = List.map  f  l ++ List.map  f  m.
+induction l.
+reflexivity.
+simpl.
+intro m ; apply f_equal with (list B);apply IHl.
+Qed.
+
+Lemma length_map : forall (A B:Set) (f:A -> B) l, 
+length (List.map  f l) = length l.
+induction l.
+reflexivity.
+simpl; apply f_equal with nat;apply IHl.
+Qed.
+
+Lemma Lget_map : forall (A B:Set) (f:A -> B) i l, 
+Lget i (List.map  f l) = 
+match Lget i l with Some a => 
+Some (f a) | None => None end.
+induction i;intros [ | x l ] ;trivial.
+simpl;auto.
+Qed.
+
+Lemma Lget_app : forall (A:Set) (a:A) l i,
+Lget i (l ++ a :: nil) = if nat_eq i (length l) then Some a else Lget i l.
+induction l;simpl Lget;simpl length.
+intros [ | i];simpl;reflexivity.
+intros [ | i];simpl.
+reflexivity.
+auto.
+Qed.
+
+Lemma Lget_app_Some : forall (A:Set) l delta i (a: A), 
+Lget i l = Some a ->
+Lget i (l ++ delta) = Some a.
+induction l;destruct i;simpl;try congruence;auto.
+Qed.
+
+Section Store.
+
+Variable A:Type.
+
+Inductive Poption : Type:=
+  PSome : A -> Poption
+| PNone : Poption.
+
+Inductive Tree : Type :=
+   Tempty : Tree
+ | Branch0 : Tree -> Tree -> Tree
+ | Branch1 : A -> Tree -> Tree -> Tree.
+        
+Fixpoint Tget (p:positive) (T:Tree) {struct p} : Poption := 
+  match T with
+    Tempty => PNone
+  | Branch0 T1 T2 =>
+    match p with
+      xI pp => Tget pp T2
+    | xO pp => Tget pp T1
+    | xH => PNone
+    end
+  | Branch1 a T1 T2 =>
+    match p with
+      xI pp => Tget pp T2
+    | xO pp => Tget pp T1
+    | xH => PSome a
+    end
+end.
+
+Fixpoint Tadd (p:positive) (a:A) (T:Tree) {struct p}: Tree := 
+ match T with
+   | Tempty =>
+       match p with
+       | xI pp => Branch0 Tempty (Tadd pp a Tempty)
+       | xO pp => Branch0 (Tadd pp a Tempty) Tempty
+       | xH => Branch1 a Tempty Tempty
+       end
+   | Branch0 T1 T2 =>
+       match p with
+       | xI pp => Branch0 T1 (Tadd pp a T2)
+       | xO pp => Branch0 (Tadd pp a T1) T2
+       | xH => Branch1 a T1 T2
+       end
+   | Branch1 b T1 T2 =>
+       match p with
+       | xI pp => Branch1 b T1 (Tadd pp a T2)
+       | xO pp => Branch1 b (Tadd pp a T1) T2
+       | xH => Branch1 a T1 T2
+       end
+   end.
+
+Definition mkBranch0 (T1 T2:Tree) :=
+  match T1,T2 with
+    Tempty ,Tempty => Tempty
+  | _,_ => Branch0 T1 T2
+  end.
+  
+Fixpoint Tremove (p:positive) (T:Tree) {struct p}: Tree :=
+   match T with
+      | Tempty => Tempty
+      | Branch0 T1 T2 => 
+        match p with
+        | xI pp => mkBranch0 T1 (Tremove pp T2)                  
+        | xO pp => mkBranch0 (Tremove pp T1) T2
+        | xH => T
+        end
+      | Branch1 b T1 T2 =>
+        match p with
+        | xI pp => Branch1 b T1 (Tremove pp T2)
+        | xO pp => Branch1 b (Tremove pp T1) T2
+        | xH => mkBranch0 T1 T2
+        end
+      end.
+                                                                                                                        
+ 
+Theorem Tget_Tempty: forall (p : positive), Tget p (Tempty) = PNone.
+destruct p;reflexivity.
+Qed.
+
+Theorem Tget_Tadd: forall i j a T,
+       Tget i (Tadd j a T) =
+       match (i ?= j) Eq with
+         Eq => PSome a
+       | Lt => Tget i T
+       | Gt => Tget i T
+       end.
+intros i j.
+caseq ((i ?= j) Eq).
+intro H;rewrite (Pcompare_Eq_eq _ _ H);intros a;clear i H.
+induction j;destruct T;simpl;try (apply IHj);congruence.
+generalize i;clear i;induction j;destruct T;simpl in H|-*;
+destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence.
+generalize i;clear i;induction j;destruct T;simpl in H|-*;
+destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence.
+Qed.
+
+Record Store : Type :=  
+mkStore  {index:positive;contents:Tree}.
+
+Definition empty := mkStore xH Tempty.
+
+Definition push a  S :=
+mkStore (Psucc (index S)) (Tadd (index S) a (contents S)).
+
+Definition get i S := Tget i (contents S).
+
+Lemma get_empty : forall i, get i empty = PNone.
+intro i; case i; unfold empty,get; simpl;reflexivity.
+Qed.
+
+Inductive Full : Store -> Type:=
+    F_empty : Full empty
+  | F_push : forall a S, Full S -> Full (push a S).
+
+Theorem get_Full_Gt : forall S, Full S ->
+       forall i, (i ?= index S) Eq = Gt -> get i S = PNone.
+intros S W;induction W.
+unfold empty,index,get,contents;intros;apply Tget_Tempty.
+unfold index,get,push;simpl contents.
+intros i e;rewrite Tget_Tadd.
+rewrite (Gt_Psucc _ _ e). 
+unfold get in IHW.
+apply IHW;apply Gt_Psucc;assumption.
+Qed.
+
+Theorem get_Full_Eq : forall S, Full S -> get (index S) S = PNone.
+intros [index0 contents0] F.
+case F.
+unfold empty,index,get,contents;intros;apply Tget_Tempty.
+unfold index,get,push;simpl contents.
+intros a S.
+rewrite Tget_Tadd.
+rewrite Psucc_Gt.
+intro W.
+change (get (Psucc (index S)) S =PNone).
+apply get_Full_Gt; auto.
+apply Psucc_Gt.
+Qed.
+
+Theorem get_push_Full : 
+  forall i a S, Full S -> 
+  get i (push a S) =
+  match (i ?= index S) Eq with
+    Eq => PSome a
+  | Lt => get i S
+  | Gt => PNone
+end.
+intros i a S F.
+caseq ((i ?= index S) Eq).
+intro e;rewrite (Pcompare_Eq_eq _ _ e).
+destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd.
+rewrite Pcompare_refl;reflexivity.
+intros;destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd.
+simpl index in H;rewrite H;reflexivity.
+intro H;generalize H;clear H.
+unfold get,push;simpl index;simpl contents.
+rewrite Tget_Tadd;intro e;rewrite e.
+change (get i S=PNone).
+apply get_Full_Gt;auto.
+Qed.
+
+Lemma Full_push_compat : forall i a S, Full S ->
+forall x, get i S = PSome x -> 
+ get i (push a S) = PSome x.
+intros i a S F x H. 
+caseq ((i ?= index S) Eq);intro test.
+rewrite (Pcompare_Eq_eq _ _ test) in H.
+rewrite (get_Full_Eq _ F) in H;congruence.
+rewrite <- H.
+rewrite (get_push_Full i a).
+rewrite test;reflexivity.
+assumption.
+rewrite (get_Full_Gt _ F) in H;congruence.
+Qed.
+
+Lemma Full_index_one_empty : forall S, Full S -> index S = 1 -> S=empty. 
+intros [ind cont] F one; inversion F.
+reflexivity.
+simpl index in one;assert (h:=Psucc_not_one (index S)).
+congruence.
+Qed.
+
+Lemma push_not_empty: forall a S, (push a S) <> empty.
+intros a [ind cont];unfold push,empty.
+simpl;intro H;injection H; intros _ ; apply Psucc_not_one.
+Qed. 
+
+Fixpoint In (x:A) (S:Store) (F:Full S) {struct F}: Prop :=
+match F with
+F_empty => False
+| F_push a SS FF => x=a \/ In x SS FF
+end.
+
+Lemma get_In : forall (x:A) (S:Store) (F:Full S) i , 
+get i S = PSome x -> In x S F.
+induction F.
+intro i;rewrite get_empty; congruence.
+intro i;rewrite get_push_Full;trivial.
+caseq ((i ?= index S) Eq);simpl.
+left;congruence.
+right;eauto.
+congruence.
+Qed.
+
+End Store.
+
+Implicit Arguments PNone [A].
+Implicit Arguments PSome [A].
+
+Implicit Arguments Tempty [A].
+Implicit Arguments Branch0 [A].
+Implicit Arguments Branch1 [A].
+
+Implicit Arguments Tget [A].
+Implicit Arguments Tadd [A].
+
+Implicit Arguments Tget_Tempty [A].
+Implicit Arguments Tget_Tadd [A].
+
+Implicit Arguments mkStore [A].
+Implicit Arguments index [A].
+Implicit Arguments contents [A].
+
+Implicit Arguments empty [A].
+Implicit Arguments get [A].
+Implicit Arguments push [A].
+
+Implicit Arguments get_empty [A].
+Implicit Arguments get_push_Full [A].
+
+Implicit Arguments Full [A].
+Implicit Arguments F_empty [A].
+Implicit Arguments F_push [A].
+Implicit Arguments In [A].
+
+Section Map. 
+
+Variables A B:Set.
+
+Variable f: A -> B.
+
+Fixpoint Tmap (T: Tree A) : Tree B :=
+match T with
+Tempty => Tempty
+| Branch0 t1 t2 => Branch0 (Tmap t1) (Tmap t2)
+| Branch1 a t1 t2 => Branch1 (f a) (Tmap t1) (Tmap t2)
+end.
+
+Lemma Tget_Tmap: forall T i, 
+Tget i (Tmap T)= match Tget i T with PNone => PNone 
+| PSome a => PSome (f a) end.
+induction T;intro i;case i;simpl;auto.
+Defined.
+
+Lemma Tmap_Tadd: forall i a T,
+Tmap (Tadd i a T) = Tadd i (f a) (Tmap T).
+induction i;intros a T;case T;simpl;intros;try (rewrite IHi);simpl;reflexivity.
+Defined.
+
+Definition map (S:Store A) : Store B :=
+mkStore (index S) (Tmap (contents S)).
+
+Lemma get_map: forall i S, 
+get i (map S)= match get i S with PNone => PNone 
+| PSome a => PSome (f a) end.
+destruct S;unfold get,map,contents,index;apply Tget_Tmap.
+Defined.
+
+Lemma map_push: forall a S, 
+map (push a S) = push (f a) (map S).
+intros a S.
+case S.
+unfold push,map,contents,index.
+intros;rewrite Tmap_Tadd;reflexivity.
+Defined.
+
+Theorem Full_map : forall S, Full S -> Full (map S).
+intros S F. 
+induction F.
+exact F_empty.
+rewrite map_push;constructor 2;assumption.
+Defined.
+
+End Map.
+
+Implicit Arguments Tmap [A B].
+Implicit Arguments map [A B].
+Implicit Arguments Full_map [A B f].
+
+Notation "hyps \ A" := (push A hyps) (at level 72,left associativity).
diff --git a/contrib/rtauto/Rtauto.v b/contrib/rtauto/Rtauto.v
new file mode 100644
index 000000000..0e3d697c1
--- /dev/null
+++ b/contrib/rtauto/Rtauto.v
@@ -0,0 +1,399 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+
+Require Export List.
+Require Export CCSolve.
+Require Export Bintree.
+Require Import Bool.
+Unset Boxed Definitions.
+
+Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
+Ltac clean:=try (simpl;congruence).
+
+Inductive form:Set:=
+Atom : positive -> form
+| Arrow : form -> form -> form
+| Bot
+| Conjunct : form -> form -> form 
+| Disjunct : form -> form -> form.
+
+Notation "[ n ]":=(Atom n).
+Notation "A =>> B":= (Arrow A B) (at level 59, right associativity).
+Notation "#" := Bot.
+Notation "A //\\ B" := (Conjunct A B) (at level 57, left associativity).
+Notation "A \\// B" := (Disjunct A B) (at level 58, left associativity).
+
+Definition ctx := Store form.
+
+Fixpoint pos_eq (m n:positive) {struct m} :bool :=
+match m with
+  xI mm => match n with xI nn => pos_eq mm nn | _ => false end
+| xO mm => match n with xO nn => pos_eq mm nn | _ => false end
+| xH => match n with xH => true | _ => false end
+end. 
+
+Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n.
+induction m;simpl;destruct n;congruence ||
+(intro e;apply f_equal with positive;auto).
+Qed.
+
+Fixpoint form_eq (p q:form) {struct p} :bool :=
+match p with
+  Atom m => match q with Atom n => pos_eq m n | _ => false end
+| Arrow p1 p2 => 
+match q with 
+  Arrow q1 q2 => form_eq p1 q1 && form_eq p2 q2 
+| _ => false end
+| Bot => match q with Bot => true | _ => false end
+| Conjunct p1 p2 => 
+match q with 
+  Conjunct q1 q2 => form_eq p1 q1 && form_eq p2 q2 
+| _ => false 
+end
+| Disjunct p1 p2 => 
+match q with 
+  Disjunct q1 q2 => form_eq p1 q1 && form_eq p2 q2 
+| _ => false 
+end
+end. 
+
+Theorem form_eq_refl: forall p q, form_eq p q = true -> p = q.
+induction p;destruct q;simpl;clean.
+intro h;generalize (pos_eq_refl _ _ h);congruence.
+caseq (form_eq p1 q1);clean.
+intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. 
+caseq (form_eq p1 q1);clean.
+intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. 
+caseq (form_eq p1 q1);clean.
+intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. 
+Qed.
+
+Implicit Arguments form_eq_refl [p q].
+
+Section with_env.
+
+Variable env:Store Prop.
+
+Fixpoint interp_form (f:form): Prop :=
+match f with
+[n]=> match get n env with PNone => True | PSome P => P end
+| A =>> B => (interp_form A) -> (interp_form B)
+| # => False
+| A //\\ B => (interp_form A) /\ (interp_form B)
+| A \\// B => (interp_form A) \/ (interp_form B)
+end.
+
+Notation "[[ A ]]" := (interp_form A).
+
+Fixpoint interp_ctx (hyps:ctx) (F:Full hyps) (G:Prop) {struct F} : Prop :=
+match F with
+  F_empty => G
+| F_push H hyps0 F0 =>  interp_ctx hyps0 F0  ([[H]] -> G)
+end.
+
+Require Export BinPos.
+
+Ltac wipe := intros;simpl;constructor.  
+
+Lemma compose0 : 
+forall hyps F (A:Prop),
+ A -> 
+ (interp_ctx hyps F A).
+induction F;intros A H;simpl;auto.
+Qed.
+
+Lemma compose1 : 
+forall hyps F (A B:Prop),
+ (A -> B) ->
+ (interp_ctx hyps F A) ->
+ (interp_ctx hyps F B).
+induction F;intros A B H;simpl;auto.
+apply IHF;auto.
+Qed.
+
+Theorem compose2 : 
+forall hyps F (A B C:Prop),
+ (A -> B -> C) -> 
+ (interp_ctx hyps F A) ->
+ (interp_ctx hyps F B) ->
+ (interp_ctx hyps F C).
+induction F;intros A B C H;simpl;auto.
+apply IHF;auto.
+Qed.
+
+Theorem compose3 : 
+forall hyps F (A B C D:Prop),
+ (A -> B -> C -> D) -> 
+ (interp_ctx hyps F A) -> 
+ (interp_ctx hyps F B) ->
+ (interp_ctx hyps F C) ->
+ (interp_ctx hyps F D).
+induction F;intros A B C D H;simpl;auto.
+apply IHF;auto.
+Qed.
+
+Lemma weaken : forall hyps F f G,
+ (interp_ctx hyps F G) ->
+ (interp_ctx (hyps\f)  (F_push f hyps F) G).
+induction F;simpl;intros;auto.
+apply compose1 with ([[a]]-> G);auto.
+Qed.
+
+Theorem project_In : forall hyps F g, 
+In g hyps F ->
+interp_ctx hyps F [[g]].
+induction F;simpl.
+contradiction.
+intros g H;destruct H.
+subst;apply compose0;simpl;trivial.
+apply compose1 with [[g]];auto.
+Qed.
+
+Theorem project : forall hyps F p g, 
+get  p hyps = PSome g->
+interp_ctx hyps F [[g]].
+intros hyps F p g e; apply project_In.
+apply get_In with p;assumption.
+Qed.
+
+Implicit Arguments project [hyps p g].
+
+Inductive proof:Set :=
+  Ax : positive -> proof
+| I_Arrow : proof -> proof
+| E_Arrow : positive -> positive -> proof -> proof
+| D_Arrow : positive -> proof -> proof -> proof
+| E_False : positive -> proof
+| I_And: proof -> proof -> proof
+| E_And: positive -> proof -> proof
+| D_And: positive -> proof -> proof
+| I_Or_l: proof -> proof
+| I_Or_r: proof -> proof
+| E_Or: positive -> proof -> proof -> proof
+| D_Or: positive -> proof -> proof
+| Cut: form -> proof -> proof -> proof.
+
+Notation "hyps \ A" := (push A hyps) (at level 72,left associativity).
+
+Fixpoint check_proof (hyps:ctx) (gl:form) (P:proof) {struct P}: bool :=
+ match P with
+   Ax i => 
+     match get i hyps with
+         PSome F => form_eq F gl
+ | _ => false
+    end 
+| I_Arrow p =>
+   match gl with
+      A  =>> B  => check_proof (hyps \ A) B p
+   | _ => false        
+    end 
+| E_Arrow i j p =>
+   match get i hyps,get j hyps with
+       PSome A,PSome (B =>>C) =>
+         form_eq A B && check_proof (hyps \ C) (gl) p
+    | _,_ => false
+    end
+| D_Arrow i p1 p2 => 
+   match get i hyps with
+      PSome  ((A =>>B)=>>C) =>
+     (check_proof ( hyps \ B =>> C \ A) B p1) && (check_proof (hyps \ C) gl p2)
+    | _ => false
+  end
+| E_False i =>
+  match get i hyps with
+    PSome # => true
+  | _ => false
+  end
+| I_And p1 p2 =>
+   match gl with
+      A //\\ B =>
+      check_proof hyps A p1 && check_proof hyps B p2
+      | _ => false
+      end
+| E_And i p => 
+   match get i hyps with
+      PSome  (A //\\ B) => check_proof (hyps \ A \ B) gl p
+    | _=> false
+   end
+| D_And i p => 
+   match get i hyps with
+      PSome  (A //\\ B =>> C) => check_proof (hyps \ A=>>B=>>C) gl p
+    | _=> false
+   end
+| I_Or_l p =>
+   match gl with
+      (A \\// B) => check_proof hyps A p
+      | _ => false
+      end
+| I_Or_r p =>
+   match gl with
+      (A \\// B) => check_proof hyps B p
+      | _ => false
+      end
+| E_Or i p1 p2 =>
+  match get i hyps with
+  PSome (A \\// B) =>
+  check_proof (hyps \ A) gl p1 && check_proof (hyps \ B) gl p2
+  | _=> false
+  end
+| D_Or i p => 
+   match get i hyps with
+      PSome  (A \\// B =>> C) =>
+      (check_proof (hyps \ A=>>C \ B=>>C) gl p)
+    | _=> false
+   end
+| Cut A p1 p2 =>
+  check_proof hyps A p1 && check_proof (hyps \ A) gl p2
+end. 
+
+Theorem interp_proof: 
+forall p hyps F gl, 
+check_proof hyps gl p = true -> interp_ctx hyps F [[gl]].
+
+induction p;intros hyps F gl.
+
+(* cas Axiom *)
+Focus 1.
+simpl;caseq (get p hyps);clean.
+intros f nth_f e;rewrite <- (form_eq_refl e).
+apply project with p;trivial.
+
+(* Cas Arrow_Intro *)
+Focus 1.
+destruct gl;clean.
+simpl;intros.
+change (interp_ctx (hyps\gl1)  (F_push gl1 hyps F) [[gl2]]).
+apply IHp;try constructor;trivial.
+
+(* Cas Arrow_Elim *)
+Focus 1.
+simpl check_proof;caseq (get p hyps);clean.
+intros f ef;caseq (get p0 hyps);clean.
+intros f0 ef0;destruct f0;clean.
+caseq (form_eq f f0_1);clean.
+simpl;intros e check_p1.
+generalize  (project  F ef) (project  F ef0) 
+(IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1);
+clear check_p1 IHp p p0 p1 ef ef0.
+simpl.
+apply compose3.
+rewrite (form_eq_refl e).
+auto.
+
+(* cas Arrow_Destruct *)
+Focus 1.
+simpl;caseq (get p1 hyps);clean.
+intros f ef;destruct f;clean.
+destruct f1;clean.
+caseq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean.
+intros check_p1 check_p2.
+generalize (project F ef)
+(IHp1 (hyps \ f1_2 =>> f2 \ f1_1)   
+(F_push f1_1 (hyps \ f1_2 =>> f2)
+ (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1)
+(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2).
+simpl;apply compose3;auto.
+
+(* Cas False_Elim *)
+Focus 1.
+simpl;caseq (get p hyps);clean.
+intros f ef;destruct f;clean.
+intros _; generalize (project F ef).
+apply compose1;apply False_ind.
+
+(* Cas And_Intro *)
+Focus 1.
+simpl;destruct gl;clean.
+caseq (check_proof hyps gl1 p1);clean.
+intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2).
+apply compose2 ;simpl;auto.
+
+(* cas And_Elim *)
+Focus 1.
+simpl;caseq (get p hyps);clean.
+intros f ef;destruct f;clean.
+intro check_p;generalize  (project F ef)
+(IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p).
+simpl;apply compose2;intros [h1 h2];auto.
+
+(* cas And_Destruct *)
+Focus 1.
+simpl;caseq (get p hyps);clean.
+intros f ef;destruct f;clean.
+destruct f1;clean.
+intro H;generalize  (project F ef)
+(IHp (hyps \ f1_1 =>> f1_2 =>> f2)  
+(F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H);clear H;simpl.
+apply compose2;auto.
+
+(* cas Or_Intro_left *)
+Focus 1.
+destruct gl;clean.
+intro Hp;generalize (IHp hyps F gl1 Hp).
+apply compose1;simpl;auto.
+
+(* cas Or_Intro_right *)
+Focus 1.
+destruct gl;clean.
+intro Hp;generalize (IHp hyps F gl2 Hp).
+apply compose1;simpl;auto.
+
+(* cas Or_elim *)
+Focus 1.
+simpl;caseq (get p1 hyps);clean.
+intros f ef;destruct f;clean.
+caseq (check_proof (hyps \ f1) gl p2);clean.
+intros check_p1 check_p2;generalize (project F ef)
+(IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1)
+(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2);
+simpl;apply compose3;simpl;intro h;destruct h;auto.
+
+(* cas Or_Destruct *)
+Focus 1.
+simpl;caseq (get p hyps);clean.
+intros f ef;destruct f;clean.
+destruct f1;clean.
+intro check_p0;generalize (project F ef)
+(IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2)
+(F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) 
+ (F_push (f1_1 =>> f2) hyps F)) gl check_p0);simpl.
+apply compose2;auto.
+
+(* cas Cut *)
+Focus 1.
+simpl;caseq (check_proof hyps f p1);clean.
+intros check_p1 check_p2;
+generalize (IHp1 hyps F f check_p1) 
+(IHp2 (hyps\f) (F_push f hyps F) gl check_p2);
+simpl; apply compose2;auto.
+Qed.
+
+Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True.
+intros gl prf;caseq (check_proof empty gl prf);intro check_prf.
+change (interp_ctx empty F_empty [[gl]]) ;
+apply interp_proof with prf;assumption.
+trivial.
+Qed.
+
+End with_env.
+
+(*
+(* A small example *)
+Parameters A B C D:Prop.
+Theorem toto:A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).
+exact (Reflect (empty \ A \ B \ C)
+([1] //\\ ([2] \\// [3]) =>> [1] //\\ [2] \\// [1] //\\ [3])
+(I_Arrow (E_And 1 (E_Or 3 
+  (I_Or_l (I_And (Ax 2) (Ax 4))) 
+  (I_Or_r (I_And (Ax 2) (Ax 4))))))).
+Qed.
+Print toto.
+*)
\ No newline at end of file
diff --git a/contrib/rtauto/g_rtauto.ml4 b/contrib/rtauto/g_rtauto.ml4
new file mode 100644
index 000000000..ee47d0b02
--- /dev/null
+++ b/contrib/rtauto/g_rtauto.ml4
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$*)
+
+(*i camlp4deps: "parsing/grammar.cma"  i*)
+
+TACTIC EXTEND Rtauto
+  [ "Rtauto" ] -> [ Refl_tauto.rtauto_tac ]
+END
+
diff --git a/contrib/rtauto/proof_search.ml b/contrib/rtauto/proof_search.ml
new file mode 100644
index 000000000..9d9d66bb2
--- /dev/null
+++ b/contrib/rtauto/proof_search.ml
@@ -0,0 +1,546 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Term
+open Util  
+open Goptions
+
+type s_info=
+    {mutable created_steps     : int; (* node count*)
+     mutable pruned_steps      : int;
+     mutable created_branches  : int; (* path count *)
+     mutable pruned_branches   : int;
+     mutable created_hyps      : int; (* hyps count *)
+     mutable pruned_hyps       : int;
+     mutable branch_failures   : int;
+     mutable branch_successes  : int;
+     mutable nd_branching      : int}
+
+let s_info=
+    {created_steps    = 0; (* node count*)
+     pruned_steps     = 0;
+     created_branches = 0; (* path count *)
+     pruned_branches  = 0;
+     created_hyps     = 0; (* hyps count *)
+     pruned_hyps      = 0;
+     branch_failures  = 0;
+     branch_successes = 0;
+     nd_branching     = 0}
+
+let reset_info () =
+     s_info.created_steps    <- 0; (* node count*)
+     s_info.pruned_steps     <- 0;
+     s_info.created_branches <- 0; (* path count *)
+     s_info.pruned_branches  <- 0;
+     s_info.created_hyps     <- 0; (* hyps count *)
+     s_info.pruned_hyps      <- 0;
+     s_info.branch_failures  <- 0;
+     s_info.branch_successes <- 0;
+     s_info.nd_branching     <- 0
+
+let pruning = ref true
+
+let opt_pruning=
+  {optsync=true;
+   optname="Rtauto Pruning";
+   optkey=SecondaryTable("Rtauto","Pruning");
+   optread=(fun () -> !pruning);
+   optwrite=(fun b -> pruning:=b)}
+
+let _ = declare_bool_option opt_pruning 
+
+type form=
+    Atom of int
+  | Arrow of form * form
+  | Bot 
+  | Conjunct of form * form
+  | Disjunct of form * form
+
+type tag=int
+
+let decomp_form=function
+    Atom i -> Some (i,[])
+  | Arrow (f1,f2) -> Some (-1,[f1;f2]) 
+  | Bot -> Some (-2,[])
+  | Conjunct (f1,f2) -> Some (-3,[f1;f2])
+  | Disjunct (f1,f2) -> Some (-4,[f1;f2])
+
+module Fmap=Map.Make(struct type t=form let compare=compare end)
+
+type sequent = 
+    {rev_hyps: form Intmap.t;
+     norev_hyps: form Intmap.t;
+     size:int;
+     left:int Fmap.t;
+     right:(int*form) list Fmap.t;
+     cnx:(int*int*form*form) list;
+     abs:int option;
+     gl:form}
+
+let add_one_arrow i f1 f2 m=
+  try Fmap.add f1 ((i,f2)::(Fmap.find f1 m)) m with
+      Not_found ->
+	Fmap.add f1 [i,f2] m
+
+type proof =
+    Ax of int
+  | I_Arrow of proof
+  | E_Arrow of int*int*proof
+  | D_Arrow of int*proof*proof
+  | E_False of int
+  | I_And of proof*proof
+  | E_And of int*proof
+  | D_And of int*proof
+  | I_Or_l of proof
+  | I_Or_r of proof
+  | E_Or of int*proof*proof
+  | D_Or of int*proof
+  | Pop of int*proof
+      
+type rule =
+    SAx of int
+  | SI_Arrow 
+  | SE_Arrow of int*int
+  | SD_Arrow of int
+  | SE_False of int
+  | SI_And 
+  | SE_And of int
+  | SD_And of int
+  | SI_Or_l
+  | SI_Or_r
+  | SE_Or of int
+  | SD_Or of int
+
+let add_step s sub =
+  match s,sub with
+      SAx i,[] -> Ax i
+    | SI_Arrow,[p] -> I_Arrow p
+    | SE_Arrow(i,j),[p] -> E_Arrow (i,j,p)
+    | SD_Arrow i,[p1;p2] -> D_Arrow (i,p1,p2)
+    | SE_False i,[] -> E_False i
+    | SI_And,[p1;p2] -> I_And(p1,p2)
+    | SE_And i,[p] -> E_And(i,p)
+    | SD_And i,[p] -> D_And(i,p)
+    | SI_Or_l,[p] -> I_Or_l p
+    | SI_Or_r,[p] -> I_Or_r p
+    | SE_Or i,[p1;p2] -> E_Or(i,p1,p2)
+    | SD_Or i,[p] -> D_Or(i,p)
+    | _,_ -> anomaly "add_step: wrong arity" 
+    
+type 'a with_deps = 
+    {dep_it:'a;
+     dep_goal:bool;
+     dep_hyps:Intset.t}
+
+type slice=
+    {proofs_done:proof list;
+     proofs_todo:sequent with_deps list;
+     step:rule;
+     needs_goal:bool;
+     needs_hyps:Intset.t;
+     changes_goal:bool;
+     creates_hyps:Intset.t}
+
+type state = 
+    Complete of proof
+  | Incomplete of sequent * slice list
+
+let project = function
+    Complete prf -> prf
+  | Incomplete (_,_) -> anomaly "not a successful state"
+
+let pop n prf =
+  let nprf=
+    match prf.dep_it with
+	Pop (i,p) -> Pop (i+n,p)
+      | p -> Pop(n,p) in
+    {prf with dep_it = nprf}
+
+let rec fill stack proof =
+  match stack with 
+      [] -> Complete proof.dep_it
+    | slice::super ->
+	if 
+	  !pruning &&
+	  slice.proofs_done=[] &&
+	  not (slice.changes_goal && proof.dep_goal) &&
+	  not (Intset.exists 
+		 (fun i -> Intset.mem i proof.dep_hyps) 
+		 slice.creates_hyps)
+	then
+	  begin
+	    s_info.pruned_steps<-s_info.pruned_steps+1;
+	    s_info.pruned_branches<- s_info.pruned_branches +
+	    List.length slice.proofs_todo;
+	    let created_here=Intset.cardinal slice.creates_hyps in
+	      s_info.pruned_hyps<-s_info.pruned_hyps+
+	      List.fold_left 
+		(fun sum dseq -> sum + Intset.cardinal dseq.dep_hyps) 
+		created_here slice.proofs_todo;
+	    fill super (pop (Intset.cardinal slice.creates_hyps) proof)
+	  end
+	else
+	  let dep_hyps=
+	    Intset.union slice.needs_hyps 
+	      (Intset.diff proof.dep_hyps slice.creates_hyps) in
+	  let dep_goal=
+	    slice.needs_goal || 
+	    ((not slice.changes_goal) && proof.dep_goal) in
+	  let proofs_done=
+	    proof.dep_it::slice.proofs_done in
+	    match slice.proofs_todo with
+		[] ->
+		  fill super {dep_it = 
+				add_step slice.step (List.rev proofs_done);
+			      dep_goal = dep_goal;
+			      dep_hyps = dep_hyps}
+	      | current::next ->
+		  let nslice=
+		    {proofs_done=proofs_done;
+		     proofs_todo=next;
+		     step=slice.step;
+		     needs_goal=dep_goal;
+		     needs_hyps=dep_hyps;
+		     changes_goal=current.dep_goal;
+		     creates_hyps=current.dep_hyps} in
+		    Incomplete (current.dep_it,nslice::super)
+
+let append stack (step,subgoals) =
+  s_info.created_steps<-s_info.created_steps+1;
+  match subgoals with 
+      [] -> 
+	s_info.branch_successes<-s_info.branch_successes+1;
+	fill stack {dep_it=add_step step.dep_it [];
+		    dep_goal=step.dep_goal;
+		    dep_hyps=step.dep_hyps}
+    | hd :: next ->
+	s_info.created_branches<-
+	s_info.created_branches+List.length next;
+	let slice=
+	  {proofs_done=[];
+	   proofs_todo=next;
+	   step=step.dep_it;
+	   needs_goal=step.dep_goal;
+	   needs_hyps=step.dep_hyps;
+	   changes_goal=hd.dep_goal;
+	   creates_hyps=hd.dep_hyps} in
+	  Incomplete(hd.dep_it,slice::stack)
+
+let embed seq=
+  {dep_it=seq;
+   dep_goal=false;
+   dep_hyps=Intset.empty}
+
+let change_goal seq gl=
+    {seq with 
+       dep_it={seq.dep_it with gl=gl};
+       dep_goal=true}
+	
+let add_hyp seqwd f=
+  s_info.created_hyps<-s_info.created_hyps+1;
+  let seq=seqwd.dep_it in
+  let num = seq.size+1 in
+  let left = Fmap.add f num seq.left in
+  let cnx,right=
+    try
+      let l=Fmap.find f seq.right in
+	List.fold_right (fun (i,f0) l0 -> (num,i,f,f0)::l0) l seq.cnx,
+	Fmap.remove f seq.right
+    with Not_found -> seq.cnx,seq.right in
+  let nseq=
+    match f with
+	Bot -> 
+	  {seq with 
+	     left=left;
+	     right=right;
+	     size=num;
+	     abs=Some num;
+	     cnx=cnx}
+      | Atom _ ->
+	  {seq with 
+	     size=num;
+	     left=left;
+	     right=right;
+	     cnx=cnx}
+      | Conjunct (_,_) | Disjunct (_,_) ->
+	  {seq with
+	     rev_hyps=Intmap.add num f seq.rev_hyps; 
+	     size=num;
+	     left=left;
+	     right=right;
+	     cnx=cnx}
+      | Arrow (f1,f2) ->
+	  let ncnx,nright=
+	    try 
+	      let i = Fmap.find f1 seq.left in	  
+		(i,num,f1,f2)::cnx,right
+	    with Not_found ->
+	      cnx,(add_one_arrow num f1 f2 right) in
+	    match f1 with
+		Conjunct (_,_) | Disjunct (_,_) ->
+		  {seq with
+		     rev_hyps=Intmap.add num f seq.rev_hyps; 
+		     size=num;
+		     left=left;
+		     right=nright;
+		     cnx=ncnx}
+	      | Arrow(_,_) ->
+		  {seq with
+		     norev_hyps=Intmap.add num f seq.norev_hyps; 
+		     size=num;
+		     left=left;
+		     right=nright;
+		     cnx=ncnx}
+	      | _ -> 
+		  {seq with
+		     size=num;
+		     left=left;
+		     right=nright;
+		     cnx=ncnx} in
+    {seqwd with 
+       dep_it=nseq;
+       dep_hyps=Intset.add num seqwd.dep_hyps}
+
+exception Here_is of (int*form)
+
+let choose m= 
+  try 
+    Intmap.iter (fun i f -> raise (Here_is (i,f))) m;
+    raise Not_found
+  with 
+      Here_is (i,f) -> (i,f)
+
+
+let search_or seq=
+  match seq.gl with
+      Disjunct (f1,f2) -> 
+	[{dep_it = SI_Or_l;
+	  dep_goal = true;
+	  dep_hyps = Intset.empty},
+	 [change_goal (embed seq) f1];
+	 {dep_it = SI_Or_r;
+	  dep_goal = true;
+	  dep_hyps = Intset.empty},
+	 [change_goal (embed seq) f2]]
+    | _ -> []
+
+let search_norev seq=
+  let goals=ref (search_or seq) in
+  let add_one i f= 
+    match f with
+	Arrow (Arrow (f1,f2),f3) ->
+	  let nseq = 
+	    {seq with norev_hyps=Intmap.remove i seq.norev_hyps} in
+	    goals:=
+	      ({dep_it=SD_Arrow(i);
+		dep_goal=false;
+		dep_hyps=Intset.singleton i},
+	       [add_hyp 
+		  (add_hyp 
+		     (change_goal (embed nseq) f2) 
+		     (Arrow(f2,f3))) 
+		  f1;
+		add_hyp (embed nseq) f3]):: !goals
+      | _ -> anomaly "search_no_rev: can't happen" in
+    Intmap.iter add_one seq.norev_hyps;
+    List.rev !goals
+
+let search_in_rev_hyps seq=
+  try 
+    let i,f=choose seq.rev_hyps in
+    let make_step step=
+      {dep_it=step;
+       dep_goal=false;
+       dep_hyps=Intset.singleton i} in
+    let nseq={seq with rev_hyps=Intmap.remove i seq.rev_hyps} in
+      match f with
+	  Conjunct (f1,f2) -> 
+	    [make_step (SE_And(i)),
+	     [add_hyp (add_hyp (embed nseq) f1) f2]]
+	| Disjunct (f1,f2) ->
+	    [make_step (SE_Or(i)),
+	     [add_hyp (embed nseq) f1;add_hyp (embed nseq) f2]]
+	| Arrow (Conjunct (f1,f2),f0) -> 
+	    [make_step (SD_And(i)),
+	     [add_hyp (embed nseq) (Arrow (f1,Arrow (f2,f0)))]]
+	| Arrow (Disjunct (f1,f2),f0) ->
+	    [make_step (SD_Or(i)),
+	     [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]]
+	| _ -> anomaly "search_in_rev_hyps: can't happen"	      
+  with
+      Not_found -> search_norev seq
+ 
+let search_rev seq=
+  match seq.cnx with
+      (i,j,f1,f2)::next -> 
+	let nseq=
+	  match f1 with
+	      Conjunct (_,_) | Disjunct (_,_) ->
+		{seq with cnx=next;
+		   rev_hyps=Intmap.remove j seq.rev_hyps}
+	    | Arrow (_,_) ->
+		{seq with cnx=next;
+		   norev_hyps=Intmap.remove j seq.norev_hyps}
+	    | _ ->
+		{seq with cnx=next} in
+	  [{dep_it=SE_Arrow(i,j);
+	    dep_goal=false;
+	    dep_hyps=Intset.add i (Intset.singleton j)},
+	   [add_hyp (embed nseq) f2]]
+    | [] -> 
+	match seq.gl with
+	    Arrow (f1,f2) ->
+	      [{dep_it=SI_Arrow;
+		dep_goal=true;
+		dep_hyps=Intset.empty},
+	       [add_hyp (change_goal (embed seq) f2) f1]]
+	  | Conjunct (f1,f2) ->
+	      [{dep_it=SI_And;
+		dep_goal=true;
+		dep_hyps=Intset.empty},[change_goal (embed seq) f1;
+					change_goal (embed seq) f2]]
+	  | _ -> search_in_rev_hyps seq
+
+let search_all seq=
+  match seq.abs with
+      Some i -> 
+	[{dep_it=SE_False (i);
+	  dep_goal=false;
+	  dep_hyps=Intset.singleton i},[]]
+    | None ->
+	try 
+	  let ax = Fmap.find seq.gl seq.left in
+	    [{dep_it=SAx (ax);
+	      dep_goal=true;
+	      dep_hyps=Intset.singleton ax},[]]
+	with Not_found -> search_rev seq
+
+let bare_sequent = embed 
+		     {rev_hyps=Intmap.empty;
+		      norev_hyps=Intmap.empty;
+		      size=0;
+		      left=Fmap.empty;
+		      right=Fmap.empty;
+		      cnx=[];
+		      abs=None;
+		      gl=Bot}
+		     
+let init_state hyps gl=
+  let init = change_goal bare_sequent gl in
+  let goal=List.fold_right (fun (_,f,_) seq ->add_hyp seq f) hyps init in
+    Incomplete (goal.dep_it,[])
+
+let success= function
+    Complete _ -> true
+  | Incomplete (_,_) -> false
+
+let branching = function
+    Incomplete (seq,stack) ->
+      check_for_interrupt ();
+      let successors = search_all seq in
+      let _ =
+	match successors with
+	    [] -> s_info.branch_failures<-s_info.branch_failures+1
+	  | _::next ->  
+	      s_info.nd_branching<-s_info.nd_branching+List.length next in
+	List.map (append stack) successors
+  | Complete prf -> anomaly "already succeeded"
+
+open Pp 
+
+let rec pp_form =
+  function
+      Arrow(f1,f2) -> (pp_or f1) ++ (str " -> ") ++ (pp_form f2)
+    | f -> pp_or f
+and pp_or = function
+    Disjunct(f1,f2) ->
+      (pp_or f1) ++ (str " \\/ ") ++ (pp_and f2)
+  | f -> pp_and f
+and pp_and = function
+    Conjunct(f1,f2) ->
+      (pp_and f1) ++ (str " /\\ ") ++ (pp_atom f2)
+  | f -> pp_atom f
+and pp_atom= function
+    Bot -> str "#"
+  | Atom n -> int n
+  | f -> str "(" ++ hv 2 (pp_form f) ++ str ")" 
+
+let pr_form f = msg (pp_form f)
+
+let pp_intmap map = 
+  let pp=ref (str "") in  
+   Intmap.iter (fun i obj -> pp:= (!pp ++ 
+		pp_form obj ++ cut ())) map;
+    str "{ " ++ v 0 (!pp) ++ str " }"
+
+let pp_list pp_obj l=
+let pp=ref (str "") in
+  List.iter (fun o -> pp := !pp ++ (pp_obj o) ++ str ", ") l;
+  str "[ " ++ !pp ++ str "]"
+
+let pp_mapint map =
+  let pp=ref (str "") in  
+   Fmap.iter (fun obj l -> pp:= (!pp ++ 
+		pp_form obj ++ str " => " ++ 
+				 pp_list (fun (i,f) -> pp_form f) l ++ 
+				 cut ()) ) map;
+    str "{ " ++ vb 0 ++  (!pp) ++ str " }" ++ close ()
+
+let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2
+
+let pp_gl gl= cut () ++
+  str "{ " ++ vb 0 ++ 
+	      begin
+		match gl.abs with
+		    None -> str ""
+		  | Some i -> str "ABSURD" ++ cut ()
+	      end ++
+  str "rev   =" ++ pp_intmap gl.rev_hyps ++ cut () ++
+  str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++
+  str "arrows=" ++ pp_mapint gl.right ++ cut () ++ 
+  str "cnx   =" ++ pp_list pp_connect gl.cnx ++ cut () ++ 
+  str "goal  =" ++ pp_form gl.gl ++ str " }" ++ close ()
+
+let pp = 
+  function
+      Incomplete(gl,ctx) -> msgnl (pp_gl gl)
+    | _ -> msg (str "<complete>")
+
+let pp_info () = 
+  let count_info = 
+    if !pruning then
+	str "Proof steps : " ++ 
+	int s_info.created_steps ++ str " created / " ++ 
+	int s_info.pruned_steps ++ str " pruned" ++ fnl () ++
+	str "Proof branches : " ++ 
+	int s_info.created_branches ++ str " created / " ++ 
+	int s_info.pruned_branches ++ str " pruned" ++ fnl () ++
+	str "Hypotheses : " ++ 
+	int s_info.created_hyps ++ str " created / " ++ 
+	int s_info.pruned_hyps ++ str " pruned" ++ fnl ()
+    else
+	str "Pruning is off" ++ fnl () ++
+	str "Proof steps : " ++ 
+	int s_info.created_steps ++ str " created" ++ fnl () ++
+	str "Proof branches : " ++ 
+	int s_info.created_branches ++ str " created" ++ fnl () ++
+	str "Hypotheses : " ++ 
+	int s_info.created_hyps ++ str " created" ++ fnl () in
+    msgnl
+      ( str "Proof-search statistics :" ++ fnl () ++
+	count_info ++ 
+	str "Branch ends: " ++
+	int s_info.branch_successes ++ str " successes / " ++
+	int s_info.branch_failures ++ str " failures" ++ fnl () ++
+	str "Non-deterministic choices : " ++
+	int s_info.nd_branching ++ str " branches")
+
+
+ 
diff --git a/contrib/rtauto/proof_search.mli b/contrib/rtauto/proof_search.mli
new file mode 100644
index 000000000..a0e86b8d6
--- /dev/null
+++ b/contrib/rtauto/proof_search.mli
@@ -0,0 +1,49 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+type form=
+    Atom of int
+  | Arrow of form * form
+  | Bot 
+  | Conjunct of form * form
+  | Disjunct of form * form
+  
+type proof =
+    Ax of int
+  | I_Arrow of proof
+  | E_Arrow of int*int*proof
+  | D_Arrow of int*proof*proof
+  | E_False of int
+  | I_And of proof*proof
+  | E_And of int*proof
+  | D_And of int*proof
+  | I_Or_l of proof
+  | I_Or_r of proof
+  | E_Or of int*proof*proof
+  | D_Or of int*proof
+  | Pop of int*proof
+
+type state
+
+val project: state -> proof
+
+val init_state : ('a * form * 'b)  list -> form -> state
+
+val branching: state -> state list
+
+val success: state -> bool
+
+val pp: state -> unit
+
+val pr_form : form -> unit
+
+val reset_info : unit -> unit
+
+val pp_info : unit -> unit
diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml
new file mode 100644
index 000000000..0865a825c
--- /dev/null
+++ b/contrib/rtauto/refl_tauto.ml
@@ -0,0 +1,337 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+module Search = Explore.Make(Proof_search)
+
+open Util
+open Term
+open Termops
+open Names
+open Evd
+open Tacmach
+open Proof_search
+
+let force count lazc = incr count;Lazy.force lazc 
+
+let step_count = ref 0
+
+let node_count = ref 0  
+
+let logic_constant = 
+  Coqlib.gen_constant "refl_tauto" ["Init";"Logic"] 
+
+let li_False = lazy (destInd (logic_constant "False"))
+let li_and = lazy (destInd (logic_constant "and"))
+let li_or =  lazy (destInd (logic_constant "or"))
+
+let data_constant =
+  Coqlib.gen_constant "refl_tauto" ["Init";"Datatypes"] 
+
+let l_true_equals_true = 
+  lazy (mkApp(logic_constant "refl_equal", 
+        [|data_constant "bool";data_constant "true"|]))
+
+let pos_constant =
+  Coqlib.gen_constant "refl_tauto" ["NArith";"BinPos"]
+
+let l_xI = lazy (pos_constant "xI")
+let l_xO = lazy (pos_constant "xO")
+let l_xH = lazy (pos_constant "xH")
+
+let store_constant = 
+  Coqlib.gen_constant "refl_tauto" ["rtauto";"Bintree"]
+
+let l_empty = lazy (store_constant "empty")
+let l_push = lazy (store_constant "push")
+
+let constant=
+  Coqlib.gen_constant "refl_tauto" ["rtauto";"Rtauto"]
+
+let l_Reflect = lazy (constant "Reflect")
+
+let l_Atom = lazy (constant "Atom")
+let l_Arrow = lazy (constant "Arrow")
+let l_Bot = lazy (constant "Bot")
+let l_Conjunct = lazy (constant "Conjunct")
+let l_Disjunct = lazy (constant "Disjunct")
+
+let l_Ax = lazy (constant "Ax")
+let l_I_Arrow = lazy (constant "I_Arrow")
+let l_E_Arrow = lazy (constant "E_Arrow")
+let l_D_Arrow = lazy (constant "D_Arrow")
+let l_E_False = lazy (constant "E_False")
+let l_I_And = lazy (constant "I_And")
+let l_E_And = lazy (constant "E_And")
+let l_D_And = lazy (constant "D_And")
+let l_I_Or_l = lazy (constant "I_Or_l")
+let l_I_Or_r = lazy (constant "I_Or_r")
+let l_E_Or = lazy (constant "E_Or")
+let l_D_Or = lazy (constant "D_Or")
+
+
+let special_whd gl=
+  let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
+
+let special_nf gl=
+  let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
+    (fun t -> Closure.norm_val infos (Closure.inject t))
+
+type atom_env=
+    {mutable next:int;
+     mutable env:(constr*int) list}
+
+let make_atom atom_env term=
+  try
+    let (_,i)=
+      List.find (fun (t,_)-> eq_constr term t) atom_env.env
+    in Atom i
+  with Not_found ->
+    let i=atom_env.next in
+      atom_env.env <- (term,i)::atom_env.env;
+      atom_env.next<- i + 1;
+      Atom i
+
+let rec make_form atom_env gls term =
+  let normalize=special_nf gls in
+  let cciterm=special_whd gls term  in
+    match kind_of_term cciterm with
+	Prod(_,a,b) -> 
+	  if not (dependent (mkRel 1) b) && 
+	    Retyping.get_sort_family_of 
+	    (pf_env gls) (Tacmach.project gls) a = InProp
+	  then 
+	    let fa=make_form atom_env gls a in
+	    let fb=make_form atom_env gls b in
+	      Arrow (fa,fb)
+	  else
+	    make_atom atom_env (normalize term)
+      | Cast(a,b) -> 
+	  make_form atom_env gls a
+      | Ind ind ->
+	  if ind = Lazy.force li_False then
+	    Bot
+	  else
+	    make_atom atom_env (normalize term)
+      | App(hd,argv) when Array.length argv = 2 ->
+	  begin
+	    try 
+	      let ind = destInd hd in
+		if ind = Lazy.force li_and then
+		  let fa=make_form atom_env gls argv.(0) in
+		  let fb=make_form atom_env gls argv.(1) in
+		    Conjunct (fa,fb)
+		else if ind = Lazy.force li_or then
+		  let fa=make_form atom_env gls argv.(0) in
+		  let fb=make_form atom_env gls argv.(1) in
+		    Disjunct (fa,fb)
+		else make_atom atom_env (normalize term)
+	    with Invalid_argument _ -> make_atom atom_env (normalize term)
+	  end
+      | _ -> make_atom atom_env (normalize term)
+
+let rec make_hyps atom_env gls lenv = function
+    [] -> []
+  | (_,Some body,typ)::rest -> 
+      make_hyps atom_env gls (typ::body::lenv) rest  
+  | (id,None,typ)::rest ->
+      let hrec=
+	make_hyps atom_env gls (typ::lenv) rest in
+	if List.exists (dependent (mkVar id)) lenv || 
+	  (Retyping.get_sort_family_of 
+	     (pf_env gls) (Tacmach.project gls) typ <> InProp) 
+	then
+	  hrec 
+	else
+	  (id,make_form atom_env gls typ)::hrec
+
+let rec build_pos n =
+  if n<=1 then force node_count l_xH 
+  else if n land 1 = 0 then 
+    mkApp (force node_count l_xO,[|build_pos (n asr 1)|])
+  else 
+    mkApp (force node_count l_xI,[|build_pos (n asr 1)|])
+
+let rec build_form = function
+    Atom n -> mkApp (force node_count l_Atom,[|build_pos n|])
+  | Arrow (f1,f2) -> 
+      mkApp (force node_count l_Arrow,[|build_form f1;build_form f2|])
+  | Bot -> force node_count l_Bot
+  | Conjunct (f1,f2) -> 
+      mkApp (force node_count l_Conjunct,[|build_form f1;build_form f2|])
+  | Disjunct (f1,f2) -> 
+      mkApp (force node_count l_Disjunct,[|build_form f1;build_form f2|])
+
+let rec decal k = function 
+    [] -> k
+  | (start,delta)::rest -> 
+      if k>start then
+	k - delta
+      else 
+	decal k rest
+
+let add_pop size d pops=
+  match pops with
+      [] -> [size+d,d]
+    | (_,sum)::_ -> (size+sum,sum+d)::pops  
+
+let rec build_proof pops size = 
+  function
+      Ax i ->
+	mkApp (force step_count l_Ax,
+	       [|build_pos (decal i pops)|])
+      | I_Arrow p -> 
+	  mkApp (force step_count l_I_Arrow,
+		 [|build_proof pops (size + 1) p|])
+      | E_Arrow(i,j,p) -> 
+	  mkApp (force step_count l_E_Arrow, 
+		 [|build_pos (decal i pops);
+		   build_pos (decal j pops);
+		   build_proof pops (size + 1) p|])
+      | D_Arrow(i,p1,p2) -> 
+	  mkApp (force step_count l_D_Arrow, 
+		 [|build_pos (decal i pops);
+		   build_proof pops (size + 2) p1;
+		   build_proof pops (size + 1) p2|])
+      | E_False i -> 
+	  mkApp (force step_count l_E_False,
+		 [|build_pos (decal i pops)|])
+      | I_And(p1,p2) -> 
+	  mkApp (force step_count l_I_And, 
+		 [|build_proof pops size p1;
+		   build_proof pops size p2|])
+      | E_And(i,p) -> 
+	  mkApp (force step_count l_E_And,
+		 [|build_pos (decal i pops);
+		   build_proof pops (size + 2) p|])
+      | D_And(i,p) -> 
+	  mkApp (force step_count l_D_And,
+		 [|build_pos (decal i pops);
+		   build_proof pops (size + 1) p|])
+      | I_Or_l(p) -> 
+	  mkApp (force step_count l_I_Or_l,
+		 [|build_proof pops size p|])
+      | I_Or_r(p) -> 
+	  mkApp (force step_count l_I_Or_r,
+		 [|build_proof pops size p|])
+      | E_Or(i,p1,p2) ->
+	  mkApp (force step_count l_E_Or, 
+		 [|build_pos (decal i pops);
+		   build_proof pops (size + 1) p1;
+		   build_proof pops (size + 1) p2|])
+      | D_Or(i,p) -> 
+	  mkApp (force step_count l_D_Or,
+		 [|build_pos (decal i pops);
+		   build_proof pops (size + 2) p|])
+      | Pop(d,p) ->
+	  build_proof (add_pop size d pops) size p 
+	    
+let build_env gamma=
+  List.fold_right (fun (p,_) e -> 
+		     mkApp(force node_count l_push,[|mkProp;p;e|])) 
+    gamma.env (mkApp (force node_count l_empty,[|mkProp|]))
+
+open Goptions
+
+let verbose = ref false
+
+let opt_verbose=
+  {optsync=true;
+   optname="Rtauto Verbose";
+   optkey=SecondaryTable("Rtauto","Verbose");
+   optread=(fun () -> !verbose);
+   optwrite=(fun b -> verbose:=b)}
+
+let _ = declare_bool_option opt_verbose 
+
+let check = ref false
+
+let opt_check=
+  {optsync=true;
+   optname="Rtauto Check";
+   optkey=SecondaryTable("Rtauto","Check");
+   optread=(fun () -> !check);
+   optwrite=(fun b -> check:=b)}
+
+let _ = declare_bool_option opt_check 
+
+open Pp
+
+let rtauto_tac gls=
+  Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"];
+  let gamma={next=1;env=[]} in
+  let gl=gls.it.evar_concl in
+  let _=
+    if Retyping.get_sort_family_of 
+      (pf_env gls) (Tacmach.project gls) gl <> InProp 
+    then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in
+  let glf=make_form gamma gls gl in
+  let hyps=make_hyps gamma gls [gl] gls.it.evar_hyps in
+  let formula=
+    List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in  
+  let search_fun = 
+    if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then
+      Search.debug_depth_first
+    else 
+      Search.depth_first in
+  let _ = 
+    begin
+      reset_info ();
+      if !verbose then
+	msgnl (str "Starting proof-search ...");
+    end in
+  let search_start_time = System.get_time () in
+  let prf = 
+    try project (search_fun (init_state [] formula)) 
+    with Not_found ->
+      errorlabstrm "rtauto" (Pp.str "rtauto could'nt find any proof") in
+  let search_end_time = System.get_time () in
+  let _ = if !verbose then
+    begin
+      msgnl (str "Proof tree found in " ++ 
+	     System.fmt_time_difference search_start_time search_end_time);
+      pp_info ();
+      msgnl (str "Building proof term ... ")
+    end in
+  let build_start_time=System.get_time () in
+  let _ = step_count := 0; node_count := 0 in
+  let nhyps = List.length hyps in
+  let main = mkApp (force node_count l_Reflect,
+		    [|build_env gamma;
+		      build_form formula;
+		      build_proof [] 0 prf|]) in
+  let term=
+    Term.applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
+  let build_end_time=System.get_time () in
+  let _ = if !verbose then
+    begin
+      msgnl (str "Proof term built in " ++ 
+	     System.fmt_time_difference build_start_time build_end_time ++
+	     fnl () ++
+	     str "Proof size : " ++ int !step_count ++ 
+	     str " steps" ++ fnl () ++
+	     str "Proof term size : " ++ int (!step_count+ !node_count) ++
+	     str " nodes (constants)" ++ fnl () ++
+	     str "Giving proof term to Coq ... ")
+    end in
+  let tac_start_time = System.get_time () in
+  let result=
+    if !check then 
+      Tactics.exact_check term gls
+    else
+      Tactics.exact_no_check term gls in
+  let tac_end_time = System.get_time () in
+  let _ = 
+    if !check then msgnl (str "Proof term type-checking is on");
+    if !verbose then
+      msgnl (str "Internal tactic executed in " ++ 
+	     System.fmt_time_difference tac_start_time tac_end_time) in
+    result
+
diff --git a/contrib/rtauto/refl_tauto.mli b/contrib/rtauto/refl_tauto.mli
new file mode 100644
index 000000000..a6d68a226
--- /dev/null
+++ b/contrib/rtauto/refl_tauto.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(* $Id$ *)
+
+(* raises Not_found if no proof is found *)
+
+type atom_env=
+    {mutable next:int;
+     mutable env:(Term.constr*int) list}
+
+val make_form : atom_env ->
+    Proof_type.goal Tacmach.sigma -> Term.types -> Proof_search.form
+
+val make_hyps :
+    atom_env ->
+    Proof_type.goal Tacmach.sigma ->
+    Term.types list ->
+    (Names.identifier * Term.types option * Term.types) list ->
+    (Names.identifier * Proof_search.form) list
+
+val rtauto_tac : Proof_type.tactic