(**************************************************************************) (* ___ *) (* ||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 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 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.*) 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" 'Lift n k M = (lift M k n). 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 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 \$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_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_sort: ∀i,k,n. lift (Sort i) k n = Sort i. //; nqed. nlemma lift_rel: ∀i,n. lift (Rel i) 0 n = Rel (i+n). //; 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: ∀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/; ##|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_lift1: ∀t.∀i,j,k. lift(lift t k j) k i = lift t k (j+i). #t;/3/; nqed. 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. *) 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;//; ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize; ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?); nnormalize;/2/ ##|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_sort: ∀A.∀n,k. subst (Sort n) k A = Sort n. //; nqed. nlemma subst_rel: ∀A.subst (Rel 0) 0 A = A. nnormalize; //; nqed. nlemma subst_rel1: ∀A.∀k,i. i < k → 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 (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 (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_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); ##[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;//; ##|/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 (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; 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 (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 *) 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 sym_eq; 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) ?); ##[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.