From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 26 Aug 2007 16:29:31 +0000 (+0000)
Subject: proof by "introduction" (impi) implemented in full
X-Git-Tag: 0.4.95@7852~255
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=78d54ce55b983b74fa6cce3cb085f207215c5cac;p=helm.git

proof by "introduction" (impi) implemented in full
---

diff --git a/matita/contribs/LOGIC/Track/defs.ma b/matita/contribs/LOGIC/Track/defs.ma
index ef83e6706..a9c4479ac 100644
--- a/matita/contribs/LOGIC/Track/defs.ma
+++ b/matita/contribs/LOGIC/Track/defs.ma
@@ -26,18 +26,13 @@ inductive Track: Context \to Proof \to Sequent \to Prop \def
                  Track P (parx h) (pair (posr h) (posr h))
    | track_impw: \forall P,r,D,a,b. Track P r (pair lleaf D) \to
                  Track P (impw r) (pair (impl a b) D)
-   | track_impi: \forall P,r. \forall a,b:Formula. 
+   | track_impr: \forall P,r. \forall a,b:Formula. 
                  Track P r (pair a b) \to 
-                 Track P (impi r) (pair lleaf (impl a b))
-   | track_impe: \forall P,Q,r,D,i. \forall a,b:Formula.
-                 Track Q r (pair lleaf D) \to
-                 Insert (pair a b) i P Q \to
-                 Track P (impe r) (pair (impl a b) D) 
-(*   
-   | track_impe: \forall P,p,q,r,A,B,D,a,b.
-                 Track P p (pair A (rinj a)) \to
-                 Track P q (pair (linj b) B) \to
-		 Track (abst P (pair A B)) r (pair lleaf D) \to
-		 Track P (impe p q r) (pair (linj (impl a b)) D)
-*)
+                 Track P (impr r) (pair lleaf (impl a b))
+   | track_impi: \forall P,Q,p,q,r,A,B,D,i. \forall a,b:Formula.
+                 Track P p (pair A a) \to
+                 Track P q (pair b B) \to
+		 Track Q r (pair lleaf D) \to
+		 Insert (pair A B) i P Q \to
+		 Track P (impi p q r) (pair (impl a b) D)
 .
diff --git a/matita/contribs/LOGIC/Track/inv.ma b/matita/contribs/LOGIC/Track/inv.ma
index db945de13..347d7fccb 100644
--- a/matita/contribs/LOGIC/Track/inv.ma
+++ b/matita/contribs/LOGIC/Track/inv.ma
@@ -18,58 +18,48 @@ include "Track/defs.ma".
 
 theorem track_inv_lref: \forall Q,S,i. Track Q (lref i) S \to
                         \exists P. Insert S i P Q.
- intros. inversion H; clear H; intros; subst. autobatch.
-qed.     
+ intros; inversion H; clear H; intros; subst; autobatch.
+qed.
 
 theorem track_inv_parx: \forall P,S,h. Track P (parx h) S \to
                         S = pair (posr h) (posr h).
- intros. inversion H; clear H; intros; subst. autobatch.
+ intros; inversion H; clear H; intros; subst; autobatch.
 qed.
 
 theorem track_inv_impw: \forall P,p,S. Track P (impw p) S \to
                         \exists B,a,b. 
                         S = pair (impl a b) B \land 
                         Track P p (pair lleaf B).
- intros. inversion H; clear H; intros; subst. autobatch depth = 5.
+ intros; inversion H; clear H; intros; subst; autobatch depth = 5.
 qed.
 
-theorem track_inv_impi: \forall P,p,S. Track P (impi p) S \to
+theorem track_inv_impr: \forall P,p,S. Track P (impr p) S \to
                         \exists a,b:Formula. 
                         S = pair lleaf (impl a b) \land
                         Track P p (pair a b).
- intros. inversion H; clear H; intros; subst. autobatch depth = 4.
+ intros; inversion H; clear H; intros; subst; autobatch depth = 4.
 qed.
 
-theorem track_inv_impe: \forall P,r,S. Track P (impe r) S \to
-                        \exists Q,D,i. \exists a,b:Formula.
+theorem track_inv_impi: \forall P,p,q,r,S. Track P (impi p q r) S \to
+                        \exists Q,A,B,D,i. \exists a,b:Formula.
                         S = pair (impl a b) D \land
+                        Track P p (pair A a) \land
+                        Track P q (pair b B) \land
                         Track Q r (pair lleaf D) \land
-                        Insert (pair a b) i P Q.
- intros. inversion H; clear H; intros; subst. autobatch depth = 8 size = 10.
+                        Insert (pair A B) i P Q.
+ intros; inversion H; clear H; intros; subst; autobatch depth = 12 width = 5 size = 16.
+qed.
+
+theorem track_inv_scut: \forall P,q,r,S. Track P (scut q r) S \to False.
+ intros; inversion H; clear H; intros; subst.
 qed.
 
 theorem track_inv_lleaf_impl: 
    \forall Q,p,a,b. Track Q p (pair lleaf (impl a b)) \to
    (\exists P,i. p = lref i \land Insert (pair lleaf (impl a b)) i P Q) \lor
-   (\exists r. p = impi r \land Track Q r (pair a b)).
- intros. inversion H; clear H; intros; subst;
+   (\exists r. p = impr r \land Track Q r (pair a b)).
+ intros; inversion H; clear H; intros; subst;
  [ autobatch depth = 5
- | subst. autobatch depth = 4
- ].
-qed.
-(*
-theorem track_inv_impe: \forall P,p,q,r,S. Track P (impe p q r) S \to
-                        \exists A,B,D. \exists a,b:Formula.
-                        S = pair (impl a b) D \land
-                        Track P p (pair A a) \land
-                        Track P q (pair b B) \land
-                        Track (abst P (pair A B)) r (pair lleaf D).
- intros. inversion H; clear H; intros; subst;
- [ destruct H2
- | destruct H1
- | destruct H3
- | destruct H3
- | destruct H7. clear H7. subst. autobatch depth = 9
+ | subst; autobatch depth = 4
  ].
 qed.
-*)
diff --git a/matita/contribs/LOGIC/Track/order.ma b/matita/contribs/LOGIC/Track/order.ma
index ee813d62c..de6ebaf71 100644
--- a/matita/contribs/LOGIC/Track/order.ma
+++ b/matita/contribs/LOGIC/Track/order.ma
@@ -20,76 +20,84 @@ include "Track/props.ma".
 
 theorem track_refl: \forall P. \forall c:Formula. \exists r. 
                     Track P r (pair c c).
- intros. elim c; clear c;
+ intros; elim c; clear c;
  [ autobatch
  | lapply (insert_total (pair f f1) zero P); [2:autobatch];
-   decompose. autobatch depth = 5 
+   decompose; autobatch depth = 5 width = 4 size = 8
  ].
 qed.
-
+(*
 theorem track_trans: \forall p,q,A,B. \forall c:Formula.
                      Track leaf p (pair A c) \to Track leaf q (pair c B) \to
                      \exists r. Track leaf r (pair A B).
  intros 1; elim p names 0; clear p;
- [ intros. clear H1.
-   lapply linear track_inv_lref to H. decompose.
-   lapply insert_inv_leaf_2 to H. decompose
- | intros.
-   lapply linear track_inv_parx to H. subst. autobatch.
- | intros.
-   lapply linear track_inv_impw to H1.
-   decompose. subst.
-   lapply linear H to H4, H2. decompose. autobatch
- | intros 3. elim q; clear q;
-   [ clear H H1.
-     lapply linear track_inv_lref to H2. decompose.
-     lapply insert_inv_leaf_2 to H. decompose
-   | lapply linear track_inv_parx to H2. subst. autobatch
-   | clear H H1.
-     lapply linear track_inv_impi to H2.
-     lapply linear track_inv_impw to H3.
-     decompose. subst. autobatch
-   | clear H H1 H2.
-     lapply linear track_inv_impi to H3.
-     decompose. subst
-   | clear H H1.
-     lapply linear track_inv_impi to H2.
-     lapply linear track_inv_impe to H3.
-     decompose. subst. autobatch
+ [ intros; clear H1;
+   lapply linear track_inv_lref to H; decompose;
+   lapply insert_inv_leaf_2 to H; decompose
+ | intros;
+   lapply linear track_inv_parx to H; subst; autobatch;
+ | intros;
+   lapply linear track_inv_impw to H1;
+   decompose; subst;
+   lapply linear H to H4, H2; decompose; autobatch
+ | intros 3; elim q; clear q;
+   [ clear H H1;
+     lapply linear track_inv_lref to H2; decompose;
+     lapply insert_inv_leaf_2 to H; decompose
+   | lapply linear track_inv_parx to H2; subst; autobatch
+   | clear H H1;
+     lapply linear track_inv_impr to H2;
+     lapply linear track_inv_impw to H3;
+     decompose; subst; autobatch
+   | clear H H1 H2;
+     lapply linear track_inv_impr to H3;
+     decompose; subst
+   | clear H2 H3;
+     lapply linear track_inv_impr to H4;
+     lapply linear track_inv_impi to H5;
+     decompose; subst;
+     lapply linear H to H5, H8; decompose;
+     
+     
+     lapply linear insert_inv_leaf_1 to H4; decompose; subst;
+     apply ex_intro; [| ]
+     
+     autobatch depth = 100 width = 40 size = 100
    ]
- | intros 3. elim q; clear q;
-   [ clear H H1.
-     lapply linear track_inv_lref to H2. decompose.
-     lapply insert_inv_leaf_2 to H. decompose 
-   | clear H.
-     lapply linear track_inv_parx to H2.
-     subst. autobatch
-   | clear H H1.
-     lapply linear track_inv_impe to H2.
-     lapply linear track_inv_impw to H3.
-     decompose. subst. autobatch
-   | clear H H1 H2.
-     lapply linear track_inv_impi to H3. decompose. subst
-   | clear H H1.
-     lapply linear track_inv_impe to H2.
-     lapply linear track_inv_impe to H3.
-     decompose. subst.
-     lapply linear track_inv_lleaf_impl to H5. decompose; subst;
-     [ clear H4 H6.
-       lapply linear insert_inv_leaf_1 to H3. decompose. subst.
-       lapply linear insert_inv_abst_2 to H2. decompose. subst
-     | lapply insert_conf to H3, H4. clear H4. decompose.
-       lapply linear track_weak to H6, H4. decompose.
-       lapply linear track_comp to H2, H, H1. decompose. autobatch
+ | intros 3; elim q; clear q;
+   [ clear H H1;
+     lapply linear track_inv_lref to H2; decompose;
+     lapply insert_inv_leaf_2 to H; decompose 
+   | clear H;
+     lapply linear track_inv_parx to H2;
+     subst; autobatch
+   | clear H H1;
+     lapply linear track_inv_impe to H2;
+     lapply linear track_inv_impw to H3;
+     decompose; subst; autobatch
+   | clear H H1 H2;
+     lapply linear track_inv_impi to H3; decompose; subst
+   | clear H H1;
+     lapply linear track_inv_impe to H2;
+     lapply linear track_inv_impe to H3;
+     decompose; subst;
+     lapply linear track_inv_lleaf_impl to H5; decompose; subst;
+     [ clear H4 H6;
+       lapply linear insert_inv_leaf_1 to H3; decompose; subst;
+       lapply linear insert_inv_abst_2 to H2; decompose; subst
+     | lapply insert_conf to H3, H4; clear H4; decompose;
+       lapply linear track_weak to H6, H4; decompose;
+       lapply linear track_comp to H2, H, H1; decompose; autobatch
      ]
    ]
  ].
 qed.    
 (*   
-   | lapply linear track_inv_impi to H4.
-     lapply linear track_inv_impe to H5.
-     decompose. subst.
-     destruct H4. destruct H5. clear H4 H5. subst.
-     unfold linj in Hcut. unfold rinj in Hcut3. destruct Hcut. destruct Hcut3. clear Hcut Hcut3. subst.
-     destruct Hcut2. clear Hcut2. subst.
+   | lapply linear track_inv_impi to H4;
+     lapply linear track_inv_impe to H5;
+     decompose; subst;
+     destruct H4; destruct H5; clear H4 H5; subst;
+     unfold linj in Hcut; unfold rinj in Hcut3; destruct Hcut; destruct Hcut3; clear Hcut Hcut3; subst;
+     destruct Hcut2; clear Hcut2; subst;
+*)
 *)
diff --git a/matita/contribs/LOGIC/Track/props.ma b/matita/contribs/LOGIC/Track/props.ma
index a7d79f571..fc57cf006 100644
--- a/matita/contribs/LOGIC/Track/props.ma
+++ b/matita/contribs/LOGIC/Track/props.ma
@@ -20,34 +20,38 @@ include "Track/inv.ma".
 theorem track_weak: \forall R,p,P,Q,S,i. 
                     Track P p S \to Insert R i P Q \to 
                     \exists q. Track Q q S.
- intros 2. elim p; clear p;
+ intros 2; elim p; clear p;
  [ lapply linear track_inv_lref to H as H0; decompose;
    lapply linear insert_trans to H, H1; decompose; autobatch
- | lapply linear track_inv_parx to H. subst. autobatch
- | lapply linear track_inv_impw to H1. decompose. subst.
-   lapply linear H to H4, H2. decompose. autobatch
- | lapply linear track_inv_impi to H1. decompose. subst.
-   lapply linear H to H4, H2. decompose. autobatch
- | lapply linear track_inv_impe to H1. decompose. subst.
-   lapply linear insert_conf to H2, H4. decompose.
-   lapply linear H to H5, H3. decompose. autobatch
+ | lapply linear track_inv_parx to H; subst; autobatch
+ | lapply linear track_inv_impw to H1; decompose; subst;
+   lapply linear H to H4, H2; decompose; autobatch
+ | lapply linear track_inv_impr to H1; decompose; subst;
+   lapply linear H to H4, H2; decompose; autobatch
+ | lapply linear track_inv_impi to H3; decompose; subst;
+   lapply insert_conf to H4, H6; clear H6; decompose;
+   lapply H to H9, H4; clear H H9; lapply linear H1 to H8, H4;
+   lapply linear H2 to H7, H6; decompose; autobatch width = 4
+ | lapply linear track_inv_scut to H2; decompose
  ]
 qed.
 
 theorem track_comp: \forall R,q,p,P,Q,S,i. 
                     Track P p R \to Track Q q S \to Insert R i P Q \to
                     \exists r. Track P r S.
- intros 2. elim q; clear q;
+ intros 2; elim q; clear q;
  [ lapply linear track_inv_lref to H1 as H0; decompose;
    lapply linear insert_conf_rev_full to H1,H2; decompose; subst; autobatch
- | lapply linear track_inv_parx to H1. subst. autobatch
- | lapply linear track_inv_impw to H2. decompose. subst.
-   lapply linear H to H1, H5, H3. decompose. autobatch
- | lapply linear track_inv_impi to H2. decompose. subst.
-   lapply linear H to H1, H5, H3. decompose. autobatch
- | lapply linear track_inv_impe to H2. decompose. subst.
-   lapply linear insert_trans to H3, H5. decompose.
-   lapply track_weak to H1, H3. clear H1. decompose.
-   lapply linear H to H1, H6, H4. decompose. autobatch
+ | lapply linear track_inv_parx to H1; subst; autobatch
+ | lapply linear track_inv_impw to H2; decompose; subst;
+   lapply linear H to H1, H5, H3; decompose; autobatch
+ | lapply linear track_inv_impr to H2; decompose; subst;
+   lapply linear H to H1, H5, H3; decompose; autobatch
+ | lapply linear track_inv_impi to H4; decompose; subst;
+   lapply insert_trans to H5, H7; clear H7; decompose;
+   lapply track_weak to H3, H6; decompose;
+   lapply H to H3, H10, H5; clear H H10; lapply linear H1 to H3, H9, H5;
+   lapply linear H2 to H4, H8, H7; decompose; autobatch width = 4
+ | lapply linear track_inv_scut to H3; decompose
  ].
 qed.
diff --git a/matita/contribs/LOGIC/datatypes/Proof.ma b/matita/contribs/LOGIC/datatypes/Proof.ma
index 8643eb826..357b044f5 100644
--- a/matita/contribs/LOGIC/datatypes/Proof.ma
+++ b/matita/contribs/LOGIC/datatypes/Proof.ma
@@ -22,12 +22,10 @@ set "baseuri" "cic:/matita/LOGIC/datatypes/Proof".
 include "preamble.ma".
 
 inductive Proof: Type \def
-   | lref: Nat \to Proof
-   | parx: Nat \to Proof
-   | impw: Proof \to Proof
-   | impi: Proof \to Proof
-   | impe: Proof \to Proof
-(*   
-   | impe: Proof \to Proof \to Proof \to Proof
-*)
+   | lref: Nat \to Proof                       (* projection         *)
+   | parx: Nat \to Proof                       (*                    *)
+   | impw: Proof \to Proof                     (* weakening          *)
+   | impr: Proof \to Proof                     (* right introduction *)
+   | impi: Proof \to Proof \to Proof \to Proof (* left introduction  *)
+   | scut: Proof \to Proof \to Proof           (* symmetric cut      *)
 .