From b8254eac73531e90312e3a40dc12ae51b18c5c92 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 26 Aug 2007 16:29:31 +0000 Subject: [PATCH] proof by "introduction" (impi) implemented in full --- .../matita/contribs/LOGIC/Track/defs.ma | 21 ++- .../matita/contribs/LOGIC/Track/inv.ma | 48 +++---- .../matita/contribs/LOGIC/Track/order.ma | 124 ++++++++++-------- .../matita/contribs/LOGIC/Track/props.ma | 42 +++--- .../matita/contribs/LOGIC/datatypes/Proof.ma | 14 +- 5 files changed, 122 insertions(+), 127 deletions(-) diff --git a/helm/software/matita/contribs/LOGIC/Track/defs.ma b/helm/software/matita/contribs/LOGIC/Track/defs.ma index ef83e6706..a9c4479ac 100644 --- a/helm/software/matita/contribs/LOGIC/Track/defs.ma +++ b/helm/software/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/helm/software/matita/contribs/LOGIC/Track/inv.ma b/helm/software/matita/contribs/LOGIC/Track/inv.ma index db945de13..347d7fccb 100644 --- a/helm/software/matita/contribs/LOGIC/Track/inv.ma +++ b/helm/software/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/helm/software/matita/contribs/LOGIC/Track/order.ma b/helm/software/matita/contribs/LOGIC/Track/order.ma index ee813d62c..de6ebaf71 100644 --- a/helm/software/matita/contribs/LOGIC/Track/order.ma +++ b/helm/software/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/helm/software/matita/contribs/LOGIC/Track/props.ma b/helm/software/matita/contribs/LOGIC/Track/props.ma index a7d79f571..fc57cf006 100644 --- a/helm/software/matita/contribs/LOGIC/Track/props.ma +++ b/helm/software/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/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma b/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma index 8643eb826..357b044f5 100644 --- a/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma +++ b/helm/software/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 *) . -- 2.39.2