From f3091151495bc605ce2022e55741f6420f708d8e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 23 Mar 2011 21:31:24 +0000 Subject: [PATCH] - terms.ma: we included 'is_dummy" and "neutral" (maybe "is_neutral would be better) - sn.ma rc_sat.ma: we introduced the axioms for dummy --- matita/matita/lib/lambda/ext_lambda.ma | 15 ++------ matita/matita/lib/lambda/rc_sat.ma | 52 +++++++++++++++----------- matita/matita/lib/lambda/sn.ma | 25 +++++++++---- matita/matita/lib/lambda/terms.ma | 16 ++++++++ 4 files changed, 67 insertions(+), 41 deletions(-) diff --git a/matita/matita/lib/lambda/ext_lambda.ma b/matita/matita/lib/lambda/ext_lambda.ma index 952161107..a183047e0 100644 --- a/matita/matita/lib/lambda/ext_lambda.ma +++ b/matita/matita/lib/lambda/ext_lambda.ma @@ -17,19 +17,10 @@ include "lambda/subst.ma". (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************) -(* terms **********************************************************************) - -(* FG: not needed for now -(* nautral terms *) -inductive neutral: T → Prop ≝ - | neutral_sort: ∀n.neutral (Sort n) - | neutral_rel: ∀i.neutral (Rel i) - | neutral_app: ∀M,N.neutral (App M N) -. -*) - (* substitution ***************************************************************) - +(* +axiom is_dummy_lift: ∀p,t,k. is_dummy (lift t k p) = is_dummy t. +*) (* FG: do we need this? definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *) diff --git a/matita/matita/lib/lambda/rc_sat.ma b/matita/matita/lib/lambda/rc_sat.ma index ddbafc71a..4e15b07d3 100644 --- a/matita/matita/lib/lambda/rc_sat.ma +++ b/matita/matita/lib/lambda/rc_sat.ma @@ -29,7 +29,9 @@ record RC : Type[0] ≝ { cr1 : CR1 mem; sat0: SAT0 mem; sat1: SAT1 mem; - sat2: SAT2 mem + sat2: SAT2 mem; + sat3: SAT3 mem; (* we add the clusure by rev dapp *) + sat4: SAT4 mem (* we add the clusure by dummies *) }. (* HIDDEN BUG: * if SAT0 and SAT1 are expanded, @@ -65,21 +67,21 @@ interpretation "extensional equality (reducibility candidate)" 'Eq C1 C2 = (rceq C1 C2). -definition rceql ≝ λl1,l2. all2 ? rceq l1 l2. +definition rceql ≝ λl1,l2. all2 … rceq l1 l2. interpretation "extensional equality (context of reducibility candidates)" 'Eq C1 C2 = (rceql C1 C2). -theorem reflexive_rceq: reflexive … rceq. +lemma reflexive_rceq: reflexive … rceq. /2/ qed. -theorem symmetric_rceq: symmetric … rceq. -#x #y #H #M (elim (H M)) -H /3/ +lemma symmetric_rceq: symmetric … rceq. +#x #y #H #M elim (H M) -H /3/ qed. -theorem transitive_rceq: transitive … rceq. -#x #y #z #Hxy #Hyz #M (elim (Hxy M)) -Hxy (elim (Hyz M)) -Hyz /4/ +lemma 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. @@ -90,54 +92,60 @@ qed. * Without the type specification, this statement has two interpretations * but matita does not complain *) -theorem mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≅ C2 → M ∈ C2. -#M #C1 #C2 #H1 #H12 (elim (H12 M)) -H12 /2/ +lemma mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≅ C2 → M ∈ C2. +#M #C1 #C2 #H1 #H12 elim (H12 M) -H12 /2/ qed. - +(* (* NOTE: hd_repl and tl_repl are proved essentially by the same script *) -theorem hd_repl: ∀C1,C2. C1 ≅ C2 → ∀l1,l2. l1 ≅ l2 → hd ? l1 C1 ≅ hd ? l2 C2. +lemma hd_repl: ∀C1,C2. C1 ≅ C2 → ∀l1,l2. l1 ≅ l2 → hd ? l1 C1 ≅ hd ? l2 C2. #C1 #C2 #QC #l1 (elim l1) -l1 [ #l2 #Q >Q // ] #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ] #hd2 #tl2 #_ #Q elim Q // qed. -theorem tl_repl: ∀l1,l2. l1 ≅ l2 → tail ? l1 ≅ tail ? l2. +lemma tl_repl: ∀l1,l2. l1 ≅ l2 → tail ? l1 ≅ tail ? l2. #l1 (elim l1) -l1 [ #l2 #Q >Q // ] #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ] #hd2 #tl2 #_ #Q elim Q // qed. -theorem nth_repl: ∀C1,C2. C1 ≅ C2 → ∀i,l1,l2. l1 ≅ l2 → +lemma nth_repl: ∀C1,C2. C1 ≅ C2 → ∀i,l1,l2. l1 ≅ l2 → nth i ? l1 C1 ≅ nth i ? l2 C2. #C1 #C2 #QC #i (elim i) /3/ qed. - +*) (* the r.c for a (dependent) product type. ************************************) definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C. -theorem dep_cr1: ∀B,C. CR1 (dep_mem B C). +lemma dep_cr1: ∀B,C. CR1 (dep_mem B C). #B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) /2 by SAT0_sort/ /3/ (**) (* adiacent auto *) qed. -theorem dep_sat0: ∀B,C. SAT0 (dep_mem B C). +lemma dep_sat0: ∀B,C. SAT0 (dep_mem B C). /5/ qed. -theorem dep_sat1: ∀B,C. SAT1 (dep_mem B C). +lemma dep_sat1: ∀B,C. SAT1 (dep_mem B C). /5/ qed. (* NOTE: @sat2 is not needed if append_cons is enabled *) -theorem dep_sat2: ∀B,C. SAT2 (dep_mem B C). +lemma dep_sat2: ∀B,C. SAT2 (dep_mem B C). #B #C #N #L #M #l #HN #HL #HM #K #HK associative_append /3/ +qed. + +lemma dep_sat4: ∀B,C. SAT4 (dep_mem B C). +#B #C #N #HN #M #HM @SAT3_1 /3/ +qed. + definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) …. /2/ qed. -theorem dep_repl: ∀B1,B2,C1,C2. B1 ≅ B2 → C1 ≅ C2 → - depRC B1 C1 ≅ depRC B2 C2. +lemma dep_repl: ∀B1,B2,C1,C2. B1 ≅ B2 → C1 ≅ C2 → + depRC B1 C1 ≅ depRC B2 C2. #B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2 [ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/ qed. - - diff --git a/matita/matita/lib/lambda/sn.ma b/matita/matita/lib/lambda/sn.ma index c30cfecc7..9b6478455 100644 --- a/matita/matita/lib/lambda/sn.ma +++ b/matita/matita/lib/lambda/sn.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "lambda/ext.ma". +include "lambda/ext_lambda.ma". (* STRONGLY NORMALIZING TERMS *************************************************) @@ -34,12 +34,21 @@ definition SAT1 ≝ λ(P:?->Prop). ∀i,l. SNl l → P (Appl (Rel i) l). definition SAT2 ≝ λ(P:?→Prop). ∀N,L,M,l. SN N → SN L → P (Appl M[0:=L] l) → P (Appl (Lambda N M) (L::l)). -theorem SAT0_sort: ∀P,n. SAT0 P → P (Sort n). -#P #n #H @(H n (nil ?) …) // +definition SAT3 ≝ λ(P:?→Prop). ∀N,l1,l2. P (Appl (D (Appl N l1)) l2) → + P (Appl (D N) (l1@l2)). + +definition SAT4 ≝ λ(P:?→Prop). ∀M. P M → P (D M). + +lemma SAT0_sort: ∀P,n. SAT0 P → P (Sort n). +#P #n #HP @(HP n (nil ?) …) // +qed. + +lemma SAT1_rel: ∀P,i. SAT1 P → P (Rel i). +#P #i #HP @(HP i (nil ?) …) // qed. -theorem SAT1_rel: ∀P,i. SAT1 P → P (Rel i). -#P #i #H @(H i (nil ?) …) // +lemma SAT3_1: ∀P,N,M. SAT3 P → P (D (App N M)) → P (App (D N) M). +#P #N #M #HP #H @(HP … ([?]) ([])) @H qed. (* axiomatization *************************************************************) @@ -50,10 +59,12 @@ axiom sn_rel: SAT1 SN. axiom sn_beta: SAT2 SN. +axiom sn_dapp: SAT3 SN. + +axiom sn_dummy: SAT4 SN. + 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_dummy: ∀M. SN M → SN (D M). - axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M. diff --git a/matita/matita/lib/lambda/terms.ma b/matita/matita/lib/lambda/terms.ma index 915c13446..a0d262363 100644 --- a/matita/matita/lib/lambda/terms.ma +++ b/matita/matita/lib/lambda/terms.ma @@ -32,3 +32,19 @@ 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 // qed. + +let rec is_dummy t ≝ match t with + [ Sort _ ⇒ false + | Rel _ ⇒ false + | App M _ ⇒ is_dummy M + | Lambda _ M ⇒ is_dummy M + | Prod _ _ ⇒ false (* not so sure yet *) + | D _ ⇒ true + ]. + +(* nautral terms *) +inductive neutral: T → Prop ≝ + | neutral_sort: ∀n.neutral (Sort n) + | neutral_rel: ∀i.neutral (Rel i) + | neutral_app: ∀M,N.neutral (App M N) +. -- 2.39.2