(* *)
(**************************************************************************)
-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 <H;
- ncut (∃m:nat. S m = n);
- ##[napply (lt_O_n_elim … posn); #m;@ m;//;
- ##|*; #m; #Hm; nrewrite < Hm;
- nrewrite > (delift ???????);nnormalize;/2/;
- ##]
-nqed.
-
(*************************** substl *****************************)
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)
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.
*)
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 *)
(*
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); //;
*)
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;
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;
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 <H;
+ ncut (∃m:nat. S m = n);
+ ##[napply (lt_O_n_elim … posn); #m;@ m;//;
+ ##|*; #m; #Hm; nrewrite < Hm;
+ nrewrite > (delift ???????);nnormalize;/2/;
+ ##]
+nqed.
+
+
+
+
projects / helm.git / commitdiff