From 471987d6759c57e40fb89d435345cf654dc4aa39 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 23 Mar 2010 07:32:33 +0000 Subject: [PATCH] Keeping only lift_aux e subst_aux (renamed to lift and subst). From: asperti --- helm/software/matita/nlibrary/PTS/gpts.ma | 150 ++++++++++++++------- helm/software/matita/nlibrary/PTS/subst.ma | 100 +++++++------- 2 files changed, 154 insertions(+), 96 deletions(-) diff --git a/helm/software/matita/nlibrary/PTS/gpts.ma b/helm/software/matita/nlibrary/PTS/gpts.ma index d43efef3f..9a53cc00f 100644 --- a/helm/software/matita/nlibrary/PTS/gpts.ma +++ b/helm/software/matita/nlibrary/PTS/gpts.ma @@ -19,17 +19,18 @@ include "PTS/subst.ma". nlet rec substl (G:list T) (N:T) : list T ≝ match G with [ nil ⇒ nil T - | cons A D ⇒ ((subst_aux A (length T D) N)::(substl D N)) + | cons A D ⇒ ((subst A (length T D) N)::(substl D N)) ]. (* nlemma substl_cons: ∀A,N.∀G. substl (A::G) N = (subst_aux A (length T G) N)::(substl G N). //; nqed. +*) +(* nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1. -/2/; nqed. -*) +/2/; nqed.*) (****************************************************************) @@ -37,20 +38,15 @@ naxiom A: nat → nat → Prop. naxiom R: nat → nat → nat → Prop. naxiom conv: T → T → Prop. -nlemma mah: ∀A,i. lift A i = lift_aux A 0 i. -//; nqed. - -ncheck subst. - ninductive TJ: list T → T → T → Prop ≝ | ax : ∀i,j. A i j → TJ (nil T) (Sort i) (Sort j) - | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 1) + | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1) | weak: ∀G.∀A,B,C.∀i. - TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 1) (lift B 1) + TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 0 1) (lift B 0 1) | prod: ∀G.∀A,B.∀i,j,k. R i j k → TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k) | app: ∀G.∀F,A,B,a. - TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst a B) + TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B 0 a) | abs: ∀G.∀A,B,b.∀i. TJ (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B) | conv: ∀G.∀A,B,C.∀i. conv B C → @@ -105,7 +101,7 @@ A i j → Glegal G → G ⊢ Sort i: Sort j. (* bello *) nqed. ntheorem start_rel: ∀G.∀A.∀C.∀n,i,q. -G ⊢ C: Sort q → G ⊢ Rel n: lift A i → (C::G) ⊢ Rel (S n): lift A (S i). +G ⊢ C: Sort q → G ⊢ Rel n: lift A 0 i → (C::G) ⊢ Rel (S n): lift A 0 (S i). #G; #A; #C; #n; #i; #p; #tjC; #tjn; napplyS (weak G (Rel n));//. (* bello *) (* @@ -117,7 +113,7 @@ G ⊢ C: Sort q → G ⊢ Rel n: lift A i → (C::G) ⊢ Rel (S n): lift A (S i) nqed. ntheorem start_lemma2: ∀G. -Glegal G → ∀n. n < |G| → G ⊢ Rel n: lift (nth n T G (Rel O)) (S n). +Glegal G → ∀n. n < |G| → G ⊢ Rel n: lift (nth n T G (Rel O)) 0 (S n). #G; #Gleg; ncases Gleg; #A; #B; #tjAB; nelim tjAB; /2/; ##[#i; #j; #axij; #p; nnormalize; #abs; napply False_ind; napply (absurd … abs); //; @@ -178,12 +174,94 @@ ntheorem substitution_tj: ##] ##|#G; #A1; #i; #tjA; #Hind; #G1; #D; ncases D; ##[#N; #Heq; #tjN; - nrewrite > (delift (lift N O) A1 O O O ??); //; + nrewrite > (delift (lift N O O) A1 O O O ??); //; nnormalize in Heq; ndestruct;/2/; ##|#H; #L; #N1; #Heq; nnormalize in Heq; - #tjN1; nnormalize; ndestruct; + #tjN1; nnormalize; ndestruct; + ncheck( let clause_829: + ∀x1947: ?. + ∀x1948: ?. + ∀x1949: ?. + ∀x1950: ?. + ∀x1951: ?. + eq T (lift (subst x1947 (plus x1948 x1949) x1950) x1949 x1951) + (subst (lift x1947 x1949 x1951) (plus x1948 (plus x1949 x1951)) + x1950) + ≝ λx1947:?. + λx1948:?. + λx1949:?. + λx1950:?. + λx1951:?. + rewrite_l nat (plus (plus x1948 x1949) x1951) + (λx:nat. + eq T (lift (subst x1947 (plus x1948 x1949) x1950) x1949 x1951) + (subst (lift x1947 x1949 x1951) x x1950)) + (lift_subst_ijk x1950 x1947 x1951 x1948 x1949) + (plus x1948 (plus x1949 x1951)) + (associative_plus x1948 x1949 x1951) in + let clause_60: ∀x156: ?. eq nat (S x156) (plus x156 (S O)) + ≝ λx156:?. + rewrite_r nat (plus x156 O) (λx:nat. eq nat (S x) (plus x156 (S O))) + (plus_n_Sm x156 O) x156 (plus_n_O x156) in + let clause_996 : + eq Type + (TJ (cons T (subst ? ? ?) ?) (Rel O) + (subst (lift ? O (S O)) (plus ? (S O)) ?)) + (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1)) + (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)) + ≝ rewrite_l nat (S (length T L)) + (λx:nat. + eq Type + (TJ + (cons T (subst H (length T L) N1) (append T (substl L N1) G1)) + (Rel O) (subst (lift H O (S O)) x N1)) + (TJ + (cons T (subst H (length T L) N1) (append T (substl L N1) G1)) + (Rel O) (subst (lift H O (S O)) (S (length T L)) N1))) + (refl Type + (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1)) + (Rel O) (subst (lift H O (S O)) (S (length T L)) N1))) + (plus (length T L) (S O)) (clause_60 (length T L)) in + let clause_995: + eq Type + (TJ (cons T (subst ? ? ?) ?) (Rel O) + (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?)) + (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1)) + (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)) + ≝ rewrite_l nat (S O) + (λx:nat. + eq Type + (TJ (cons T (subst ? ? ?) ?) (Rel O) + (subst (lift ? O (S O)) (plus ? x) ?)) + (TJ + (cons T (subst H (length T L) N1) + (append T (substl L N1) G1)) (Rel O) + (subst (lift H O (S O)) (S (length T L)) N1))) clause_996 + (plus O (S O)) (plus_O_n (S O)) in + rewrite_r T + (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?) + (λx:T. + eq Type + (TJ (cons T (subst ? (plus ? O) ?) ?) (Rel O) x) + (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1)) + (Rel O) (subst (lift H O (S O)) (S (length T L)) N1))) + (rewrite_l nat ? + (λx:nat. + eq Type + (TJ (cons T (subst ? x ?) ?) (Rel O) + (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?)) + (TJ + (cons T (subst H (length T L) N1) (append T (substl L N1) G1)) + (Rel O) (subst (lift H O (S O)) (S (length T L)) N1))) + clause_995 (plus ? O) (plus_n_O ?)) + (lift (subst ? (plus ? O) ?) O (S O)) + (clause_829 ? ? O ? (S O)) +). + napplyS start; + (* napplyS start; *) (* napplyS start non va *) ncut (S (length T L) = ((length T L)+0+1)); ##[//##] #Heq; + ncheck start. napplyS start;/2/; ##] ##|#G; #P; #Q; #R; #i; #tjP; #tjR; #Hind1; #Hind2; @@ -199,49 +277,25 @@ ntheorem substitution_tj: #G1; #D; #N; #Heq; #tjN; nnormalize; napply (prod … Ax); ##[/2/; - ##|ncheck (Hind2 G1 (P::D) N ? tjN). - ncut (S (length T D) = (length T D)+1); ##[//##] #Heq1; - nrewrite < Heq1; + ##|ncut (S (length T D) = (length T D)+1); ##[//##] #Heq1; + nrewrite < Heq1; napply (Hind2 ? (P::D));//; ##] ##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2; #G1; #D; #N; #Heq; #tjN; nnormalize; + ncheck ( + (subst (subst_aux S (length T D) N) + (subst_aux R (length T D) N)) + ). + napplyS (app (substl D N@G1) (subst_aux P (length T D) N) A (subst_aux R (length T D) N) (subst_aux S (length T D) N) ?). nlapply (subst_lemma R S N (length ? D) 0); #sl; nrewrite < (plus_n_O ?) in sl; #sl; nrewrite > sl; + nauto demod; napply app; nnormalize in Hind1;/2/; ##| - - - -ntheorem substitution_tj: -∀E.∀A,B,M.TJ E M B → ∀G,D.∀N. E = D@A::G → TJ G N A → -∀k.length ? D = k → - TJ ((substl D N)@G) (subst_aux M k N) (subst_aux B k N). -#E; #A; #B; #M; #tjMB; nelim tjMB; - ##[nnormalize; (* /3/; *) - ##|#G; #A1; #i; #tjA; #Hind; - #G1; #D; ncases D; - ##[#N; #Heq; #tjN; #k; nnormalize in ⊢ (% → ?); #kO; - nrewrite < kO; - nrewrite > (delift (lift N O) A1 O O O ??); //; - nnormalize in Heq; ndestruct;/2/; - ##|#H; #L; #N1; #Heq; nnormalize in Heq; - #tjN1; #k; #len; nnormalize in len; - nrewrite < len; - nnormalize; ndestruct; - (* porcherie *) - ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq; - nrewrite > Heq; - nrewrite < (lift_subst_aux_k N1 H (length T L) O); - nrewrite < (plus_n_O (length T L)); - napply (start (substl L N1@G1) (subst_aux H (length T L) N1) i ?). - napply Hind;//; - ##] - - - + diff --git a/helm/software/matita/nlibrary/PTS/subst.ma b/helm/software/matita/nlibrary/PTS/subst.ma index 7ca2fdc03..a37074b4d 100644 --- a/helm/software/matita/nlibrary/PTS/subst.ma +++ b/helm/software/matita/nlibrary/PTS/subst.ma @@ -22,61 +22,64 @@ ninductive T : Type ≝ | Prod: T → T → T (* type, body *) . -nlet rec lift_aux t k p ≝ +nlet rec lift t k p ≝ match t with [ Sort n ⇒ Sort n | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) (Rel (n+p)) - | App m n ⇒ App (lift_aux m k p) (lift_aux n k p) - | Lambda m n ⇒ Lambda (lift_aux m k p) (lift_aux n (k+1) p) - | Prod m n ⇒ Prod (lift_aux m k p) (lift_aux n (k+1) p) + | App m n ⇒ App (lift m k p) (lift n k p) + | Lambda m n ⇒ Lambda (lift m k p) (lift n (k+1) p) + | Prod m n ⇒ Prod (lift m k p) (lift n (k+1) p) ]. -ndefinition lift ≝ λt.λp.lift_aux t 0 p. +(* +ndefinition lift ≝ λt.λp.lift_aux t 0 p.*) -notation "↑ \sup n ( M )" non associative with precedence 70 for @{'Lift $n $M}. -notation "↑ \sub k \sup n ( M )" non associative with precedence 70 for @{'Lift_aux $n $k $M}. +notation "↑ \sup n ( M )" non associative with precedence 70 for @{'Lift O $M}. +notation "↑ \sub k \sup n ( M )" non associative with precedence 70 for @{'Lift $n $k $M}. -interpretation "Lift" 'Lift n M = (lift M n). -interpretation "Lift_aux" 'Lift_aux n k M = (lift_aux M k n). +(* interpretation "Lift" 'Lift n M = (lift M n). *) +interpretation "Lift" 'Lift n k M = (lift M k n). -nlet rec subst_aux t k a ≝ +nlet rec subst t k a ≝ match t with [ Sort n ⇒ Sort n | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) - (if_then_else T (eqb n k) (lift a n) (Rel (n-1))) - | App m n ⇒ App (subst_aux m k a) (subst_aux n k a) - | Lambda m n ⇒ Lambda (subst_aux m k a) (subst_aux n (k+1) a) - | Prod m n ⇒ Prod (subst_aux m k a) (subst_aux n (k+1) a) + (if_then_else T (eqb n k) (lift a 0 n) (Rel (n-1))) + | App m n ⇒ App (subst m k a) (subst n k a) + | Lambda m n ⇒ Lambda (subst m k a) (subst n (k+1) a) + | Prod m n ⇒ Prod (subst m k a) (subst n (k+1) a) ]. +(* meglio non definire ndefinition subst ≝ λa.λt.subst_aux t 0 a. - notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}. -notation "M [ k ← N]" non associative with precedence 90 for @{'Subst_aux $M $k $N}. +*) + +notation "M [ k ← N]" non associative with precedence 90 for @{'Subst $M $k $N}. -interpretation "Subst" 'Subst N M = (subst N M). -interpretation "Subst_aux" 'Subst_aux M k N = (subst_aux M k N). +(* interpretation "Subst" 'Subst N M = (subst N M). *) +interpretation "Subst" 'Subst M k N = (subst M k N). (*** properties of lift and subst ***) -nlemma lift_aux_0: ∀t:T.∀k. lift_aux t k 0 = t. +nlemma lift_0: ∀t:T.∀k. lift t k 0 = t. #t; nelim t; nnormalize; //; #n; #k; ncases (leb (S n) k); nnormalize;//;nqed. -nlemma lift_0: ∀t:T. lift t 0 = t. -#t; nelim t; nnormalize; //; nqed. +(* nlemma lift_0: ∀t:T. lift t 0 = t. +#t; nelim t; nnormalize; //; nqed. *) -nlemma lift_sort: ∀i,k. lift (Sort i) k = Sort i. +nlemma lift_sort: ∀i,k,n. lift (Sort i) k n = Sort i. //; nqed. -nlemma lift_rel: ∀i,k. lift (Rel i) k = Rel (i+k). +nlemma lift_rel: ∀i,n. lift (Rel i) 0 n = Rel (i+n). //; nqed. -nlemma lift_rel1: ∀i.lift (Rel i) 1 = Rel (S i). -#i; nchange with (lift (Rel i) 1 = Rel (1 + i)); //; nqed. +nlemma lift_rel1: ∀i.lift (Rel i) 0 1 = Rel (S i). +#i; nchange with (lift (Rel i) 0 1 = Rel (1 + i)); //; nqed. -nlemma lift_lift_aux: ∀t.∀i,j.j ≤ i → ∀h,k. -lift_aux (lift_aux t k i) (j+k) h = lift_aux t k (i+h). +nlemma lift_lift: ∀t.∀i,j.j ≤ i → ∀h,k. + lift (lift t k i) (j+k) h = lift t k (i+h). #t; #i; #j; #h; nelim t; nnormalize; //; #n; #h;#k; napply (leb_elim (S n) k); #Hnk;nnormalize; ##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/; @@ -86,17 +89,19 @@ napply (leb_elim (S n) k); #Hnk;nnormalize; ##] nqed. -nlemma lift_lift_aux1: ∀t.∀i,j,k. lift_aux (lift_aux t k j) k i = lift_aux t k (j+i). +nlemma lift_lift1: ∀t.∀i,j,k. + lift(lift t k j) k i = lift t k (j+i). #t;/3/; nqed. -nlemma lift_lift_aux2: ∀t.∀i,j,k. lift_aux (lift_aux t k j) (j+k) i = lift_aux t k (j+i). +nlemma lift_lift2: ∀t.∀i,j,k. + lift (lift t k j) (j+k) i = lift t k (j+i). #t; /2/; nqed. +(* nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i). -nnormalize; //; nqed. +nnormalize; //; nqed. *) -nlemma subst_lift_aux_k: ∀A,B.∀k. - subst_aux (lift_aux B k 1) k A = B. +nlemma subst_lift_k: ∀A,B.∀k. subst (lift B k 1) k A = B. #A; #B; nelim B; nnormalize; /2/; #n; #k; napply (leb_elim (S n) k); nnormalize; #Hnk; ##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//; @@ -108,39 +113,38 @@ napply (leb_elim (S n) k); nnormalize; #Hnk; ##] nqed. +(* nlemma subst_lift: ∀A,B. subst A (lift B 1) = B. -nnormalize; //; nqed. - -nlemma subst_aux_sort: ∀A.∀n,k. subst_aux (Sort n) k A = Sort n. -//; nqed. +nnormalize; //; nqed. *) -nlemma subst_sort: ∀A.∀n. subst A (Sort n) = Sort n. +nlemma subst_sort: ∀A.∀n,k. subst (Sort n) k A = Sort n. //; nqed. -nlemma subst_rel: ∀A.subst A (Rel O) = A. +nlemma subst_rel: ∀A.subst (Rel 0) 0 A = A. nnormalize; //; nqed. nlemma subst_rel1: ∀A.∀k,i. i < k → - subst_aux (Rel i) k A = Rel i. + subst (Rel i) k A = Rel i. #A; #k; #i; nnormalize; #ltik; nrewrite > (le_to_leb_true (S i) k ?); //; nqed. -nlemma subst_rel2: ∀A.∀k. subst_aux (Rel k) k A = lift A k. +nlemma subst_rel2: ∀A.∀k. + subst (Rel k) k A = lift A 0 k. #A; #k; nnormalize; nrewrite > (lt_to_leb_false (S k) k ?); //; nrewrite > (eq_to_eqb_true … (refl …)); //; nqed. nlemma subst_rel3: ∀A.∀k,i. k < i → - subst_aux (Rel i) k A = Rel (i-1). + subst (Rel i) k A = Rel (i-1). #A; #k; #i; nnormalize; #ltik; nrewrite > (lt_to_leb_false (S i) k ?); /2/; nrewrite > (not_eq_to_eqb_false i k ?); //; napply nmk; #eqik; nelim (lt_to_not_eq … (ltik …)); /2/; nqed. -nlemma lift_subst_aux_ijk: ∀A,B.∀i,j,k. - lift_aux (subst_aux B (j+k) A) k i = subst_aux (lift_aux B k i) (j+k+i) A. +nlemma lift_subst_ijk: ∀A,B.∀i,j,k. + lift (subst B (j+k) A) k i = subst (lift B k i) (j+k+i) A. #A; #B; #i; #j; nelim B; nnormalize; /2/; #n; #k; napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk; ##[nelim (leb (S n) k); @@ -151,7 +155,7 @@ napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk; ##[nrewrite > (lt_to_leb_false (S n) k ?); ##[ncut (j+k+i = n+i);##[//;##] #Heq; nrewrite > Heq; nrewrite > (subst_rel2 A ?); - nnormalize; napplyS lift_lift_aux;//; + nnormalize; napplyS lift_lift;//; ##|/2/; ##] ##|ncut (j + k < n); @@ -171,7 +175,7 @@ napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk; nqed. ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k → - subst_aux (lift_aux B i (S k)) j A = (lift_aux B i k). + subst (lift B i (S k)) j A = (lift B i k). #A; #B; nelim B; nnormalize; /2/; ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk; napply eq_f2;/2/; napply Hind2; @@ -194,8 +198,8 @@ nqed. (********************* substitution lemma ***********************) nlemma subst_lemma: ∀A,B,C.∀k,i. - subst_aux (subst_aux A i B) (k+i) C = - subst_aux (subst_aux A (S (k+i)) C) i (subst_aux B k C). + subst (subst A i B) (k+i) C = + subst (subst A (S (k+i)) C) i (subst B k C). #A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *) #n; #i; napply (leb_elim (S n) i); #Hle; ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *) @@ -208,7 +212,7 @@ nlemma subst_lemma: ∀A,B,C.∀k,i. nrewrite > (le_to_leb_true i (k+i) ?); //; nrewrite > (subst_rel2 …); nnormalize; napply symmetric_eq; - napplyS (lift_subst_aux_ijk C B i k O); + napplyS (lift_subst_ijk C B i k O); ##|napply (leb_elim (S (n-1)) (k+i)); #nk; ##[nrewrite > (subst_rel1 C (k+i) (n-1) nk); nrewrite > (le_to_leb_true n (k+i) ?); -- 2.39.2