From bfafdf7d8313ddd24c06d8ce3bba874f780403a9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 15 Mar 2011 12:03:55 +0000 Subject: [PATCH] - some ignores - new service lemmas --- matita/matita/lib/lambda/ext.ma | 41 ++++++- matita/matita/lib/lambda/rc_eval.ma | 179 ++++++++++++++++------------ matita/matita/lib/lambda/rc_hsat.ma | 10 +- matita/matita/lib/lambda/rc_sat.ma | 17 +-- 4 files changed, 151 insertions(+), 96 deletions(-) diff --git a/matita/matita/lib/lambda/ext.ma b/matita/matita/lib/lambda/ext.ma index d37fb9f52..cd619adf5 100644 --- a/matita/matita/lib/lambda/ext.ma +++ b/matita/matita/lib/lambda/ext.ma @@ -43,6 +43,10 @@ qed. (* lists **********************************************************************) +lemma length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|. +#A #l2 #l1 (elim l1) -l1 (normalize) // +qed. + (* all(?,P,l) holds when P holds for all members of l *) let rec all (A:Type[0]) (P:A→Prop) l on l ≝ match l with [ nil ⇒ True @@ -66,16 +70,45 @@ lemma all_append: ∀A,P,l2,l1. all A P l1 → all A P l2 → all A P (l1 @ l2). qed. (* all2(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *) -let rec all2 (A:Type[0]) (P:A→A→Prop) l1 l2 on l1 ≝ match l1 with +let rec all2 (A,B:Type[0]) (P:A→B→Prop) l1 l2 on l1 ≝ match l1 with [ nil ⇒ l2 = nil ? | cons hd1 tl1 ⇒ match l2 with [ nil ⇒ False - | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A P tl1 tl2 + | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A B P tl1 tl2 ] ]. -lemma length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|. -#A #l2 #l1 (elim l1) -l1 (normalize) // +lemma all2_length: ∀A,B:Type[0]. ∀P:A→B→Prop. + ∀l1,l2. all2 … P l1 l2 → |l1|=|l2|. +#A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ] +#x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ] +#x2 #l2 #_ #H elim H normalize /3/ +qed. + +lemma all2_hd: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b → + ∀l1,l2. all2 … P l1 l2 → P (hd … l1 a) (hd … l2 b). +#A #B #P #a #b #Hab #l1 elim l1 -l1 [ #l2 #H2 >H2 @Hab ] +#x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ] +#x2 #l2 #_ #H elim H // +qed. + +lemma all2_tl: ∀A,B:Type[0]. ∀P:A→B→Prop. + ∀l1,l2. all2 … P l1 l2 → all2 … P (tail … l1) (tail … l2). +#A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ] +#x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ] +#x2 #l2 #_ #H elim H // +qed. + +lemma all2_nth: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b → + ∀i,l1,l2. all2 … P l1 l2 → P (nth i … l1 a) (nth i … l2 b). +#A #B #P #a #b #Hab #i elim i -i [ @all2_hd // | #i #IH #l1 #l2 #H @IH /2/ ] +qed. + +lemma all2_append: ∀A,B,P,l2,m2. all2 A B P l2 m2 → + ∀l1,m1. all2 A B P l1 m1 → all2 A B P (l1 @ l2) (m1 @ m2). +#A #B #P #l2 #m2 #H2 #l1 (elim l1) -l1 [ #m1 #H >H @H2 ] +#x1 #l1 #IH1 #m2 elim m2 -m2 [ #false elim false ] +#x2 #m2 #_ #H elim H /3/ qed. (* terms **********************************************************************) diff --git a/matita/matita/lib/lambda/rc_eval.ma b/matita/matita/lib/lambda/rc_eval.ma index 515c67421..3fdeed410 100644 --- a/matita/matita/lib/lambda/rc_eval.ma +++ b/matita/matita/lib/lambda/rc_eval.ma @@ -12,115 +12,138 @@ (* *) (**************************************************************************) -include "lambda/rc_sat.ma". +include "lambda/rc_hsat.ma". (* THE EVALUATION *************************************************************) -(* The interpretation of a type t as a r.c. denoted by 〚t〛. - * For the "conv" rule we need 〚M〛 ≈ 〚N〛 when M and N are convertible, so: - * 1) 〚(λB.M N)〛 ≈ 〚N[0≝N]〛 implies that 〚(M N)〛 and 〚λB.M〛 are evaluated by - * stacking the application arguments like a reduction machine does - * 2) ∀M,N. 〚D M〛 ≈ 〚D N〛, implies that 〚D M〛 must be a constant. - *) -let rec ev E K t on t : RC ≝ match t with (* E: environment, K: stack *) - [ Sort _ ⇒ snRC (* from λ→ *) - | Rel i ⇒ nth i … E snRC (* from F *) - | App M N ⇒ ev E (ev E ([]) N :: K) M (* machine-like push *) - | Lambda _ M ⇒ ev (hd … K snRC :: E) (tail … K) M (* machine-like pop *) - | Prod N M ⇒ let C ≝ (ev E ([]) N) in - depRC C (ev (C :: E) K M) (* from λ→ and F *) - | D _ ⇒ snRC (* see note 2 above *) +(* The arity of a term t in an environment E *) +let rec aa E t on t ≝ match t with + [ Sort _ ⇒ SORT + | Rel i ⇒ nth i … E SORT + | App M N ⇒ pred (aa E M) + | Lambda N M ⇒ let Q ≝ aa E N in ABST Q (aa (Q::E) M) + | Prod N M ⇒ aa ((aa E N)::E) M + | D M ⇒ aa E M ]. -interpretation "interpretation of a type" 'Eval2 t E K = (ev E K t). +interpretation "arity assignment (term)" 'Eval1 t E = (aa E t). -(* extensional equality of the interpretations *) -definition eveq: T → T → Prop ≝ λt1,t2. ∀E,K. 〚t1〛_[E, K] ≅ 〚t2〛_[E, K]. - -interpretation - "extensional equality of the type interpretations" - 'napart t1 t2 = (eveq t1 t2). - -(* The interpretation of a context of types as a context of r.c.'s *) -let rec cev E G on G : list RC ≝ match G with +(* The arity of a type context *) +let rec caa E G on G ≝ match G with [ nil ⇒ E - | cons t F ⇒ let D ≝ cev E F in 〚t〛_[D,[]] :: D + | cons t F ⇒ let D ≝ caa E F in 〚t〛_[D] :: D ]. -interpretation "interpretation of a context" 'Eval1 G E = (cev E G). +interpretation "arity assignment (type context)" 'Eval1 G E = (caa E G). -theorem ev_app: ∀M,N,E,K. 〚App M N〛_[E, K] = 〚M〛_[E, 〚N〛_[E,[]]::K]. +lemma aa_app: ∀M,N,E. 〚App M N〛_[E] = pred (〚M〛_[E]). // qed. -theorem ev_lambda: ∀M,N,E,K. - 〚Lambda N M〛_[E, K] = 〚M〛_[hd … K snRC :: E, tail … K]. +lemma aa_lambda: ∀M,N,E. 〚Lambda N M〛_[E] = ABST (〚N〛_[E]) (〚M〛_[〚N〛_[E]::E]). // qed. -theorem ev_prod: ∀M,N,E,K. - 〚Prod N M〛_[E,K] = depRC (〚N〛_[E,[]]) (〚M〛_[〚N〛_[E,[]]::E,K]). +lemma aa_prod: ∀M,N,E. 〚Prod N M〛_[E] = 〚M〛_[〚N〛_[E]::E]. // qed. -theorem ev_repl: ∀t,E1,E2,K1,K2. E1 ≅ E2 → K1 ≅ K2 → 〚t〛_[E1,K1] ≅ 〚t〛_[E2,K2]. -#t (elim t) /5/ -qed. - -theorem ev_rel_lt: ∀K,D,E,i. (S i) ≤ |E| → 〚Rel i〛_[E @ D, K] = 〚Rel i〛_[E,K]. -#K #D #E (elim E) -E [1: #i #Hie (elim (not_le_Sn_O i)) #Hi (elim (Hi Hie)) ] +lemma aa_rel_lt: ∀D,E,i. (S i) ≤ |E| → 〚Rel i〛_[E @ D] = 〚Rel i〛_[E]. +#D #E (elim E) -E [1: #i #Hie (elim (not_le_Sn_O i)) #Hi (elim (Hi Hie)) ] #C #F #IHE #i (elim i) -i // #i #_ #Hie @IHE @le_S_S_to_le @Hie qed. -theorem ev_rel_ge: ∀K,D,E,i. (S i) ≰ |E| → - 〚Rel i〛_[E @ D, K] = 〚Rel (i-|E|)〛_[D,K]. -#K #D #E (elim E) -E [ normalize // ] +lemma aa_rel_ge: ∀D,E,i. (S i) ≰ |E| → + 〚Rel i〛_[E @ D] = 〚Rel (i-|E|)〛_[D]. +#D #E (elim E) -E [ normalize // ] #C #F #IHE #i (elim i) -i [1: -IHE #Hie (elim Hie) -Hie #Hie (elim (Hie ?)) /2/ ] normalize #i #_ #Hie @IHE /2/ qed. -theorem ev_app_repl: ∀M1,M2,N1,N2. M1 ≈ M2 → N1 ≈ N2 → - App M1 N1 ≈ App M2 N2. -#M1 #M2 #N1 #N2 #IHM #IHN #E #K >ev_app (@transitive_rceq) /3/ -qed. - -theorem ev_lambda_repl: ∀N1,N2,M1,M2. N1 ≈ N2 → M1 ≈ M2 → - Lambda N1 M1 ≈ Lambda N2 M2. -#N1 #N2 #M1 #M2 #IHN #IHM #E #K >ev_lambda (@transitive_rceq) // -qed. - -theorem ev_prod_repl: ∀N1,N2,M1,M2. N1 ≈ N2 → M1 ≈ M2 → - Prod N1 M1 ≈ Prod N2 M2. -#N1 #N2 #M1 #M2 #IHN #IHM #E #K >ev_prod @dep_repl // -(@transitive_rceq) [2: @IHM | skip ] /3/ -qed. - -(* weakeing and thinning lemma for the type interpretation *) +(* weakeing and thinning lemma arity assignment *) (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *) -theorem ev_lift: ∀E,Ep,t,Ek,K. - 〚lift t (|Ek|) (|Ep|)〛_[Ek @ Ep @ E, K] ≅ 〚t〛_[Ek @ E, K]. +lemma aa_lift: ∀E,Ep,t,Ek. + 〚lift t (|Ek|) (|Ep|)〛_[Ek @ Ep @ E] = 〚t〛_[Ek @ E]. #E #Ep #t (elim t) -t - [ #n >lift_sort /by SAT0_sort/ - | #i #Ek #K @(leb_elim (S i) (|Ek|)) #Hik - [ >(lift_rel_lt … Hik) >(ev_rel_lt … Hik) >(ev_rel_lt … Hik) // - | >(lift_rel_ge … Hik) >(ev_rel_ge … Hik) (ev_rel_ge …) (>length_append) + [ #n // + | #i #Ek @(leb_elim (S i) (|Ek|)) #Hik + [ >(lift_rel_lt … Hik) >(aa_rel_lt … Hik) >(aa_rel_lt … Hik) // + | >(lift_rel_ge … Hik) >(aa_rel_ge … Hik) (aa_rel_ge …) (>length_append) [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ] ] - | #M #N #IHM #IHN #Ek #K >lift_app >ev_app (@transitive_rceq) /3/ - | #N #M #IHN #IHM #Ek #K >lift_lambda >ev_lambda (@transitive_rceq) - [2: >commutative_plus @(IHM (? :: ?)) | skip ] // - | #N #M #IHN #IHM #Ek #K >lift_prod >ev_prod (@dep_repl) // - (@transitive_rceq) [2: >commutative_plus @(IHM (? :: ?)) | skip ] /3/ - | // + | /4/ + | #N #M #IHN #IHM #Ek >lift_lambda >aa_lambda + >commutative_plus >(IHM (? :: ?)) /3/ + | #N #M #IHN #IHM #Ek >lift_prod >aa_prod + >commutative_plus >(IHM (? :: ?)) /3/ + | #M #IHM #Ek @IHM ] qed. +(* substitution lemma arity assignment *) +(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *) +lemma aa_subst: ∀v,E,t,Ek. 〚t[|Ek|≝v]〛_[Ek @ E] = 〚t〛_[Ek @ 〚v〛_[E]::E]. +#v #E #t (elim t) -t + [ // + | #i #Ek @(leb_elim (S i) (|Ek|)) #H1ik + [ >(aa_rel_lt … H1ik) >(subst_rel1 … H1ik) >(aa_rel_lt … H1ik) // + | @(eqb_elim i (|Ek|)) #H2ik + [ >(aa_rel_ge … H1ik) >H2ik -H2ik H1ik >subst_rel2 + >(aa_lift ? ? ? ([])) (subst_rel3 … Hik)) (>aa_rel_ge) [2: /2/ ] + <(associative_append ? ? ([?]) ?) + >aa_rel_ge >length_append (>commutative_plus) + [ subst_lambda > aa_lambda + >commutative_plus >(IHM (? :: ?)) /3/ + | #N #M #IHN #IHM #Ek >subst_prod > aa_prod + >commutative_plus >(IHM (? :: ?)) /4/ + | #M #IHM #Ek @IHM +qed. + + + + + + + + + + + + + + + + + + + + (* -theorem tj_ev: ∀G,A,B. G ⊢A:B → ∀H,l. l ∈ 〚G〛_(H) → A[l] ∈ 〚B[l]〛_〚G〛_(H). -#G #A #B #tjAB (elim tjAB) -G A B tjAB - [ #i #j #_ #H #l #_ >substc_sort >substc_sort /2 by SAT0_sort/ - | #G #B #n #tjB #IH #H #l (elim l) -l (normalize) +(* extensional equality of the interpretations *) +definition eveq: T → T → Prop ≝ λt1,t2. ∀E,K. 〚t1〛_[E, K] ≅ 〚t2〛_[E, K]. + +interpretation + "extensional equality of the type interpretations" + 'napart t1 t2 = (eveq t1 t2). +*) + +axiom ev_lift_0_S: ∀t,p,C,E,K. 〚lift t 0 (S p)〛_[C::E, K] ≅ 〚lift t 0 p〛_[E, K]. + +theorem tj_ev: ∀G,t,u. G ⊢t:u → ∀E,l. l ∈ 〚G〛_[E] → t[l] ∈ 〚u[l]〛_[[], []]. +#G #t #u #tjtu (elim tjtu) -G t u tjtu + [ #i #j #_ #E #l #_ >tsubst_sort >tsubst_sort /2 by SAT0_sort/ + | #G #u #n #tju #IHu #E #l (elim l) -l (normalize) [ #_ /2 by SAT1_rel/ - | #C #D #IHl #mem (elim mem) -mem #mem #memc - >lift_0 >delift // >lift_0 + | #hd #tl #_ #H (elim H) -H #Hhd #Htl + >lift_0 >delift // >lift_0 + + + + (@mem_rceq_trans) [3: @symmetric_rceq @ev_lift_0_S | skip ] *) (* @@ -137,4 +160,4 @@ theorem tev_rel_S: ∀i,R,H. 〚Rel (S i)〛_(R::H) = 〚Rel i〛_(H). theorem append_cons: ∀(A:Type[0]). ∀(l1,l2:list A). ∀a. (a :: l1) @ l2 = a :: (l1 @ l2). // qed. -*) \ No newline at end of file +*) diff --git a/matita/matita/lib/lambda/rc_hsat.ma b/matita/matita/lib/lambda/rc_hsat.ma index 55f8cba43..7426d812b 100644 --- a/matita/matita/lib/lambda/rc_hsat.ma +++ b/matita/matita/lib/lambda/rc_hsat.ma @@ -17,10 +17,6 @@ include "lambda/rc_sat.ma". (* HIGHER ORDER REDUCIBILITY CANDIDATES ***************************************) (* An arity is a type of λ→ to be used as carrier for a h.o. r.c. *) -inductive ARITY: Type[0] ≝ - | SORT: ARITY - | IMPL: ARITY → ARITY → ARITY -. (* The type of the higher order r.c.'s having a given carrier. * a h.o. r.c is implemented as an inductively defined metalinguistic function @@ -28,7 +24,7 @@ inductive ARITY: Type[0] ≝ *) let rec HRC P ≝ match P with [ SORT ⇒ RC - | IMPL Q P ⇒ HRC Q → HRC P + | ABST Q P ⇒ HRC Q → HRC P ]. (* The default h.o r.c. @@ -36,7 +32,7 @@ let rec HRC P ≝ match P with *) let rec defHRC P ≝ match P return λP. HRC P with [ SORT ⇒ snRC - | IMPL Q P ⇒ λ_. defHRC P + | ABST Q P ⇒ λ_. defHRC P ]. (* extensional equality *******************************************************) @@ -47,7 +43,7 @@ let rec defHRC P ≝ match P return λP. HRC P with *) let rec hrceq P ≝ match P return λP. HRC P → HRC P → Prop with [ SORT ⇒ λC1,C2. C1 ≅ C2 - | IMPL Q P ⇒ λC1,C2. ∀B1,B2. hrceq Q B1 B2 → hrceq P (C1 B1) (C2 B2) + | ABST Q P ⇒ λC1,C2. ∀B1,B2. hrceq Q B1 B2 → hrceq P (C1 B1) (C2 B2) ]. interpretation diff --git a/matita/matita/lib/lambda/rc_sat.ma b/matita/matita/lib/lambda/rc_sat.ma index bcf829604..ddbafc71a 100644 --- a/matita/matita/lib/lambda/rc_sat.ma +++ b/matita/matita/lib/lambda/rc_sat.ma @@ -18,11 +18,11 @@ include "lambda/sn.ma". (* The reducibility candidate (r.c.) ******************************************) -(* We use saturated subsets of strongly normalizing terms - * (see for instance [Cescutti 2001], but a better citation is required) - * rather than standard reducibility candidates. +(* We use saturated subsets of strongly normalizing terms [1] + * rather than standard reducibility candidates [2]. * The benefit is that reduction is not needed to define such subsets. - * Also, this approach was never tried on a system with dependent types. + * [1] Geuvers, H. 1994. A Short and Flexible Proof of Strong Normalization for the Calculus of Constructions. + * [2] Barras, B. 1996. Coq en Coq. Rapport de Recherche 3026, INRIA. *) record RC : Type[0] ≝ { mem : T → Prop; @@ -42,6 +42,7 @@ interpretation "membership (reducibility candidate)" 'mem A R = (mem R A). definition snRC: RC ≝ mk_RC SN …. /2/ qed. +(* (* a generalization of mem on lists *) let rec memc E l on l : Prop ≝ match l with [ nil ⇒ True @@ -54,7 +55,7 @@ let rec memc E l on l : Prop ≝ match l with interpretation "componentwise membership (context of reducibility candidates)" 'mem l H = (memc H l). - +*) (* extensional equality of r.c.'s *********************************************) definition rceq: RC → RC → Prop ≝ @@ -80,11 +81,11 @@ qed. theorem transitive_rceq: transitive … rceq. #x #y #z #Hxy #Hyz #M (elim (Hxy M)) -Hxy (elim (Hyz M)) -Hyz /4/ qed. - +(* theorem reflexive_rceql: reflexive … rceql. #l (elim l) /2/ qed. - +*) (* HIDDEN BUG: * Without the type specification, this statement has two interpretations * but matita does not complain @@ -138,3 +139,5 @@ theorem dep_repl: ∀B1,B2,C1,C2. B1 ≅ B2 → C1 ≅ C2 → #B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2 [ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/ qed. + + -- 2.39.2