From f5f0e9cd26adc526ee69a693d5e10ccb47cc399e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 26 Feb 2011 20:28:06 +0000 Subject: [PATCH] - new file ext.ma with the objects needed for the normalization so far, that should be removed or should go into other files - sn.ma: we parametrized the saturation conditions - rc_sat.ma (first part of former rc.ma): we introduced extensional equality on candidates --- matita/matita/lib/lambda/ext.ma | 129 ++++++++++++++++++++++++++++ matita/matita/lib/lambda/rc.ma | 108 ----------------------- matita/matita/lib/lambda/rc_sat.ma | 133 +++++++++++++++++++++++++++++ matita/matita/lib/lambda/sn.ma | 46 +++++----- 4 files changed, 288 insertions(+), 128 deletions(-) create mode 100644 matita/matita/lib/lambda/ext.ma delete mode 100644 matita/matita/lib/lambda/rc.ma create mode 100644 matita/matita/lib/lambda/rc_sat.ma diff --git a/matita/matita/lib/lambda/ext.ma b/matita/matita/lib/lambda/ext.ma new file mode 100644 index 000000000..b933ed7b6 --- /dev/null +++ b/matita/matita/lib/lambda/ext.ma @@ -0,0 +1,129 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "lambda/types.ma". + +(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************) + +(* from sn.ma *****************************************************************) + +(* all(P,l) holds when P holds for all members of l *) +let rec all (P:T→Prop) l on l ≝ match l with + [ nil ⇒ True + | cons A D ⇒ P A ∧ all P D + ]. + +(* all(?,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 + [ nil ⇒ l2 = nil ? + | cons hd1 tl1 ⇒ match l2 with + [ nil ⇒ False + | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A P tl1 tl2 + ] + ]. + +(* Appl F l generalizes App applying F to a list of arguments + * The head of l is applied first + *) +let rec Appl F l on l ≝ match l with + [ nil ⇒ F + | cons A D ⇒ Appl (App F A) D + ]. + +(* FG: do we need this? +definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *) + +theorem lift_appl: ∀p,k,l,F. lift (Appl F l) p k = + Appl (lift F p k) (map … (lift0 p k) l). +#p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl // +qed. +*) + +(* from rc.ma *****************************************************************) + +theorem arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y. +#x #y #HS @nmk (elim HS) -HS /3/ +qed. + +theorem arith2: ∀i,p,k. k ≤ i → i + p - (k + p) = i - k. +#i #p #k #H @plus_to_minus +>commutative_plus >(commutative_plus k) >associative_plus @eq_f /2/ +qed. + +theorem arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z. +#x #y #z #H @nmk (elim H) -H /3/ +qed. + +theorem length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|. +#A #l2 #l1 (elim l1) -l1 (normalize) // +qed. + +theorem lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i. +#i #p #k #Hik normalize >(le_to_leb_true … Hik) // +qed. + +theorem lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p). +#i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/ +qed. + +theorem lift_app: ∀M,N,k,p. + lift (App M N) k p = App (lift M k p) (lift N k p). +// qed. + +theorem lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p = + Lambda (lift N k p) (lift M (k + 1) p). +// qed. + +theorem lift_prod: ∀N,M,k,p. + lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p). +// qed. + +(* telescopic non-delifting substitution of l in M. + * [this is the telescoping delifting substitution lifted by |l|] + * Rel 0 is replaced with the head of l + *) +let rec substc M l on l ≝ match l with + [ nil ⇒ M + | cons A D ⇒ (lift (substc M[0≝A] D) 0 1) + ]. + +notation "M [ l ]" non associative with precedence 90 for @{'Substc $M $l}. + +interpretation "Substc" 'Substc M l = (substc M l). + +(* this is just to test that substitution works as expected +theorem test1: ∀A,B,C. (App (App (Rel 0) (Rel 1)) (Rel 2))[A::B::C::nil ?] = + App (App (lift A 0 1) (lift B 0 2)) (lift C 0 3). +#A #B #C normalize +>lift_0 >lift_0 >lift_0 +>lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1 +normalize +qed. +*) + +theorem substc_refl: ∀l,t. (lift t 0 (|l|))[l] = (lift t 0 (|l|)). +#l (elim l) -l (normalize) // #A #D #IHl #t cut (S (|D|) = |D| + 1) // (**) (* eliminate cut *) +qed. + +theorem substc_sort: ∀n,l. (Sort n)[l] = Sort n. +// +qed. +(* 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) +. +*) diff --git a/matita/matita/lib/lambda/rc.ma b/matita/matita/lib/lambda/rc.ma deleted file mode 100644 index fe049658c..000000000 --- a/matita/matita/lib/lambda/rc.ma +++ /dev/null @@ -1,108 +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 *) -(* *) -(**************************************************************************) - -include "lambda/sn.ma". - -let rec substc M l on l ≝ match l with - [ nil ⇒ M - | cons A D ⇒ lift (substc M D)[0≝A] 0 1 - ]. - -notation "M [ l ]" non associative with precedence 90 for @{'Substc $M $l}. - -interpretation "Substc" 'Substc M l = (substc M l). - -theorem substc_sort: ∀n,l. (Sort n)[l] = Sort n. -#n #l (elim l) -l // #A #D #IH normalize >IH -IH. normalize // -qed. - -(* REDUCIBILITY CANDIDATES ****************************************************) - -(* 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) -. - -(* the reducibility candidates (r.c.) *) -record RC : Type[0] ≝ { - mem : T → Prop; - cr1 : ∀t. mem t → SN t; - sat0: ∀l,n. all mem l → mem (Appl (Sort n) l); - sat1: ∀l,i. all mem l → mem (Appl (Rel i) l); - sat2: ∀F,A,B,l. mem B → mem A → - mem (Appl F[0:=A] l) → mem (Appl (Lambda B F) (A::l)) -}. - -interpretation "membership (reducibility candidate)" 'mem A R = (mem R A). - -(* the r.c. of all s.n. terms *) -definition snRC: RC ≝ mk_RC SN …. -/2/ qed. - -(* the carrier of the r.c. of a (dependent) product type *) -definition dep_mem ≝ λRA,RB,M. ∀N. N ∈ RA → App M N ∈ RB. - -(* the r.c. of a (dependent) product type *) -axiom depRC: RC → RC → RC. -(* FG - * ≝ λRA,RB. mk_RC (dev_mem RA RB) ?. - *) - -(* a generalization of mem on lists *) -let rec memc H l on l : Prop ≝ match l with - [ nil ⇒ True - | cons A D ⇒ match H with - [ nil ⇒ A ∈ snRC ∧ memc H D - | cons R K ⇒ A ∈ R ∧ memc K D - ] - ]. - -interpretation "componentwise membership (context of reducibility candidates)" 'mem l H = (memc H l). - -(* the r.c. associated to a type *) -let rec trc H t on t : RC ≝ match t with - [ Sort _ ⇒ snRC - | Rel i ⇒ nth i … H snRC - | App _ _ ⇒ snRC (* FG ??? *) - | Lambda _ _ ⇒ snRC - | Prod A B ⇒ depRC (trc H A) (trc (trc H A :: H) B) - | D _ ⇒ snRC (* FG ??? *) - ]. - -notation "hvbox(〚T〛 _ term 90 E)" non associative with precedence 50 for @{'InterpE $T $E}. - -interpretation "interpretation of a type" 'InterpE t H = (trc H t). - -(* the r.c. context associated to a context *) -let rec trcc H G on G : list RC ≝ match G with - [ nil ⇒ H - | cons A D ⇒ 〚A〛_(trcc H D) :: trcc H D - ]. - -interpretation "interpretation of a context" 'InterpE G H = (trcc H G). - -theorem tj_trc: ∀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 @(sn_sort (nil ?)) // - | #G #B #n #tjB #IH #H #l (elim l) -l (normalize) - [ #_ - | #C #D #IHl #mem (elim mem) -mem #mem #memc -(* -theorem tj_sn: ∀G,A,B. G ⊢A:B → SN A. -#G #A #B #tjAB lapply (tj_trc … tjAB (nil ?) (nil ?)) -tjAB (normalize) /3/ -qed. -*) \ No newline at end of file diff --git a/matita/matita/lib/lambda/rc_sat.ma b/matita/matita/lib/lambda/rc_sat.ma new file mode 100644 index 000000000..768e5344e --- /dev/null +++ b/matita/matita/lib/lambda/rc_sat.ma @@ -0,0 +1,133 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "lambda/sn.ma". + +(* REDUCIBILITY CANDIDATES ****************************************************) + +(* 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. + * The benefit is that reduction is not needed to define such subsets. + * Also, this approach was never tried on a system with dependent types. + *) +record RC : Type[0] ≝ { + mem : T → Prop; + cr1 : CR1 mem; + sat0: SAT0 mem; + sat1: SAT1 mem; + sat2: SAT2 mem +}. +(* HIDDEN BUG: + * if SAT0 and SAT1 are expanded, + * the projections sat0 and sat1 are not generated + *) + +interpretation "membership (reducibility candidate)" 'mem A R = (mem R A). + +(* the r.c. of all s.n. terms *) +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 + | cons hd tl ⇒ match E with + [ nil ⇒ hd ∈ snRC ∧ memc E tl + | cons C D ⇒ hd ∈ C ∧ memc D tl + ] + ]. + +interpretation + "componentwise membership (context of reducibility candidates)" + 'mem l H = (memc H l). + +(* extensional equality of r.c.'s *********************************************) + +definition rceq: RC → RC → Prop ≝ + λC1,C2. ∀M. (M ∈ C1 → M ∈ C2) ∧ (M ∈ C2 → M ∈ C1). + +interpretation + "extensional equality (reducibility candidate)" + 'napart C1 C2 = (rceq C1 C2). + +definition rceql ≝ λl1,l2. all2 ? rceq l1 l2. + +interpretation + "extensional equality (context of reducibility candidates)" + 'napart C1 C2 = (rceql C1 C2). + +theorem reflexive_rceq: reflexive … rceq. +/2/ qed. + +theorem 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/ +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 + *) +theorem 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. +#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. +#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 → + 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. + +axiom dep_cr1: ∀B,C. CR1 (dep_mem B C). + +axiom dep_sat0: ∀B,C. SAT0 (dep_mem B C). + +axiom dep_sat1: ∀B,C. SAT1 (dep_mem B C). + +axiom dep_sat2: ∀B,C. SAT2 (dep_mem B C). + +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. +#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 339aa424a..26b1f9e77 100644 --- a/matita/matita/lib/lambda/sn.ma +++ b/matita/matita/lib/lambda/sn.ma @@ -12,21 +12,24 @@ (* *) (**************************************************************************) -include "lambda/types.ma". - -(* all(P,l) holds when P holds for all members of l *) -let rec all (P:T→Prop) l on l ≝ match l with - [ nil ⇒ True - | cons A D ⇒ P A ∧ all P D - ]. - -(* Appl F l generalizes App applying F to a list of arguments - * The head of l is applied first - *) -let rec Appl F l on l ≝ match l with - [ nil ⇒ F - | cons A D ⇒ Appl (App F A) D - ]. +include "lambda/ext.ma". + +(* saturation conditions on an explicit subset ********************************) + +definition SAT0 ≝ λP. ∀l,n. all P l → P (Appl (Sort n) l). + +definition SAT1 ≝ λP. ∀l,i. all P l → P (Appl (Rel i) l). + +definition SAT2 ≝ λ(P:?→Prop). ∀F,A,B,l. P B → P A → + P (Appl F[0:=A] l) → P (Appl (Lambda B F) (A::l)). + +theorem SAT0_sort: ∀P,n. SAT0 P → P (Sort n). +#P #n #H @(H (nil ?) …) // +qed. + +theorem SAT1_rel: ∀P,i. SAT1 P → P (Rel i). +#P #i #H @(H (nil ?) …) // +qed. (* STRONGLY NORMALIZING TERMS *************************************************) @@ -34,13 +37,16 @@ let rec Appl F l on l ≝ match l with (* FG: we axiomatize it for now because we dont have reduction yet *) axiom SN: T → Prop. -(* axiomatization of SN *******************************************************) +definition CR1 ≝ λ(P:?→Prop). ∀M. P M → SN M. -axiom sn_sort: ∀l,n. all SN l → SN (Appl (Sort n) l). +axiom sn_sort: SAT0 SN. -axiom sn_rel: ∀l,i. all SN l → SN (Appl (Rel i) l). +axiom sn_rel: SAT1 SN. axiom sn_lambda: ∀B,F. SN B → SN F → SN (Lambda B F). -axiom sn_beta: ∀F,A,B,l. SN B → SN A → - SN (Appl F[0:=A] l) → SN (Appl (Lambda B F) (A::l)). +axiom sn_beta: SAT2 SN. + +(* FG: do we need this? +axiom sn_lift: ∀t,k,p. SN t → SN (lift t p k). +*) -- 2.39.2