+++ /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 "finite_lambda/reduction.ma".
-
-
-axiom canonical_to_T: ∀O,D.∀M:T O D.∀ty.(* type_of M ty → *)
- ∃a:FinSet_of_FType O D ty. star ? (red O D) M (to_T O D ty a).
-
-axiom normal_to_T: ∀O,D,M,ty,a. red O D (to_T O D ty a) M → False.
-
-axiom red_closed: ∀O,D,M,M1.
- is_closed O D 0 M → red O D M M1 → is_closed O D 0 M1.
-
-lemma critical: ∀O,D,ty,M,N.
- ∃M3:T O D
- .star (T O D) (red O D) (subst O D M 0 N) M3
- ∧star (T O D) (red O D)
- (App O D
- (Vec O D ty
- (map (FinSet_of_FType O D ty) (T O D)
- (λa0:FinSet_of_FType O D ty.subst O D M 0 (to_T O D ty a0))
- (enum (FinSet_of_FType O D ty)))) N) M3.
-#O #D #ty #M #N
-lapply (canonical_to_T O D N ty) * #a #Ha
-%{(subst O D M 0 (to_T O D ty a))} (* CR-term *)
-%[@red_star_subst @Ha
- |@trans_star [|@(star_red_appr … Ha)] @R_to_star @riota
- lapply (enum_complete (FinSet_of_FType O D ty) a)
- elim (enum (FinSet_of_FType O D ty))
- [normalize #H1 destruct (H1)
- |#hd #tl #Hind #H cases (orb_true_l … H) -H #Hcase
- [normalize >Hcase >(\P Hcase) //
- |normalize cases (true_or_false (a==hd)) #Hcase1
- [normalize >Hcase1 >(\P Hcase1) // |>Hcase1 @Hind @Hcase]
- ]
- ]
- ]
-qed.
-
-lemma critical2: ∀O,D,ty,a,M,M1,M2,v.
- red O D (Vec O D ty v) M →
- red O D (App O D (Vec O D ty v) (to_T O D ty a)) M1 →
- assoc (FinSet_of_FType O D ty) (T O D) a (enum (FinSet_of_FType O D ty)) v
- =Some (T O D) M2 →
- ∃M3:T O D
- .star (T O D) (red O D) M2 M3
- ∧star (T O D) (red O D) (App O D M (to_T O D ty a)) M3.
-#O #D #ty #a #M #M1 #M2 #v #redM #redM1 #Ha lapply (red_vec … redM) -redM
-* #N * #N1 * #v1 * #v2 * * #Hred1 #Hv #HM0 >HM0 -HM0 >Hv in Ha; #Ha
-cases (same_assoc … a (enum (FinSet_of_FType O D ty)) v1 v2 N N1)
- [* >Ha -Ha #H1 destruct (H1) #Ha
- %{N1} (* CR-term *) % [@R_to_star //|@R_to_star @(riota … Ha)]
- |#Ha1 %{M2} (* CR-term *) % [// | @R_to_star @riota <Ha1 @Ha]
- ]
-qed.
-
-
-lemma critical3: ∀O,D,ty,M1,M2. red O D M1 M2 →
- ∃M3:T O D.star (T O D) (red O D) (Lambda O D ty M2) M3
- ∧star (T O D) (red O D)
- (Vec O D ty
- (map (FinSet_of_FType O D ty) (T O D)
- (λa:FinSet_of_FType O D ty.subst O D M1 0 (to_T O D ty a))
- (enum (FinSet_of_FType O D ty)))) M3.
-#O #D #ty #M1 #M2 #Hred
- %{(Vec O D ty
- (map (FinSet_of_FType O D ty) (T O D)
- (λa:FinSet_of_FType O D ty.subst O D M2 0 (to_T O D ty a))
- (enum (FinSet_of_FType O D ty))))} (* CR-term *) %
- [@R_to_star @rmem
- |@star_red_vec2 [>length_map >length_map //] #n #M0
- cases (true_or_false (leb (|enum (FinSet_of_FType O D ty)|) n)) #Hcase
- [>nth_to_default [2:>length_map @(leb_true_to_le … Hcase)]
- >nth_to_default [2:>length_map @(leb_true_to_le … Hcase)] //
- |cut (n < |enum (FinSet_of_FType O D ty)|)
- [@not_le_to_lt @leb_false_to_not_le @Hcase] #Hlt
- cut (∃a:FinSet_of_FType O D ty.True)
- [lapply Hlt lapply (enum_complete (FinSet_of_FType O D ty))
- cases (enum (FinSet_of_FType O D ty))
- [#_ normalize #H @False_ind @(absurd … H) @lt_to_not_le //
- |#a #l #_ #_ %{a} //
- ]
- ] * #a #_
- >(nth_map ?????? a Hlt) >(nth_map ?????? a Hlt) #_
- @red_star_subst2 //
- ]
- ]
-qed.
-
-(* we need to proceed by structural induction on the term and then
-by inversion on the two redexes. The problem are the moves in a
-same subterm, since we need an induction hypothesis, there *)
-
-lemma local_confluence: ∀O,D,M,M1,M2. red O D M M1 → red O D M M2 →
-∃M3. star ? (red O D) M1 M3 ∧ star ? (red O D) M2 M3.
-#O #D #M @(T_elim … M)
- [#o #a #M1 #M2 #H elim(red_val ????? H)
- |#n #M1 #M2 #H elim(red_rel ???? H)
- |(* app : this is the interesting case *)
- #P #Q #HindP #HindQ
- #M1 #M2 #H1 inversion H1 -H1
- [(* right redex is beta *)
- #ty #Q #N #Hc #HM >HM -HM #HM1 >HM1 - HM1 #Hl inversion Hl
- [#ty1 #Q1 #N1 #Hc1 #H1 destruct (H1) #H_
- %{(subst O D Q1 0 N1)} (* CR-term *) /2/
- |#ty #v #a #M0 #_ #H1 destruct (H1) (* vacuous *)
- |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #_ cases (red_lambda … redM0)
- [* #Q1 * #redQ #HM10 >HM10
- %{(subst O D Q1 0 N0)} (* CR-term *) %
- [@red_star_subst2 //|@R_to_star @rbeta @Hc]
- |#HM1 >HM1 @critical
- ]
- |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #HM2
- %{(subst O D Q 0 N1)} (* CR-term *)
- %[@red_star_subst @R_to_star //|@R_to_star @rbeta @(red_closed … Hc) //]
- |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
- |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
- |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
- ]
- |(* right redex is iota *)#ty #v #a #M3 #Ha #_ #_ #Hl inversion Hl
- [#P1 #M1 #N1 #_ #H1 destruct (H1) (* vacuous *)
- |#ty1 #v1 #a1 #M4 #Ha1 #H1 destruct (H1) -H1 #HM4 >(inj_to_T … e0) in Ha;
- >Ha1 #H1 destruct (H1) %{M3} (* CR-term *) /2/
- |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 @(critical2 … redM0 Hl Ha)
- |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) elim (normal_to_T … redN0N1)
- |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
- |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
- |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
- ]
- |(* right redex is appl *)#M3 #M4 #N #redM3M4 #_ #H1 destruct (H1) #_
- #Hl inversion Hl
- [#ty1 #M1 #N1 #Hc #H1 destruct (H1) #HM2 lapply (red_lambda … redM3M4) *
- [* #M3 * #H1 #H2 >H2 %{(subst O D M3 0 N1)} %
- [@R_to_star @rbeta @Hc|@red_star_subst2 // ]
- |#H >H -H lapply (critical O D ty1 M1 N1) * #M3 * #H1 #H2
- %{M3} /2/
- ]
- |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct
- lapply (critical2 … redM3M4 Hl Ha1) * #M3 * #H1 #H2 %{M3} /2/
- |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
- lapply (HindP … redM0 redM3M4) * #M3 * #H1 #H2
- %{(App O D M3 N0)} (* CR-term *) % [@star_red_appl //|@star_red_appl //]
- |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #_
- %{(App O D M4 N1)} % @R_to_star [@rappr //|@rappl //]
- |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
- |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
- |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
- ]
- |(* right redex is appr *)#M3 #N #N1 #redN #_ #H1 destruct (H1) #_
- #Hl inversion Hl
- [#ty1 #M0 #N0 #Hc #H1 destruct (H1) #HM2
- %{(subst O D M0 0 N1)} (* CR-term *) %
- [@R_to_star @rbeta @(red_closed … Hc) //|@red_star_subst @R_to_star // ]
- |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct (H1) elim (normal_to_T … redN)
- |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
- %{(App O D M10 N1)} (* CR-term *) % @R_to_star [@rappl //|@rappr //]
- |#M0 #N0 #N10 #redN0 #_ #H1 destruct (H1) #_
- lapply (HindQ … redN0 redN) * #M3 * #H1 #H2
- %{(App O D M0 M3)} (* CR-term *) % [@star_red_appr //|@star_red_appr //]
- |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
- |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
- |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
- ]
- |(* right redex is rlam *) #ty #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
- |(* right redex is rmem *) #ty #M0 #H1 destruct (H1) (* vacuous *)
- |(* right redex is vec *) #ty #N #N1 #v #v1 #_ #_
- #H1 destruct (H1) (* vacuous *)
- ]
- |#ty #M1 #Hind #M2 #M3 #H1 #H2 (* this case is not trivial any more *)
- lapply (red_lambda … H1) *
- [* #M4 * #H3 #H4 >H4 lapply (red_lambda … H2) *
- [* #M5 * #H5 #H6 >H6 lapply(Hind … H3 H5) * #M6 * #H7 #H8
- %{(Lambda O D ty M6)} (* CR-term *) % @star_red_lambda //
- |#H5 >H5 @critical3 //
- ]
- |#HM2 >HM2 lapply (red_lambda … H2) *
- [* #M4 * #Hred #HM3 >HM3 lapply (critical3 … ty ?? Hred) * #M5
- * #H3 #H4 %{M5} (* CR-term *) % //
- |#HM3 >HM3 %{M3} (* CR-term *) % //
- ]
- ]
- |#ty #v1 #Hind #M1 #M2 #H1 #H2
- lapply (red_vec … H1) * #N11 * #N12 * #v11 * #v12 * * #redN11 #Hv1 #HM1
- lapply (red_vec … H2) * #N21* #N22 * #v21 * #v22 * * #redN21 #Hv2 #HM2
- >Hv1 in Hv2; #Hvv lapply (compare_append … Hvv) -Hvv *
- (* we must proceed by cases on the list *) * normalize
- [(* N11 = N21 *) *
- [>append_nil * #Hl1 #Hl2 destruct lapply(Hind N11 … redN11 redN21)
- [@mem_append_l2 %1 //]
- * #M3 * #HM31 #HM32
- %{(Vec O D ty (v21@M3::v12))} (* CR-term *)
- % [@star_red_vec //|@star_red_vec //]
- |>append_nil * #Hl1 #Hl2 destruct lapply(Hind N21 … redN21 redN11)
- [@mem_append_l2 %1 //]
- * #M3 * #HM31 #HM32
- %{(Vec O D ty (v11@M3::v22))} (* CR-term *)
- % [@star_red_vec //|@star_red_vec //]
- ]
- |(* N11 ≠ N21 *) -Hind #P #l *
- [* #Hv11 #Hv22 destruct
- %{((Vec O D ty ((v21@N22::l)@N12::v12)))} (* CR-term *) % @R_to_star
- [>associative_append >associative_append normalize @rvec //
- |>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
- ]
- |* #Hv11 #Hv22 destruct
- %{((Vec O D ty ((v11@N12::l)@N22::v22)))} (* CR-term *) % @R_to_star
- [>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
- |>associative_append >associative_append normalize @rvec //
- ]
- ]
- ]
- ]
-qed.
-
-
-
-
+++ /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 "finite_lambda/terms_and_types.ma".
-
-(* some auxiliary lemmas *)
-
-lemma nth_to_default: ∀A,l,n,d.
- |l| ≤ n → nth n A l d = d.
-#A #l elim l [//] #a #tl #Hind #n cases n
- [#d normalize #H @False_ind @(absurd … H) @lt_to_not_le //
- |#m #d normalize #H @Hind @le_S_S_to_le @H
- ]
-qed.
-
-lemma mem_nth: ∀A,l,n,d.
- n < |l| → mem ? (nth n A l d) l.
-#A #l elim l
- [#n #d normalize #H @False_ind @(absurd … H) @lt_to_not_le //
- |#a #tl #Hind * normalize
- [#_ #_ %1 //| #m #d #HSS %2 @Hind @le_S_S_to_le @HSS]
- ]
-qed.
-
-lemma nth_map: ∀A,B,l,f,n,d1,d2.
- n < |l| → nth n B (map … f l) d1 = f (nth n A l d2).
-#n #B #l #f elim l
- [#m #d1 #d2 normalize #H @False_ind @(absurd … H) @lt_to_not_le //
- |#a #tl #Hind #m #d1 #d2 cases m normalize //
- #m1 #H @Hind @le_S_S_to_le @H
- ]
-qed.
-
-
-
-(* end of auxiliary lemmas *)
-
-let rec to_T O D ty on ty: FinSet_of_FType O D ty → T O D ≝
- match ty return (λty.FinSet_of_FType O D ty → T O D) with
- [atom o ⇒ λa.Val O D o a
- |arrow ty1 ty2 ⇒ λa:FinFun ??.Vec O D ty1
- (map ((FinSet_of_FType O D ty1)×(FinSet_of_FType O D ty2))
- (T O D) (λp.to_T O D ty2 (snd … p)) (pi1 … a))
- ]
-.
-
-lemma is_closed_to_T: ∀O,D,ty,a. is_closed O D 0 (to_T O D ty a).
-#O #D #ty elim ty //
-#ty1 #ty2 #Hind1 #Hind2 #a normalize @cvec #m #Hmem
-lapply (mem_map ????? Hmem) * #a1 * #H1 #H2 <H2 @Hind2
-qed.
-
-axiom inj_to_T: ∀O,D,ty,a1,a2. to_T O D ty a1 = to_T O D ty a2 → a1 = a2.
-(* complicata
-#O #D #ty elim ty
- [#o normalize #a1 #a2 #H destruct //
- |#ty1 #ty2 #Hind1 #Hind2 * #l1 #Hl1 * #l2 #Hl2 normalize #H destruct -H
- cut (l1=l2) [2: #H generalize in match Hl1; >H //] -Hl1 -Hl2
- lapply e0 -e0 lapply l2 -l2 elim l1
- [#l2 cases l2 normalize [// |#a1 #tl1 #H destruct]
- |#a1 #tl1 #Hind #l2 cases l2
- [normalize #H destruct
- |#a2 #tl2 normalize #H @eq_f2
- [@Hind2 *)
-
-let rec assoc (A:FinSet) (B:Type[0]) (a:A) l1 l2 on l1 : option B ≝
- match l1 with
- [ nil ⇒ None ?
- | cons hd1 tl1 ⇒ match l2 with
- [ nil ⇒ None ?
- | cons hd2 tl2 ⇒ if a==hd1 then Some ? hd2 else assoc A B a tl1 tl2
- ]
- ].
-
-lemma same_assoc: ∀A,B,a,l1,v1,v2,N,N1.
- assoc A B a l1 (v1@N::v2) = Some ? N ∧ assoc A B a l1 (v1@N1::v2) = Some ? N1
- ∨ assoc A B a l1 (v1@N::v2) = assoc A B a l1 (v1@N1::v2).
-#A #B #a #l1 #v1 #v2 #N #N1 lapply v1 -v1 elim l1
- [#v1 %2 // |#hd #tl #Hind * normalize cases (a==hd) normalize /3/]
-qed.
-
-lemma assoc_to_mem: ∀A,B,a,l1,l2,b.
- assoc A B a l1 l2 = Some ? b → mem ? b l2.
-#A #B #a #l1 elim l1
- [#l2 #b normalize #H destruct
- |#hd1 #tl1 #Hind *
- [#b normalize #H destruct
- |#hd2 #tl2 #b normalize cases (a==hd1) normalize
- [#H %1 destruct //|#H %2 @Hind @H]
- ]
- ]
-qed.
-
-lemma assoc_to_mem2: ∀A,B,a,l1,l2,b.
- assoc A B a l1 l2 = Some ? b → ∃l21,l22.l2=l21@b::l22.
-#A #B #a #l1 elim l1
- [#l2 #b normalize #H destruct
- |#hd1 #tl1 #Hind *
- [#b normalize #H destruct
- |#hd2 #tl2 #b normalize cases (a==hd1) normalize
- [#H %{[]} %{tl2} destruct //
- |#H lapply (Hind … H) * #la * #lb #H1
- %{(hd2::la)} %{lb} >H1 //]
- ]
- ]
-qed.
-
-lemma assoc_map: ∀A,B,C,a,l1,l2,f,b.
- assoc A B a l1 l2 = Some ? b → assoc A C a l1 (map ?? f l2) = Some ? (f b).
-#A #B #C #a #l1 elim l1
- [#l2 #f #b normalize #H destruct
- |#hd1 #tl1 #Hind *
- [#f #b normalize #H destruct
- |#hd2 #tl2 #f #b normalize cases (a==hd1) normalize
- [#H destruct // |#H @(Hind … H)]
- ]
- ]
-qed.
-
-(*************************** One step reduction *******************************)
-
-inductive red (O:Type[0]) (D:O→FinSet) : T O D →T O D → Prop ≝
- | (* we only allow beta on closed arguments *)
- rbeta: ∀P,M,N. is_closed O D 0 N →
- red O D (App O D (Lambda O D P M) N) (subst O D M 0 N)
- | riota: ∀ty,v,a,M.
- assoc ?? a (enum (FinSet_of_FType O D ty)) v = Some ? M →
- red O D (App O D (Vec O D ty v) (to_T O D ty a)) M
- | rappl: ∀M,M1,N. red O D M M1 → red O D (App O D M N) (App O D M1 N)
- | rappr: ∀M,N,N1. red O D N N1 → red O D (App O D M N) (App O D M N1)
- | rlam: ∀ty,N,N1. red O D N N1 → red O D (Lambda O D ty N) (Lambda O D ty N1)
- | rmem: ∀ty,M. red O D (Lambda O D ty M)
- (Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a))
- (enum (FinSet_of_FType O D ty))))
- | rvec: ∀ty,N,N1,v,v1. red O D N N1 →
- red O D (Vec O D ty (v@N::v1)) (Vec O D ty (v@N1::v1)).
-
-(*********************************** inversion ********************************)
-lemma red_vec: ∀O,D,ty,v,M.
- red O D (Vec O D ty v) M → ∃N,N1,v1,v2.
- red O D N N1 ∧ v = v1@N::v2 ∧ M = Vec O D ty (v1@N1::v2).
-#O #D #ty #v #M #Hred inversion Hred
- [#ty1 #M0 #N #Hc #H destruct
- |#ty1 #v1 #a #M0 #_ #H destruct
- |#M0 #M1 #N #_ #_ #H destruct
- |#M0 #M1 #N #_ #_ #H destruct
- |#ty1 #M #M1 #_ #_ #H destruct
- |#ty1 #M0 #H destruct
- |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct #_ %{N} %{N1} %{v1} %{v2} /3/
- ]
-qed.
-
-lemma red_lambda: ∀O,D,ty,M,N.
- red O D (Lambda O D ty M) N →
- (∃M1. red O D M M1 ∧ N = (Lambda O D ty M1)) ∨
- N = Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a))
- (enum (FinSet_of_FType O D ty))).
-#O #D #ty #M #N #Hred inversion Hred
- [#ty1 #M0 #N #Hc #H destruct
- |#ty1 #v1 #a #M0 #_ #H destruct
- |#M0 #M1 #N #_ #_ #H destruct
- |#M0 #M1 #N #_ #_ #H destruct
- |#ty1 #P #P1 #redP #_ #H #H1 destruct %1 %{P1} % //
- |#ty1 #M0 #H destruct #_ %2 //
- |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
- ]
-qed.
-
-lemma red_val: ∀O,D,ty,a,N.
- red O D (Val O D ty a) N → False.
-#O #D #ty #M #N #Hred inversion Hred
- [#ty1 #M0 #N #Hc #H destruct
- |#ty1 #v1 #a #M0 #_ #H destruct
- |#M0 #M1 #N #_ #_ #H destruct
- |#M0 #M1 #N #_ #_ #H destruct
- |#ty1 #N1 #N2 #_ #_ #H destruct
- |#ty1 #M0 #H destruct #_
- |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
- ]
-qed.
-
-lemma red_rel: ∀O,D,n,N.
- red O D (Rel O D n) N → False.
-#O #D #n #N #Hred inversion Hred
- [#ty1 #M0 #N #Hc #H destruct
- |#ty1 #v1 #a #M0 #_ #H destruct
- |#M0 #M1 #N #_ #_ #H destruct
- |#M0 #M1 #N #_ #_ #H destruct
- |#ty1 #N1 #N2 #_ #_ #H destruct
- |#ty1 #M0 #H destruct #_
- |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
- ]
-qed.
-
-(*************************** multi step reduction *****************************)
-lemma star_red_appl: ∀O,D,M,M1,N. star ? (red O D) M M1 →
- star ? (red O D) (App O D M N) (App O D M1 N).
-#O #D #M #N #N1 #H elim H //
-#P #Q #Hind #HPQ #Happ %1[|@Happ] @rappl @HPQ
-qed.
-
-lemma star_red_appr: ∀O,D,M,N,N1. star ? (red O D) N N1 →
- star ? (red O D) (App O D M N) (App O D M N1).
-#O #D #M #N #N1 #H elim H //
-#P #Q #Hind #HPQ #Happ %1[|@Happ] @rappr @HPQ
-qed.
-
-lemma star_red_vec: ∀O,D,ty,N,N1,v1,v2. star ? (red O D) N N1 →
- star ? (red O D) (Vec O D ty (v1@N::v2)) (Vec O D ty (v1@N1::v2)).
-#O #D #ty #N #N1 #v1 #v2 #H elim H //
-#P #Q #Hind #HPQ #Hvec %1[|@Hvec] @rvec @HPQ
-qed.
-
-lemma star_red_vec1: ∀O,D,ty,v1,v2,v. |v1| = |v2| →
- (∀n,M. n < |v1| → star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) →
- star ? (red O D) (Vec O D ty (v@v1)) (Vec O D ty (v@v2)).
-#O #D #ty #v1 elim v1
- [#v2 #v normalize #Hv2 >(lenght_to_nil … (sym_eq … Hv2)) normalize //
- |#N1 #tl1 #Hind * [normalize #v #H destruct] #N2 #tl2 #v normalize #HS
- #H @(trans_star … (Vec O D ty (v@N2::tl1)))
- [@star_red_vec @(H 0 N1) @le_S_S //
- |>append_cons >(append_cons ??? tl2) @(Hind… (injective_S … HS))
- #n #M #H1 @(H (S n)) @le_S_S @H1
- ]
- ]
-qed.
-
-lemma star_red_vec2: ∀O,D,ty,v1,v2. |v1| = |v2| →
- (∀n,M. n < |v1| → star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) →
- star ? (red O D) (Vec O D ty v1) (Vec O D ty v2).
-#O #D #ty #v1 #v2 @(star_red_vec1 … [ ])
-qed.
-
-lemma star_red_lambda: ∀O,D,ty,N,N1. star ? (red O D) N N1 →
- star ? (red O D) (Lambda O D ty N) (Lambda O D ty N1).
-#O #D #ty #N #N1 #H elim H //
-#P #Q #Hind #HPQ #Hlam %1[|@Hlam] @rlam @HPQ
-qed.
-
-(************************ reduction and substitution **************************)
-
-lemma red_star_subst : ∀O,D,M,N,N1,i.
- star ? (red O D) N N1 → star ? (red O D) (subst O D M i N) (subst O D M i N1).
-#O #D #M #N #N1 #i #Hred lapply i -i @(T_elim … M) normalize
- [#o #a #i //
- |#i #n cases (leb n i) normalize // cases (eqb n i) normalize //
- |#P #Q #HindP #HindQ #n normalize
- @(trans_star … (App O D (subst O D P n N1) (subst O D Q n N)))
- [@star_red_appl @HindP |@star_red_appr @HindQ]
- |#ty #P #HindP #i @star_red_lambda @HindP
- |#ty #v #Hindv #i @star_red_vec2 [>length_map >length_map //]
- #j #Q inversion v [#_ normalize //] #a #tl #_ #Hv
- cases (true_or_false (leb (S j) (|a::tl|))) #Hcase
- [lapply (leb_true_to_le … Hcase) -Hcase #Hcase
- >(nth_map ?????? a Hcase) >(nth_map ?????? a Hcase) #_ @Hindv >Hv @mem_nth //
- |>nth_to_default
- [2:>length_map @le_S_S_to_le @not_le_to_lt @leb_false_to_not_le //]
- >nth_to_default
- [2:>length_map @le_S_S_to_le @not_le_to_lt @leb_false_to_not_le //] //
- ]
- ]
-qed.
-
-lemma red_star_subst2 : ∀O,D,M,M1,N,i. is_closed O D 0 N →
- red O D M M1 → star ? (red O D) (subst O D M i N) (subst O D M1 i N).
-#O #D #M #M1 #N #i #HNc #Hred lapply i -i elim Hred
- [#ty #P #Q #HQc #i normalize @starl_to_star @sstepl
- [|@rbeta >(subst_closed … HQc) //] >(subst_closed … HQc) //
- lapply (subst_lemma ?? P ?? i 0 (is_closed_mono … HQc) HNc) //
- <plus_n_Sm <plus_n_O #H <H //
- |#ty #v #a #P #HP #i normalize >(subst_closed … (le_O_n …)) //
- @R_to_star @riota @assoc_map @HP
- |#P #P1 #Q #Hred #Hind #i normalize @star_red_appl @Hind
- |#P #P1 #Q #Hred #Hind #i normalize @star_red_appr @Hind
- |#ty #P #P1 #Hred #Hind #i normalize @star_red_lambda @Hind
- |#ty #P #i normalize @starl_to_star @sstepl [|@rmem]
- @star_to_starl @star_red_vec2 [>length_map >length_map >length_map //]
- #n #Q >length_map #H
- cut (∃a:(FinSet_of_FType O D ty).True)
- [lapply H -H lapply (enum_complete (FinSet_of_FType O D ty))
- cases (enum (FinSet_of_FType O D ty))
- [#x normalize #H @False_ind @(absurd … H) @lt_to_not_le //
- |#x #l #_ #_ %{x} //
- ]
- ] * #a #_
- >(nth_map ?????? a H) >(nth_map ?????? Q) [2:>length_map @H]
- >(nth_map ?????? a H)
- lapply (subst_lemma O D P (to_T O D ty
- (nth n (FinSet_of_FType O D ty) (enum (FinSet_of_FType O D ty)) a))
- N i 0 (is_closed_mono … (is_closed_to_T …)) HNc) // <plus_n_O #H1 >H1
- <plus_n_Sm <plus_n_O //
- |#ty #P #Q #v #v1 #Hred #Hind #n normalize
- <map_append <map_append @star_red_vec @Hind
- ]
-qed.
-
-
-
-
-
+++ /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.
-
-
+++ /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 "finite_lambda/reduction.ma".
-
-
-(****************************************************************)
-
-inductive TJ (O: Type[0]) (D:O → FinSet): list (FType O) → T O D → FType O → Prop ≝
- | tval: ∀G,o,a. TJ O D G (Val O D o a) (atom O o)
- | trel: ∀G1,ty,G2,n. length ? G1 = n → TJ O D (G1@ty::G2) (Rel O D n) ty
- | tapp: ∀G,M,N,ty1,ty2. TJ O D G M (arrow O ty1 ty2) → TJ O D G N ty1 →
- TJ O D G (App O D M N) ty2
- | tlambda: ∀G,M,ty1,ty2. TJ O D (ty1::G) M ty2 →
- TJ O D G (Lambda O D ty1 M) (arrow O ty1 ty2)
- | tvec: ∀G,v,ty1,ty2.
- (|v| = |enum (FinSet_of_FType O D ty1)|) →
- (∀M. mem ? M v → TJ O D G M ty2) →
- TJ O D G (Vec O D ty1 v) (arrow O ty1 ty2).
-
-lemma wt_to_T: ∀O,D,G,ty,a.TJ O D G (to_T O D ty a) ty.
-#O #D #G #ty elim ty
- [#o #a normalize @tval
- |#ty1 #ty2 #Hind1 #Hind2 normalize * #v #Hv @tvec
- [<Hv >length_map >length_map //
- |#M elim v
- [normalize @False_ind |#a #v1 #Hind3 * [#eqM >eqM @Hind2 |@Hind3]]
- ]
- ]
-qed.
-
-lemma inv_rel: ∀O,D,G,n,ty.
- TJ O D G (Rel O D n) ty → ∃G1,G2.|G1|=n∧G=G1@ty::G2.
-#O #D #G #n #ty #Hrel inversion Hrel
- [#G1 #o #a #_ #H destruct
- |#G1 #ty1 #G2 #n1 #H1 #H2 #H3 #H4 destruct %{G1} %{G2} /2/
- |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
- |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct
- |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct
- ]
-qed.
-
-lemma inv_tlambda: ∀O,D,G,M,ty1,ty2,ty3.
- TJ O D G (Lambda O D ty1 M) (arrow O ty2 ty3) →
- ty1 = ty2 ∧ TJ O D (ty2::G) M ty3.
-#O #D #G #M #ty1 #ty2 #ty3 #Hlam inversion Hlam
- [#G1 #o #a #_ #H destruct
- |#G1 #ty #G2 #n #_ #_ #H destruct
- |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
- |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct % //
- |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct
- ]
-qed.
-
-lemma inv_tvec: ∀O,D,G,v,ty1,ty2,ty3.
- TJ O D G (Vec O D ty1 v) (arrow O ty2 ty3) →
- (|v| = |enum (FinSet_of_FType O D ty1)|) ∧
- (∀M. mem ? M v → TJ O D G M ty3).
-#O #D #G #v #ty1 #ty2 #ty3 #Hvec inversion Hvec
- [#G #o #a #_ #H destruct
- |#G1 #ty #G2 #n #_ #_ #H destruct
- |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
- |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct
- |#G1 #v1 #ty4 #ty5 #Hv #Hmem #_ #_ #H #H1 destruct % // @Hmem
- ]
-qed.
-
-(* could be generalized *)
-lemma weak_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n →
- TJ O D (G1@G2) (Rel O D n) ty1 →
- TJ O D (G1@ty2::G2) (Rel O D (S n)) ty1.
-#O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel)
-* #G3 * #G4 * #H1 #H2 lapply (compare_append … H2)
-* #G5 *
- [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4
- @(absurd … H4) @le_to_not_lt //
- |* #H3 #H4 >H4 >append_cons <associative_append @trel
- >length_append >length_append <H1 >H3 >length_append normalize
- >plus_n_Sm >associative_plus @eq_f //
- ]
-qed.
-
-lemma strength_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n →
- TJ O D (G1@ty2::G2) (Rel O D n) ty1 →
- TJ O D (G1@G2) (Rel O D (n-1)) ty1.
-#O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel)
-* #G3 * #G4 * #H1 #H2 lapply (compare_append … H2)
-* #G5 *
- [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4
- @(absurd … H4) @le_to_not_lt //
- |lapply G5 -G5 *
- [>append_nil normalize * #H3 #H4 destruct @False_ind @(absurd … HG1)
- @le_to_not_lt //
- |#ty3 #G5 * #H3 normalize #H4 destruct (H4) <associative_append @trel
- <H1 >H3 >length_append >length_append normalize <plus_minus_associative //
- ]
- ]
-qed.
-
-lemma no_matter: ∀O,D,G,N,tyN.
- TJ O D G N tyN → ∀G1,G2,G3.G=G1@G2 → is_closed O D (|G1|) N →
- TJ O D (G1@G3) N tyN.
-#O #D #G #N #tyN #HN elim HN -HN -tyN -N -G
- [#G #o #a #G1 #G2 #G3 #_ #_ @tval
- |#G #ty #G2 #n #HG #G3 #G4 #G5 #H #HNC normalize
- lapply (is_closed_rel … HNC) #Hlt lapply (compare_append … H) * #G6 *
- [* #H1 @False_ind @(absurd ? Hlt) @le_to_not_lt <HG >H1 >length_append //
- |* cases G6
- [>append_nil normalize #H1 @False_ind
- @(absurd ? Hlt) @le_to_not_lt <HG >H1 //
- |#ty1 #G7 #H1 normalize #H2 destruct >associative_append @trel //
- ]
- ]
- |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #G3
- #Heq #Hc lapply (is_closed_app … Hc) -Hc * #HMc #HNc
- @(tapp … (HindM … Heq HMc) (HindN … Heq HNc))
- |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #G3 #Heq #Hc
- lapply (is_closed_lam … Hc) -Hc #HMc
- @tlambda @(HindM (ty1::G1) G2) [>Heq // |@HMc]
- |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #G3 #H1 #Hc @tvec
- [>length_map //
- |#M #Hmem @Hind // lapply (is_closed_vec … Hc) #Hvc @Hvc //
- ]
- ]
-qed.
-
-lemma nth_spec: ∀A,a,d,l1,l2,n. |l1| = n → nth n A (l1@a::l2) d = a.
-#A #a #d #l1 elim l1 normalize
- [#l2 #n #Hn <Hn //
- |#b #tl #Hind #l2 #m #Hm <Hm normalize @Hind //
- ]
-qed.
-
-lemma wt_subst_gen: ∀O,D,G,M,tyM.
- TJ O D G M tyM →
- ∀G1,G2,N,tyN.G=(G1@tyN::G2) →
- TJ O D G2 N tyN → is_closed O D 0 N →
- TJ O D (G1@G2) (subst O D M (|G1|) N) tyM.
-#O #D #G #M #tyM #HM elim HM -HM -tyM -M -G
- [#G #o #a #G1 #G2 #N #tyN #_ #HG #_ normalize @tval
- |#G #ty #G2 #n #Hlen #G21 #G22 #N #tyN #HG #HN #HNc
- normalize cases (true_or_false (leb (|G21|) n))
- [#H >H cases (le_to_or_lt_eq … (leb_true_to_le … H))
- [#ltn >(not_eq_to_eqb_false … (lt_to_not_eq … ltn)) normalize
- lapply (compare_append … HG) * #G3 *
- [* #HG1 #HG2 @(strength_rel … tyN … ltn) <HG @trel @Hlen
- |* #HG >HG in ltn; >length_append #ltn @False_ind
- @(absurd … ltn) @le_to_not_lt >Hlen //
- ]
- |#HG21 >(eq_to_eqb_true … HG21)
- cut (ty = tyN)
- [<(nth_spec ? ty ty ? G2 … Hlen) >HG @nth_spec @HG21] #Hty >Hty
- normalize <HG21 @(no_matter ????? HN []) //
- ]
- |#H >H normalize lapply (compare_append … HG) * #G3 *
- [* #H1 @False_ind @(absurd ? Hlen) @sym_not_eq @lt_to_not_eq >H1
- >length_append @(lt_to_le_to_lt n (|G21|)) // @not_le_to_lt
- @(leb_false_to_not_le … H)
- |cases G3
- [>append_nil * #H1 @False_ind @(absurd ? Hlen) <H1 @sym_not_eq
- @lt_to_not_eq @not_le_to_lt @(leb_false_to_not_le … H)
- |#ty2 #G4 * #H1 normalize #H2 destruct >associative_append @trel //
- ]
- ]
- ]
- |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #N0 #tyN0 #eqG
- #HN0 #Hc normalize @(tapp … ty1)
- [@(HindM … eqG HN0 Hc) |@(HindN … eqG HN0 Hc)]
- |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #N0 #tyN0 #eqG
- #HN0 #Hc normalize @(tlambda … ty1) @(HindM (ty1::G1) … HN0) // >eqG //
- |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #N0 #tyN0 #eqG
- #HN0 #Hc normalize @(tvec … ty1)
- [>length_map @Hlen
- |#M #Hmem lapply (mem_map ????? Hmem) * #a * -Hmem #Hmem #eqM <eqM
- @(Hind … Hmem … eqG HN0 Hc)
- ]
- ]
-qed.
-
-lemma wt_subst: ∀O,D,M,N,G,ty1,ty2.
- TJ O D (ty1::G) M ty2 →
- TJ O D G N ty1 → is_closed O D 0 N →
- TJ O D G (subst O D M 0 N) ty2.
-#O #D #M #N #G #ty1 #ty2 #HM #HN #Hc @(wt_subst_gen …(ty1::G) … [ ] … HN) //
-qed.
-
-lemma subject_reduction: ∀O,D,M,M1,G,ty.
- TJ O D G M ty → red O D M M1 → TJ O D G M1 ty.
-#O #D #M #M1 #G #ty #HM lapply M1 -M1 elim HM -HM -ty -G -M
- [#G #o #a #M1 #Hval elim (red_val ????? Hval)
- |#G #ty #G1 #n #_ #M1 #Hrel elim (red_rel ???? Hrel)
- |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #M1 #Hred inversion Hred
- [#P #M0 #N0 #Hc #H1 destruct (H1) #HM1 @(wt_subst … HN) //
- @(proj2 … (inv_tlambda … HM))
- |#ty #v #a #M0 #Ha #H1 #H2 destruct @(proj2 … (inv_tvec … HM))
- @(assoc_to_mem … Ha)
- |#M2 #M3 #N0 #Hredl #_ #H1 destruct (H1) #eqM1 @(tapp … HN) @HindM @Hredl
- |#M2 #M3 #N0 #Hredr #_ #H1 destruct (H1) #eqM1 @(tapp … HM) @HindN @Hredr
- |#ty #N0 #N1 #_ #_ #H1 destruct (H1)
- |#ty #M0 #H1 destruct (H1)
- |#ty #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1)
- ]
- |#G #P #ty1 #ty2 #HP #Hind #M1 #Hred lapply(red_lambda ????? Hred) *
- [* #P1 * #HredP #HM1 >HM1 @tlambda @Hind //
- |#HM1 >HM1 @tvec // #N #HN lapply(mem_map ????? HN)
- * #a * #mema #eqN <eqN -eqN @(wt_subst …HP) // @wt_to_T
- ]
- |#G #v #ty1 #ty2 #Hlen #Hv #Hind #M1 #Hred lapply(red_vec ????? Hred)
- * #N * #N1 * #v1 * #v2 * * #H1 #H2 #H3 >H3 @tvec
- [<Hlen >H2 >length_append >length_append @eq_f //
- |#M2 #Hmem cases (mem_append ???? Hmem) -Hmem #Hmem
- [@Hv >H2 @mem_append_l1 //
- |cases Hmem
- [#HM2 >HM2 -HM2 @(Hind N … H1) >H2 @mem_append_l2 %1 //
- |-Hmem #Hmem @Hv >H2 @mem_append_l2 %2 //
- ]
- ]
- ]
- ]
-qed.
-
--- /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/deqsets.ma".
+include "basics/lists/listb.ma".
+
+(*
+
+record DeqSet : Type[1] ≝ {
+ carr :> Type[0];
+ eqb: carr → carr → bool;
+ eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
+}. *)
+
+
+(* list *)
+
+let rec eq_list (A:DeqSet) (l1,l2:list A) on l1 ≝
+ match l1 with
+ [ nil ⇒ match l2 with [nil ⇒ true | _ ⇒ false]
+ | cons a1 tl1 ⇒
+ match l2 with [nil ⇒ false | cons a2 tl2 ⇒ a1 ==a2 ∧ eq_list A tl1 tl2]].
+
+lemma eq_list_true: ∀A:DeqSet.∀l1,l2:list A.
+ eq_list A l1 l2 = true ↔ l1 = l2.
+#A #l1 elim l1
+ [* [% // |#a #tl % normalize #H destruct ]
+ |#a1 #tl1 #Hind *
+ [normalize % #H destruct
+ |#a2 #tl2 normalize %
+ [cases (true_or_false (a1==a2)) #Heq >Heq normalize
+ [#Htl >(\P Heq) >(proj1 … (Hind tl2) Htl) // | #H destruct ]
+ |#H destruct >(\b (refl … )) >(proj2 … (Hind tl2) (refl …)) //
+ ]
+ ]
+ ]
+qed.
+
+definition DeqList ≝ λA:DeqSet.
+ mk_DeqSet (list A) (eq_list A) (eq_list_true A).
+
+unification hint 0 ≔ C;
+ T ≟ carr C,
+ X ≟ DeqList C
+(* ---------------------------------------- *) ⊢
+ list T ≡ carr X.
+
+alias id "eqb" = "cic:/matita/basics/deqsets/eqb#fix:0:0:3".
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type0".
+unification hint 0 ≔ T,a1,a2;
+ X ≟ DeqList T
+(* ---------------------------------------- *) ⊢
+ eq_list T a1 a2 ≡ eqb X a1 a2.
+
+
\ / GNU General Public License Version 2
V_______________________________________________________________ *)
-include "basics/lists/listb.ma".
+include "basics/deqlist.ma".
(****** DeqSet: a set with a decidable equality ******)
#A #B #f #a #b #eqf @memb_filter_l [@(\b eqf)]
@enum_prod_complete //
qed.
+
+(* FinFun *)
+
+definition enum_fun_raw: ∀A,B:DeqSet.list A → list B → list (list (DeqProd A B)) ≝
+ λA,B,lA,lB.foldr A (list (list (DeqProd A B)))
+ (λa.compose ??? (λb. cons ? 〈a,b〉) lB) [[]] lA.
+
+lemma enum_fun_raw_cons: ∀A,B,a,lA,lB.
+ enum_fun_raw A B (a::lA) lB =
+ compose ??? (λb. cons ? 〈a,b〉) lB (enum_fun_raw A B lA lB).
+//
+qed.
+
+definition is_functional ≝ λA,B:DeqSet.λlA:list A.λl: list (DeqProd A B).
+ map ?? (fst A B) l = lA.
+
+definition carr_fun ≝ λA,B:FinSet.
+ DeqSig (DeqList (DeqProd A B)) (is_functional A B (enum A)).
+
+definition carr_fun_l ≝ λA,B:DeqSet.λl.
+ DeqSig (DeqList (DeqProd A B)) (is_functional A B l).
+
+lemma compose_spec1 : ∀A,B,C:DeqSet.∀f:A→B→C.∀a:A.∀b:B.∀lA:list A.∀lB:list B.
+ a ∈ lA = true → b ∈ lB = true → ((f a b) ∈ (compose A B C f lA lB)) = true.
+#A #B #C #f #a #b #lA elim lA
+ [normalize #lB #H destruct
+ |#a1 #tl #Hind #lB #Ha #Hb cases (orb_true_l ?? Ha) #Hcase
+ [>(\P Hcase) normalize @memb_append_l1 @memb_map //
+ |@memb_append_l2 @Hind //
+ ]
+ ]
+qed.
+
+lemma compose_cons: ∀A,B,C.∀f:A→B→C.∀l1,l2,a.
+ compose A B C f (a::l1) l2 =
+ (map ?? (f a) l2)@(compose A B C f l1 l2).
+// qed.
+
+lemma compose_spec2 : ∀A,B,C:DeqSet.∀f:A→B→C.∀c:C.∀lA:list A.∀lB:list B.
+ c ∈ (compose A B C f lA lB) = true →
+ ∃a,b.a ∈ lA = true ∧ b ∈ lB = true ∧ c = f a b.
+#A #B #C #f #c #lA elim lA
+ [normalize #lB #H destruct
+ |#a1 #tl #Hind #lB >compose_cons #Hc cases (memb_append … Hc) #Hcase
+ [lapply(memb_map_to_exists … Hcase) * #b * #Hb #Hf
+ %{a1} %{b} /3/
+ |lapply(Hind ? Hcase) * #a2 * #b * * #Ha #Hb #Hf %{a2} %{b} % // % //
+ @orb_true_r2 //
+ ]
+ ]
+qed.
+
+definition compose2 ≝
+ λA,B:DeqSet.λa:A.λl. compose B (carr_fun_l A B l) (carr_fun_l A B (a::l))
+ (λb,tl. mk_Sig ?? (〈a,b〉::(pi1 … tl)) ?).
+normalize @eq_f @(pi2 … tl)
+qed.
+
+let rec Dfoldr (A:Type[0]) (B:list A → Type[0])
+ (f:∀a:A.∀l.B l → B (a::l)) (b:B [ ]) (l:list A) on l : B l ≝
+ match l with [ nil ⇒ b | cons a l ⇒ f a l (Dfoldr A B f b l)].
+
+definition empty_graph: ∀A,B:DeqSet. carr_fun_l A B [].
+#A #B %{[]} // qed.
+
+definition enum_fun: ∀A,B:DeqSet.∀lA:list A.list B → list (carr_fun_l A B lA) ≝
+ λA,B,lA,lB.Dfoldr A (λl.list (carr_fun_l A B l))
+ (λa,l.compose2 ?? a l lB) [empty_graph A B] lA.
+
+lemma mem_enum_fun: ∀A,B:DeqSet.∀lA,lB.∀x:carr_fun_l A B lA.
+ pi1 … x ∈ map ?? (pi1 … ) (enum_fun A B lA lB) = true →
+ x ∈ enum_fun A B lA lB = true .
+#A #B #lA #lB #x @(memb_map_inj
+ (DeqSig (DeqList (DeqProd A B))
+ (λx0:DeqList (DeqProd A B).is_functional A B lA x0))
+ (DeqList (DeqProd A B)) (pi1 …))
+* #l1 #H1 * #l2 #H2 #Heq lapply H1 lapply H2 >Heq //
+qed.
+
+lemma enum_fun_cons: ∀A,B,a,lA,lB.
+ enum_fun A B (a::lA) lB =
+ compose ??? (λb,tl. mk_Sig ?? (〈a,b〉::(pi1 … tl)) ?) lB (enum_fun A B lA lB).
+//
+qed.
+
+lemma map_map: ∀A,B,C.∀f:A→B.∀g:B→C.∀l.
+ map ?? g (map ?? f l) = map ?? (g ∘ f) l.
+#A #B #C #f #g #l elim l [//]
+#a #tl #Hind normalize @eq_f @Hind
+qed.
+
+lemma map_compose: ∀A,B,C,D.∀f:A→B→C.∀g:C→D.∀l1,l2.
+ map ?? g (compose A B C f l1 l2) = compose A B D (λa,b. g (f a b)) l1 l2.
+#A #B #C #D #f #g #l1 elim l1 [//]
+#a #tl #Hind #l2 >compose_cons >compose_cons <map_append @eq_f2
+ [@map_map |@Hind]
+qed.
+
+definition enum_fun_graphs: ∀A,B,lA,lB.
+ map ?? (pi1 … ) (enum_fun A B lA lB) = enum_fun_raw A B lA lB.
+#A #B #lA elim lA [normalize //]
+#a #tl #Hind #lB >(enum_fun_cons A B a tl lB) >enum_fun_raw_cons >map_compose
+cut (∀lB2. compose B (Σx:DeqList (DeqProd A B).is_functional A B tl x)
+ (DeqList (DeqProd A B))
+ (λa0:B
+ .λb:Σx:DeqList (DeqProd A B).is_functional A B tl x
+ .〈a,a0〉
+ ::pi1 (list (A×B)) (λx:DeqList (DeqProd A B).is_functional A B tl x) b) lB
+ (enum_fun A B tl lB2)
+ =compose B (list (A×B)) (list (A×B)) (λb:B.cons (A×B) 〈a,b〉) lB
+ (enum_fun_raw A B tl lB2))
+ [#lB2 elim lB
+ [normalize //
+ |#b #tlb #Hindb >compose_cons in ⊢ (???%); >compose_cons
+ @eq_f2 [<Hind >map_map // |@Hindb]]]
+#Hcut @Hcut
+qed.
+
+lemma uniqueb_compose: ∀A,B,C:DeqSet.∀f,l1,l2.
+ (∀a1,a2,b1,b2. f a1 b1 = f a2 b2 → a1 = a2 ∧ b1 = b2) →
+ uniqueb ? l1 = true → uniqueb ? l2 = true →
+ uniqueb ? (compose A B C f l1 l2) = true.
+#A #B #C #f #l1 #l2 #Hinj elim l1 //
+#a #tl #Hind #HuA #HuB >compose_cons @uniqueb_append
+ [@(unique_map_inj … HuB) #b1 #b2 #Hb1b2 @(proj2 … (Hinj … Hb1b2))
+ |@Hind // @(andb_true_r … HuA)
+ |#c #Hc lapply(memb_map_to_exists … Hc) * #b * #Hb2 #Hfab % #Hc
+ lapply(compose_spec2 … Hc) * #a1 * #b1 * * #Ha1 #Hb1 <Hfab #H
+ @(absurd (a=a1))
+ [@(proj1 … (Hinj … H))
+ |% #eqa @(absurd … Ha1) % <eqa #H lapply(andb_true_l … HuA) >H
+ normalize #H1 destruct (H1)
+ ]
+ ]
+qed.
+
+lemma enum_fun_unique: ∀A,B:DeqSet.∀lA,lB.
+ uniqueb ? lA = true → uniqueb ? lB = true →
+ uniqueb ? (enum_fun A B lA lB) = true.
+#A #B #lA elim lA
+ [#lB #_ #ulB //
+ |#a #tlA #Hind #lB #uA #uB lapply (enum_fun_cons A B a tlA lB) #H >H
+ @(uniqueb_compose B (carr_fun_l A B tlA) (carr_fun_l A B (a::tlA)))
+ [#b1 #b2 * #l1 #funl1 * #l2 #funl2 #H1 destruct (H1) /2/
+ |//
+ |@(Hind … uB) @(andb_true_r … uA)
+ ]
+ ]
+qed.
+
+lemma enum_fun_complete: ∀A,B:FinSet.∀l1,l2.
+ (∀x:A. memb A x l1 = true) →
+ (∀x:B. memb B x l2 = true) →
+ ∀x:carr_fun_l A B l1. memb ? x (enum_fun A B l1 l2) = true.
+#A #B #l1 #l2 #H1 #H2 * #g #H @mem_enum_fun >enum_fun_graphs
+lapply H -H lapply g -g elim l1
+ [* // #p #tlg normalize #H destruct (H)
+ |#a #tl #Hind #g cases g
+ [normalize in ⊢ (%→?); #H destruct (H)
+ |* #a1 #b #tl1 normalize in ⊢ (%→?); #H
+ cut (is_functional A B tl tl1) [destruct (H) //] #Hfun
+ >(cons_injective_l ????? H)
+ >(enum_fun_raw_cons … ) @(compose_spec1 … (λb. cons ? 〈a,b〉))
+ [@H2 |@Hind @Hfun]
+ ]
+ ]
+qed.
+
+definition FinFun ≝
+λA,B:FinSet.mk_FinSet (carr_fun A B)
+ (enum_fun A B (enum A) (enum B))
+ (enum_fun_unique A B … (enum_unique A) (enum_unique B))
+ (enum_fun_complete A B … (enum_complete A) (enum_complete B)).
+
+(*
+unification hint 0 ≔ C1,C2;
+ T1 ≟ FinSetcarr C1,
+ T2 ≟ FinSetcarr C2,
+ X ≟ FinProd C1 C2
+(* ---------------------------------------- *) ⊢
+ T1×T2 ≡ FinSetcarr X. *)
\ No newline at end of file
--- /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 "finite_lambda/reduction.ma".
+
+
+axiom canonical_to_T: ∀O,D.∀M:T O D.∀ty.(* type_of M ty → *)
+ ∃a:FinSet_of_FType O D ty. star ? (red O D) M (to_T O D ty a).
+
+axiom normal_to_T: ∀O,D,M,ty,a. red O D (to_T O D ty a) M → False.
+
+axiom red_closed: ∀O,D,M,M1.
+ is_closed O D 0 M → red O D M M1 → is_closed O D 0 M1.
+
+lemma critical: ∀O,D,ty,M,N.
+ ∃M3:T O D
+ .star (T O D) (red O D) (subst O D M 0 N) M3
+ ∧star (T O D) (red O D)
+ (App O D
+ (Vec O D ty
+ (map (FinSet_of_FType O D ty) (T O D)
+ (λa0:FinSet_of_FType O D ty.subst O D M 0 (to_T O D ty a0))
+ (enum (FinSet_of_FType O D ty)))) N) M3.
+#O #D #ty #M #N
+lapply (canonical_to_T O D N ty) * #a #Ha
+%{(subst O D M 0 (to_T O D ty a))} (* CR-term *)
+%[@red_star_subst @Ha
+ |@trans_star [|@(star_red_appr … Ha)] @R_to_star @riota
+ lapply (enum_complete (FinSet_of_FType O D ty) a)
+ elim (enum (FinSet_of_FType O D ty))
+ [normalize #H1 destruct (H1)
+ |#hd #tl #Hind #H cases (orb_true_l … H) -H #Hcase
+ [normalize >Hcase >(\P Hcase) //
+ |normalize cases (true_or_false (a==hd)) #Hcase1
+ [normalize >Hcase1 >(\P Hcase1) // |>Hcase1 @Hind @Hcase]
+ ]
+ ]
+ ]
+qed.
+
+lemma critical2: ∀O,D,ty,a,M,M1,M2,v.
+ red O D (Vec O D ty v) M →
+ red O D (App O D (Vec O D ty v) (to_T O D ty a)) M1 →
+ assoc (FinSet_of_FType O D ty) (T O D) a (enum (FinSet_of_FType O D ty)) v
+ =Some (T O D) M2 →
+ ∃M3:T O D
+ .star (T O D) (red O D) M2 M3
+ ∧star (T O D) (red O D) (App O D M (to_T O D ty a)) M3.
+#O #D #ty #a #M #M1 #M2 #v #redM #redM1 #Ha lapply (red_vec … redM) -redM
+* #N * #N1 * #v1 * #v2 * * #Hred1 #Hv #HM0 >HM0 -HM0 >Hv in Ha; #Ha
+cases (same_assoc … a (enum (FinSet_of_FType O D ty)) v1 v2 N N1)
+ [* >Ha -Ha #H1 destruct (H1) #Ha
+ %{N1} (* CR-term *) % [@R_to_star //|@R_to_star @(riota … Ha)]
+ |#Ha1 %{M2} (* CR-term *) % [// | @R_to_star @riota <Ha1 @Ha]
+ ]
+qed.
+
+
+lemma critical3: ∀O,D,ty,M1,M2. red O D M1 M2 →
+ ∃M3:T O D.star (T O D) (red O D) (Lambda O D ty M2) M3
+ ∧star (T O D) (red O D)
+ (Vec O D ty
+ (map (FinSet_of_FType O D ty) (T O D)
+ (λa:FinSet_of_FType O D ty.subst O D M1 0 (to_T O D ty a))
+ (enum (FinSet_of_FType O D ty)))) M3.
+#O #D #ty #M1 #M2 #Hred
+ %{(Vec O D ty
+ (map (FinSet_of_FType O D ty) (T O D)
+ (λa:FinSet_of_FType O D ty.subst O D M2 0 (to_T O D ty a))
+ (enum (FinSet_of_FType O D ty))))} (* CR-term *) %
+ [@R_to_star @rmem
+ |@star_red_vec2 [>length_map >length_map //] #n #M0
+ cases (true_or_false (leb (|enum (FinSet_of_FType O D ty)|) n)) #Hcase
+ [>nth_to_default [2:>length_map @(leb_true_to_le … Hcase)]
+ >nth_to_default [2:>length_map @(leb_true_to_le … Hcase)] //
+ |cut (n < |enum (FinSet_of_FType O D ty)|)
+ [@not_le_to_lt @leb_false_to_not_le @Hcase] #Hlt
+ cut (∃a:FinSet_of_FType O D ty.True)
+ [lapply Hlt lapply (enum_complete (FinSet_of_FType O D ty))
+ cases (enum (FinSet_of_FType O D ty))
+ [#_ normalize #H @False_ind @(absurd … H) @lt_to_not_le //
+ |#a #l #_ #_ %{a} //
+ ]
+ ] * #a #_
+ >(nth_map ?????? a Hlt) >(nth_map ?????? a Hlt) #_
+ @red_star_subst2 //
+ ]
+ ]
+qed.
+
+(* we need to proceed by structural induction on the term and then
+by inversion on the two redexes. The problem are the moves in a
+same subterm, since we need an induction hypothesis, there *)
+
+lemma local_confluence: ∀O,D,M,M1,M2. red O D M M1 → red O D M M2 →
+∃M3. star ? (red O D) M1 M3 ∧ star ? (red O D) M2 M3.
+#O #D #M @(T_elim … M)
+ [#o #a #M1 #M2 #H elim(red_val ????? H)
+ |#n #M1 #M2 #H elim(red_rel ???? H)
+ |(* app : this is the interesting case *)
+ #P #Q #HindP #HindQ
+ #M1 #M2 #H1 inversion H1 -H1
+ [(* right redex is beta *)
+ #ty #Q #N #Hc #HM >HM -HM #HM1 >HM1 - HM1 #Hl inversion Hl
+ [#ty1 #Q1 #N1 #Hc1 #H1 destruct (H1) #H_
+ %{(subst O D Q1 0 N1)} (* CR-term *) /2/
+ |#ty #v #a #M0 #_ #H1 destruct (H1) (* vacuous *)
+ |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #_ cases (red_lambda … redM0)
+ [* #Q1 * #redQ #HM10 >HM10
+ %{(subst O D Q1 0 N0)} (* CR-term *) %
+ [@red_star_subst2 //|@R_to_star @rbeta @Hc]
+ |#HM1 >HM1 @critical
+ ]
+ |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #HM2
+ %{(subst O D Q 0 N1)} (* CR-term *)
+ %[@red_star_subst @R_to_star //|@R_to_star @rbeta @(red_closed … Hc) //]
+ |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
+ |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ ]
+ |(* right redex is iota *)#ty #v #a #M3 #Ha #_ #_ #Hl inversion Hl
+ [#P1 #M1 #N1 #_ #H1 destruct (H1) (* vacuous *)
+ |#ty1 #v1 #a1 #M4 #Ha1 #H1 destruct (H1) -H1 #HM4 >(inj_to_T … e0) in Ha;
+ >Ha1 #H1 destruct (H1) %{M3} (* CR-term *) /2/
+ |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 @(critical2 … redM0 Hl Ha)
+ |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) elim (normal_to_T … redN0N1)
+ |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
+ |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ ]
+ |(* right redex is appl *)#M3 #M4 #N #redM3M4 #_ #H1 destruct (H1) #_
+ #Hl inversion Hl
+ [#ty1 #M1 #N1 #Hc #H1 destruct (H1) #HM2 lapply (red_lambda … redM3M4) *
+ [* #M3 * #H1 #H2 >H2 %{(subst O D M3 0 N1)} %
+ [@R_to_star @rbeta @Hc|@red_star_subst2 // ]
+ |#H >H -H lapply (critical O D ty1 M1 N1) * #M3 * #H1 #H2
+ %{M3} /2/
+ ]
+ |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct
+ lapply (critical2 … redM3M4 Hl Ha1) * #M3 * #H1 #H2 %{M3} /2/
+ |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
+ lapply (HindP … redM0 redM3M4) * #M3 * #H1 #H2
+ %{(App O D M3 N0)} (* CR-term *) % [@star_red_appl //|@star_red_appl //]
+ |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #_
+ %{(App O D M4 N1)} % @R_to_star [@rappr //|@rappl //]
+ |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
+ |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ ]
+ |(* right redex is appr *)#M3 #N #N1 #redN #_ #H1 destruct (H1) #_
+ #Hl inversion Hl
+ [#ty1 #M0 #N0 #Hc #H1 destruct (H1) #HM2
+ %{(subst O D M0 0 N1)} (* CR-term *) %
+ [@R_to_star @rbeta @(red_closed … Hc) //|@red_star_subst @R_to_star // ]
+ |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct (H1) elim (normal_to_T … redN)
+ |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
+ %{(App O D M10 N1)} (* CR-term *) % @R_to_star [@rappl //|@rappr //]
+ |#M0 #N0 #N10 #redN0 #_ #H1 destruct (H1) #_
+ lapply (HindQ … redN0 redN) * #M3 * #H1 #H2
+ %{(App O D M0 M3)} (* CR-term *) % [@star_red_appr //|@star_red_appr //]
+ |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
+ |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ ]
+ |(* right redex is rlam *) #ty #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ |(* right redex is rmem *) #ty #M0 #H1 destruct (H1) (* vacuous *)
+ |(* right redex is vec *) #ty #N #N1 #v #v1 #_ #_
+ #H1 destruct (H1) (* vacuous *)
+ ]
+ |#ty #M1 #Hind #M2 #M3 #H1 #H2 (* this case is not trivial any more *)
+ lapply (red_lambda … H1) *
+ [* #M4 * #H3 #H4 >H4 lapply (red_lambda … H2) *
+ [* #M5 * #H5 #H6 >H6 lapply(Hind … H3 H5) * #M6 * #H7 #H8
+ %{(Lambda O D ty M6)} (* CR-term *) % @star_red_lambda //
+ |#H5 >H5 @critical3 //
+ ]
+ |#HM2 >HM2 lapply (red_lambda … H2) *
+ [* #M4 * #Hred #HM3 >HM3 lapply (critical3 … ty ?? Hred) * #M5
+ * #H3 #H4 %{M5} (* CR-term *) % //
+ |#HM3 >HM3 %{M3} (* CR-term *) % //
+ ]
+ ]
+ |#ty #v1 #Hind #M1 #M2 #H1 #H2
+ lapply (red_vec … H1) * #N11 * #N12 * #v11 * #v12 * * #redN11 #Hv1 #HM1
+ lapply (red_vec … H2) * #N21* #N22 * #v21 * #v22 * * #redN21 #Hv2 #HM2
+ >Hv1 in Hv2; #Hvv lapply (compare_append … Hvv) -Hvv *
+ (* we must proceed by cases on the list *) * normalize
+ [(* N11 = N21 *) *
+ [>append_nil * #Hl1 #Hl2 destruct lapply(Hind N11 … redN11 redN21)
+ [@mem_append_l2 %1 //]
+ * #M3 * #HM31 #HM32
+ %{(Vec O D ty (v21@M3::v12))} (* CR-term *)
+ % [@star_red_vec //|@star_red_vec //]
+ |>append_nil * #Hl1 #Hl2 destruct lapply(Hind N21 … redN21 redN11)
+ [@mem_append_l2 %1 //]
+ * #M3 * #HM31 #HM32
+ %{(Vec O D ty (v11@M3::v22))} (* CR-term *)
+ % [@star_red_vec //|@star_red_vec //]
+ ]
+ |(* N11 ≠ N21 *) -Hind #P #l *
+ [* #Hv11 #Hv22 destruct
+ %{((Vec O D ty ((v21@N22::l)@N12::v12)))} (* CR-term *) % @R_to_star
+ [>associative_append >associative_append normalize @rvec //
+ |>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
+ ]
+ |* #Hv11 #Hv22 destruct
+ %{((Vec O D ty ((v11@N12::l)@N22::v22)))} (* CR-term *) % @R_to_star
+ [>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
+ |>associative_append >associative_append normalize @rvec //
+ ]
+ ]
+ ]
+ ]
+qed.
+
+
+
+
--- /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 "finite_lambda/terms_and_types.ma".
+
+(* some auxiliary lemmas *)
+
+lemma nth_to_default: ∀A,l,n,d.
+ |l| ≤ n → nth n A l d = d.
+#A #l elim l [//] #a #tl #Hind #n cases n
+ [#d normalize #H @False_ind @(absurd … H) @lt_to_not_le //
+ |#m #d normalize #H @Hind @le_S_S_to_le @H
+ ]
+qed.
+
+lemma mem_nth: ∀A,l,n,d.
+ n < |l| → mem ? (nth n A l d) l.
+#A #l elim l
+ [#n #d normalize #H @False_ind @(absurd … H) @lt_to_not_le //
+ |#a #tl #Hind * normalize
+ [#_ #_ %1 //| #m #d #HSS %2 @Hind @le_S_S_to_le @HSS]
+ ]
+qed.
+
+lemma nth_map: ∀A,B,l,f,n,d1,d2.
+ n < |l| → nth n B (map … f l) d1 = f (nth n A l d2).
+#n #B #l #f elim l
+ [#m #d1 #d2 normalize #H @False_ind @(absurd … H) @lt_to_not_le //
+ |#a #tl #Hind #m #d1 #d2 cases m normalize //
+ #m1 #H @Hind @le_S_S_to_le @H
+ ]
+qed.
+
+
+
+(* end of auxiliary lemmas *)
+
+let rec to_T O D ty on ty: FinSet_of_FType O D ty → T O D ≝
+ match ty return (λty.FinSet_of_FType O D ty → T O D) with
+ [atom o ⇒ λa.Val O D o a
+ |arrow ty1 ty2 ⇒ λa:FinFun ??.Vec O D ty1
+ (map ((FinSet_of_FType O D ty1)×(FinSet_of_FType O D ty2))
+ (T O D) (λp.to_T O D ty2 (snd … p)) (pi1 … a))
+ ]
+.
+
+lemma is_closed_to_T: ∀O,D,ty,a. is_closed O D 0 (to_T O D ty a).
+#O #D #ty elim ty //
+#ty1 #ty2 #Hind1 #Hind2 #a normalize @cvec #m #Hmem
+lapply (mem_map ????? Hmem) * #a1 * #H1 #H2 <H2 @Hind2
+qed.
+
+axiom inj_to_T: ∀O,D,ty,a1,a2. to_T O D ty a1 = to_T O D ty a2 → a1 = a2.
+(* complicata
+#O #D #ty elim ty
+ [#o normalize #a1 #a2 #H destruct //
+ |#ty1 #ty2 #Hind1 #Hind2 * #l1 #Hl1 * #l2 #Hl2 normalize #H destruct -H
+ cut (l1=l2) [2: #H generalize in match Hl1; >H //] -Hl1 -Hl2
+ lapply e0 -e0 lapply l2 -l2 elim l1
+ [#l2 cases l2 normalize [// |#a1 #tl1 #H destruct]
+ |#a1 #tl1 #Hind #l2 cases l2
+ [normalize #H destruct
+ |#a2 #tl2 normalize #H @eq_f2
+ [@Hind2 *)
+
+let rec assoc (A:FinSet) (B:Type[0]) (a:A) l1 l2 on l1 : option B ≝
+ match l1 with
+ [ nil ⇒ None ?
+ | cons hd1 tl1 ⇒ match l2 with
+ [ nil ⇒ None ?
+ | cons hd2 tl2 ⇒ if a==hd1 then Some ? hd2 else assoc A B a tl1 tl2
+ ]
+ ].
+
+lemma same_assoc: ∀A,B,a,l1,v1,v2,N,N1.
+ assoc A B a l1 (v1@N::v2) = Some ? N ∧ assoc A B a l1 (v1@N1::v2) = Some ? N1
+ ∨ assoc A B a l1 (v1@N::v2) = assoc A B a l1 (v1@N1::v2).
+#A #B #a #l1 #v1 #v2 #N #N1 lapply v1 -v1 elim l1
+ [#v1 %2 // |#hd #tl #Hind * normalize cases (a==hd) normalize /3/]
+qed.
+
+lemma assoc_to_mem: ∀A,B,a,l1,l2,b.
+ assoc A B a l1 l2 = Some ? b → mem ? b l2.
+#A #B #a #l1 elim l1
+ [#l2 #b normalize #H destruct
+ |#hd1 #tl1 #Hind *
+ [#b normalize #H destruct
+ |#hd2 #tl2 #b normalize cases (a==hd1) normalize
+ [#H %1 destruct //|#H %2 @Hind @H]
+ ]
+ ]
+qed.
+
+lemma assoc_to_mem2: ∀A,B,a,l1,l2,b.
+ assoc A B a l1 l2 = Some ? b → ∃l21,l22.l2=l21@b::l22.
+#A #B #a #l1 elim l1
+ [#l2 #b normalize #H destruct
+ |#hd1 #tl1 #Hind *
+ [#b normalize #H destruct
+ |#hd2 #tl2 #b normalize cases (a==hd1) normalize
+ [#H %{[]} %{tl2} destruct //
+ |#H lapply (Hind … H) * #la * #lb #H1
+ %{(hd2::la)} %{lb} >H1 //]
+ ]
+ ]
+qed.
+
+lemma assoc_map: ∀A,B,C,a,l1,l2,f,b.
+ assoc A B a l1 l2 = Some ? b → assoc A C a l1 (map ?? f l2) = Some ? (f b).
+#A #B #C #a #l1 elim l1
+ [#l2 #f #b normalize #H destruct
+ |#hd1 #tl1 #Hind *
+ [#f #b normalize #H destruct
+ |#hd2 #tl2 #f #b normalize cases (a==hd1) normalize
+ [#H destruct // |#H @(Hind … H)]
+ ]
+ ]
+qed.
+
+(*************************** One step reduction *******************************)
+
+inductive red (O:Type[0]) (D:O→FinSet) : T O D →T O D → Prop ≝
+ | (* we only allow beta on closed arguments *)
+ rbeta: ∀P,M,N. is_closed O D 0 N →
+ red O D (App O D (Lambda O D P M) N) (subst O D M 0 N)
+ | riota: ∀ty,v,a,M.
+ assoc ?? a (enum (FinSet_of_FType O D ty)) v = Some ? M →
+ red O D (App O D (Vec O D ty v) (to_T O D ty a)) M
+ | rappl: ∀M,M1,N. red O D M M1 → red O D (App O D M N) (App O D M1 N)
+ | rappr: ∀M,N,N1. red O D N N1 → red O D (App O D M N) (App O D M N1)
+ | rlam: ∀ty,N,N1. red O D N N1 → red O D (Lambda O D ty N) (Lambda O D ty N1)
+ | rmem: ∀ty,M. red O D (Lambda O D ty M)
+ (Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a))
+ (enum (FinSet_of_FType O D ty))))
+ | rvec: ∀ty,N,N1,v,v1. red O D N N1 →
+ red O D (Vec O D ty (v@N::v1)) (Vec O D ty (v@N1::v1)).
+
+(*********************************** inversion ********************************)
+lemma red_vec: ∀O,D,ty,v,M.
+ red O D (Vec O D ty v) M → ∃N,N1,v1,v2.
+ red O D N N1 ∧ v = v1@N::v2 ∧ M = Vec O D ty (v1@N1::v2).
+#O #D #ty #v #M #Hred inversion Hred
+ [#ty1 #M0 #N #Hc #H destruct
+ |#ty1 #v1 #a #M0 #_ #H destruct
+ |#M0 #M1 #N #_ #_ #H destruct
+ |#M0 #M1 #N #_ #_ #H destruct
+ |#ty1 #M #M1 #_ #_ #H destruct
+ |#ty1 #M0 #H destruct
+ |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct #_ %{N} %{N1} %{v1} %{v2} /3/
+ ]
+qed.
+
+lemma red_lambda: ∀O,D,ty,M,N.
+ red O D (Lambda O D ty M) N →
+ (∃M1. red O D M M1 ∧ N = (Lambda O D ty M1)) ∨
+ N = Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a))
+ (enum (FinSet_of_FType O D ty))).
+#O #D #ty #M #N #Hred inversion Hred
+ [#ty1 #M0 #N #Hc #H destruct
+ |#ty1 #v1 #a #M0 #_ #H destruct
+ |#M0 #M1 #N #_ #_ #H destruct
+ |#M0 #M1 #N #_ #_ #H destruct
+ |#ty1 #P #P1 #redP #_ #H #H1 destruct %1 %{P1} % //
+ |#ty1 #M0 #H destruct #_ %2 //
+ |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
+ ]
+qed.
+
+lemma red_val: ∀O,D,ty,a,N.
+ red O D (Val O D ty a) N → False.
+#O #D #ty #M #N #Hred inversion Hred
+ [#ty1 #M0 #N #Hc #H destruct
+ |#ty1 #v1 #a #M0 #_ #H destruct
+ |#M0 #M1 #N #_ #_ #H destruct
+ |#M0 #M1 #N #_ #_ #H destruct
+ |#ty1 #N1 #N2 #_ #_ #H destruct
+ |#ty1 #M0 #H destruct #_
+ |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
+ ]
+qed.
+
+lemma red_rel: ∀O,D,n,N.
+ red O D (Rel O D n) N → False.
+#O #D #n #N #Hred inversion Hred
+ [#ty1 #M0 #N #Hc #H destruct
+ |#ty1 #v1 #a #M0 #_ #H destruct
+ |#M0 #M1 #N #_ #_ #H destruct
+ |#M0 #M1 #N #_ #_ #H destruct
+ |#ty1 #N1 #N2 #_ #_ #H destruct
+ |#ty1 #M0 #H destruct #_
+ |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
+ ]
+qed.
+
+(*************************** multi step reduction *****************************)
+lemma star_red_appl: ∀O,D,M,M1,N. star ? (red O D) M M1 →
+ star ? (red O D) (App O D M N) (App O D M1 N).
+#O #D #M #N #N1 #H elim H //
+#P #Q #Hind #HPQ #Happ %1[|@Happ] @rappl @HPQ
+qed.
+
+lemma star_red_appr: ∀O,D,M,N,N1. star ? (red O D) N N1 →
+ star ? (red O D) (App O D M N) (App O D M N1).
+#O #D #M #N #N1 #H elim H //
+#P #Q #Hind #HPQ #Happ %1[|@Happ] @rappr @HPQ
+qed.
+
+lemma star_red_vec: ∀O,D,ty,N,N1,v1,v2. star ? (red O D) N N1 →
+ star ? (red O D) (Vec O D ty (v1@N::v2)) (Vec O D ty (v1@N1::v2)).
+#O #D #ty #N #N1 #v1 #v2 #H elim H //
+#P #Q #Hind #HPQ #Hvec %1[|@Hvec] @rvec @HPQ
+qed.
+
+lemma star_red_vec1: ∀O,D,ty,v1,v2,v. |v1| = |v2| →
+ (∀n,M. n < |v1| → star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) →
+ star ? (red O D) (Vec O D ty (v@v1)) (Vec O D ty (v@v2)).
+#O #D #ty #v1 elim v1
+ [#v2 #v normalize #Hv2 >(lenght_to_nil … (sym_eq … Hv2)) normalize //
+ |#N1 #tl1 #Hind * [normalize #v #H destruct] #N2 #tl2 #v normalize #HS
+ #H @(trans_star … (Vec O D ty (v@N2::tl1)))
+ [@star_red_vec @(H 0 N1) @le_S_S //
+ |>append_cons >(append_cons ??? tl2) @(Hind… (injective_S … HS))
+ #n #M #H1 @(H (S n)) @le_S_S @H1
+ ]
+ ]
+qed.
+
+lemma star_red_vec2: ∀O,D,ty,v1,v2. |v1| = |v2| →
+ (∀n,M. n < |v1| → star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) →
+ star ? (red O D) (Vec O D ty v1) (Vec O D ty v2).
+#O #D #ty #v1 #v2 @(star_red_vec1 … [ ])
+qed.
+
+lemma star_red_lambda: ∀O,D,ty,N,N1. star ? (red O D) N N1 →
+ star ? (red O D) (Lambda O D ty N) (Lambda O D ty N1).
+#O #D #ty #N #N1 #H elim H //
+#P #Q #Hind #HPQ #Hlam %1[|@Hlam] @rlam @HPQ
+qed.
+
+(************************ reduction and substitution **************************)
+
+lemma red_star_subst : ∀O,D,M,N,N1,i.
+ star ? (red O D) N N1 → star ? (red O D) (subst O D M i N) (subst O D M i N1).
+#O #D #M #N #N1 #i #Hred lapply i -i @(T_elim … M) normalize
+ [#o #a #i //
+ |#i #n cases (leb n i) normalize // cases (eqb n i) normalize //
+ |#P #Q #HindP #HindQ #n normalize
+ @(trans_star … (App O D (subst O D P n N1) (subst O D Q n N)))
+ [@star_red_appl @HindP |@star_red_appr @HindQ]
+ |#ty #P #HindP #i @star_red_lambda @HindP
+ |#ty #v #Hindv #i @star_red_vec2 [>length_map >length_map //]
+ #j #Q inversion v [#_ normalize //] #a #tl #_ #Hv
+ cases (true_or_false (leb (S j) (|a::tl|))) #Hcase
+ [lapply (leb_true_to_le … Hcase) -Hcase #Hcase
+ >(nth_map ?????? a Hcase) >(nth_map ?????? a Hcase) #_ @Hindv >Hv @mem_nth //
+ |>nth_to_default
+ [2:>length_map @le_S_S_to_le @not_le_to_lt @leb_false_to_not_le //]
+ >nth_to_default
+ [2:>length_map @le_S_S_to_le @not_le_to_lt @leb_false_to_not_le //] //
+ ]
+ ]
+qed.
+
+lemma red_star_subst2 : ∀O,D,M,M1,N,i. is_closed O D 0 N →
+ red O D M M1 → star ? (red O D) (subst O D M i N) (subst O D M1 i N).
+#O #D #M #M1 #N #i #HNc #Hred lapply i -i elim Hred
+ [#ty #P #Q #HQc #i normalize @starl_to_star @sstepl
+ [|@rbeta >(subst_closed … HQc) //] >(subst_closed … HQc) //
+ lapply (subst_lemma ?? P ?? i 0 (is_closed_mono … HQc) HNc) //
+ <plus_n_Sm <plus_n_O #H <H //
+ |#ty #v #a #P #HP #i normalize >(subst_closed … (le_O_n …)) //
+ @R_to_star @riota @assoc_map @HP
+ |#P #P1 #Q #Hred #Hind #i normalize @star_red_appl @Hind
+ |#P #P1 #Q #Hred #Hind #i normalize @star_red_appr @Hind
+ |#ty #P #P1 #Hred #Hind #i normalize @star_red_lambda @Hind
+ |#ty #P #i normalize @starl_to_star @sstepl [|@rmem]
+ @star_to_starl @star_red_vec2 [>length_map >length_map >length_map //]
+ #n #Q >length_map #H
+ cut (∃a:(FinSet_of_FType O D ty).True)
+ [lapply H -H lapply (enum_complete (FinSet_of_FType O D ty))
+ cases (enum (FinSet_of_FType O D ty))
+ [#x normalize #H @False_ind @(absurd … H) @lt_to_not_le //
+ |#x #l #_ #_ %{x} //
+ ]
+ ] * #a #_
+ >(nth_map ?????? a H) >(nth_map ?????? Q) [2:>length_map @H]
+ >(nth_map ?????? a H)
+ lapply (subst_lemma O D P (to_T O D ty
+ (nth n (FinSet_of_FType O D ty) (enum (FinSet_of_FType O D ty)) a))
+ N i 0 (is_closed_mono … (is_closed_to_T …)) HNc) // <plus_n_O #H1 >H1
+ <plus_n_Sm <plus_n_O //
+ |#ty #P #Q #v #v1 #Hred #Hind #n normalize
+ <map_append <map_append @star_red_vec @Hind
+ ]
+qed.
+
+
+
+
+
--- /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.
+
+
--- /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 "finite_lambda/reduction.ma".
+
+
+(****************************************************************)
+
+inductive TJ (O: Type[0]) (D:O → FinSet): list (FType O) → T O D → FType O → Prop ≝
+ | tval: ∀G,o,a. TJ O D G (Val O D o a) (atom O o)
+ | trel: ∀G1,ty,G2,n. length ? G1 = n → TJ O D (G1@ty::G2) (Rel O D n) ty
+ | tapp: ∀G,M,N,ty1,ty2. TJ O D G M (arrow O ty1 ty2) → TJ O D G N ty1 →
+ TJ O D G (App O D M N) ty2
+ | tlambda: ∀G,M,ty1,ty2. TJ O D (ty1::G) M ty2 →
+ TJ O D G (Lambda O D ty1 M) (arrow O ty1 ty2)
+ | tvec: ∀G,v,ty1,ty2.
+ (|v| = |enum (FinSet_of_FType O D ty1)|) →
+ (∀M. mem ? M v → TJ O D G M ty2) →
+ TJ O D G (Vec O D ty1 v) (arrow O ty1 ty2).
+
+lemma wt_to_T: ∀O,D,G,ty,a.TJ O D G (to_T O D ty a) ty.
+#O #D #G #ty elim ty
+ [#o #a normalize @tval
+ |#ty1 #ty2 #Hind1 #Hind2 normalize * #v #Hv @tvec
+ [<Hv >length_map >length_map //
+ |#M elim v
+ [normalize @False_ind |#a #v1 #Hind3 * [#eqM >eqM @Hind2 |@Hind3]]
+ ]
+ ]
+qed.
+
+lemma inv_rel: ∀O,D,G,n,ty.
+ TJ O D G (Rel O D n) ty → ∃G1,G2.|G1|=n∧G=G1@ty::G2.
+#O #D #G #n #ty #Hrel inversion Hrel
+ [#G1 #o #a #_ #H destruct
+ |#G1 #ty1 #G2 #n1 #H1 #H2 #H3 #H4 destruct %{G1} %{G2} /2/
+ |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
+ |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct
+ |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct
+ ]
+qed.
+
+lemma inv_tlambda: ∀O,D,G,M,ty1,ty2,ty3.
+ TJ O D G (Lambda O D ty1 M) (arrow O ty2 ty3) →
+ ty1 = ty2 ∧ TJ O D (ty2::G) M ty3.
+#O #D #G #M #ty1 #ty2 #ty3 #Hlam inversion Hlam
+ [#G1 #o #a #_ #H destruct
+ |#G1 #ty #G2 #n #_ #_ #H destruct
+ |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
+ |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct % //
+ |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct
+ ]
+qed.
+
+lemma inv_tvec: ∀O,D,G,v,ty1,ty2,ty3.
+ TJ O D G (Vec O D ty1 v) (arrow O ty2 ty3) →
+ (|v| = |enum (FinSet_of_FType O D ty1)|) ∧
+ (∀M. mem ? M v → TJ O D G M ty3).
+#O #D #G #v #ty1 #ty2 #ty3 #Hvec inversion Hvec
+ [#G #o #a #_ #H destruct
+ |#G1 #ty #G2 #n #_ #_ #H destruct
+ |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
+ |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct
+ |#G1 #v1 #ty4 #ty5 #Hv #Hmem #_ #_ #H #H1 destruct % // @Hmem
+ ]
+qed.
+
+(* could be generalized *)
+lemma weak_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n →
+ TJ O D (G1@G2) (Rel O D n) ty1 →
+ TJ O D (G1@ty2::G2) (Rel O D (S n)) ty1.
+#O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel)
+* #G3 * #G4 * #H1 #H2 lapply (compare_append … H2)
+* #G5 *
+ [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4
+ @(absurd … H4) @le_to_not_lt //
+ |* #H3 #H4 >H4 >append_cons <associative_append @trel
+ >length_append >length_append <H1 >H3 >length_append normalize
+ >plus_n_Sm >associative_plus @eq_f //
+ ]
+qed.
+
+lemma strength_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n →
+ TJ O D (G1@ty2::G2) (Rel O D n) ty1 →
+ TJ O D (G1@G2) (Rel O D (n-1)) ty1.
+#O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel)
+* #G3 * #G4 * #H1 #H2 lapply (compare_append … H2)
+* #G5 *
+ [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4
+ @(absurd … H4) @le_to_not_lt //
+ |lapply G5 -G5 *
+ [>append_nil normalize * #H3 #H4 destruct @False_ind @(absurd … HG1)
+ @le_to_not_lt //
+ |#ty3 #G5 * #H3 normalize #H4 destruct (H4) <associative_append @trel
+ <H1 >H3 >length_append >length_append normalize <plus_minus_associative //
+ ]
+ ]
+qed.
+
+lemma no_matter: ∀O,D,G,N,tyN.
+ TJ O D G N tyN → ∀G1,G2,G3.G=G1@G2 → is_closed O D (|G1|) N →
+ TJ O D (G1@G3) N tyN.
+#O #D #G #N #tyN #HN elim HN -HN -tyN -N -G
+ [#G #o #a #G1 #G2 #G3 #_ #_ @tval
+ |#G #ty #G2 #n #HG #G3 #G4 #G5 #H #HNC normalize
+ lapply (is_closed_rel … HNC) #Hlt lapply (compare_append … H) * #G6 *
+ [* #H1 @False_ind @(absurd ? Hlt) @le_to_not_lt <HG >H1 >length_append //
+ |* cases G6
+ [>append_nil normalize #H1 @False_ind
+ @(absurd ? Hlt) @le_to_not_lt <HG >H1 //
+ |#ty1 #G7 #H1 normalize #H2 destruct >associative_append @trel //
+ ]
+ ]
+ |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #G3
+ #Heq #Hc lapply (is_closed_app … Hc) -Hc * #HMc #HNc
+ @(tapp … (HindM … Heq HMc) (HindN … Heq HNc))
+ |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #G3 #Heq #Hc
+ lapply (is_closed_lam … Hc) -Hc #HMc
+ @tlambda @(HindM (ty1::G1) G2) [>Heq // |@HMc]
+ |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #G3 #H1 #Hc @tvec
+ [>length_map //
+ |#M #Hmem @Hind // lapply (is_closed_vec … Hc) #Hvc @Hvc //
+ ]
+ ]
+qed.
+
+lemma nth_spec: ∀A,a,d,l1,l2,n. |l1| = n → nth n A (l1@a::l2) d = a.
+#A #a #d #l1 elim l1 normalize
+ [#l2 #n #Hn <Hn //
+ |#b #tl #Hind #l2 #m #Hm <Hm normalize @Hind //
+ ]
+qed.
+
+lemma wt_subst_gen: ∀O,D,G,M,tyM.
+ TJ O D G M tyM →
+ ∀G1,G2,N,tyN.G=(G1@tyN::G2) →
+ TJ O D G2 N tyN → is_closed O D 0 N →
+ TJ O D (G1@G2) (subst O D M (|G1|) N) tyM.
+#O #D #G #M #tyM #HM elim HM -HM -tyM -M -G
+ [#G #o #a #G1 #G2 #N #tyN #_ #HG #_ normalize @tval
+ |#G #ty #G2 #n #Hlen #G21 #G22 #N #tyN #HG #HN #HNc
+ normalize cases (true_or_false (leb (|G21|) n))
+ [#H >H cases (le_to_or_lt_eq … (leb_true_to_le … H))
+ [#ltn >(not_eq_to_eqb_false … (lt_to_not_eq … ltn)) normalize
+ lapply (compare_append … HG) * #G3 *
+ [* #HG1 #HG2 @(strength_rel … tyN … ltn) <HG @trel @Hlen
+ |* #HG >HG in ltn; >length_append #ltn @False_ind
+ @(absurd … ltn) @le_to_not_lt >Hlen //
+ ]
+ |#HG21 >(eq_to_eqb_true … HG21)
+ cut (ty = tyN)
+ [<(nth_spec ? ty ty ? G2 … Hlen) >HG @nth_spec @HG21] #Hty >Hty
+ normalize <HG21 @(no_matter ????? HN []) //
+ ]
+ |#H >H normalize lapply (compare_append … HG) * #G3 *
+ [* #H1 @False_ind @(absurd ? Hlen) @sym_not_eq @lt_to_not_eq >H1
+ >length_append @(lt_to_le_to_lt n (|G21|)) // @not_le_to_lt
+ @(leb_false_to_not_le … H)
+ |cases G3
+ [>append_nil * #H1 @False_ind @(absurd ? Hlen) <H1 @sym_not_eq
+ @lt_to_not_eq @not_le_to_lt @(leb_false_to_not_le … H)
+ |#ty2 #G4 * #H1 normalize #H2 destruct >associative_append @trel //
+ ]
+ ]
+ ]
+ |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #N0 #tyN0 #eqG
+ #HN0 #Hc normalize @(tapp … ty1)
+ [@(HindM … eqG HN0 Hc) |@(HindN … eqG HN0 Hc)]
+ |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #N0 #tyN0 #eqG
+ #HN0 #Hc normalize @(tlambda … ty1) @(HindM (ty1::G1) … HN0) // >eqG //
+ |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #N0 #tyN0 #eqG
+ #HN0 #Hc normalize @(tvec … ty1)
+ [>length_map @Hlen
+ |#M #Hmem lapply (mem_map ????? Hmem) * #a * -Hmem #Hmem #eqM <eqM
+ @(Hind … Hmem … eqG HN0 Hc)
+ ]
+ ]
+qed.
+
+lemma wt_subst: ∀O,D,M,N,G,ty1,ty2.
+ TJ O D (ty1::G) M ty2 →
+ TJ O D G N ty1 → is_closed O D 0 N →
+ TJ O D G (subst O D M 0 N) ty2.
+#O #D #M #N #G #ty1 #ty2 #HM #HN #Hc @(wt_subst_gen …(ty1::G) … [ ] … HN) //
+qed.
+
+lemma subject_reduction: ∀O,D,M,M1,G,ty.
+ TJ O D G M ty → red O D M M1 → TJ O D G M1 ty.
+#O #D #M #M1 #G #ty #HM lapply M1 -M1 elim HM -HM -ty -G -M
+ [#G #o #a #M1 #Hval elim (red_val ????? Hval)
+ |#G #ty #G1 #n #_ #M1 #Hrel elim (red_rel ???? Hrel)
+ |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #M1 #Hred inversion Hred
+ [#P #M0 #N0 #Hc #H1 destruct (H1) #HM1 @(wt_subst … HN) //
+ @(proj2 … (inv_tlambda … HM))
+ |#ty #v #a #M0 #Ha #H1 #H2 destruct @(proj2 … (inv_tvec … HM))
+ @(assoc_to_mem … Ha)
+ |#M2 #M3 #N0 #Hredl #_ #H1 destruct (H1) #eqM1 @(tapp … HN) @HindM @Hredl
+ |#M2 #M3 #N0 #Hredr #_ #H1 destruct (H1) #eqM1 @(tapp … HM) @HindN @Hredr
+ |#ty #N0 #N1 #_ #_ #H1 destruct (H1)
+ |#ty #M0 #H1 destruct (H1)
+ |#ty #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1)
+ ]
+ |#G #P #ty1 #ty2 #HP #Hind #M1 #Hred lapply(red_lambda ????? Hred) *
+ [* #P1 * #HredP #HM1 >HM1 @tlambda @Hind //
+ |#HM1 >HM1 @tvec // #N #HN lapply(mem_map ????? HN)
+ * #a * #mema #eqN <eqN -eqN @(wt_subst …HP) // @wt_to_T
+ ]
+ |#G #v #ty1 #ty2 #Hlen #Hv #Hind #M1 #Hred lapply(red_vec ????? Hred)
+ * #N * #N1 * #v1 * #v2 * * #H1 #H2 #H3 >H3 @tvec
+ [<Hlen >H2 >length_append >length_append @eq_f //
+ |#M2 #Hmem cases (mem_append ???? Hmem) -Hmem #Hmem
+ [@Hv >H2 @mem_append_l1 //
+ |cases Hmem
+ [#HM2 >HM2 -HM2 @(Hind N … H1) >H2 @mem_append_l2 %1 //
+ |-Hmem #Hmem @Hv >H2 @mem_append_l2 %2 //
+ ]
+ ]
+ ]
+ ]
+qed.
+
projects / helm.git / commitdiff