[build] Consolidate stdlib's .v files under a single directory.

Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.

This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.

We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.

Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.

This could also imply a performance gain as we now effectively
traverse less directories when locating a library.

See also discussion in #10003

2 files changed, 795 insertions, 0 deletions

diff --git a/theories/rtauto/Bintree.v b/theories/rtauto/Bintree.v
new file mode 100644
index 0000000000..6b92445326
--- /dev/null
+++ b/theories/rtauto/Bintree.v
@@ -0,0 +1,385 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Export List.
+Require Export BinPos.
+Require Arith.EqNat.
+
+Open Scope positive_scope.
+
+Ltac clean := try (simpl; congruence).
+
+Lemma Gt_Psucc: forall p q,
+       (p ?= Pos.succ q) = Gt -> (p ?= q) = Gt.
+Proof.
+intros. rewrite <- Pos.compare_succ_succ.
+now apply Pos.lt_gt, Pos.lt_lt_succ, Pos.gt_lt.
+Qed.
+
+Lemma Psucc_Gt : forall p,
+       (Pos.succ p ?= p) = Gt.
+Proof.
+intros. apply Pos.lt_gt, Pos.lt_succ_diag_r.
+Qed.
+
+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 .
+
+Arguments Lget [A] n l.
+
+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;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;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 Arith.EqNat.beq_nat i (length l) then Some a else Lget i l.
+Proof.
+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.
+
+Inductive Poption {A} : Type:=
+  PSome : A -> Poption
+| PNone : Poption.
+Arguments Poption : clear implicits.
+
+Inductive Tree {A} : Type :=
+   Tempty : Tree
+ | Branch0 : Tree -> Tree -> Tree
+ | Branch1 : A -> Tree -> Tree -> Tree.
+Arguments Tree : clear implicits.
+
+Section Store.
+
+Variable A:Type.
+
+Notation Poption := (Poption A).
+Notation Tree := (Tree A).
+
+
+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) with
+         Eq => PSome a
+       | Lt => Tget i T
+       | Gt => Tget i T
+       end.
+Proof.
+intros i j.
+case_eq (i ?= j).
+intro H;rewrite (Pos.compare_eq _ _ H);intros a;clear i H.
+induction j;destruct T;simpl;try (apply IHj);congruence.
+unfold Pos.compare.
+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.
+unfold Pos.compare.
+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 (Pos.succ (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) = Gt -> get i S = PNone.
+Proof.
+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 push,index,get;simpl @contents.
+intros a S.
+rewrite Tget_Tadd.
+rewrite Psucc_Gt.
+intro W.
+change (get (Pos.succ (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) with
+    Eq => PSome a
+  | Lt => get i S
+  | Gt => PNone
+end.
+Proof.
+intros i a S F.
+case_eq (i ?= index S).
+intro e;rewrite (Pos.compare_eq _ _ e).
+destruct S;unfold get,push,index;simpl @contents;rewrite Tget_Tadd.
+rewrite Pos.compare_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.
+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.
+Proof.
+intros i a S F x H.
+case_eq (i ?= index S);intro test.
+rewrite (Pos.compare_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:=Pos.succ_not_1 (index S)).
+congruence.
+Qed.
+
+Lemma push_not_empty: forall a S, (push a S) <> empty.
+intros a [ind cont];unfold push,empty.
+intros [= H%Pos.succ_not_1]. assumption.
+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.
+case_eq (i ?= index S);simpl.
+left;congruence.
+right;eauto.
+congruence.
+Qed.
+
+End Store.
+
+Arguments PNone {A}.
+Arguments PSome [A] _.
+
+Arguments Tempty {A}.
+Arguments Branch0 [A] _ _.
+Arguments Branch1 [A] _ _ _.
+
+Arguments Tget [A] p T.
+Arguments Tadd [A] p a T.
+
+Arguments Tget_Tempty [A] p.
+Arguments Tget_Tadd [A] i j a T.
+
+Arguments mkStore [A] index contents.
+Arguments index [A] s.
+Arguments contents [A] s.
+
+Arguments empty {A}.
+Arguments get [A] i S.
+Arguments push [A] a S.
+
+Arguments get_empty [A] i.
+Arguments get_push_Full [A] i a S _.
+
+Arguments Full [A] _.
+Arguments F_empty {A}.
+Arguments F_push [A] a S _.
+Arguments In [A] x S F.
+
+Register empty as plugins.rtauto.empty.
+Register push as plugins.rtauto.push.
+
+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.
+
+Arguments Tmap [A B] f T.
+Arguments map [A B] f S.
+Arguments Full_map [A B f] S _.
+
+Notation "hyps \ A" := (push A hyps) (at level 72,left associativity).
diff --git a/theories/rtauto/Rtauto.v b/theories/rtauto/Rtauto.v
new file mode 100644
index 0000000000..2e9b4347b9
--- /dev/null
+++ b/theories/rtauto/Rtauto.v
@@ -0,0 +1,410 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+
+Require Export List.
+Require Export Bintree.
+Require Import Bool BinPos.
+
+Declare ML Module "rtauto_plugin".
+
+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;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.
+case_eq (form_eq p1 q1);clean.
+intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
+case_eq (form_eq p1 q1);clean.
+intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
+case_eq (form_eq p1 q1);clean.
+intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
+Qed.
+
+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.
+
+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.
+
+Arguments project [hyps] F [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.
+
+- (* Axiom *)
+  simpl;case_eq (get p hyps);clean.
+  intros f nth_f e;rewrite <- (form_eq_refl e).
+  apply project with p;trivial.
+
+- (* Arrow_Intro *)
+  destruct gl; clean.
+  simpl; intros.
+  change (interp_ctx (hyps\gl1)  (F_push gl1 hyps F) [[gl2]]).
+  apply IHp; try constructor; trivial.
+
+- (* Arrow_Elim *)
+  simpl check_proof; case_eq (get p hyps); clean.
+  intros f ef; case_eq (get p0 hyps); clean.
+  intros f0 ef0; destruct f0; clean.
+  case_eq (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.
+
+- (* Arrow_Destruct *)
+  simpl; case_eq (get p1 hyps); clean.
+  intros f ef; destruct f; clean.
+  destruct f1; clean.
+  case_eq (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.
+
+- (* False_Elim *)
+  simpl; case_eq (get p hyps); clean.
+  intros f ef; destruct f; clean.
+  intros _; generalize (project F ef).
+  apply compose1; apply False_ind.
+
+- (* And_Intro *)
+  simpl; destruct gl; clean.
+  case_eq (check_proof hyps gl1 p1); clean.
+  intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2).
+  apply compose2 ; simpl; auto.
+
+- (* And_Elim *)
+  simpl; case_eq (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.
+
+- (* And_Destruct*)
+  simpl; case_eq (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.
+
+- (* Or_Intro_left *)
+  destruct gl; clean.
+  intro Hp; generalize (IHp hyps F gl1 Hp).
+  apply compose1; simpl; auto.
+
+- (* Or_Intro_right *)
+  destruct gl; clean.
+  intro Hp; generalize (IHp hyps F gl2 Hp).
+  apply compose1; simpl; auto.
+
+- (* Or_elim *)
+  simpl; case_eq (get p1 hyps); clean.
+  intros f ef; destruct f; clean.
+  case_eq (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.
+
+- (* Or_Destruct *)
+  simpl; case_eq (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.
+
+- (* Cut *)
+  simpl; case_eq (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;case_eq (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.
+*)
+
+Register Reflect as plugins.rtauto.Reflect.
+
+Register Atom as plugins.rtauto.Atom.
+Register Arrow as plugins.rtauto.Arrow.
+Register Bot as plugins.rtauto.Bot.
+Register Conjunct as plugins.rtauto.Conjunct.
+Register Disjunct as plugins.rtauto.Disjunct.
+
+Register Ax as plugins.rtauto.Ax.
+Register I_Arrow as plugins.rtauto.I_Arrow.
+Register E_Arrow as plugins.rtauto.E_Arrow.
+Register D_Arrow as plugins.rtauto.D_Arrow.
+Register E_False as plugins.rtauto.E_False.
+Register I_And as plugins.rtauto.I_And.
+Register E_And as plugins.rtauto.E_And.
+Register D_And as plugins.rtauto.D_And.
+Register I_Or_l as plugins.rtauto.I_Or_l.
+Register I_Or_r as plugins.rtauto.I_Or_r.
+Register E_Or as plugins.rtauto.E_Or.
+Register D_Or as plugins.rtauto.D_Or.