+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
-
-include "basics/finset.ma".
-include "basics/star.ma".
-
-
-inductive FType (O:Type[0]): Type[0] ≝
- | atom : O → FType O
- | arrow : FType O → FType O → FType O.
-
-inductive T (O:Type[0]) (D:O → FinSet): Type[0] ≝
- | Val: ∀o:O.carr (D o) → T O D (* a value in a finset *)
- | Rel: nat → T O D (* DB index, base is 0 *)
- | App: T O D → T O D → T O D (* function, argument *)
- | Lambda: FType O → T O D → T O D (* type, body *)
- | Vec: FType O → list (T O D) → T O D (* type, body *)
-.
-
-let rec FinSet_of_FType O (D:O→FinSet) (ty:FType O) on ty : FinSet ≝
- match ty with
- [atom o ⇒ D o
- |arrow ty1 ty2 ⇒ FinFun (FinSet_of_FType O D ty1) (FinSet_of_FType O D ty2)
- ].
-
-(* size *)
-
-let rec size O D (M:T O D) on M ≝
-match M with
- [Val o a ⇒ 1
- |Rel n ⇒ 1
- |App P Q ⇒ size O D P + size O D Q + 1
- |Lambda Ty P ⇒ size O D P + 1
- |Vec Ty v ⇒ foldr ?? (λx,a. size O D x + a) 0 v +1
- ]
-.
-
-(* axiom pos_size: ∀M. 1 ≤ size M. *)
-
-theorem Telim_size: ∀O,D.∀P: T O D → Prop.
- (∀M. (∀N. size O D N < size O D M → P N) → P M) → ∀M. P M.
-#O #D #P #H #M (cut (∀p,N. size O D N = p → P N))
- [2: /2/]
-#p @(nat_elim1 p) #m #H1 #N #sizeN @H #N0 #Hlt @(H1 (size O D N0)) //
-qed.
-
-lemma T_elim:
- ∀O: Type[0].∀D:O→FinSet.∀P:T O D→Prop.
- (∀o:O.∀x:D o.P (Val O D o x)) →
- (∀n:ℕ.P(Rel O D n)) →
- (∀m,n:T O D.P m→P n→P (App O D m n)) →
- (∀Ty:FType O.∀m:T O D.P m→P(Lambda O D Ty m)) →
- (∀Ty:FType O.∀v:list (T O D).
- (∀x:T O D. mem ? x v → P x) → P(Vec O D Ty v)) →
- ∀x:T O D.P x.
-#O #D #P #Hval #Hrel #Happ #Hlam #Hvec @Telim_size #x cases x //
- [ (* app *) #m #n #Hind @Happ @Hind // /2 by le_minus_to_plus/
- | (* lam *) #ty #m #Hind @Hlam @Hind normalize //
- | (* vec *) #ty #v #Hind @Hvec #x lapply Hind elim v
- [#Hind normalize *
- |#hd #tl #Hind1 #Hind2 *
- [#Hx >Hx @Hind2 normalize //
- |@Hind1 #N #H @Hind2 @(lt_to_le_to_lt … H) normalize //
- ]
- ]
- ]
-qed.
-
-(* since we only consider beta reduction with closed arguments we could avoid
-lifting. We define it for the sake of generality *)
-
-(* arguments: k is the nesting depth (starts from 0), p is the lift
-let rec lift O D t k p on t ≝
- match t with
- [ Val o a ⇒ Val O D o a
- | Rel n ⇒ if (leb k n) then Rel O D (n+p) else Rel O D n
- | App m n ⇒ App O D (lift O D m k p) (lift O D n k p)
- | Lambda Ty n ⇒ Lambda O D Ty (lift O D n (S k) p)
- | Vec Ty v ⇒ Vec O D Ty (map ?? (λx. lift O D x k p) v)
- ].
-
-notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift 0 $n $M}.
-notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}.
-
-interpretation "Lift" 'Lift n k M = (lift ?? M k n).
-
-let rec subst O D t k s on t ≝
- match t with
- [ Val o a ⇒ Val O D o a
- | Rel n ⇒ if (leb k n) then
- (if (eqb k n) then lift O D s 0 n else Rel O D (n-1))
- else(Rel O D n)
- | App m n ⇒ App O D (subst O D m k s) (subst O D n k s)
- | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s)
- | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v)
- ].
-*)
-
-(* simplified version of subst, assuming the argument s is closed *)
-
-let rec subst O D t k s on t ≝
- match t with
- [ Val o a ⇒ Val O D o a
- | Rel n ⇒ if (leb k n) then
- (if (eqb k n) then (* lift O D s 0 n*) s else Rel O D (n-1))
- else(Rel O D n)
- | App m n ⇒ App O D (subst O D m k s) (subst O D n k s)
- | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s)
- | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v)
- ].
-(* notation "hvbox(M break [ k ≝ N ])"
- non associative with precedence 90
- for @{'Subst1 $M $k $N}. *)
-
-interpretation "Subst" 'Subst1 M k N = (subst M k N).
-
-(*
-lemma subst_rel1: ∀O,D,A.∀k,i. i < k →
- (Rel O D i) [k ≝ A] = Rel O D i.
-#A #k #i normalize #ltik >(lt_to_leb_false … ltik) //
-qed.
-
-lemma subst_rel2: ∀O,D, A.∀k.
- (Rel k) [k ≝ A] = lift A 0 k.
-#A #k normalize >(le_to_leb_true k k) // >(eq_to_eqb_true … (refl …)) //
-qed.
-
-lemma subst_rel3: ∀A.∀k,i. k < i →
- (Rel i) [k ≝ A] = Rel (i-1).
-#A #k #i normalize #ltik >(le_to_leb_true k i) /2/
->(not_eq_to_eqb_false k i) // @lt_to_not_eq //
-qed. *)
-
-
-(* closed terms ????
-let rec closed_k O D (t: T O D) k on t ≝
- match t with
- [ Val o a ⇒ True
- | Rel n ⇒ n < k
- | App m n ⇒ (closed_k O D m k) ∧ (closed_k O D n k)
- | Lambda T n ⇒ closed_k O D n (k+1)
- | Vec T v ⇒ closed_list O D v k
- ]
-
-and closed_list O D (l: list (T O D)) k on l ≝
- match l with
- [ nil ⇒ True
- | cons hd tl ⇒ closed_k O D hd k ∧ closed_list O D tl k
- ]
-. *)
-
-inductive is_closed (O:Type[0]) (D:O→FinSet): nat → T O D → Prop ≝
-| cval : ∀k,o,a.is_closed O D k (Val O D o a)
-| crel : ∀k,n. n < k → is_closed O D k (Rel O D n)
-| capp : ∀k,m,n. is_closed O D k m → is_closed O D k n →
- is_closed O D k (App O D m n)
-| clam : ∀T,k,m. is_closed O D (S k) m → is_closed O D k (Lambda O D T m)
-| cvec: ∀T,k,v. (∀m. mem ? m v → is_closed O D k m) →
- is_closed O D k (Vec O D T v).
-
-lemma is_closed_rel: ∀O,D,n,k.
- is_closed O D k (Rel O D n) → n < k.
-#O #D #n #k #H inversion H
- [#k0 #o #a #eqk #H destruct
- |#k0 #n0 #ltn0 #eqk #H destruct //
- |#k0 #M #N #_ #_ #_ #_ #_ #H destruct
- |#T #k0 #M #_ #_ #_ #H destruct
- |#T #k0 #v #_ #_ #_ #H destruct
- ]
-qed.
-
-lemma is_closed_app: ∀O,D,k,M, N.
- is_closed O D k (App O D M N) → is_closed O D k M ∧ is_closed O D k N.
-#O #D #k #M #N #H inversion H
- [#k0 #o #a #eqk #H destruct
- |#k0 #n0 #ltn0 #eqk #H destruct
- |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct % //
- |#T #k0 #M #_ #_ #_ #H destruct
- |#T #k0 #v #_ #_ #_ #H destruct
- ]
-qed.
-
-lemma is_closed_lam: ∀O,D,k,ty,M.
- is_closed O D k (Lambda O D ty M) → is_closed O D (S k) M.
-#O #D #k #ty #M #H inversion H
- [#k0 #o #a #eqk #H destruct
- |#k0 #n0 #ltn0 #eqk #H destruct
- |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct
- |#T #k0 #M1 #HM1 #_ #_ #H1 destruct //
- |#T #k0 #v #_ #_ #_ #H destruct
- ]
-qed.
-
-lemma is_closed_vec: ∀O,D,k,ty,v.
- is_closed O D k (Vec O D ty v) → ∀m. mem ? m v → is_closed O D k m.
-#O #D #k #ty #M #H inversion H
- [#k0 #o #a #eqk #H destruct
- |#k0 #n0 #ltn0 #eqk #H destruct
- |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct
- |#T #k0 #M1 #HM1 #_ #_ #H1 destruct
- |#T #k0 #v #Hv #_ #_ #H1 destruct @Hv
- ]
-qed.
-
-lemma is_closed_S: ∀O,D,M,m.
- is_closed O D m M → is_closed O D (S m) M.
-#O #D #M #m #H elim H //
- [#k #n0 #Hlt @crel @le_S //
- |#k #P #Q #HP #HC #H1 #H2 @capp //
- |#ty #k #P #HP #H1 @clam //
- |#ty #k #v #Hind #Hv @cvec @Hv
- ]
-qed.
-
-lemma is_closed_mono: ∀O,D,M,m,n. m ≤ n →
- is_closed O D m M → is_closed O D n M.
-#O #D #M #m #n #lemn elim lemn // #i #j #H #H1 @is_closed_S @H @H1
-qed.
-
-
-(*** properties of lift and subst ***)
-
-(*
-lemma lift_0: ∀O,D.∀t:T O D.∀k. lift O D t k 0 = t.
-#O #D #t @(T_elim … t) normalize //
- [#n #k cases (leb k n) normalize //
- |#o #v #Hind #k @eq_f lapply Hind -Hind elim v //
- #hd #tl #Hind #Hind1 normalize @eq_f2
- [@Hind1 %1 //|@Hind #x #Hx @Hind1 %2 //]
- ]
-qed.
-
-lemma lift_closed: ∀O,D.∀t:T O D.∀k,p.
- is_closed O D k t → lift O D t k p = t.
-#O #D #t @(T_elim … t) normalize //
- [#n #k #p #H >(not_le_to_leb_false … (lt_to_not_le … (is_closed_rel … H))) //
- |#M #N #HindM #HindN #k #p #H lapply (is_closed_app … H) * #HcM #HcN
- >(HindM … HcM) >(HindN … HcN) //
- |#ty #M #HindM #k #p #H lapply (is_closed_lam … H) -H #H >(HindM … H) //
- |#ty #v #HindM #k #p #H lapply (is_closed_vec … H) -H #H @eq_f
- cut (∀m. mem ? m v → lift O D m k p = m)
- [#m #Hmem @HindM [@Hmem | @H @Hmem]] -HindM
- elim v // #a #tl #Hind #H1 normalize @eq_f2
- [@H1 %1 //|@Hind #m #Hmem @H1 %2 @Hmem]
- ]
-qed.
-
-*)
-
-lemma subst_closed: ∀O,D,M,N,k,i. k ≤ i →
- is_closed O D k M → subst O D M i N = M.
-#O #D #M @(T_elim … M)
- [#o #a normalize //
- |#n #N #k #j #Hlt #Hc lapply (is_closed_rel … Hc) #Hnk normalize
- >not_le_to_leb_false [2:@lt_to_not_le @(lt_to_le_to_lt … Hnk Hlt)] //
- |#P #Q #HindP #HindQ #N #k #i #ltki #Hc lapply (is_closed_app … Hc) *
- #HcP #HcQ normalize >(HindP … ltki HcP) >(HindQ … ltki HcQ) //
- |#ty #P #HindP #N #k #i #ltki #Hc lapply (is_closed_lam … Hc)
- #HcP normalize >(HindP … HcP) // @le_S_S @ltki
- |#ty #v #Hindv #N #k #i #ltki #Hc lapply (is_closed_vec … Hc)
- #Hcv normalize @eq_f
- cut (∀m:T O D.mem (T O D) m v→ subst O D m i N=m)
- [#m #Hmem @(Hindv … Hmem N … ltki) @Hcv @Hmem]
- elim v // #a #tl #Hind #H normalize @eq_f2
- [@H %1 //| @Hind #Hmem #Htl @H %2 @Htl]
- ]
-qed.
-
-lemma subst_lemma: ∀O,D,A,B,C,k,i. is_closed O D k B → is_closed O D i C →
- subst O D (subst O D A i B) (k+i) C =
- subst O D (subst O D A (k+S i) C) i B.
-#O #D #A #B #C #k @(T_elim … A) normalize
- [//
- |#n #i #HBc #HCc @(leb_elim i n) #Hle
- [@(eqb_elim i n) #eqni
- [<eqni >(lt_to_leb_false (k+(S i)) i) // normalize
- >(subst_closed … HBc) // >le_to_leb_true // >eq_to_eqb_true //
- |(cut (i < n))
- [cases (le_to_or_lt_eq … Hle) // #eqin @False_ind /2/] #ltin
- (cut (0 < n)) [@(le_to_lt_to_lt … ltin) //] #posn
- normalize @(leb_elim (k+i) (n-1)) #nk
- [@(eqb_elim (k+i) (n-1)) #H normalize
- [cut (k+(S i) = n); [/2 by S_pred/] #H1
- >(le_to_leb_true (k+(S i)) n) /2/
- >(eq_to_eqb_true … H1) normalize >(subst_closed … HCc) //
- |(cut (k+i < n-1)) [@not_eq_to_le_to_lt; //] #Hlt
- >(le_to_leb_true (k+(S i)) n) normalize
- [>(not_eq_to_eqb_false (k+(S i)) n) normalize
- [>le_to_leb_true [2:@lt_to_le @(le_to_lt_to_lt … Hlt) //]
- >not_eq_to_eqb_false // @lt_to_not_eq @(le_to_lt_to_lt … Hlt) //
- |@(not_to_not … H) #Hn /2 by plus_minus/
- ]
- |<plus_n_Sm @(lt_to_le_to_lt … Hlt) //
- ]
- ]
- |>(not_le_to_leb_false (k+(S i)) n) normalize
- [>(le_to_leb_true … Hle) >(not_eq_to_eqb_false … eqni) //
- |@(not_to_not … nk) #H @le_plus_to_minus_r //
- ]
- ]
- ]
- |(cut (n < k+i)) [@(lt_to_le_to_lt ? i) /2 by not_le_to_lt/] #ltn
- >not_le_to_leb_false [2: @lt_to_not_le @(transitive_lt …ltn) //] normalize
- >not_le_to_leb_false [2: @lt_to_not_le //] normalize
- >(not_le_to_leb_false … Hle) //
- ]
- |#M #N #HindM #HindN #i #HBC #HCc @eq_f2 [@HindM // |@HindN //]
- |#ty #M #HindM #i #HBC #HCc @eq_f >plus_n_Sm >plus_n_Sm @HindM //
- @is_closed_S //
- |#ty #v #Hindv #i #HBC #HCc @eq_f
- cut (∀m.mem ? m v → subst O D (subst O D m i B) (k+i) C =
- subst O D (subst O D m (k+S i) C) i B)
- [#m #Hmem @Hindv //] -Hindv elim v normalize [//]
- #a #tl #Hind #H @eq_f2 [@H %1 // | @Hind #m #Hmem @H %2 //]
- ]
-qed.
-
-
projects / helm.git / blobdiff