From: Ferruccio Guidi Date: Tue, 25 Sep 2007 17:38:28 +0000 (+0000) Subject: bug fix in Track definition X-Git-Tag: 0.4.95@7852~146 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4d3fcebb0b24901b69f54d0eaf067885a80dcae0;p=helm.git bug fix in Track definition started PRed: parallel reduction simulating cut elimination --- diff --git a/matita/contribs/LOGIC/CLE/defs.ma b/matita/contribs/LOGIC/CLE/defs.ma index 7a2c7606c..31bd7694e 100644 --- a/matita/contribs/LOGIC/CLE/defs.ma +++ b/matita/contribs/LOGIC/CLE/defs.ma @@ -7,7 +7,8 @@ include "datatypes/Context.ma". inductive CLE: Nat \to Context \to Prop \def | cle_zero: \forall Q. CLE zero Q - | cle_succ: \forall Q,R,i. CLE i Q \to CLE (succ i) (abst Q R) + | cle_succ: \forall Q,i. CLE i Q \to + \forall p1,p2,R. CLE (succ i) (abst Q p1 p2 R) . interpretation "order relation between positions and contexts" diff --git a/matita/contribs/LOGIC/Insert/defs.ma b/matita/contribs/LOGIC/Insert/defs.ma index 7b72c5c7c..a5c9b273a 100644 --- a/matita/contribs/LOGIC/Insert/defs.ma +++ b/matita/contribs/LOGIC/Insert/defs.ma @@ -17,10 +17,14 @@ set "baseuri" "cic:/matita/LOGIC/Insert/defs". (* INSERT RELATION FOR CONTEXTS *) +include "Lift/defs.ma". include "datatypes/Context.ma". -inductive Insert (S:Sequent): Nat \to Context \to Context \to Prop \def - | insert_zero: \forall P. Insert S zero P (abst P S) - | insert_succ: \forall P,Q,R,i. - Insert S i P Q \to Insert S (succ i) (abst P R) (abst Q R) +inductive Insert (p,q:Proof) (S:Sequent): + Nat \to Context \to Context \to Prop \def + | insert_zero: \forall P. Insert p q S zero P (abst P p q S) + | insert_succ: \forall P,Q,i. Insert p q S i P Q \to + \forall p1,p2. Lift i (succ zero) p1 p2 \to + \forall q1,q2. Lift i (succ zero) q1 q2 \to \forall R. + Insert p q S (succ i) (abst P p1 q1 R) (abst Q p2 q2 R) . diff --git a/matita/contribs/LOGIC/Insert/fun.ma b/matita/contribs/LOGIC/Insert/fun.ma index 5661c0a27..f0cc5e514 100644 --- a/matita/contribs/LOGIC/Insert/fun.ma +++ b/matita/contribs/LOGIC/Insert/fun.ma @@ -18,7 +18,7 @@ include "CLE/defs.ma". include "Insert/inv.ma". (* Functional properties ****************************************************) - +(* theorem insert_total: \forall S,i,P. i <= P \to \exists Q. Insert S i P Q. intros 4; elim H; clear H i P; decompose; autobatch. @@ -31,3 +31,4 @@ theorem insert_inj: \forall S1,i,P, Q. Insert S1 i P Q \to | lapply linear insert_inv_succ to H3; decompose; subst; autobatch ]. qed. +*) diff --git a/matita/contribs/LOGIC/Insert/inv.ma b/matita/contribs/LOGIC/Insert/inv.ma index 229b9cc33..b612858a3 100644 --- a/matita/contribs/LOGIC/Insert/inv.ma +++ b/matita/contribs/LOGIC/Insert/inv.ma @@ -18,7 +18,7 @@ set "baseuri" "cic:/matita/LOGIC/Insert/inv". *) include "Insert/defs.ma". - +(* theorem insert_inv_zero: \forall S,P,Q. Insert S zero P Q \to Q = abst P S. intros; inversion H; clear H; intros; subst; autobatch. qed. @@ -54,3 +54,4 @@ theorem insert_inv_abst_2: \forall P,i. \forall R,S:Sequent. | clear H1. lapply linear insert_inv_leaf_2 to H. decompose ]. qed. +*) diff --git a/matita/contribs/LOGIC/Insert/props.ma b/matita/contribs/LOGIC/Insert/props.ma index 1e0bc5454..6daa22ea6 100644 --- a/matita/contribs/LOGIC/Insert/props.ma +++ b/matita/contribs/LOGIC/Insert/props.ma @@ -18,7 +18,7 @@ set "baseuri" "cic:/matita/LOGIC/Insert/props". *) include "Insert/fun.ma". - +(* theorem insert_conf: \forall P,Q1,S1,i1. Insert S1 i1 P Q1 \to \forall Q2,S2,i2. Insert S2 i2 P Q2 \to \exists Q,j1,j2. @@ -70,3 +70,4 @@ theorem insert_conf_rev_full: \forall P1,Q,S1,i1. Insert S1 i1 P1 Q \to | autobatch depth = 7 size = 8 ]. qed. +*) diff --git a/matita/contribs/LOGIC/Lift/defs.ma b/matita/contribs/LOGIC/Lift/defs.ma new file mode 100644 index 000000000..ae4f9cb0a --- /dev/null +++ b/matita/contribs/LOGIC/Lift/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/Lift/defs". + +(* PROOF RELOCATION +*) + +include "datatypes/Proof.ma". + +inductive Lift: Nat \to Nat \to Proof \to Proof \to Prop \def + | lift_lref_lt: \forall jd,jh,i. i < jd \to Lift jd jh (lref i) (lref i) + | lift_lref_ge: \forall jd,jh,i1,i2. jd <= i1 \to (i1 + jh == i2) \to + Lift jd jh (lref i1) (lref i2) + | lift_prin : \forall jd,jh,h. Lift jd jh (prin h) (prin h) + | lift_impw : \forall jd,jh,p1,p2. + Lift jd jh p1 p2 \to Lift jd jh (impw p1) (impw p2) + | lift_impr : \forall jd,jh,p1,p2. + Lift jd jh p1 p2 \to Lift jd jh (impr p1) (impr p2) + | lift_impi : \forall jd,jh,p1,p2. Lift jd jh p1 p2 \to + \forall q1,q2. Lift jd jh q1 q2 \to + \forall r1,r2. Lift (succ jd) jh r1 r2 \to + Lift jd jh (impi p1 q1 r1) (impi p2 q2 r2) + | lift_scut : \forall jd,jh,p1,p2. Lift jd jh p1 p2 \to + \forall q1,q2. Lift jd jh q1 q2 \to + Lift jd jh (scut p1 q1) (scut p2 q2) +. diff --git a/matita/contribs/LOGIC/NTrack/defs.ma b/matita/contribs/LOGIC/NTrack/defs.ma index b04cf4bd1..1bf18389f 100644 --- a/matita/contribs/LOGIC/NTrack/defs.ma +++ b/matita/contribs/LOGIC/NTrack/defs.ma @@ -17,9 +17,8 @@ set "baseuri" "cic:/matita/LOGIC/NTrack/defs". (* NORMAL PROOF TREE TRACKS *) -include "datatypes/Proof.ma". include "Insert/defs.ma". - +(* inductive NTrack: Context \to Proof \to Sequent \to Prop \def | ntrack_proj: \forall P,Q,S,i. Insert S i P Q \to NTrack Q (lref i) S | ntrack_posr: \forall P,h. @@ -36,3 +35,4 @@ inductive NTrack: Context \to Proof \to Sequent \to Prop \def Insert (pair A B) i P Q \to NTrack P (impi p q r) (pair (impl a b) D) . +*) diff --git a/matita/contribs/LOGIC/NTrack/inv.ma b/matita/contribs/LOGIC/NTrack/inv.ma index 9f334f19f..6c57c2040 100644 --- a/matita/contribs/LOGIC/NTrack/inv.ma +++ b/matita/contribs/LOGIC/NTrack/inv.ma @@ -15,7 +15,7 @@ set "baseuri" "cic:/matita/LOGIC/NTrack/inv". include "NTrack/defs.ma". - +(* theorem ntrack_inv_lref: \forall Q,S,i. NTrack Q (lref i) S \to \exists P. Insert S i P Q. intros; inversion H; clear H; intros; subst; autobatch. @@ -63,3 +63,4 @@ theorem ntrack_inv_lleaf_impl: | subst; autobatch depth = 4 ]. qed. +*) diff --git a/matita/contribs/LOGIC/NTrack/order.ma b/matita/contribs/LOGIC/NTrack/order.ma index 2b41ad83e..11868b6ef 100644 --- a/matita/contribs/LOGIC/NTrack/order.ma +++ b/matita/contribs/LOGIC/NTrack/order.ma @@ -18,7 +18,7 @@ include "Track/order.ma". include "NTrack/props.ma". (* Order properties *********************************************************) - +(* theorem ntrack_refl: \forall P. \forall c:Formula. \exists r. NTrack P r (pair c c). intros; elim c; clear c; @@ -36,3 +36,4 @@ theorem ntrack_trans: \forall p,q,A,B. \forall c:Formula. lapply linear ntrack_track to H1 as H; lapply linear track_trans to H0, H as H1; decompose; *) +*) diff --git a/matita/contribs/LOGIC/NTrack/props.ma b/matita/contribs/LOGIC/NTrack/props.ma index a7edc402f..7d41aebdf 100644 --- a/matita/contribs/LOGIC/NTrack/props.ma +++ b/matita/contribs/LOGIC/NTrack/props.ma @@ -17,7 +17,7 @@ set "baseuri" "cic:/matita/LOGIC/NTrack/props". include "Insert/props.ma". include "Track/defs.ma". include "NTrack/inv.ma". - +(* theorem ntrack_weak: \forall R,p,P,Q,S,i. NTrack P p S \to Insert R i P Q \to \exists q. NTrack Q q S. @@ -60,3 +60,4 @@ qed. theorem ntrack_track: \forall R,p,P. NTrack P p R \to Track P p R. intros; elim H names 0; clear H P p R; intros; autobatch width = 4. qed. +*) diff --git a/matita/contribs/LOGIC/PNF/defs.ma b/matita/contribs/LOGIC/PNF/defs.ma index 12a3b7be8..feea35b43 100644 --- a/matita/contribs/LOGIC/PNF/defs.ma +++ b/matita/contribs/LOGIC/PNF/defs.ma @@ -18,7 +18,8 @@ set "baseuri" "cic:/matita/LOGIC/PNF/defs". *) include "PRed/defs.ma". - +(* inductive PNF: Proof \to Prop \def | pnf: \forall p. (\forall q. p => q \to p = q) \to PNF p . +*) diff --git a/matita/contribs/LOGIC/PRed/defs.ma b/matita/contribs/LOGIC/PRed/defs.ma index 36b431098..ef0f86194 100644 --- a/matita/contribs/LOGIC/PRed/defs.ma +++ b/matita/contribs/LOGIC/PRed/defs.ma @@ -18,22 +18,40 @@ set "baseuri" "cic:/matita/LOGIC/PRed/defs". For cut elimination *) -include "datatypes/Proof.ma". - -inductive PRed: Proof \to Proof \to Prop \def - | pred_lref: \forall i. PRed (lref i) (lref i) - | pred_parx: \forall h. PRed (parx h) (parx h) - | pred_impw: \forall p1,p2. PRed p1 p2 \to PRed (impw p1) (impw p2) - | pred_impr: \forall p1,p2. PRed p1 p2 \to PRed (impr p1) (impr p2) - | pred_impi: \forall p1,p2. PRed p1 p2 \to \forall q1,q2. PRed q1 q2 \to - \forall r1,r2. PRed r1 r2 \to - PRed (impi p1 q1 r1) (impi p2 q2 r2) - | pred_scut: \forall p1,p2. PRed p1 p2 \to \forall q1,q2. PRed q1 q2 \to - PRed (scut p1 q1) (scut p2 q2) +include "Insert/defs.ma". + +inductive PRed: Context \to Proof \to Sequent \to + Context \to Proof \to Sequent \to Prop \def + | pred_lref: \forall P,i,S. PRed P (lref i) S P (lref i) S + | pred_prin: \forall P,h,S. PRed P (prin h) S P (prin h) S + | pred_impw: \forall Q1,Q2,p1,p2. (\forall S. PRed Q1 p1 S Q2 p2 S) \to + \forall S. PRed Q1 (impw p1) S Q2 (impw p2) S + | pred_impr: \forall Q1,Q2,p1,p2. (\forall S. PRed Q1 p1 S Q2 p2 S) \to + \forall S. PRed Q1 (impr p1) S Q2 (impr p2) S + | pred_impi: \forall Q1,Q2,p1,p2. (\forall S. PRed Q1 p1 S Q2 p2 S) \to + \forall q1,q2. (\forall S. PRed Q1 q1 S Q2 q2 S) \to + \forall r1,r2. (\forall S,R. PRed (abst Q1 p1 q1 R) r1 S (abst Q2 p2 q2 R) r2 S) \to + \forall S. PRed Q1 (impi p1 q1 r1) S Q2 (impi p2 q2 r2) S + | pred_scut: \forall Q1,Q2,p1,p2. (\forall S. PRed Q1 p1 S Q2 p2 S) \to + \forall q1,q2. (\forall S. PRed Q1 q1 S Q2 q2 S) \to + \forall S. PRed Q1 (scut p1 q1) S Q2 (scut p2 q2) S + | pred_a_sx: \forall p1,p2,R,P,Q1,i. Insert p1 p2 R i P Q1 \to + \forall q0,S,Q2. Insert p1 (scut p2 q0) S i P Q2 \to + \forall q. Lift zero i q0 q \to + PRed Q1 (scut (lref i) q) S Q2 (lref i) S + | pred_a_dx: \forall q1,q2,R,P,Q1,i. Insert q1 q2 R i P Q1 \to + \forall p0,S,Q2. Insert (scut p0 q1) q2 S i P Q2 \to + \forall p. Lift zero i p0 p \to + PRed Q1 (scut p (lref i)) S Q2 (lref i) S + | pred_b_sx: \forall q1,q2,P1,P2,S. PRed P1 q1 S P2 q2 S \to + \forall h. PRed P1 (scut (prin h) q1) S P2 q2 S + | pred_b_dx: \forall p1,p2,Q1,Q2,S. PRed Q1 p1 S Q2 p2 S \to + \forall h. PRed Q1 (scut p1 (prin h)) S Q2 p2 S . (*CSC: the URI must disappear: there is a bug now *) interpretation "single step parallel reduction in B->" - 'parred x y = (cic:/matita/LOGIC/PRed/defs/PRed.ind#xpointer(1/1) x y) + 'parred3 x1 y1 z1 x2 y2 z2 = + (cic:/matita/LOGIC/PRed/defs/PRed.ind#xpointer(1/1) x1 y1 z1 x2 y2 z2) . diff --git a/matita/contribs/LOGIC/Track/defs.ma b/matita/contribs/LOGIC/Track/defs.ma index c5e6e69be..25cf7c0b5 100644 --- a/matita/contribs/LOGIC/Track/defs.ma +++ b/matita/contribs/LOGIC/Track/defs.ma @@ -17,24 +17,23 @@ 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_proj: \forall P,Q,p1,p2,S,i. + Insert p1 p2 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 P (prin 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_impi: \forall P,p,q,r,A,B,D. \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) + Track (abst P p q (pair A B)) r (pair lleaf D) \to + Track P (impi p q r) (pair (impl a b) D) | track_scut: \forall P,p,q,A,B. \forall c:Formula. Track P p (pair A c) \to Track P q (pair c B) \to diff --git a/matita/contribs/LOGIC/Track/inv.ma b/matita/contribs/LOGIC/Track/inv.ma new file mode 100644 index 000000000..77d1107cd --- /dev/null +++ b/matita/contribs/LOGIC/Track/inv.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + +(* Main inversion lemmas ****************************************************) + +theorem track_inv_lref: \forall Q,S,i. Track Q (lref i) S \to + \exists p1,p2,P. Insert p1 p2 S i P Q. + intros; inversion H; clear H; intros; subst; autobatch depth = 4. +qed. + +theorem track_inv_prin: \forall P,S,h. Track P (prin 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 Q,p,S. Track Q (impr p) S \to + \exists a,b:Formula. + S = pair lleaf (impl a b) \land + Track Q 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 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 p q (pair A B)) r (pair lleaf D). + intros; inversion H; clear H; intros; subst; autobatch depth = 9 width = 4 size = 12. +qed. + +theorem track_inv_scut: \forall P,q,r,S. Track P (scut q r) S \to + \exists A,B. \exists c:Formula. + S = pair A B \land + Track P q (pair A c) \land + Track P r (pair c B). + intros; inversion H; clear H; intros; subst; autobatch depth = 6 size = 8. +qed. diff --git a/matita/contribs/LOGIC/Track/order.ma b/matita/contribs/LOGIC/Track/order.ma index 6487433dd..2c90f3303 100644 --- a/matita/contribs/LOGIC/Track/order.ma +++ b/matita/contribs/LOGIC/Track/order.ma @@ -18,7 +18,7 @@ include "Insert/fun.ma". include "Track/defs.ma". (* Order properties *********************************************************) - +(* theorem track_refl: \forall P. \forall c:Formula. \exists r. Track P r (pair c c). intros; elim c; clear c; @@ -33,3 +33,4 @@ theorem track_trans: \forall P,p,q,A,B. \forall c:Formula. \exists r. Track P r (pair A B). intros; autobatch. qed. +*) diff --git a/matita/contribs/LOGIC/Track/pred.ma b/matita/contribs/LOGIC/Track/pred.ma new file mode 100644 index 000000000..3b640b97c --- /dev/null +++ b/matita/contribs/LOGIC/Track/pred.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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/pred". + +(**) + +include "Track/inv.ma". +include "PRed/defs.ma". + +theorem track_pred: \forall Q1,Q2,p1,p2,S1,S2. PRed Q1 p1 S1 Q2 p2 S2 \to + Track Q1 p1 S1 \to Track Q2 p2 S2. + intros 7; elim H; clear H Q1 Q2 p1 p2 S1 S2; + [ autobatch + | autobatch + | lapply linear track_inv_impw to H3; decompose; subst; autobatch + | lapply linear track_inv_impr to H3; decompose; subst; autobatch + | lapply linear track_inv_impi to H7; decompose; subst; autobatch size = 7 + | lapply linear track_inv_scut to H5; decompose; subst; autobatch + | lapply linear track_inv_scut to H4; decompose; subst; + lapply linear track_inv_lref to H6; decompose; autobatch + | lapply linear track_inv_scut to H4; decompose; subst; + lapply linear track_inv_lref to H5; decompose; autobatch + | lapply linear track_inv_scut to H3; decompose; subst; + lapply linear track_inv_prin to H5; subst; autobatch + | lapply linear track_inv_scut to H3; decompose; subst; + lapply linear track_inv_prin to H4; subst; autobatch + ]. +qed. diff --git a/matita/contribs/LOGIC/datatypes/Context.ma b/matita/contribs/LOGIC/datatypes/Context.ma index 0de237801..44d626648 100644 --- a/matita/contribs/LOGIC/datatypes/Context.ma +++ b/matita/contribs/LOGIC/datatypes/Context.ma @@ -19,13 +19,15 @@ set "baseuri" "cic:/matita/LOGIC/datatypes/Context". - contexts: P Q *) +include "datatypes/Proof.ma". include "datatypes/Sequent.ma". inductive Context: Type \def | leaf: Context - | abst: Context \to Sequent \to Context + | abst: Context \to Proof \to Proof \to Sequent \to Context . - +(* definition inj: Sequent \to Context \def abst leaf. coercion cic:/matita/LOGIC/datatypes/Context/inj.con. +*) diff --git a/matita/contribs/LOGIC/datatypes/Proof.ma b/matita/contribs/LOGIC/datatypes/Proof.ma index 357b044f5..f6260b026 100644 --- a/matita/contribs/LOGIC/datatypes/Proof.ma +++ b/matita/contribs/LOGIC/datatypes/Proof.ma @@ -23,7 +23,7 @@ include "preamble.ma". inductive Proof: Type \def | lref: Nat \to Proof (* projection *) - | parx: Nat \to Proof (* *) + | prin: Nat \to Proof (* pos rel inhabitant *) | impw: Proof \to Proof (* weakening *) | impr: Proof \to Proof (* right introduction *) | impi: Proof \to Proof \to Proof \to Proof (* left introduction *) diff --git a/matita/contribs/LOGIC/preamble.ma b/matita/contribs/LOGIC/preamble.ma index 9f28e1bd3..b1e50f811 100644 --- a/matita/contribs/LOGIC/preamble.ma +++ b/matita/contribs/LOGIC/preamble.ma @@ -19,4 +19,4 @@ set "baseuri" "cic:/matita/LOGIC/preamble". (* PREAMBLE *) -include "../RELATIONAL/datatypes/Nat.ma". +include "../RELATIONAL/NLE/defs.ma".