Attempting to generalize rtauto - now with moduels

rtauto extension

(* Attempting to generalize the Gallina side of rtauto over the logic *)

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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.

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] _.

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.


Declare Scope Sem_scope.
Delimit Scope Sem_scope with sem.

Module Type RtautoLogic.

Parameter Sem : Type.
Parameter (STrue SFalse: Sem) (Simp Sand Sor : Sem -> Sem -> Sem).
Parameter holds : Sem -> Prop.

Bind Scope Sem_scope with Sem.

Notation "|- F" := (holds F) (at level 200): type_scope.

Infix "->" := Simp : Sem_scope.
Infix "/\" := Sand : Sem_scope.
Infix "\/" := Sor : Sem_scope.

Axiom AxK: forall {A B}, |- A -> B -> A.
Axiom AxS: forall {A B C}, |- (A -> B -> C) -> (A -> B) -> (A -> C).
Axiom MP : forall {A B}, (|- A -> B) -> (|- A) -> (|- B).
Axiom AxEF: forall {A}, |- SFalse -> A.

Axiom AxAndI: forall {A B}, |- A -> B -> A /\ B.
Axiom AxAndEL: forall {A B}, |- A /\ B -> A.
Axiom AxAndER: forall {A B}, |- A /\ B -> B.
Axiom AxOrIL: forall {A B}, |- A -> A \/ B.
Axiom AxOrIR: forall {A B}, |- B -> A \/ B.
Axiom AxOrE: forall {A B C}, |- A \/ B -> (A -> C) -> (B -> C) -> C.

End RtautoLogic.

(*
Module Type Classic.
Open RtautoLogic.
Axiom AxDNE: forall {A}, |- ((A -> SFalse) -> SFalse) -> A.

Lemma LmEF: forall {A}, |- SFalse -> A.
Proof.
  intro A.
  apply (compose AxDNE), AxK.
Qed.


Definition DNot (A:Sem): Sem := A -> SFalse.
Definition DOr (A B:Sem): Sem := DNot A -> B.
Definition DAnd (A B:Sem): Sem := DNot (DOr (DNot A) (DNot B)).

Lemma LmDNI: forall {A}, |- A -> ((A -> SFalse) -> SFalse).
Proof.
  intro A.
  (* fun a f => f a
     fun a => (S I) (K a)
     S (K (S I)) K *)
  exact (MP (MP AxS (MP AxK (MP AxS LmI))) AxK).
Defined.

Lemma DAndI: forall {A B}, |- A -> B -> DAnd A B.
Proof.
  intros A B.
  unfold DAnd. unfold DNot at 1, DOr. unfold DNot at 3.
  (* [a b f] => f (LMDNI a) b
     [a b] =>  C(CI(LMDNI a))b
     [a] =>  C((CI)(LMDNI a))
     (BC)(B(CI)LMDNI) *)
  refine (MP (MP LmB LmC) _).
  refine (MP (MP LmB (MP LmC LmI)) LmDNI).
Qed.
*)


Module RtautoSound(L:RtautoLogic).

Import L.

Section with_env.

Variable env:Store Sem.

Fixpoint interp_form (f:form): Sem :=
match f with
[n]=> match get n env with PNone => STrue | PSome P => P end
| A =>> B => (interp_form A) -> (interp_form B)
| # => SFalse
| A //\\ B => (interp_form A) /\ (interp_form B)
| A \\// B => (interp_form A) \/ (interp_form B)
end.

Notation "[[ A ]]" := (interp_form A) : Sem_scope.

Fixpoint interp_ctx (hyps:ctx) (F:Full hyps) (G:Sem) {struct F} : Sem :=
match F with
  F_empty => G
| F_push H hyps0 F0 =>  interp_ctx hyps0 F0  ([[H]] -> G)
end.

Ltac wipe := intros;simpl;constructor.


Definition LmI: forall {A}, |- A -> A :=
  (* (fun a => a) == (fun a => K a (K a)) == S K K *)
  fun A => MP (MP AxS AxK) (@AxK _ A).

(* Bxyz =x(yz) "right" *)
Lemma LmB: forall {A B C}, (|- (B -> C) -> (A -> B) -> A -> C).
Proof.
  intros A B C.
  (* fun x y z => x (y z)
     fun x y => S (K x) y
     fun x => S (K x)
     S (K S) K *)
  exact (MP (MP AxS (MP AxK AxS)) AxK).
Qed.

(* Cxyz = xzy "left" *)
Lemma LmC: forall {A B C}, (|- (A -> B -> C) -> B -> A -> C).
Proof.
  intros A B C.
  (* fun x y z => x z y
     fun x y => (S x) (K y)
     fun x => B (S x) K  -- or fun x => S(K(Sx))K
     S(fun x => B(Sx))(KK)
     S(BBS)(KK)
   *)
  exact (MP (MP AxS (MP (MP LmB LmB) AxS)) (MP AxK AxK)).
Qed.

(* B'Pxyz =Px(yz) "right over a direction string" *)
Lemma LmB': forall {A B C D},
    |- (B -> C -> D) -> B -> (A -> C) -> A -> D.
Proof.
  intros.
  (* fun p x y z => px(yz)
     fun p x y => B(px)y
     fun p x => B(px)
     fun p => BBp
     BB
   *)
  refine (MP LmB LmB).
Qed.

(* C'Pxyz =P(xz)y "left over a direction string" *)
Lemma LmC': forall {A B C D},
    |- (B -> C -> D) -> (A -> B) -> C -> A -> D.
Proof.
  intros.
  (* fun p x y z => p(xz)y
     fun p x y => C(Bpx)y
           @(@(p,@(x z)),y)
           @[C](@[B](p,x),y)
     fun p x => C(Bpx)
          @[C](@[B](p,x),o) ??
     fun p => BC(Bp)
          [x] @[C](@[B](p,x),o)
          @[BC](@[B](p,o),o)
     B(BC)B
   *)
  refine (MP (MP LmB (MP LmB LmC)) LmB).
Qed.

Lemma LmAndE: forall {A B C}, |- A /\ B -> (A -> B -> C) -> C.
Proof.
  intros.
  (* fun p f => f (andEL p) (andER p)
     fun p => C(CI(andEL p)) (andER p)
     S(BC(B(CI)andEL))andER
   *)
  refine (MP (MP AxS _) AxAndER).
  refine (MP (MP LmB LmC) _).
  refine (MP (MP LmB (MP LmC LmI)) AxAndEL).
Qed.

Definition compose: forall {A B C}, (|- B -> C) -> (|- A -> B) -> (|- A -> C) :=
  (* (fun a => f (g a)) == S (K f) g *)
  fun A B C f g => MP (MP AxS (MP AxK f)) g.

Lemma compose0 :
forall hyps F (A:Sem),
  |- A -> interp_ctx hyps F A.
Proof.
  induction F; intro A; simpl.
  - apply LmI.
  - apply (compose (IHF ([[a]] -> A)%sem)).
    exact AxK.
Qed.

Lemma composeApp :
forall hyps F (A B:Sem),
  |- interp_ctx hyps F (A -> B) -> interp_ctx hyps F A -> interp_ctx hyps F B.
Proof.
  induction F; intros A B; simpl.
  - apply LmI.
  - apply (compose (IHF ([[a]]->A) ([[a]]->B)))%sem.
    apply (MP (IHF _ _)).
    apply (MP (compose0 _ _ _)).
    exact AxS.
Qed.

Lemma under_hyps:
forall (hyps:ctx) F (A B G:Sem),
  (|- interp_ctx hyps F B -> G) ->
  |- (A -> B) -> interp_ctx hyps F A -> G.
Proof.
  induction F; simpl; intros A B G H.
  - exact (MP AxS (MP AxK H)).
  - apply (compose (IHF _ _ _ H)).
    exact (MP (MP AxS (MP AxK AxS)) AxK).
Qed.

Lemma under_hyps':
forall (hyps:ctx) F (A B G:Sem),
  (|- interp_ctx hyps F B -> G) ->
  |- interp_ctx hyps F (A -> B) -> interp_ctx hyps F A -> G.
Proof.
  intros.
  pose proof (composeApp hyps F A B) as Comp.
  refine (compose _ Comp).
  refine (MP AxS (MP AxK H)).
Qed.

Lemma compose1 :
forall hyps F (A B:Sem),
 |- (A -> B) ->
 (interp_ctx hyps F A) ->
 (interp_ctx hyps F B).
Proof.
  intros.
  apply under_hyps, LmI.
Qed.

Lemma compose1' :
forall hyps F (A B:Sem),
 (|- (A -> B)) ->
 (|-interp_ctx hyps F A) ->
 (|-interp_ctx hyps F B).
Proof.
  intros.
  exact (MP (MP (compose1 _ _ A B) H) H0).
Qed.

Theorem compose2 :
forall hyps F (A B C:Sem),
 |- (A -> B -> C) ->
 (interp_ctx hyps F A) ->
 (interp_ctx hyps F B) ->
 (interp_ctx hyps F C).
Proof.
  intros.
  apply under_hyps, composeApp.
Qed.

Theorem compose3 :
forall hyps F (A B C D:Sem),
 |- (A -> B -> C -> D) ->
 (interp_ctx hyps F A) ->
 (interp_ctx hyps F B) ->
 (interp_ctx hyps F C) ->
 (interp_ctx hyps F D).
Proof.
  intros.
  apply under_hyps, under_hyps', composeApp.
Qed.

Lemma drop_interp:
forall hyps F (A:Sem),
  (|- A) ->
  |- interp_ctx hyps F A.
Proof.
  intros.
  exact (MP (compose0 _ _ _) H).
Qed.

Theorem compose2' :
forall hyps F (A B C:Sem),
 (|- (A -> B -> C)) ->
 (|- interp_ctx hyps F A) ->
 (|- interp_ctx hyps F B) ->
 (|- interp_ctx hyps F C).
Proof.
  intros.
  pose proof (compose2 hyps F A B C).
  eauto using MP.
Qed.

Theorem compose3' :
forall hyps F (A B C D:Sem),
 (|- (A -> B -> C -> D)) ->
 (|- interp_ctx hyps F A) ->
 (|- interp_ctx hyps F B) ->
 (|- interp_ctx hyps F C) ->
 (|- interp_ctx hyps F D).
Proof.
  intros.
  pose proof (compose3 hyps F A B C D).
  eauto using MP.
Qed.

Lemma composeApp' :
forall hyps F (A B:Sem),
  (|- interp_ctx hyps F (A -> B)) ->
  (|- interp_ctx hyps F A) ->
  |- interp_ctx hyps F B.
Proof.
  intros ? ? A B HF HA.
  exact (MP (MP (composeApp hyps F A B) HF) HA).
Qed.

Lemma interpK :
  forall hyps F (A B:Sem),
    (|- interp_ctx hyps F A) ->
    |- interp_ctx hyps F (B -> A).
Proof.
  intros until B.
  apply MP.
  apply (MP (compose1 _ _ _ _)).
  apply AxK.
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]].
Proof.
induction F;simpl.
contradiction.
intros g H;destruct H.
solve[subst;apply drop_interp, LmI].
apply interpK;auto.
Qed.

Theorem project : forall hyps F p g,
get  p hyps = PSome g->
|- interp_ctx hyps F [[g]].
Proof.
intros hyps F p g e. apply project_In.
apply get_In with p;assumption.
Qed.

Arguments project [hyps] F [p g] _.

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 form_eq_refl in e;subst f.
  intros.
  repeat match goal with
  | [H : (|- interp_ctx ?Hyps ?F (_ -> ?G)) |- (|- interp_ctx ?Hyps ?F ?G)] =>
    apply (composeApp' Hyps F _ _ H)
  end.
  assumption.

- (* 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.
  intros.
  repeat match goal with
  | [H : (|- interp_ctx ?Hyps ?F (_ -> ?G)) |- (|- interp_ctx ?Hyps ?F ?G)] =>
    apply (composeApp' Hyps F _ _ H)
  end.
  revert H. apply compose1'.
  apply (MP (MP LmC LmB)), AxK.

- (* False_Elim *)
  simpl; case_eq (get p hyps); clean.
  intros f ef; destruct f; clean.
  intros _; generalize (project F ef).
  apply compose1'. apply AxEF.

- (* 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'. apply AxAndI.

- (* 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'.
  apply LmAndE.

- (* 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'.
  (*  (A/\B->C)  -> ((A->B->C) -> D) -> D
      x f => f (?? x)
      x => C I (?? x)
      B (C I) ??
   *)
  refine (MP (MP LmB (MP LmC LmI)) _).
  (* (A/\B->C) -> A -> B -> C
     f a b => f (andI a b)
     f a => B f (andI a)
     f => (B'B) f andI
     C(B'B)andI
   *)
  refine (MP (MP LmC (MP LmB' LmB)) AxAndI).

- (* Or_Intro_left *)
  destruct gl; clean.
  intro Hp; generalize (IHp hyps F gl1 Hp).
  apply compose1'; simpl.
  apply AxOrIL.

- (* Or_Intro_right *)
  destruct gl; clean.
  intro Hp; generalize (IHp hyps F gl2 Hp).
  apply compose1'; simpl.
  apply AxOrIR.

- (* 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'.
  apply AxOrE.

- (* 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'.
  (* (A \/ B -> C) -> ((A -> C) -> (B -> C) -> D) -> D
     x f => (f (??1 x)) (??2 x)
      x =>  C (C I (??1 x)) (??2 x)
      S(BC(B(CI)??1))??2 *)
  (*
    x f => (f (Bx orIL) (Bx orIR))
    x =>  C ((C I) (Bx orIL)) (B x orIR)
    S (BC (B(CI)(CB orIL))) (CB orIR)
   *)
  refine (MP (MP AxS (MP (MP LmB LmC) (MP (MP LmB (MP LmC LmI)) _))) _).
  refine (MP (MP LmC LmB) AxOrIL).
  refine (MP (MP LmC LmB) AxOrIR).

- (* 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.
  intros Ha Himp.
  revert Himp Ha. apply compose2', LmI.
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.

End RtautoSound.

Module RtautoProp <: RtautoLogic.
  Definition Sem := Prop.
  Definition STrue := True.
  Definition SFalse := False.
  Definition Simp := Basics.impl.
  Definition Sand := and.

  Definition Sor := or.
  Definition holds (p:Sem) := p.
  Definition AxK (A B:Prop) : holds (A -> B -> A) := fun a b => a.
  Definition AxS (A B C:Prop) : holds ((A -> B -> C) -> (A -> B) -> A -> C) := fun x y z => (x z (y z)).
  Definition MP (A B:Prop): holds (A -> B) -> holds A -> holds B := fun f x => f x.
  Definition AxEF (A:Prop) : holds (False -> A) := False_ind A.

  Definition AxAndI := conj.
  Definition AxAndEL := proj1.
  Definition AxAndER := proj2.
  Definition AxOrIL := or_introl.
  Definition AxOrIR := or_intror.
  Definition AxOrE (A B C:Prop) := fun p f g => @or_ind A B C f g p.

End RtautoProp.

Module R := RtautoSound RtautoProp.

(*
(* 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 R.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.

Parameters A B C D:Prop.
Theorem toto:A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).
rtauto.
exact (R.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.