From 34a5ef53f3ad2771cb45f90a2da6713bccdf3608 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 17 Mar 2010 11:51:01 +0000 Subject: [PATCH] Splitted gpts in two files. --- helm/software/matita/nlibrary/PTS/gpts.ma | 402 ++------------------- helm/software/matita/nlibrary/PTS/subst.ma | 264 ++++++++++++++ 2 files changed, 295 insertions(+), 371 deletions(-) create mode 100644 helm/software/matita/nlibrary/PTS/subst.ma diff --git a/helm/software/matita/nlibrary/PTS/gpts.ma b/helm/software/matita/nlibrary/PTS/gpts.ma index bf149812d..c6aeb1bd4 100644 --- a/helm/software/matita/nlibrary/PTS/gpts.ma +++ b/helm/software/matita/nlibrary/PTS/gpts.ma @@ -12,348 +12,8 @@ (* *) (**************************************************************************) -include "basics/list2.ma". - -ninductive T : Type ≝ - | Sort: nat → T - | Rel: nat → T - | App: T → T → T - | Lambda: T → T → T (* type, body *) - | Prod: T → T → T (* type, body *) -. - -nlet rec lift_aux 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) - ]. - -ndefinition lift ≝ λt.λp.lift_aux t 0 p. - -nlet rec subst_aux 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) - ]. - -ndefinition subst ≝ λa.λt.subst_aux t 0 a. - -(*** properties of lift and subst ***) -nlemma lift_aux_0: ∀t:T.∀k. lift_aux 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_sort: ∀i,k. lift (Sort i) k = Sort i. -//; nqed. - -nlemma lift_rel: ∀i,k. lift (Rel i) k = Rel (i+k). -//; 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_lift_aux: ∀t.∀i,j,k,k1. k ≤ k1 → k1 ≤ k+j → -lift_aux (lift_aux t k j) k1 i = lift_aux t k (j+i). -#t; nelim t; nnormalize; //; #n; #i;#j; #k; #k1; #lel; #ler; -napply (leb_elim (S n) k); #Hnk;nnormalize; - ##[nrewrite > (le_to_leb_true ? ? Hnk);nnormalize;//; - ##|nrewrite > (lt_to_leb_false (S n+j) k ?); - nnormalize;//;napply (lt_to_le_to_lt ? (S n)); - ##[napply not_le_to_lt;/2/; - ##|(* lento /2/; *) napply le_S_S;/1/; - ##] -nqed. *) - -nlemma lift_lift_aux: ∀t.∀i,j,k. lift_aux (lift_aux t k j) k i = lift_aux t k (j+i). -#t; nelim t; nnormalize; //; #n; #i;#j; #k; -napply (leb_elim (S n) k); #Hnk;nnormalize; - ##[nrewrite > (le_to_leb_true ? ? Hnk);nnormalize;//; - ##|nrewrite > (lt_to_leb_false (S n+j) k ?); - nnormalize;//; napply (lt_to_le_to_lt ? (S n)); - ##[napply not_le_to_lt;//; - ##|napply le_S_S;//; - ##] -nqed. - -nlemma lift_lift_aux1: ∀t.∀i,j,k. lift_aux (lift_aux t k j) (j+k) i = lift_aux t k (j+i). -#t; nelim t; nnormalize; //; #n; #i;#j; #k; -napply (leb_elim (S n) k); #Hnk;nnormalize; - ##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/; - ##|nrewrite > (lt_to_leb_false (S n+j) (j+k) ?); - nnormalize;//; napply le_S_S; napplyS monotonic_le_plus_r; - /3/; - ##] -nqed. - -nlemma lift_lift_aux2: ∀t.∀i,j.j ≤ i → ∀h,k. -lift_aux (lift_aux t k i) (j+k) h = lift_aux 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/; - ##|nrewrite > (lt_to_leb_false (S n+i) (j+k) ?); - nnormalize;//;napply le_S_S; nrewrite > (symmetric_plus j k); - napply le_plus;//;napply not_lt_to_le;/2/; - ##] -nqed. - -nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i). -nnormalize; //; -nqed. - -nlemma subst_lift_aux_k: ∀A,B.∀k. - subst_aux (lift_aux 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;//; - ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize; - ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?); - nnormalize;/2/; napply (not_to_not … Hnk);//; - ##|napply le_S; napplyS (not_le_to_lt (S n) k 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. - -nlemma subst_sort: ∀A.∀n. subst A (Sort n) = Sort n. -//; nqed. - -nlemma subst_rel: ∀A.subst A (Rel O) = A. -nnormalize; //; nqed. - -nlemma subst_rel1: ∀A.∀k,i. i < k → - subst_aux (Rel i) k A = Rel i. -#A; #k; #i; nnormalize; #ltik; -nrewrite > (le_to_leb_true (S i) k ?); //; nqed. +include "PTS/subst.ma". -nlemma subst_rel2: ∀A.∀k. subst_aux (Rel k) k A = lift A 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). -#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. - -(* versione con plus -nlemma lift_subst_aux_k: ∀A,B.∀j,k. - lift_aux (subst_aux B (j+k) A) k 1 = subst_aux (lift_aux B k 1) (j+k+1) A. -#A; #B; #j; nelim B; nnormalize; /2/; #n; #k; -napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk; - ##[nelim (leb (S n) k); - ##[nrewrite > (subst_rel1 A (j+k+1) n ?);/2/; - ##|nrewrite > (subst_rel1 A (j+k+1) (n+1) ?);/2/; - ##] - ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk; - ##[nrewrite > (lt_to_leb_false (S n) k ?); - ##[ncut (j+k+1 = n+1);##[//;##] #Heq; - nrewrite > Heq; nrewrite > (subst_rel2 A ?); nnormalize; - napplyS lift_lift_aux2 (* bello *);//; - ##|/2/; - ##] - ##|ncut (j + k < n); - ##[napply not_eq_to_le_to_lt; - ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##] - ##|#ltjkn; - ncut (O < n); ##[/2/; ##] #posn; - ncut (k ≤ n); ##[/2/; ##] #lekn; - nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize; - ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn)); - nrewrite > (subst_rel3 A (j+k+1) (n+1) ?); - ##[nrewrite < (plus_minus_m_m … posn);//; - ##|napplyS monotonic_lt_plus_l; //; - ##] - ##|napply le_S_S; - napply (not_eq_to_le_to_le_minus … lekn); - /2/; (* come fa? *) - ##] - ##] - ##] -nqed. *) - -naxiom lift_subst_aux_kij: ∀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_aux_k: ∀A,B.∀j,k. - lift_aux (subst_aux B (j+k) A) k 1 = subst_aux (lift_aux B k 1) (S(j+k)) A. -#A; #B; #j; nelim B; nnormalize; /2/; #n; #k; -napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk; - ##[nelim (leb (S n) k); - ##[nrewrite > (subst_rel1 A (S(j+k)) n ?);/2/; - ##|nrewrite > (subst_rel1 A (S(j+k)) (n+1) ?);/2/; - ##] - ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk; - ##[nrewrite > (lt_to_leb_false (S n) k ?); - ##[ncut (S(j+k) = n+1);##[//;##] #Heq; - nrewrite > Heq; nrewrite > (subst_rel2 A ?); nnormalize; - napplyS lift_lift_aux2 (* bello *);//; - ##|/2/; - ##] - ##|ncut (j + k < n); - ##[napply not_eq_to_le_to_lt; - ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##] - ##|#ltjkn; - ncut (O < n); ##[/2/; ##] #posn; - ncut (k ≤ n); ##[/2/; ##] #lekn; - nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize; - ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn)); - nrewrite > (subst_rel3 A (S(j+k)) (n+1) ?); - ##[nrewrite < (plus_minus_m_m … posn);//; - ##|ncut (S n = n +1); /2/; - ##] - ##|napply le_S_S; (* /3/;*) - napply (not_eq_to_le_to_le_minus … lekn); - /3/; (* come fa? *) - ##] - ##] - ##] -nqed. - -(* -nlemma lift_subst_aux_k: ∀A,B.∀k. - lift_aux (subst_aux B k A) k 1 = subst_aux (lift_aux B k 1) (k+1) A. -#A; #B; nelim B; nnormalize; /2/; #n; #k; -napply (leb_elim (S n) k); nnormalize; #Hnk; - ##[nrewrite > (le_to_leb_true ?? Hnk); - nrewrite > (le_to_leb_true (S n) (k +1) ?);nnormalize;/2/; - ##|nrewrite > (lt_to_leb_false (S (n + 1)) (k+1) ?); - ##[##2: napply le_S_S; napply (monotonic_le_plus_l 1 k n); - napply not_lt_to_le; napply Hnk; ##] - napply (eqb_elim n k);#eqnk; - ##[nrewrite > (eq_to_eqb_true (n+1) (k+1) ?);/2/; - nnormalize; nrewrite < eqnk; //; (* strano *) - ##|nrewrite > (not_eq_to_eqb_false (n+1) (k+1) ?);/2/; - nnormalize; - ncut (O < n); - ##[napply not_le_to_lt;#len; - napply eqnk; napply le_to_le_to_eq; - ##[napply transitive_le; //; - ##|napply not_lt_to_le; /2/; - ##] - ##|#posn; - nrewrite > (lt_to_leb_false (S (n - 1)) k ?); - ##[nnormalize; - (* nrewrite < (minus_plus_m_m n 1); *) - nrewrite < (plus_minus_m_m n 1 ?);//; - ##|napply le_S_S; napply not_eq_to_le_to_le_minus; - ##[/2/; - ##|napply (not_lt_to_le … Hnk); - ##] - ##] - ##] - ##] - ##] -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). -#A; #B; nelim B; nnormalize; /2/; - ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk; - napply eq_f2;/2/; napply Hind2; - napplyS (monotonic_le_plus_l 1);// - ##|#n; #i; #j; #k; #leij; #ltjk; - napply (leb_elim (S n) i); nnormalize; #len; - ##[nrewrite > (le_to_leb_true (S n) j ?);/2/; - ##|nrewrite > (lt_to_leb_false (S (n+S k)) j ?); - ##[nnormalize; - nrewrite > (not_eq_to_eqb_false (n+S k) j ?); - nnormalize; /2/; napply (not_to_not …len); - #H; napply (le_plus_to_le_r k); (* why napplyS ltjk; *) - nnormalize; //; - ##|napply le_S_S; napply (transitive_le … ltjk); - napply le_plus;//; napply not_lt_to_le; /2/; - ##] - ##] -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). -#A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *) -#n; #i; napply (leb_elim (S n) i); #Hle; - ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *) - ncut (n ≤ k+i); ##[/2/##] #len; - nrewrite > (subst_rel1 C (k+i) n ltn); - nrewrite > (le_to_leb_true n (k+i) len); - nrewrite > (subst_rel1 … Hle);//; - ##|napply (eqb_elim n i); #eqni; - ##[nrewrite > eqni; - nrewrite > (le_to_leb_true i (k+i) ?); //; - nrewrite > (subst_rel2 …); nnormalize; - napply symmetric_eq; - napplyS (lift_subst_aux_kij 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) ?); - ##[nrewrite > (subst_rel3 ? i n ?);//; - napply not_eq_to_le_to_lt; - ##[/2/; - ##|napply not_lt_to_le;/2/; - ##] - ##|napply (transitive_le … nk);//; - ##] - ##|ncut (i < n); - ##[napply not_eq_to_le_to_lt; ##[/2/] - napply (not_lt_to_le … Hle);##] - #ltin; ncut (O < n); ##[/2/;##] #posn; - napply (eqb_elim (n-1) (k+i)); #H - ##[nrewrite > H; nrewrite > (subst_rel2 C (k+i)); - nrewrite > (lt_to_leb_false n (k+i) ?); - ##[nrewrite > (eq_to_eqb_true n (S(k+i)) ?); - ##[nnormalize; - ##|nrewrite < H; napplyS plus_minus_m_m;//; - ##] - ##|nrewrite < H; napply (lt_O_n_elim … posn); - #m; nnormalize;//; - ##] - ##|ncut (k+i < n-1); - ##[napply not_eq_to_le_to_lt; - ##[napply symmetric_not_eq; napply H; - ##|napply (not_lt_to_le … nk); - ##] - ##] - #Hlt; nrewrite > (lt_to_leb_false n (k+i) ?); - ##[nrewrite > (not_eq_to_eqb_false n (S(k+i)) ?); - ##[nrewrite > (subst_rel3 C (k+i) (n-1) Hlt); - nrewrite > (subst_rel3 ? i (n-1) ?);//; - napply (le_to_lt_to_lt … Hlt);//; - ##|napply (not_to_not … H); #Hn; nrewrite > Hn; nnormalize;//; - ##] - ##|napply (transitive_lt … Hlt); - napply (lt_O_n_elim … posn); - #m; nnormalize;//; - ##] - ##] - nrewrite (delift ???????);nnormalize;/2/; - ##] -nqed. - (*************************** substl *****************************) nlet rec substl (G:list T) (N:T) : list T ≝ @@ -362,15 +22,17 @@ nlet rec substl (G:list T) (N:T) : list T ≝ | cons A D ⇒ ((subst_aux A (length T D) N)::(substl D N)) ]. - -(*****************************************************************) +(****************************************************************) 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. + ninductive TJ: list T → T → T → Prop ≝ - | ax : ∀i,j. A i j → TJ [] (Sort i) (Sort j) + | 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) | weak: ∀G.∀A,B,C.∀i. TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 1) (lift B 1) @@ -382,23 +44,26 @@ ninductive TJ: list T → T → T → Prop ≝ 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 → TJ G A B → TJ G B (Sort i) → TJ G A C. - -ninverter TJ_inv2 for TJ (%?%) : Prop. + +notation "hvbox(G break ⊢ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}. +interpretation "type judgement" 'TJ G A B = (TJ G A B). + +(* ninverter TJ_inv2 for TJ (%?%) : Prop. *) (**** definitions ****) ninductive Glegal (G: list T) : Prop ≝ -glegalk : ∀A,B.TJ G A B → Glegal G. +glegalk : ∀A,B. G ⊢ A : B → Glegal G. ninductive Gterm (G: list T) (A:T) : Prop ≝ - | is_term: ∀B.TJ G A B → Gterm G A - | is_type: ∀B.TJ G B A → Gterm G A. + | is_term: ∀B.G ⊢ A:B → Gterm G A + | is_type: ∀B.G ⊢ B:A → Gterm G A. ninductive Gtype (G: list T) (A:T) : Prop ≝ -gtypek: ∀i.TJ G A (Sort i) → Gtype G A. +gtypek: ∀i.G ⊢ A : Sort i → Gtype G A. ninductive Gelement (G:list T) (A:T) : Prop ≝ -gelementk: ∀B.TJ G A B → Gtype G B → Gelement G A. +gelementk: ∀B.G ⊢ A:B → Gtype G B → Gelement G A. ninductive Tlegal (A:T) : Prop ≝ tlegalk: ∀G. Gterm G A → Tlegal A. @@ -423,13 +88,13 @@ subst C A *) ntheorem start_lemma1: ∀G.∀i,j. -A i j → Glegal G → TJ G (Sort i) (Sort j). +A i j → Glegal G → G ⊢ Sort i: Sort j. #G; #i; #j; #axij; #Gleg; ncases Gleg; #A; #B; #tjAB; nelim tjAB; /2/; (* bello *) nqed. ntheorem start_rel: ∀G.∀A.∀C.∀n,i,q. -TJ G C (Sort q) → TJ G (Rel n) (lift A i) → TJ (C::G) (Rel (S n)) (lift A (S i)). +G ⊢ C: Sort q → G ⊢ Rel n: lift A i → (C::G) ⊢ Rel (S n): lift A (S i). #G; #A; #C; #n; #i; #p; #tjC; #tjn; napplyS (weak G (Rel n));//. (* bello *) (* @@ -441,7 +106,7 @@ TJ G C (Sort q) → TJ G (Rel n) (lift A i) → TJ (C::G) (Rel (S n)) (lift A (S nqed. ntheorem start_lemma2: ∀G. -Glegal G → ∀n. n < length T G → TJ 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)) (S n). #G; #Gleg; ncases Gleg; #A; #B; #tjAB; nelim tjAB; /2/; ##[#i; #j; #axij; #p; nnormalize; #abs; napply False_ind; napply (absurd … abs); //; @@ -493,8 +158,8 @@ ntheorem substitution_tj: *) ntheorem substitution_tj: -∀E.∀A,B,M.TJ E M B → ∀G,D.∀N. E = D@A::G → TJ G N A → - TJ ((substl D N)@G) (subst_aux M (length ? D) N) (subst_aux B (length ? D) N). +∀E.∀A,B,M. E ⊢M:B → ∀G,D.∀N. E = D@A::G → G ⊢ N:A → + ((substl D N)@G) ⊢ M[|D| ← N]: B[|D| ← N]. #E; #A; #B; #M; #tjMB; nelim tjMB; ##[nnormalize; #i; #j; #k; #G; #D; #N; ncases D; ##[nnormalize; #isnil; ndestruct; @@ -506,31 +171,26 @@ ntheorem substitution_tj: nnormalize in Heq; ndestruct;/2/; ##|#H; #L; #N1; #Heq; nnormalize in Heq; #tjN1; 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;/2/; + (* napplyS start non va *) + ncut (S (length T L) = ((length T L)+0+1)); ##[//##] #Heq; + napplyS start;/2/; ##] ##|#G; #P; #Q; #R; #i; #tjP; #tjR; #Hind1; #Hind2; #G1; #D; #N; ncases D; nnormalize; ##[#Heq; ndestruct; #tjN; //; ##|#H; #L; #Heq; #tjN1; ndestruct; - (* porcherie *) - ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq; - nrewrite > Heq; - nrewrite < (lift_subst_aux_k N P (length T L) O); - nrewrite < (lift_subst_aux_k N Q (length T L) O); - nrewrite < (plus_n_O (length T L)); - napply weak;/2/; + (* napplyS weak non va *) + ncut (S (length T L) = (length T L)+0+1); ##[//##] #Heq; + napplyS weak; /2/; ##] ##|#G; #P; #Q; #i; #j; #k; #Ax; #tjP; #tjQ; #Hind1; #Hind2; - #G1; #D; #N; #Heq; #tjN; + #G1; #D; #N; #Heq; #tjN; nnormalize; napply (prod … Ax); ##[/2/; - ##| + ##|(* metas not found *) + napplyS (Hind2 G1 (P::D) N ); + nnormalize; ##] ##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2; #G1; #D; #N; #Heq; #tjN; nnormalize; diff --git a/helm/software/matita/nlibrary/PTS/subst.ma b/helm/software/matita/nlibrary/PTS/subst.ma new file mode 100644 index 000000000..7ca2fdc03 --- /dev/null +++ b/helm/software/matita/nlibrary/PTS/subst.ma @@ -0,0 +1,264 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +include "basics/list2.ma". + +ninductive T : Type ≝ + | Sort: nat → T + | Rel: nat → T + | App: T → T → T + | Lambda: T → T → T (* type, body *) + | Prod: T → T → T (* type, body *) +. + +nlet rec lift_aux 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) + ]. + +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}. + +interpretation "Lift" 'Lift n M = (lift M n). +interpretation "Lift_aux" 'Lift_aux n k M = (lift_aux M k n). + +nlet rec subst_aux 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) + ]. + +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}. + +interpretation "Subst" 'Subst N M = (subst N M). +interpretation "Subst_aux" 'Subst_aux M k N = (subst_aux M k N). + +(*** properties of lift and subst ***) + +nlemma lift_aux_0: ∀t:T.∀k. lift_aux 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_sort: ∀i,k. lift (Sort i) k = Sort i. +//; nqed. + +nlemma lift_rel: ∀i,k. lift (Rel i) k = Rel (i+k). +//; 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_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). +#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/; + ##|nrewrite > (lt_to_leb_false (S n+i) (j+k) ?); + nnormalize;//;napply le_S_S; nrewrite > (symmetric_plus j k); + napply le_plus;//;napply not_lt_to_le;/2/; + ##] +nqed. + +nlemma lift_lift_aux1: ∀t.∀i,j,k. lift_aux (lift_aux t k j) k i = lift_aux 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). +#t; /2/; nqed. + +nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i). +nnormalize; //; nqed. + +nlemma subst_lift_aux_k: ∀A,B.∀k. + subst_aux (lift_aux 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;//; + ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize; + ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?); + nnormalize;/2/; napply (not_to_not … Hnk);//; + ##|napply le_S; napplyS (not_le_to_lt (S n) k 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. + +nlemma subst_sort: ∀A.∀n. subst A (Sort n) = Sort n. +//; nqed. + +nlemma subst_rel: ∀A.subst A (Rel O) = A. +nnormalize; //; nqed. + +nlemma subst_rel1: ∀A.∀k,i. i < k → + subst_aux (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. +#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). +#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. +#A; #B; #i; #j; nelim B; nnormalize; /2/; #n; #k; +napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk; + ##[nelim (leb (S n) k); + ##[nrewrite > (subst_rel1 A (j+k+i) n ?);/2/; + ##|nrewrite > (subst_rel1 A (j+k+i) (n+i) ?);/2/; + ##] + ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk; + ##[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;//; + ##|/2/; + ##] + ##|ncut (j + k < n); + ##[napply not_eq_to_le_to_lt; + ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##] + ##|#ltjkn; + ncut (O < n); ##[/2/; ##] #posn; + ncut (k ≤ n); ##[/2/; ##] #lekn; + nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize; + ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn)); + nrewrite > (subst_rel3 A (j+k+i) (n+i) ?); + ##[/3/; ##|/2/; ##] + ##|napply le_S_S;/3/; (* /3/;*) + ##] + ##] + ##] +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). +#A; #B; nelim B; nnormalize; /2/; + ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk; + napply eq_f2;/2/; napply Hind2; + napplyS (monotonic_le_plus_l 1);// + ##|#n; #i; #j; #k; #leij; #ltjk; + napply (leb_elim (S n) i); nnormalize; #len; + ##[nrewrite > (le_to_leb_true (S n) j ?);/2/; + ##|nrewrite > (lt_to_leb_false (S (n+S k)) j ?); + ##[nnormalize; + nrewrite > (not_eq_to_eqb_false (n+S k) j ?); + nnormalize; /2/; napply (not_to_not …len); + #H; napply (le_plus_to_le_r k); (* why napplyS ltjk; *) + nnormalize; //; + ##|napply le_S_S; napply (transitive_le … ltjk); + napply le_plus;//; napply not_lt_to_le; /2/; + ##] + ##] +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). +#A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *) +#n; #i; napply (leb_elim (S n) i); #Hle; + ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *) + ncut (n ≤ k+i); ##[/2/##] #len; + nrewrite > (subst_rel1 C (k+i) n ltn); + nrewrite > (le_to_leb_true n (k+i) len); + nrewrite > (subst_rel1 … Hle);//; + ##|napply (eqb_elim n i); #eqni; + ##[nrewrite > eqni; + 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); + ##|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) ?); + ##[nrewrite > (subst_rel3 ? i n ?);//; + napply not_eq_to_le_to_lt; + ##[/2/; + ##|napply not_lt_to_le;/2/; + ##] + ##|napply (transitive_le … nk);//; + ##] + ##|ncut (i < n); + ##[napply not_eq_to_le_to_lt; ##[/2/] + napply (not_lt_to_le … Hle);##] + #ltin; ncut (O < n); ##[/2/;##] #posn; + napply (eqb_elim (n-1) (k+i)); #H + ##[nrewrite > H; nrewrite > (subst_rel2 C (k+i)); + nrewrite > (lt_to_leb_false n (k+i) ?); + ##[nrewrite > (eq_to_eqb_true n (S(k+i)) ?); + ##[nnormalize; + ##|nrewrite < H; napplyS plus_minus_m_m;//; + ##] + ##|nrewrite < H; napply (lt_O_n_elim … posn); + #m; nnormalize;//; + ##] + ##|ncut (k+i < n-1); + ##[napply not_eq_to_le_to_lt; + ##[napply symmetric_not_eq; napply H; + ##|napply (not_lt_to_le … nk); + ##] + ##] + #Hlt; nrewrite > (lt_to_leb_false n (k+i) ?); + ##[nrewrite > (not_eq_to_eqb_false n (S(k+i)) ?); + ##[nrewrite > (subst_rel3 C (k+i) (n-1) Hlt); + nrewrite > (subst_rel3 ? i (n-1) ?);//; + napply (le_to_lt_to_lt … Hlt);//; + ##|napply (not_to_not … H); #Hn; nrewrite > Hn; nnormalize;//; + ##] + ##|napply (transitive_lt … Hlt); + napply (lt_O_n_elim … posn); + #m; nnormalize;//; + ##] + ##] + nrewrite (delift ???????);nnormalize;/2/; + ##] +nqed. + + + + -- 2.39.2