From: Ferruccio Guidi Date: Sun, 26 Aug 2007 16:36:34 +0000 (+0000) Subject: refactoring X-Git-Tag: make_still_working~6103 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4f1bd2790a4448a8ebfbe67eb8baa481c124745c;p=helm.git refactoring --- diff --git a/helm/software/matita/contribs/LOGIC/NTrack/defs.ma b/helm/software/matita/contribs/LOGIC/NTrack/defs.ma new file mode 100644 index 000000000..a9c4479ac --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/NTrack/defs.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/Track/defs". + +(* PROOF TREE TRACKS +*) + +include "datatypes/Proof.ma". +include "Insert/defs.ma". + +inductive Track: Context \to Proof \to Sequent \to Prop \def + | track_proj: \forall P,Q,S,i. Insert S i P Q \to Track Q (lref i) S + | track_posr: \forall P,h. + 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_impr: \forall P,r. \forall a,b:Formula. + Track P r (pair a b) \to + 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/NTrack/inv.ma b/helm/software/matita/contribs/LOGIC/NTrack/inv.ma new file mode 100644 index 000000000..347d7fccb --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/NTrack/inv.ma @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/Track/inv". + +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. + +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. +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. +qed. + +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. +qed. + +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 = 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 = impr r \land Track Q r (pair a b)). + intros; inversion H; clear H; intros; subst; + [ autobatch depth = 5 + | subst; autobatch depth = 4 + ]. +qed. diff --git a/helm/software/matita/contribs/LOGIC/NTrack/order.ma b/helm/software/matita/contribs/LOGIC/NTrack/order.ma new file mode 100644 index 000000000..de6ebaf71 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/NTrack/order.ma @@ -0,0 +1,103 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/Track/order". + +include "Track/props.ma". + +(* Order properties *********************************************************) + +theorem track_refl: \forall P. \forall c:Formula. \exists r. + Track P r (pair c c). + intros; elim c; clear c; + [ autobatch + | lapply (insert_total (pair f f1) zero P); [2:autobatch]; + 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_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 + ] + ] + ]. +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; +*) +*) diff --git a/helm/software/matita/contribs/LOGIC/NTrack/props.ma b/helm/software/matita/contribs/LOGIC/NTrack/props.ma new file mode 100644 index 000000000..fc57cf006 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/NTrack/props.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/Track/props". + +include "Insert/props.ma". +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; + [ 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_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; + [ 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_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/Track/defs.ma b/helm/software/matita/contribs/LOGIC/Track/defs.ma deleted file mode 100644 index a9c4479ac..000000000 --- a/helm/software/matita/contribs/LOGIC/Track/defs.ma +++ /dev/null @@ -1,38 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/LOGIC/Track/defs". - -(* PROOF TREE TRACKS -*) - -include "datatypes/Proof.ma". -include "Insert/defs.ma". - -inductive Track: Context \to Proof \to Sequent \to Prop \def - | track_proj: \forall P,Q,S,i. Insert S i P Q \to Track Q (lref i) S - | track_posr: \forall P,h. - 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_impr: \forall P,r. \forall a,b:Formula. - Track P r (pair a b) \to - 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 deleted file mode 100644 index 347d7fccb..000000000 --- a/helm/software/matita/contribs/LOGIC/Track/inv.ma +++ /dev/null @@ -1,65 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/LOGIC/Track/inv". - -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. - -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. -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. -qed. - -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. -qed. - -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 = 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 = impr r \land Track Q r (pair a b)). - intros; inversion H; clear H; intros; subst; - [ autobatch depth = 5 - | 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 deleted file mode 100644 index de6ebaf71..000000000 --- a/helm/software/matita/contribs/LOGIC/Track/order.ma +++ /dev/null @@ -1,103 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/LOGIC/Track/order". - -include "Track/props.ma". - -(* Order properties *********************************************************) - -theorem track_refl: \forall P. \forall c:Formula. \exists r. - Track P r (pair c c). - intros; elim c; clear c; - [ autobatch - | lapply (insert_total (pair f f1) zero P); [2:autobatch]; - 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_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 - ] - ] - ]. -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; -*) -*) diff --git a/helm/software/matita/contribs/LOGIC/Track/props.ma b/helm/software/matita/contribs/LOGIC/Track/props.ma deleted file mode 100644 index fc57cf006..000000000 --- a/helm/software/matita/contribs/LOGIC/Track/props.ma +++ /dev/null @@ -1,57 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/LOGIC/Track/props". - -include "Insert/props.ma". -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; - [ 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_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; - [ 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_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.