(* lists **********************************************************************)
+lemma length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
+#A #l2 #l1 (elim l1) -l1 (normalize) //
+qed.
+
(* all(?,P,l) holds when P holds for all members of l *)
let rec all (A:Type[0]) (P:A→Prop) l on l ≝ match l with
[ nil ⇒ True
qed.
(* all2(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *)
-let rec all2 (A:Type[0]) (P:A→A→Prop) l1 l2 on l1 ≝ match l1 with
+let rec all2 (A,B:Type[0]) (P:A→B→Prop) l1 l2 on l1 ≝ match l1 with
[ nil ⇒ l2 = nil ?
| cons hd1 tl1 ⇒ match l2 with
[ nil ⇒ False
- | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A P tl1 tl2
+ | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A B P tl1 tl2
]
].
-lemma length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
-#A #l2 #l1 (elim l1) -l1 (normalize) //
+lemma all2_length: ∀A,B:Type[0]. ∀P:A→B→Prop.
+ ∀l1,l2. all2 … P l1 l2 → |l1|=|l2|.
+#A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
+#x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ]
+#x2 #l2 #_ #H elim H normalize /3/
+qed.
+
+lemma all2_hd: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
+ ∀l1,l2. all2 … P l1 l2 → P (hd … l1 a) (hd … l2 b).
+#A #B #P #a #b #Hab #l1 elim l1 -l1 [ #l2 #H2 >H2 @Hab ]
+#x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
+#x2 #l2 #_ #H elim H //
+qed.
+
+lemma all2_tl: ∀A,B:Type[0]. ∀P:A→B→Prop.
+ ∀l1,l2. all2 … P l1 l2 → all2 … P (tail … l1) (tail … l2).
+#A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
+#x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
+#x2 #l2 #_ #H elim H //
+qed.
+
+lemma all2_nth: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
+ ∀i,l1,l2. all2 … P l1 l2 → P (nth i … l1 a) (nth i … l2 b).
+#A #B #P #a #b #Hab #i elim i -i [ @all2_hd // | #i #IH #l1 #l2 #H @IH /2/ ]
+qed.
+
+lemma all2_append: ∀A,B,P,l2,m2. all2 A B P l2 m2 →
+ ∀l1,m1. all2 A B P l1 m1 → all2 A B P (l1 @ l2) (m1 @ m2).
+#A #B #P #l2 #m2 #H2 #l1 (elim l1) -l1 [ #m1 #H >H @H2 ]
+#x1 #l1 #IH1 #m2 elim m2 -m2 [ #false elim false ]
+#x2 #m2 #_ #H elim H /3/
qed.
(* terms **********************************************************************)
(* *)
(**************************************************************************)
-include "lambda/rc_sat.ma".
+include "lambda/rc_hsat.ma".
(* THE EVALUATION *************************************************************)
-(* The interpretation of a type t as a r.c. denoted by 〚t〛.
- * For the "conv" rule we need 〚M〛 ≈ 〚N〛 when M and N are convertible, so:
- * 1) 〚(λB.M N)〛 ≈ 〚N[0≝N]〛 implies that 〚(M N)〛 and 〚λB.M〛 are evaluated by
- * stacking the application arguments like a reduction machine does
- * 2) ∀M,N. 〚D M〛 ≈ 〚D N〛, implies that 〚D M〛 must be a constant.
- *)
-let rec ev E K t on t : RC ≝ match t with (* E: environment, K: stack *)
- [ Sort _ ⇒ snRC (* from λ→ *)
- | Rel i ⇒ nth i … E snRC (* from F *)
- | App M N ⇒ ev E (ev E ([]) N :: K) M (* machine-like push *)
- | Lambda _ M ⇒ ev (hd … K snRC :: E) (tail … K) M (* machine-like pop *)
- | Prod N M ⇒ let C ≝ (ev E ([]) N) in
- depRC C (ev (C :: E) K M) (* from λ→ and F *)
- | D _ ⇒ snRC (* see note 2 above *)
+(* The arity of a term t in an environment E *)
+let rec aa E t on t ≝ match t with
+ [ Sort _ ⇒ SORT
+ | Rel i ⇒ nth i … E SORT
+ | App M N ⇒ pred (aa E M)
+ | Lambda N M ⇒ let Q ≝ aa E N in ABST Q (aa (Q::E) M)
+ | Prod N M ⇒ aa ((aa E N)::E) M
+ | D M ⇒ aa E M
].
-interpretation "interpretation of a type" 'Eval2 t E K = (ev E K t).
+interpretation "arity assignment (term)" 'Eval1 t E = (aa E t).
-(* extensional equality of the interpretations *)
-definition eveq: T → T → Prop ≝ λt1,t2. ∀E,K. 〚t1〛_[E, K] ≅ 〚t2〛_[E, K].
-
-interpretation
- "extensional equality of the type interpretations"
- 'napart t1 t2 = (eveq t1 t2).
-
-(* The interpretation of a context of types as a context of r.c.'s *)
-let rec cev E G on G : list RC ≝ match G with
+(* The arity of a type context *)
+let rec caa E G on G ≝ match G with
[ nil ⇒ E
- | cons t F ⇒ let D ≝ cev E F in 〚t〛_[D,[]] :: D
+ | cons t F ⇒ let D ≝ caa E F in 〚t〛_[D] :: D
].
-interpretation "interpretation of a context" 'Eval1 G E = (cev E G).
+interpretation "arity assignment (type context)" 'Eval1 G E = (caa E G).
-theorem ev_app: ∀M,N,E,K. 〚App M N〛_[E, K] = 〚M〛_[E, 〚N〛_[E,[]]::K].
+lemma aa_app: ∀M,N,E. 〚App M N〛_[E] = pred (〚M〛_[E]).
// qed.
-theorem ev_lambda: ∀M,N,E,K.
- 〚Lambda N M〛_[E, K] = 〚M〛_[hd … K snRC :: E, tail … K].
+lemma aa_lambda: ∀M,N,E. 〚Lambda N M〛_[E] = ABST (〚N〛_[E]) (〚M〛_[〚N〛_[E]::E]).
// qed.
-theorem ev_prod: ∀M,N,E,K.
- 〚Prod N M〛_[E,K] = depRC (〚N〛_[E,[]]) (〚M〛_[〚N〛_[E,[]]::E,K]).
+lemma aa_prod: ∀M,N,E. 〚Prod N M〛_[E] = 〚M〛_[〚N〛_[E]::E].
// qed.
-theorem ev_repl: ∀t,E1,E2,K1,K2. E1 ≅ E2 → K1 ≅ K2 → 〚t〛_[E1,K1] ≅ 〚t〛_[E2,K2].
-#t (elim t) /5/
-qed.
-
-theorem ev_rel_lt: ∀K,D,E,i. (S i) ≤ |E| → 〚Rel i〛_[E @ D, K] = 〚Rel i〛_[E,K].
-#K #D #E (elim E) -E [1: #i #Hie (elim (not_le_Sn_O i)) #Hi (elim (Hi Hie)) ]
+lemma aa_rel_lt: ∀D,E,i. (S i) ≤ |E| → 〚Rel i〛_[E @ D] = 〚Rel i〛_[E].
+#D #E (elim E) -E [1: #i #Hie (elim (not_le_Sn_O i)) #Hi (elim (Hi Hie)) ]
#C #F #IHE #i (elim i) -i // #i #_ #Hie @IHE @le_S_S_to_le @Hie
qed.
-theorem ev_rel_ge: ∀K,D,E,i. (S i) ≰ |E| →
- 〚Rel i〛_[E @ D, K] = 〚Rel (i-|E|)〛_[D,K].
-#K #D #E (elim E) -E [ normalize // ]
+lemma aa_rel_ge: ∀D,E,i. (S i) ≰ |E| →
+ 〚Rel i〛_[E @ D] = 〚Rel (i-|E|)〛_[D].
+#D #E (elim E) -E [ normalize // ]
#C #F #IHE #i (elim i) -i [1: -IHE #Hie (elim Hie) -Hie #Hie (elim (Hie ?)) /2/ ]
normalize #i #_ #Hie @IHE /2/
qed.
-theorem ev_app_repl: ∀M1,M2,N1,N2. M1 ≈ M2 → N1 ≈ N2 →
- App M1 N1 ≈ App M2 N2.
-#M1 #M2 #N1 #N2 #IHM #IHN #E #K >ev_app (@transitive_rceq) /3/
-qed.
-
-theorem ev_lambda_repl: ∀N1,N2,M1,M2. N1 ≈ N2 → M1 ≈ M2 →
- Lambda N1 M1 ≈ Lambda N2 M2.
-#N1 #N2 #M1 #M2 #IHN #IHM #E #K >ev_lambda (@transitive_rceq) //
-qed.
-
-theorem ev_prod_repl: ∀N1,N2,M1,M2. N1 ≈ N2 → M1 ≈ M2 →
- Prod N1 M1 ≈ Prod N2 M2.
-#N1 #N2 #M1 #M2 #IHN #IHM #E #K >ev_prod @dep_repl //
-(@transitive_rceq) [2: @IHM | skip ] /3/
-qed.
-
-(* weakeing and thinning lemma for the type interpretation *)
+(* weakeing and thinning lemma arity assignment *)
(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
-theorem ev_lift: ∀E,Ep,t,Ek,K.
- 〚lift t (|Ek|) (|Ep|)〛_[Ek @ Ep @ E, K] ≅ 〚t〛_[Ek @ E, K].
+lemma aa_lift: ∀E,Ep,t,Ek.
+ 〚lift t (|Ek|) (|Ep|)〛_[Ek @ Ep @ E] = 〚t〛_[Ek @ E].
#E #Ep #t (elim t) -t
- [ #n >lift_sort /by SAT0_sort/
- | #i #Ek #K @(leb_elim (S i) (|Ek|)) #Hik
- [ >(lift_rel_lt … Hik) >(ev_rel_lt … Hik) >(ev_rel_lt … Hik) //
- | >(lift_rel_ge … Hik) >(
ev_rel_ge … Hik) <associative_append
- >(ev_rel_ge …) (>length_append)
+ [ #n //
+ | #i #Ek @(leb_elim (S i) (|Ek|)) #Hik
+ [ >(lift_rel_lt … Hik) >(aa_rel_lt … Hik) >(aa_rel_lt … Hik) //
+ | >(lift_rel_ge … Hik) >(
aa_rel_ge … Hik) <associative_append
+ >(aa_rel_ge …) (>length_append)
[ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ]
]
- | #M #N #IHM #IHN #Ek #K >lift_app >ev_app (@transitive_rceq) /3/
- | #N #M #IHN #IHM #Ek #K >lift_lambda >ev_lambda (@transitive_rceq)
- [2: >commutative_plus @(IHM (? :: ?)) | skip ] //
- | #N #M #IHN #IHM #Ek #K >lift_prod >ev_prod (@dep_repl) //
- (@transitive_rceq) [2: >commutative_plus @(IHM (? :: ?)) | skip ] /3/
- | //
+ | /4/
+ | #N #M #IHN #IHM #Ek >lift_lambda >aa_lambda
+ >commutative_plus >(IHM (? :: ?)) /3/
+ | #N #M #IHN #IHM #Ek >lift_prod >aa_prod
+ >commutative_plus >(IHM (? :: ?)) /3/
+ | #M #IHM #Ek @IHM
]
qed.
+(* substitution lemma arity assignment *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma aa_subst: ∀v,E,t,Ek. 〚t[|Ek|≝v]〛_[Ek @ E] = 〚t〛_[Ek @ 〚v〛_[E]::E].
+#v #E #t (elim t) -t
+ [ //
+ | #i #Ek @(leb_elim (S i) (|Ek|)) #H1ik
+ [ >(aa_rel_lt … H1ik) >(subst_rel1 … H1ik) >(aa_rel_lt … H1ik) //
+ | @(eqb_elim i (|Ek|)) #H2ik
+ [ >(aa_rel_ge … H1ik) >H2ik -H2ik H1ik >subst_rel2
+ >(aa_lift ? ? ? ([])) <minus_n_n /2/
+ | (lapply (arith4 … H1ik H2ik)) -H1ik H2ik #Hik
+ (>(subst_rel3 … Hik)) (>aa_rel_ge) [2: /2/ ]
+ <(associative_append ? ? ([?]) ?)
+ >aa_rel_ge >length_append (>commutative_plus)
+ [ <minus_plus // | @not_le_to_not_le_S_S /2/ ]
+ ]
+ ]
+ | //
+ | #N #M #IHN #IHM #Ek >subst_lambda > aa_lambda
+ >commutative_plus >(IHM (? :: ?)) /3/
+ | #N #M #IHN #IHM #Ek >subst_prod > aa_prod
+ >commutative_plus >(IHM (? :: ?)) /4/
+ | #M #IHM #Ek @IHM
+qed.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
(*
-theorem tj_ev: ∀G,A,B. G ⊢A:B → ∀H,l. l ∈ 〚G〛_(H) → A[l] ∈ 〚B[l]〛_〚G〛_(H).
-#G #A #B #tjAB (elim tjAB) -G A B tjAB
- [ #i #j #_ #H #l #_ >substc_sort >substc_sort /2 by SAT0_sort/
- | #G #B #n #tjB #IH #H #l (elim l) -l (normalize)
+(* extensional equality of the interpretations *)
+definition eveq: T → T → Prop ≝ λt1,t2. ∀E,K. 〚t1〛_[E, K] ≅ 〚t2〛_[E, K].
+
+interpretation
+ "extensional equality of the type interpretations"
+ 'napart t1 t2 = (eveq t1 t2).
+*)
+
+axiom ev_lift_0_S: ∀t,p,C,E,K. 〚lift t 0 (S p)〛_[C::E, K] ≅ 〚lift t 0 p〛_[E, K].
+
+theorem tj_ev: ∀G,t,u. G ⊢t:u → ∀E,l. l ∈ 〚G〛_[E] → t[l] ∈ 〚u[l]〛_[[], []].
+#G #t #u #tjtu (elim tjtu) -G t u tjtu
+ [ #i #j #_ #E #l #_ >tsubst_sort >tsubst_sort /2 by SAT0_sort/
+ | #G #u #n #tju #IHu #E #l (elim l) -l (normalize)
[ #_ /2 by SAT1_rel/
- | #C #D #IHl #mem (elim mem) -mem #mem #memc
- >lift_0 >delift // >lift_0
+ | #hd #tl #_ #H (elim H) -H #Hhd #Htl
+ >lift_0 >delift // >lift_0
+
+
+
+ (@mem_rceq_trans) [3: @symmetric_rceq @ev_lift_0_S | skip ]
*)
(*
theorem append_cons: ∀(A:Type[0]). ∀(l1,l2:list A). ∀a.
(a :: l1) @ l2 = a :: (l1 @ l2).
// qed.
-*)
\ No newline at end of file
+*)
projects / helm.git / commitdiff