From dbd9f7d4de8286fdd54f4b5609576f33db1050a6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 7 Dec 2012 16:36:51 +0000 Subject: [PATCH] - pts_dummy/pts_dummy_new: non compiling parts commented out - tutorial: some comments added --- matita/matita/lib/pts_dummy/CC2FO_K.ma | 5 ++-- matita/matita/lib/pts_dummy/CC2FO_K_cube.ma | 11 ++++---- matita/matita/lib/pts_dummy/arity.ma | 5 ++-- matita/matita/lib/pts_dummy/arity_eval.ma | 5 ++-- matita/matita/lib/pts_dummy/convertibility.ma | 5 ++-- matita/matita/lib/pts_dummy/cube.ma | 7 ++--- matita/matita/lib/pts_dummy/degree.ma | 5 ++-- matita/matita/lib/pts_dummy/ext.ma | 2 +- matita/matita/lib/pts_dummy/ext_lambda.ma | 7 ++--- matita/matita/lib/pts_dummy/inversion.ma | 5 ++-- matita/matita/lib/pts_dummy/lift.ma | 8 ++++-- matita/matita/lib/pts_dummy/par_reduction.ma | 5 ++-- matita/matita/lib/pts_dummy/rc_eval.ma | 5 ++-- matita/matita/lib/pts_dummy/rc_hsat.ma | 5 ++-- matita/matita/lib/pts_dummy/rc_sat.ma | 5 ++-- matita/matita/lib/pts_dummy/reduction.ma | 9 +++---- matita/matita/lib/pts_dummy/sn.ma | 5 ++-- matita/matita/lib/pts_dummy/subject.ma | 7 ++--- matita/matita/lib/pts_dummy/subst.ma | 5 ++-- matita/matita/lib/pts_dummy/subterms.ma | 5 ++-- matita/matita/lib/pts_dummy/terms.ma | 6 ++--- matita/matita/lib/pts_dummy/types.ma | 7 ++--- matita/matita/lib/pts_dummy_new/arity.ma | 5 ++-- matita/matita/lib/pts_dummy_new/arity_eval.ma | 5 ++-- .../lib/pts_dummy_new/convertibility.ma | 5 ++-- matita/matita/lib/pts_dummy_new/cube.ma | 7 ++--- matita/matita/lib/pts_dummy_new/ext.ma | 2 +- matita/matita/lib/pts_dummy_new/ext_lambda.ma | 7 ++--- matita/matita/lib/pts_dummy_new/inversion.ma | 2 +- .../matita/lib/pts_dummy_new/par_reduction.ma | 6 ++--- matita/matita/lib/pts_dummy_new/rc_eval.ma | 4 +-- matita/matita/lib/pts_dummy_new/rc_hsat.ma | 5 ++-- matita/matita/lib/pts_dummy_new/rc_sat.ma | 5 ++-- matita/matita/lib/pts_dummy_new/reduction.ma | 26 +++++++++---------- matita/matita/lib/pts_dummy_new/sn.ma | 5 ++-- matita/matita/lib/pts_dummy_new/subject.ma | 6 ++--- matita/matita/lib/pts_dummy_new/subst.ma | 11 +++++--- matita/matita/lib/pts_dummy_new/subterms.ma | 2 +- matita/matita/lib/pts_dummy_new/terms.ma | 4 +-- matita/matita/lib/pts_dummy_new/thinning.ma | 6 ++--- matita/matita/lib/pts_dummy_new/types.ma | 18 ++++++------- matita/matita/lib/tutorial/chapter6.ma | 11 +++----- matita/matita/lib/tutorial/chapter7.ma | 7 +++-- 43 files changed, 154 insertions(+), 124 deletions(-) diff --git a/matita/matita/lib/pts_dummy/CC2FO_K.ma b/matita/matita/lib/pts_dummy/CC2FO_K.ma index 752ed00c0..0983db3ba 100644 --- a/matita/matita/lib/pts_dummy/CC2FO_K.ma +++ b/matita/matita/lib/pts_dummy/CC2FO_K.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "degree.ma". - +include "pts_dummy/degree.ma". +(* (* TO BE PUT ELSEWERE *) lemma cons_append_assoc: ∀A,a. ∀l1,l2:list A. (a::l1) @ l2 = a :: (l1 @ l2). // qed. @@ -149,3 +149,4 @@ let rec KI G ≝ match G with ]. interpretation "CC2FO: K interpretation (context)" 'IK G = (KI G). +*) diff --git a/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma b/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma index 814ce59fe..b70f731f1 100644 --- a/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma +++ b/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma @@ -12,13 +12,14 @@ (* *) (**************************************************************************) -include "CC2FO_K.ma". -include "cube.ma". -include "inversion.ma". - +include "pts_dummy/CC2FO_K.ma". +include "pts_dummy/cube.ma". +include "pts_dummy/inversion.ma". +(* (* The K interpretation in the λ-Cube *****************************************) lemma ki_type: ∀G,t,u. G ⊢_{CC} t : u → u = Sort 1 → 𝕂{G} ⊢_{FO} 𝕂{t}_[G] : u. #G #t #u #H elim H -H G t u [ #i #j * #_ @ax // -| #G #A #i #HA #IHA #Heq \ No newline at end of file +| #G #A #i #HA #IHA #Heq +*) diff --git a/matita/matita/lib/pts_dummy/arity.ma b/matita/matita/lib/pts_dummy/arity.ma index 3df7811c0..b5dd81df7 100644 --- a/matita/matita/lib/pts_dummy/arity.ma +++ b/matita/matita/lib/pts_dummy/arity.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/ext.ma". - +include "pts_dummy/ext.ma". +(* (* ARITIES ********************************************************************) (* An arity is a normal term representing the functional structure of a term. @@ -218,3 +218,4 @@ lemma nth_sort_comp: ∀E1,E2. E1 ≅ E2 → ∀i. nth i ? E1 sort ≅ nth i ? E2 sort. #E1 #E2 #H #i @(all2_nth … aeq) // qed. +*) diff --git a/matita/matita/lib/pts_dummy/arity_eval.ma b/matita/matita/lib/pts_dummy/arity_eval.ma index 6fcf0e0c0..8adcc4873 100644 --- a/matita/matita/lib/pts_dummy/arity_eval.ma +++ b/matita/matita/lib/pts_dummy/arity_eval.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/arity.ma". - +include "pts_dummy/arity.ma". +(* (* ARITY ASSIGNMENT ***********************************************************) (* the arity type *************************************************************) @@ -226,3 +226,4 @@ axiom cons_comp: ∀a1,a2. a1 ≅ a2 → ∀E1,E2. E1 ≅ E2 → a1 :: E1 ≅ a2 axiom pippo: ∀A:Type[0]. ∀a,b,c. (a::b) @ c = a :: b @ c. @A qed. *) +*) diff --git a/matita/matita/lib/pts_dummy/convertibility.ma b/matita/matita/lib/pts_dummy/convertibility.ma index 045463aaa..3f548c42d 100644 --- a/matita/matita/lib/pts_dummy/convertibility.ma +++ b/matita/matita/lib/pts_dummy/convertibility.ma @@ -9,8 +9,8 @@ \ / V_______________________________________________________________ *) -include "lambda/reduction.ma". - +include "pts_dummy/reduction.ma". +(* (* inductive T : Type[0] ≝ | Sort: nat → T @@ -71,3 +71,4 @@ theorem main1: ∀M,N. conv M N → |@(ex_intro … M) @(ex_intro … M) % // % // ] *) +*) diff --git a/matita/matita/lib/pts_dummy/cube.ma b/matita/matita/lib/pts_dummy/cube.ma index 8ac3d978c..c143261ad 100644 --- a/matita/matita/lib/pts_dummy/cube.ma +++ b/matita/matita/lib/pts_dummy/cube.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "convertibility.ma". -include "types.ma". - +include "pts_dummy/convertibility.ma". +include "pts_dummy/types.ma". +(* (* PURE TYPE SYSTEMS OF THE λ-CUBE ********************************************) inductive Cube_Ax: nat → nat → Prop ≝ @@ -41,3 +41,4 @@ inductive FO_Re: nat → nat → nat → Prop ≝ . definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv. +*) diff --git a/matita/matita/lib/pts_dummy/degree.ma b/matita/matita/lib/pts_dummy/degree.ma index 1fa4ee7ec..61caa58b1 100644 --- a/matita/matita/lib/pts_dummy/degree.ma +++ b/matita/matita/lib/pts_dummy/degree.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/ext_lambda.ma". - +include "pts_dummy/ext_lambda.ma". +(* (* DEGREE ASSIGNMENT **********************************************************) (* The degree of a term *******************************************************) @@ -158,3 +158,4 @@ lemma Deg_lift_subst: ∀v,w,G. [║v║_[║G║]] = ║[w]║*_[║G║] → >append_Deg >append_Deg DegHd_Lift; [2: //] >deg_lift; [2,3: >HGk /2/] <(deg_subst … k) // >HGk /2/ qed. +*) diff --git a/matita/matita/lib/pts_dummy/ext.ma b/matita/matita/lib/pts_dummy/ext.ma index d07234a71..f698ed591 100644 --- a/matita/matita/lib/pts_dummy/ext.ma +++ b/matita/matita/lib/pts_dummy/ext.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basics/list.ma". +include "basics/lists/list.ma". (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************) diff --git a/matita/matita/lib/pts_dummy/ext_lambda.ma b/matita/matita/lib/pts_dummy/ext_lambda.ma index e0455c204..3d4c0c86e 100644 --- a/matita/matita/lib/pts_dummy/ext_lambda.ma +++ b/matita/matita/lib/pts_dummy/ext_lambda.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "lambda/ext.ma". -include "lambda/subst.ma". - +include "pts_dummy/ext.ma". +include "pts_dummy/subst.ma". +(* (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************) (* substitution ***************************************************************) @@ -79,3 +79,4 @@ qed. lemma tsubst_sort: ∀n,l. (Sort n)[/l] = Sort n. // qed. +*) diff --git a/matita/matita/lib/pts_dummy/inversion.ma b/matita/matita/lib/pts_dummy/inversion.ma index 0c2c2a98b..63831f078 100644 --- a/matita/matita/lib/pts_dummy/inversion.ma +++ b/matita/matita/lib/pts_dummy/inversion.ma @@ -9,8 +9,8 @@ \ / V_______________________________________________________________ *) -include "lambda/types.ma". - +include "pts_dummy/types.ma". +(* (* inductive TJ (p: pts): list T → T → T → Prop ≝ | ax : ∀i,j. Ax p i j → TJ p (nil T) (Sort i) (Sort j) @@ -98,3 +98,4 @@ theorem abs_inv: ∀P,G,M,N. G ⊢ _{P} M : N → ∀A,b.M = Lambda A b → ] qed. +*) diff --git a/matita/matita/lib/pts_dummy/lift.ma b/matita/matita/lib/pts_dummy/lift.ma index 27d3d192e..036f8effa 100644 --- a/matita/matita/lib/pts_dummy/lift.ma +++ b/matita/matita/lib/pts_dummy/lift.ma @@ -9,7 +9,10 @@ \ / V_______________________________________________________________ *) -include "lambda/terms.ma". +include "pts_dummy/terms.ma". + +(* to be put elsewhere *) +definition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f]. (* arguments: k is the depth (starts from 0), p is the height (starts from 0) *) let rec lift t k p ≝ @@ -32,7 +35,7 @@ notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $ interpretation "Lift" 'Lift n k M = (lift M k n). (*** properties of lift ***) - +(* BEGIN HERE lemma lift_0: ∀t:T.∀k. lift t k 0 = t. #t (elim t) normalize // #n #k cases (leb (S n) k) normalize // qed. @@ -132,3 +135,4 @@ qed. lemma Lift_length: ∀p,G. |Lift G p| = |G|. #p #G elim G -G; normalize // qed. +*) \ No newline at end of file diff --git a/matita/matita/lib/pts_dummy/par_reduction.ma b/matita/matita/lib/pts_dummy/par_reduction.ma index cea1e177b..fec59888c 100644 --- a/matita/matita/lib/pts_dummy/par_reduction.ma +++ b/matita/matita/lib/pts_dummy/par_reduction.ma @@ -9,8 +9,8 @@ \ / V_______________________________________________________________ *) -include "lambda/subterms.ma". - +include "pts_dummy/subterms.ma". +(* (* inductive T : Type[0] ≝ | Sort: nat → T @@ -305,3 +305,4 @@ pr Q S ∧ pr P S. #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/ qed. +*) diff --git a/matita/matita/lib/pts_dummy/rc_eval.ma b/matita/matita/lib/pts_dummy/rc_eval.ma index 3fdeed410..87cfd11dc 100644 --- a/matita/matita/lib/pts_dummy/rc_eval.ma +++ b/matita/matita/lib/pts_dummy/rc_eval.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/rc_hsat.ma". - +include "pts_dummy/rc_hsat.ma". +(* (* THE EVALUATION *************************************************************) (* The arity of a term t in an environment E *) @@ -161,3 +161,4 @@ theorem append_cons: ∀(A:Type[0]). ∀(l1,l2:list A). ∀a. (a :: l1) @ l2 = a :: (l1 @ l2). // qed. *) + diff --git a/matita/matita/lib/pts_dummy/rc_hsat.ma b/matita/matita/lib/pts_dummy/rc_hsat.ma index 7426d812b..d46e613b4 100644 --- a/matita/matita/lib/pts_dummy/rc_hsat.ma +++ b/matita/matita/lib/pts_dummy/rc_hsat.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/rc_sat.ma". - +include "pts_dummy/rc_sat.ma". +(* (* HIGHER ORDER REDUCIBILITY CANDIDATES ***************************************) (* An arity is a type of λ→ to be used as carrier for a h.o. r.c. *) @@ -61,3 +61,4 @@ qed. lemma reflexive_defHRC: ∀P. defHRC P ≅^P defHRC P. #P (elim P) -P (normalize) /2/ qed. +*) diff --git a/matita/matita/lib/pts_dummy/rc_sat.ma b/matita/matita/lib/pts_dummy/rc_sat.ma index 3eb04315f..993e3cb36 100644 --- a/matita/matita/lib/pts_dummy/rc_sat.ma +++ b/matita/matita/lib/pts_dummy/rc_sat.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/sn.ma". - +include "pts_dummy/sn.ma". +(* (* REDUCIBILITY CANDIDATES ****************************************************) (* The reducibility candidate (r.c.) ******************************************) @@ -179,3 +179,4 @@ qed. definition lorRC: RC → RC → RC ≝ λB,C. mk_RC (lor_mem B C) …. /2/ qed. +*) diff --git a/matita/matita/lib/pts_dummy/reduction.ma b/matita/matita/lib/pts_dummy/reduction.ma index 58e4e179a..66bcd2890 100644 --- a/matita/matita/lib/pts_dummy/reduction.ma +++ b/matita/matita/lib/pts_dummy/reduction.ma @@ -9,9 +9,9 @@ \ / V_______________________________________________________________ *) -include "lambda/par_reduction.ma". +include "pts_dummy/par_reduction.ma". include "basics/star.ma". - +(* (* inductive T : Type[0] ≝ | Sort: nat → T @@ -353,7 +353,4 @@ lemma SN_APP: ∀P.SN P → ∀N. SN N → ∀M. @red_subst1 // ] qed. - - - - +*) diff --git a/matita/matita/lib/pts_dummy/sn.ma b/matita/matita/lib/pts_dummy/sn.ma index a9fbff370..193a04e94 100644 --- a/matita/matita/lib/pts_dummy/sn.ma +++ b/matita/matita/lib/pts_dummy/sn.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/ext_lambda.ma". - +include "pts_dummy/ext_lambda.ma". +(* (* STRONGLY NORMALIZING TERMS *************************************************) (* SN(t) holds when t is strongly normalizing *) @@ -68,3 +68,4 @@ axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M). axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M). axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M. +*) diff --git a/matita/matita/lib/pts_dummy/subject.ma b/matita/matita/lib/pts_dummy/subject.ma index be34cb07f..08ac86b48 100644 --- a/matita/matita/lib/pts_dummy/subject.ma +++ b/matita/matita/lib/pts_dummy/subject.ma @@ -9,9 +9,9 @@ \ / V_______________________________________________________________ *) -include "lambda/reduction.ma". -include "lambda/inversion.ma". - +include "pts_dummy/reduction.ma". +include "pts_dummy/inversion.ma". +(* (* inductive T : Type[0] ≝ | Sort: nat → T @@ -223,3 +223,4 @@ theorem subject_reduction: ∀P,G,M,N. G ⊢_{P} M:N → ] qed. +*) diff --git a/matita/matita/lib/pts_dummy/subst.ma b/matita/matita/lib/pts_dummy/subst.ma index 4f61ef528..8583f5810 100644 --- a/matita/matita/lib/pts_dummy/subst.ma +++ b/matita/matita/lib/pts_dummy/subst.ma @@ -9,8 +9,8 @@ \ / V_______________________________________________________________ *) -include "lambda/lift.ma". - +include "pts_dummy/lift.ma". +(* let rec subst t k a ≝ match t with [ Sort n ⇒ Sort n @@ -210,3 +210,4 @@ lemma subst_lemma_comm: ∀A,B,C.∀k,i. (A [i ≝ B]) [i+k ≝ C] = (A [i+k+1 := C]) [i ≝ B [k ≝ C]]. #A #B #C #k #i >commutative_plus >subst_lemma // qed. +*) diff --git a/matita/matita/lib/pts_dummy/subterms.ma b/matita/matita/lib/pts_dummy/subterms.ma index d2b7bee30..3fe2eecd5 100644 --- a/matita/matita/lib/pts_dummy/subterms.ma +++ b/matita/matita/lib/pts_dummy/subterms.ma @@ -9,8 +9,8 @@ \ / V_______________________________________________________________ *) -include "lambda/subst.ma". - +include "pts_dummy/subst.ma". +(* inductive subterm : T → T → Prop ≝ | appl : ∀M,N. subterm M (App M N) | appr : ∀M,N. subterm N (App M N) @@ -154,3 +154,4 @@ lemma size_subterm : ∀N,M. subterm N M → size N < size M. #N #M #subH (elim subH) normalize // #M1 #N1 #P #sub1 #sub2 #size1 #size2 @(transitive_lt … size1 size2) qed. +*) diff --git a/matita/matita/lib/pts_dummy/terms.ma b/matita/matita/lib/pts_dummy/terms.ma index 554f8099c..dc066c882 100644 --- a/matita/matita/lib/pts_dummy/terms.ma +++ b/matita/matita/lib/pts_dummy/terms.ma @@ -9,8 +9,8 @@ \ / V_______________________________________________________________ *) -include "basics/list.ma". -include "lambda/lambda_notation.ma". +include "basics/lists/list.ma". +include "pts_dummy/lambda_notation.ma". inductive T : Type[0] ≝ | Sort: nat → T (* starts from 0 *) @@ -30,7 +30,7 @@ let rec Appl F l on l ≝ match l with ]. lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N. -#N #l elim l -l // #hd #tl #IHl #M >IHl // +#N #l elim l -l // #hd #tl #IHl #M >IHl normalize // qed. (* diff --git a/matita/matita/lib/pts_dummy/types.ma b/matita/matita/lib/pts_dummy/types.ma index 0c07d2e70..acc0c8b13 100644 --- a/matita/matita/lib/pts_dummy/types.ma +++ b/matita/matita/lib/pts_dummy/types.ma @@ -9,10 +9,10 @@ \ / V_______________________________________________________________ *) -include "lambda/subst.ma". -include "basics/list.ma". - +include "pts_dummy/subst.ma". +include "basics/lists/list.ma". +(* (*************************** substl *****************************) let rec substl (G:list T) (N:T) : list T ≝ @@ -190,3 +190,4 @@ lemma tj_subst_0: ∀P,G,v,w. G ⊢_{P} v : w → ∀t,u. w :: G ⊢_{P} t : u #P #G #v #w #Hv #t #u #Ht lapply (substitution_tj … Ht ? ([]) … Hv) normalize // qed. +*) diff --git a/matita/matita/lib/pts_dummy_new/arity.ma b/matita/matita/lib/pts_dummy_new/arity.ma index 3df7811c0..b5dd81df7 100644 --- a/matita/matita/lib/pts_dummy_new/arity.ma +++ b/matita/matita/lib/pts_dummy_new/arity.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/ext.ma". - +include "pts_dummy/ext.ma". +(* (* ARITIES ********************************************************************) (* An arity is a normal term representing the functional structure of a term. @@ -218,3 +218,4 @@ lemma nth_sort_comp: ∀E1,E2. E1 ≅ E2 → ∀i. nth i ? E1 sort ≅ nth i ? E2 sort. #E1 #E2 #H #i @(all2_nth … aeq) // qed. +*) diff --git a/matita/matita/lib/pts_dummy_new/arity_eval.ma b/matita/matita/lib/pts_dummy_new/arity_eval.ma index 6fcf0e0c0..8adcc4873 100644 --- a/matita/matita/lib/pts_dummy_new/arity_eval.ma +++ b/matita/matita/lib/pts_dummy_new/arity_eval.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/arity.ma". - +include "pts_dummy/arity.ma". +(* (* ARITY ASSIGNMENT ***********************************************************) (* the arity type *************************************************************) @@ -226,3 +226,4 @@ axiom cons_comp: ∀a1,a2. a1 ≅ a2 → ∀E1,E2. E1 ≅ E2 → a1 :: E1 ≅ a2 axiom pippo: ∀A:Type[0]. ∀a,b,c. (a::b) @ c = a :: b @ c. @A qed. *) +*) diff --git a/matita/matita/lib/pts_dummy_new/convertibility.ma b/matita/matita/lib/pts_dummy_new/convertibility.ma index 377d3c890..23a9c6864 100644 --- a/matita/matita/lib/pts_dummy_new/convertibility.ma +++ b/matita/matita/lib/pts_dummy_new/convertibility.ma @@ -9,8 +9,8 @@ \ / V_______________________________________________________________ *) -include "lambda/reduction.ma". - +include "pts_dummy/reduction.ma". +(* (* inductive T : Type[0] ≝ | Sort: nat → T @@ -71,3 +71,4 @@ theorem main1: ∀M,N. CO M N → |@(ex_intro … M) @(ex_intro … M) % // % // ] *) +*) \ No newline at end of file diff --git a/matita/matita/lib/pts_dummy_new/cube.ma b/matita/matita/lib/pts_dummy_new/cube.ma index 8ac3d978c..c143261ad 100644 --- a/matita/matita/lib/pts_dummy_new/cube.ma +++ b/matita/matita/lib/pts_dummy_new/cube.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "convertibility.ma". -include "types.ma". - +include "pts_dummy/convertibility.ma". +include "pts_dummy/types.ma". +(* (* PURE TYPE SYSTEMS OF THE λ-CUBE ********************************************) inductive Cube_Ax: nat → nat → Prop ≝ @@ -41,3 +41,4 @@ inductive FO_Re: nat → nat → nat → Prop ≝ . definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv. +*) diff --git a/matita/matita/lib/pts_dummy_new/ext.ma b/matita/matita/lib/pts_dummy_new/ext.ma index 7e64aba31..dcbe395a9 100644 --- a/matita/matita/lib/pts_dummy_new/ext.ma +++ b/matita/matita/lib/pts_dummy_new/ext.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basics/list.ma". +include "basics/lists/list.ma". (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************) diff --git a/matita/matita/lib/pts_dummy_new/ext_lambda.ma b/matita/matita/lib/pts_dummy_new/ext_lambda.ma index a183047e0..fe2587ae8 100644 --- a/matita/matita/lib/pts_dummy_new/ext_lambda.ma +++ b/matita/matita/lib/pts_dummy_new/ext_lambda.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "lambda/ext.ma". -include "lambda/subst.ma". - +include "pts_dummy/ext.ma". +include "pts_dummy/subst.ma". +(* (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************) (* substitution ***************************************************************) @@ -79,3 +79,4 @@ qed. lemma tsubst_sort: ∀n,l. (Sort n)[/l] = Sort n. // qed. +*) diff --git a/matita/matita/lib/pts_dummy_new/inversion.ma b/matita/matita/lib/pts_dummy_new/inversion.ma index 511fa0309..6f1743ce2 100644 --- a/matita/matita/lib/pts_dummy_new/inversion.ma +++ b/matita/matita/lib/pts_dummy_new/inversion.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambdaN/thinning.ma". +include "pts_dummy_new/thinning.ma". (* inductive TJ (p: pts): list T → T → T → Prop ≝ diff --git a/matita/matita/lib/pts_dummy_new/par_reduction.ma b/matita/matita/lib/pts_dummy_new/par_reduction.ma index 260157d4c..d906160ca 100644 --- a/matita/matita/lib/pts_dummy_new/par_reduction.ma +++ b/matita/matita/lib/pts_dummy_new/par_reduction.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambdaN/subterms.ma". +include "pts_dummy_new/subterms.ma". (* inductive T : Type[0] ≝ @@ -88,7 +88,7 @@ lemma prD: ∀M,N,P. pr (D M N) P → @(ex_intro … M2) @(ex_intro … N2) /3/ ] qed. - +(* BEGIN HERE lemma prApp_not_lambda: ∀M,N,P. pr (App M N) P → is_lambda M = false → ∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1). @@ -292,4 +292,4 @@ theorem diamond: ∀P,Q,R. pr P Q → pr P R → ∃S. pr Q S ∧ pr P S. #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/ qed. - +*) diff --git a/matita/matita/lib/pts_dummy_new/rc_eval.ma b/matita/matita/lib/pts_dummy_new/rc_eval.ma index 3fdeed410..7b7ce54d9 100644 --- a/matita/matita/lib/pts_dummy_new/rc_eval.ma +++ b/matita/matita/lib/pts_dummy_new/rc_eval.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/rc_hsat.ma". - +include "pts_dummy/rc_hsat.ma". +(* (* THE EVALUATION *************************************************************) (* The arity of a term t in an environment E *) diff --git a/matita/matita/lib/pts_dummy_new/rc_hsat.ma b/matita/matita/lib/pts_dummy_new/rc_hsat.ma index 7426d812b..d46e613b4 100644 --- a/matita/matita/lib/pts_dummy_new/rc_hsat.ma +++ b/matita/matita/lib/pts_dummy_new/rc_hsat.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/rc_sat.ma". - +include "pts_dummy/rc_sat.ma". +(* (* HIGHER ORDER REDUCIBILITY CANDIDATES ***************************************) (* An arity is a type of λ→ to be used as carrier for a h.o. r.c. *) @@ -61,3 +61,4 @@ qed. lemma reflexive_defHRC: ∀P. defHRC P ≅^P defHRC P. #P (elim P) -P (normalize) /2/ qed. +*) diff --git a/matita/matita/lib/pts_dummy_new/rc_sat.ma b/matita/matita/lib/pts_dummy_new/rc_sat.ma index 3eb04315f..993e3cb36 100644 --- a/matita/matita/lib/pts_dummy_new/rc_sat.ma +++ b/matita/matita/lib/pts_dummy_new/rc_sat.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/sn.ma". - +include "pts_dummy/sn.ma". +(* (* REDUCIBILITY CANDIDATES ****************************************************) (* The reducibility candidate (r.c.) ******************************************) @@ -179,3 +179,4 @@ qed. definition lorRC: RC → RC → RC ≝ λB,C. mk_RC (lor_mem B C) …. /2/ qed. +*) diff --git a/matita/matita/lib/pts_dummy_new/reduction.ma b/matita/matita/lib/pts_dummy_new/reduction.ma index 82891b23b..ce3d6cc71 100644 --- a/matita/matita/lib/pts_dummy_new/reduction.ma +++ b/matita/matita/lib/pts_dummy_new/reduction.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambdaN/par_reduction.ma". +include "pts_dummy_new/par_reduction.ma". include "basics/star.ma". (* @@ -93,9 +93,9 @@ qed. definition reduct ≝ λn,m. red m n. -definition SN ≝ WF ? reduct. +definition SN : T → Prop ≝ WF ? reduct. -definition NF ≝ λM. ∀N. ¬ (reduct N M). +definition NF : T → Prop ≝ λM. ∀N. ¬ (reduct N M). theorem NF_to_SN: ∀M. NF M → SN M. #M #nfM % #a #red @False_ind /2/ @@ -149,13 +149,13 @@ qed. lemma star_appl: ∀M,M1,N. star … red M M1 → star … red (App M N) (App M1 N). #M #M1 #N #star1 (elim star1) // -#B #C #starMB #redBC #H @(inj … H) /2/ +#B #C #starMB #redBC #H /3 width=3/ qed. lemma star_appr: ∀M,N,N1. star … red N N1 → star … red (App M N) (App M N1). #M #N #N1 #star1 (elim star1) // -#B #C #starMB #redBC #H @(inj … H) /2/ +#B #C #starMB #redBC #H /3 width=3/ qed. lemma star_app: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → @@ -166,13 +166,13 @@ qed. lemma star_laml: ∀M,M1,N. star … red M M1 → star … red (Lambda M N) (Lambda M1 N). #M #M1 #N #star1 (elim star1) // -#B #C #starMB #redBC #H @(inj … H) /2/ +#B #C #starMB #redBC #H /3 width=3/ qed. lemma star_lamr: ∀M,N,N1. star … red N N1 → star … red (Lambda M N) (Lambda M N1). #M #N #N1 #star1 (elim star1) // -#B #C #starMB #redBC #H @(inj … H) /2/ +#B #C #starMB #redBC #H /3 width=3/ qed. lemma star_lam: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → @@ -183,13 +183,13 @@ qed. lemma star_prodl: ∀M,M1,N. star … red M M1 → star … red (Prod M N) (Prod M1 N). #M #M1 #N #star1 (elim star1) // -#B #C #starMB #redBC #H @(inj … H) /2/ +#B #C #starMB #redBC #H /3 width=3/ qed. lemma star_prodr: ∀M,N,N1. star … red N N1 → star … red (Prod M N) (Prod M N1). #M #N #N1 #star1 (elim star1) // -#B #C #starMB #redBC #H @(inj … H) /2/ +#B #C #starMB #redBC #H /3 width=3/ qed. lemma star_prod: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → @@ -200,13 +200,13 @@ qed. lemma star_dl: ∀M,M1,N. star … red M M1 → star … red (D M N) (D M1 N). #M #M1 #N #star1 (elim star1) // -#B #C #starMB #redBC #H @(inj … H) /2/ +#B #C #starMB #redBC #H /3 width=3/ qed. lemma star_dr: ∀M,N,N1. star … red N N1 → star … red (D M N) (D M N1). #M #N #N1 #star1 (elim star1) // -#B #C #starMB #redBC #H @(inj … H) /2/ +#B #C #starMB #redBC #H /3 width=3/ qed. lemma star_d: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → @@ -357,8 +357,8 @@ lemma SN_APP: ∀P.SN P → ∀N. SN N → ∀M. #P #snP (elim snP) #A #snA #HindA #N #snN (elim snN) #B #snB #HindB #M #snM1 (cut (SH M)) [@SN_to_SH @(SN_subst … snM1)] #shM -(generalize in match snM1) (elim shM) -#C #shC #HindC #snC1 % #Q #redQ (cases (red_app … redQ)) +generalize in match snM1; elim shM +#C #shC #HindC #snC1 % #Q #redQ cases (red_app … redQ); [* [* #M2 * #N2 * #eqlam destruct #eqQ // |* #M2 * #eqQ #redlam >eqQ (cases (red_lambda …redlam)) diff --git a/matita/matita/lib/pts_dummy_new/sn.ma b/matita/matita/lib/pts_dummy_new/sn.ma index a9fbff370..193a04e94 100644 --- a/matita/matita/lib/pts_dummy_new/sn.ma +++ b/matita/matita/lib/pts_dummy_new/sn.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lambda/ext_lambda.ma". - +include "pts_dummy/ext_lambda.ma". +(* (* STRONGLY NORMALIZING TERMS *************************************************) (* SN(t) holds when t is strongly normalizing *) @@ -68,3 +68,4 @@ axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M). axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M). axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M. +*) diff --git a/matita/matita/lib/pts_dummy_new/subject.ma b/matita/matita/lib/pts_dummy_new/subject.ma index e33364f6b..57619eba6 100644 --- a/matita/matita/lib/pts_dummy_new/subject.ma +++ b/matita/matita/lib/pts_dummy_new/subject.ma @@ -9,8 +9,8 @@ \ / V_______________________________________________________________ *) -include "lambdaN/reduction.ma". -include "lambdaN/inversion.ma". +include "pts_dummy_new/reduction.ma". +include "pts_dummy_new/inversion.ma". (* inductive T : Type[0] ≝ @@ -51,7 +51,7 @@ theorem type_of_type: ∀P,G,A,B. G ⊢_{P} A : B → (∀i. B ≠ Sort i) → |#G1 #A #i #t1 #_ #P @(ex_intro … i) @(weak … t1 t1) |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #H3 (cases (H1 ?) ) [#i #Bi @(ex_intro … i) @(weak … Bi t2) - |#i @(not_to_not … (H3 i)) // + |#i @(not_to_not … (H3 i)) /2 width=2/ ] |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #H3 @False_ind /2/ |#G1 #A #B #C #D #t1 #t2 #H1 #H2 #H3 cases (H1 ?); diff --git a/matita/matita/lib/pts_dummy_new/subst.ma b/matita/matita/lib/pts_dummy_new/subst.ma index 225316e81..469691073 100644 --- a/matita/matita/lib/pts_dummy_new/subst.ma +++ b/matita/matita/lib/pts_dummy_new/subst.ma @@ -9,7 +9,10 @@ \ / V_______________________________________________________________ *) -include "lambdaN/terms.ma". +include "pts_dummy_new/terms.ma". + +(* to be put elsewhere *) +definition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f]. (* arguments: k is the depth (starts from 0), p is the height (starts from 0) *) let rec lift t k p ≝ @@ -129,7 +132,7 @@ nnormalize; //; nqed. *) lemma subst_lift_k: ∀A,B.∀k. (lift B k 1)[k ≝ A] = B. #A #B (elim B) normalize /2/ #n #k @(leb_elim k n) normalize #Hnk - [cut (k ≤ n+1) [@transitive_le //] #H + [cut (k ≤ n+1); [@transitive_le //] #H >(le_to_leb_true … H) normalize >(not_eq_to_eqb_false k (n+1)) normalize /2/ |>(lt_to_leb_false … (not_le_to_lt … Hnk)) normalize // @@ -237,7 +240,7 @@ theorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k → [2,3,4,5: #T #T0 #Hind1 #Hind2 #i #j #k #leij #lejk @eq_f2 /2/ @Hind2 (applyS (monotonic_le_plus_l 1)) // |#n #i #j #k #leij #ltjk @(leb_elim i n) normalize #len - [cut (j < n + S k) + [cut (j < n + S k); [(le_to_leb_true j (n+S k)); [normalize >(not_eq_to_eqb_false j (n+S k)) normalize /2/ @@ -267,7 +270,7 @@ lemma subst_lemma: ∀A,B,C.∀k,i. [cut (k+i+1 = n); [/2/] #H1 >(le_to_leb_true (k+i+1) n) /2/ >(eq_to_eqb_true … H1) normalize - (generalize in match ltin) + generalize in match ltin; @(lt_O_n_elim … posn) #m #leim >delift // /2/ |(cut (k+i < n-1)) [@not_eq_to_le_to_lt; //] #Hlt >(le_to_leb_true (k+i+1) n); diff --git a/matita/matita/lib/pts_dummy_new/subterms.ma b/matita/matita/lib/pts_dummy_new/subterms.ma index 86a8507ed..bc7fa2a05 100644 --- a/matita/matita/lib/pts_dummy_new/subterms.ma +++ b/matita/matita/lib/pts_dummy_new/subterms.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambdaN/subst.ma". +include "pts_dummy_new/subst.ma". inductive subterm : T → T → Prop ≝ | appl : ∀M,N. subterm M (App M N) diff --git a/matita/matita/lib/pts_dummy_new/terms.ma b/matita/matita/lib/pts_dummy_new/terms.ma index 0227f1e94..1291013ff 100644 --- a/matita/matita/lib/pts_dummy_new/terms.ma +++ b/matita/matita/lib/pts_dummy_new/terms.ma @@ -9,8 +9,8 @@ \ / V_______________________________________________________________ *) -include "basics/list.ma". -include "lambda/lambda_notation.ma". +include "basics/lists/list.ma". +include "pts_dummy/lambda_notation.ma". inductive T : Type[0] ≝ | Sort: nat → T (* starts from 0 *) diff --git a/matita/matita/lib/pts_dummy_new/thinning.ma b/matita/matita/lib/pts_dummy_new/thinning.ma index 1fcd6fe62..b412392d4 100644 --- a/matita/matita/lib/pts_dummy_new/thinning.ma +++ b/matita/matita/lib/pts_dummy_new/thinning.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambdaN/types.ma". +include "pts_dummy_new/types.ma". (* inductive TJ (p: pts): list T → T → T → Prop ≝ @@ -82,14 +82,14 @@ lemma weak_gen: ∀P,E,M,N. E ⊢_{P} M : N → #Heq1 (lift_subst_up R S 1 0 (length ? D)) @(app … (lift Q (length ? D) 1)); [@Hind1 // |@Hind2 //] |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2 #G1 #D #A #l #Heq #tjA normalize @(abs … i); [cut (∀n. S n = n +1); [//] #H (delift (lift N O O) A1 O O O ??) // - (normalize in Heq) destruct /2/ - |#H #L #N1 #Heq (normalize in Heq) + normalize in Heq; destruct normalize /2/ + |#H #L #N1 #Heq normalize in Heq; #tjN1 normalize destruct; (applyS start) /2/ ] |#G #P #Q #R #i #tjP #tjR #Hind1 #Hind2 #G1 #D #N @@ -166,16 +166,16 @@ theorem substitution_tj: #Heq1 (plus_n_O (length ? D)) in ⊢ (? ? ? ? (? ? % ?)) - >(subst_lemma R S N ? 0) (applyS app) /2/ + #G1 #D #N #Heq #tjN normalize in Hind1 ⊢ %; + >(plus_n_O (length ? D)) in ⊢ (? ? ? ? (? ? % ?)); + >(subst_lemma R S N ? 0) applyS app /2/ |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2 #G1 #D #N #Heq #tjN normalize (applyS abs) - [normalize in Hind2 /2/ + [normalize in Hind2; /2/ |(* napplyS (Hind1 G1 (P::D) N ? tjN); sistemare *) generalize in match (Hind1 G1 (P::D) N ? tjN); - [#H (normalize in H) (applyS H) | normalize // ] + [#H normalize in H; applyS H | normalize // ] ] |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2 #G1 #D #N #Heq #tjN diff --git a/matita/matita/lib/tutorial/chapter6.ma b/matita/matita/lib/tutorial/chapter6.ma index d243ce5c0..364ad35de 100644 --- a/matita/matita/lib/tutorial/chapter6.ma +++ b/matita/matita/lib/tutorial/chapter6.ma @@ -48,10 +48,7 @@ w1,w2,...wk all belonging to l, such that l = w1w2...wk. We need to define the latter operations. The following flatten function takes in input a list of words and concatenates them together. *) -(* FG: flatten in list.ma gets in the way: -alias id "flatten" = "cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)". -does not work, so we use flatten in lists for now - +(* Already in the library let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ]. *) @@ -161,7 +158,7 @@ qed. lemma cat_to_star:∀S.∀A:word S → Prop. ∀w1,w2. A w1 → A^* w2 → A^* (w1@w2). #S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l)) -% destruct // normalize /2/ +% normalize destruct /2/ (* destruct added *) qed. lemma fix_star: ∀S.∀A:word S → Prop. @@ -170,7 +167,7 @@ lemma fix_star: ∀S.∀A:word S → Prop. [* #l generalize in match w; -w cases l [normalize #w * /2/] #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); * #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl)) - % destruct /2/ whd @(ex_intro … tl) /2/ + % destruct /2/ whd @(ex_intro … tl) /2/ (* destruct added *) |* [2: whd in ⊢ (%→?); #eqw sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ] ] -qed. \ No newline at end of file +qed. -- 2.39.2