-let rec L_check (F:xheight) M on M ≝ match M with
- [ Par _ ⇒ true
- | Var _ ⇒ false
- | App N P ⇒ andb (L_check F N) (L_check F P)
- | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in
- andb (y ≟ F X (subst_Y N y (Par X)))
- (L_check F (subst_Y N y (Par X))) ].
-*)
-
-let rec L_check_aux (F:xheight) M n on n ≝ match n with
-[ O ⇒ false (* vacuous *)
-| S m ⇒ match M with
- [ Par _ ⇒ true
- | Var _ ⇒ false
- | App N P ⇒ andb (L_check_aux F N m) (L_check_aux F P m)
- | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in
- andb (y ≟ F X (subst_Y N y (Par X)))
- (L_check_aux F (subst_Y N y (Par X)) m) ]].
-
-lemma L_check_aux_sound :
- ∀F,M,n.S_len M ≤ n → L_check_aux F M (S n) = true → L F M.
-intros 2;apply (S_len_ind ?? M);intro;cases M1;intros
-[autobatch
-|simplify in H2;destruct
-|simplify in H2;generalize in match H2;
- apply (andb_elim (L_check_aux F s n) (L_check_aux F s1 n));
- apply (bool_elim ? (L_check_aux F s n));simplify;intros
- [apply LApp
- [apply (H ?? (pred n))
- [simplify;(*len*)elim daemon
- |simplify in H1;generalize in match H1;cases n;intros
- [elim (not_le_Sn_O ? H5)
- |simplify;elim daemon (* H5 *)]
- |(* H3 *) elim daemon]
- |apply (H ?? (pred n))
- [simplify;(*len*) elim daemon
- |simplify in H1;generalize in match H1;cases n;intros
- [elim (not_le_Sn_O ? H5)
- |simplify;elim daemon (* H5 *)]
- |(* H4 *) elim daemon]]
- |destruct]
-|simplify in H2;generalize in match H2;clear H2;
- apply (andb_elim (c ≟ F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s)))))
- (L_check_aux F (subst_Y s c (Par (N_fresh X (GV s)))) n));
- apply (bool_elim ? (c≟F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s))))));
- simplify;intros
- [rewrite > (p_eqb1 ??? H2);
- rewrite > (? : s =
- subst_X
- (subst_Y s c
- (Par (N_fresh X (GV s))))
- (N_fresh X (GV s))
- (Var (F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s)))))))
- in ⊢ (?? (?? %))
- [apply LAbs;apply (H ?? (pred n))
- [simplify;(*len*)elim daemon
- |simplify in H1;generalize in match H1;cases n;intros
- [elim (not_le_Sn_O ? H4)
- |simplify;elim daemon (* H4 *)]
- |rewrite > (? : S (pred n) = n)
- [assumption
- |(*arith*)elim daemon]]
- |rewrite < subst_Y_decompose
- [rewrite < (p_eqb1 ??? H2);autobatch
- |apply p_fresh]]
- |destruct]]
-qed.
-
-lemma LV_subst_X : ∀s,x,y. LV (subst_X s x (Var y)) ⊆ y::LV s.
-intros 3;elim s
-[simplify;cases (x ≟ c);simplify;
- [autobatch
- |unfold;intros;elim (not_in_list_nil ?? H)]
-|simplify;unfold;intros;autobatch
-|simplify;unfold;intros;
- cases (in_list_append_to_or_in_list ???? H2)
- [lapply (H ? H3);autobatch
- |lapply (H1 ? H3);cases (in_list_cons_case ???? Hletin)
- [applyS in_list_head
- |autobatch]]
-|simplify;unfold;intros;
- lapply (in_list_filter ???? H1);
- lapply (H ? Hletin);
- cases (in_list_cons_case ???? Hletin1)
- [rewrite > H2;autobatch
- |apply in_list_cons;apply in_list_filter_r
- [assumption
- |apply (in_list_filter_to_p_true ???? H1)]]]
-qed.
-
-lemma eq_list_nil : ∀A.∀l:list A.(∀x.x ∉ l) → l = [].
-intros 2;cases l;intro
-[reflexivity
-|elim (H a);autobatch]
-qed.
-
-(* to be revised *)
-lemma L_to_closed : ∀F:xheight.∀M.L F M → LV M = [].
-intros;elim H
-[reflexivity
-|simplify;autobatch paramodulation
-|simplify;generalize in match H2;generalize in match (F c s);elim s
- [simplify;apply (bool_elim ? (c ≟ c1));simplify;intro
- [rewrite > p_eqb3;reflexivity
- |reflexivity]
- |simplify in H3;destruct
- |simplify in H5;simplify;
- rewrite > (? :
- filter Y (LV (subst_X s1 c (Var c1))@LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)) =
- filter Y (LV (subst_X s1 c (Var c1))) (λz.¬(z≟c1))@ filter Y (LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)))
- [rewrite > H3
- [rewrite > H4
- [reflexivity
- |generalize in match H5;cases (LV s2);simplify;
- [intro;reflexivity
- |cases (LV s1);simplify;intro;destruct]]
- |generalize in match H5;cases (LV s1);simplify;intro
- [reflexivity
- |destruct]]
- |elim (LV (subst_X s1 c (Var c1)));simplify
- [reflexivity
- |cases (a ≟ c1);simplify;rewrite > H6;reflexivity]]
- |simplify;apply eq_list_nil;intro;intro;
- lapply (in_list_filter ???? H5) as H6;
- lapply (in_list_filter ???? H6) as H7;
- lapply (in_list_filter_to_p_true ???? H5) as H8;
- lapply (in_list_filter_to_p_true ???? H6) as H9;
- lapply (LV_subst_X ???? H7);
- cut (LV s1 ⊆ [c1])
- [cases (in_list_cons_case ???? Hletin)
- [rewrite > (p_eqb3 ??? H10) in H8;simplify in H8;destruct
- |lapply (Hcut ? H10);lapply (in_list_singleton_to_eq ??? Hletin1);
- rewrite > (p_eqb3 ??? Hletin2) in H9;simplify in H9;destruct]
- |simplify in H4;generalize in match H4;elim (LV s1) 0;simplify
- [intro;unfold;intros;elim (not_in_list_nil ?? H11)
- |intros 2;apply (bool_elim ? (a ≟ c1));simplify;intros
- [unfold;intros;cases (in_list_cons_case ???? H13)
- [rewrite > H14;rewrite > (p_eqb1 ??? H10);autobatch
- |apply H11;autobatch]
- |destruct]]]]]
-qed.
-
-lemma fresh_GV_subst_X_Var : ∀s,c,y.
- N_fresh X (GV (subst_X s c (Var y))) ∈ GV s →
- N_fresh X (GV (subst_X s c (Var y))) = c.
-intros;apply p_eqb1;
-apply (bool_elim ? (N_fresh X (GV (subst_X s c (Var y)))≟c));intro
-[reflexivity
-|lapply (p_eqb2 ??? H1);lapply (p_fresh ? (GV (subst_X s c (Var y))));
- lapply (GV_subst_X_Var s c y);
- elim Hletin1;cases (Hletin2 (N_fresh X (GV (subst_X s c (Var y)))));
- apply H3;apply in_list_filter_r
- [assumption
- |change in ⊢ (???%) with (¬false);apply eq_f;
- apply p_eqb4;intro;elim (p_eqb2 ??? H1);autobatch]]
-qed.
-
-lemma L_check_aux_complete :
- ∀F:xheight.∀M.LL F M → ∀n.S_len M ≤ n → L_check_aux F M (S n) = true.
-intros 3;elim H
-[reflexivity
-|simplify;simplify in H5;rewrite > (? : n = S (pred n))
- [rewrite > H2
- [rewrite > H4
- [reflexivity
- |(* H5 *) elim daemon]
- |(* H5 *) elim daemon]
- |(* H5 *) elim daemon]
-|simplify;simplify in H3;
- rewrite > (? : (F c s ≟ F (N_fresh X (GV (subst_X s c (Var (F c s)))))
- (subst_Y (subst_X s c (Var (F c s))) (F c s)
- (Par (N_fresh X (GV (subst_X s c (Var (F c s))))))))
- = true)
- [simplify;
- rewrite > (? : subst_Y (subst_X s c (Var (F c s))) (F c s)
- (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))) =
- subst_X s c (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))))
- [rewrite > (? : n = S (pred n))
- [rewrite > H2
- [reflexivity
- |autobatch
- |(* H3 *) elim daemon]
- |(* H3 *) elim daemon]
- |rewrite < subst_X_decompose
- [reflexivity
- |rewrite > (L_to_closed F)
- [autobatch
- |lapply (H1 c)
- [autobatch
- |intro;reflexivity]]
- |autobatch]]
- |rewrite < subst_X_decompose
- [rewrite > subst_X_fp
- [rewrite < (swap_left X c) in ⊢ (? ? (? ? ? (? ? % ?)) ?);
- autobatch
- |autobatch]
- |rewrite > (L_to_closed F)
- [autobatch
- |lapply (H1 c)
- [autobatch
- |intro;reflexivity]]
- |autobatch]]]
-qed.
-
-inductive typ : Type ≝
-| TPar : X → typ
-| Fun : typ → typ → typ.
-
-notation "hvbox(a break ▸ b)"
- left associative with precedence 50
-for @{ 'blacktriangleright $a $b }.
-interpretation "STT arrow type" 'blacktriangleright a b = (Fun a b).
-
-include "datatypes/constructors.ma".
-
-definition DOM : list (X × typ) → list X ≝ λC.map ?? (fst ??) C.
-
-inductive context : list (X × typ) → Prop ≝
-| ctx_nil : context []
-| ctx_cons : ∀x,t,C.x ∉ DOM C → context C → context (〈x,t〉::C).
-
-(* ▸ = \rtrif *)
-inductive typing (F:xheight): list (X × typ) → S_exp → typ → Prop ≝
-| t_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing F C (Par x) t
-| t_App : ∀C,M,N,t,u.typing F C M (t ▸ u) → typing F C N t →
- typing F C (App M N) u
-| t_Lam : ∀C,x,M,t,u.x ∉ DOM C → typing F (〈x,t〉::C) M u →
- typing F C (Abs (F x M) (subst_X M x (Var (F x M)))) (t ▸ u).
-
-inductive typing2 (F:xheight): list (X × typ) → S_exp → typ → Prop ≝
-| t2_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing2 F C (Par x) t
-| t2_App : ∀C,M,N,t,u.typing2 F C M (t ▸ u) → typing2 F C N t →
- typing2 F C (App M N) u
-| t2_Lam : ∀C,x1,M,t,u.
- (∀x2.x2 ∉ DOM C → (x2 ∈ GV M → x2 = x1) →
- typing2 F (〈x2,t〉::C) (subst_X M x1 (Par x2)) u) →
- typing2 F C (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))) (t ▸ u).
-
-notation > "C ⊢[F] M : t"
- non associative with precedence 30 for @{ 'typjudg F $C $M $t }.
-notation > "C ⊢ M : t"
- non associative with precedence 30 for @{ 'typjudg ? $C $M $t }.
-notation < "mstyle color #007f00 (hvbox(C maction (⊢) (⊢ \sub F) break M : break t))"
- non associative with precedence 30 for @{ 'typjudg $F $C $M $t }.
-interpretation "Fsub subtype judgement" 'typjudg F C M t = (typing F C M t).
-
-notation > "C ⊨[F] M : t"
- non associative with precedence 30 for @{ 'typjudg2 F $C $M $t }.
-notation > "C ⊨ M : t"
- non associative with precedence 30 for @{ 'typjudg2 ? $C $M $t }.
-notation < "mstyle color #007f00 (hvbox(C maction (⊨) (⊨ \sub F) break M : break t))"
- non associative with precedence 30 for @{ 'typjudg2 $F $C $M $t }.
-interpretation "Fsub strong subtype judgement" 'typjudg2 F C M t = (typing2 F C M t).
-
-lemma in_ctx_to_in_DOM : ∀x,t.∀C:list (X × typ).〈x,t〉 ∈ C → x ∈ DOM C.
-intros 3;elim C
-[elim (not_in_list_nil ?? H)
-|elim (in_list_cons_case ???? H1)
- [rewrite < H2;simplify;autobatch
- |cases a;simplify;autobatch]]
-qed.
-
-lemma in_DOM_to_in_ctx : ∀x,C.x ∈ DOM C → ∃t.〈x,t〉 ∈ C.
-intros 2;elim C
-[elim (not_in_list_nil X ? H)
-|elim a in H1;simplify in H1;elim (in_list_cons_case ???? H1)
- [rewrite > H2;autobatch
- |cases (H H2);autobatch]]
-qed.
-
-lemma incl_DOM : ∀l1,l2. l1 ⊆ l2 → DOM l1 ⊆ DOM l2.
-intros;unfold in H;unfold;intros;cases (in_DOM_to_in_ctx ?? H1);autobatch;
-qed.
-
-lemma typing2_weakening : ∀F,C,M,t.
- C ⊨[F] M : t → ∀D.context D → C ⊆ D → D ⊨[F] M : t.
-intros 5;elim H;try autobatch size=7;
-apply t2_Lam;intros;apply H2;
-[intro;autobatch
-|*:autobatch]
-qed.
-
-definition swap_list : ∀N:Nset.N → N → list N → list N ≝
- λN,a,b,l.map ?? (pi_swap ? a b) l.
-
-lemma in_list_swap : ∀N:Nset.∀x,l.x ∈ l → ∀a,b.swap N a b x ∈ swap_list N a b l.
-intros;elim H;simplify;autobatch;
-qed.
-
-definition ctx_swap_X : X → X → list (X × typ) → list (X × typ) ≝
- λx1,x2,C.map ?? (λp.
- match p with
- [pair x t ⇒ 〈pi_swap ? x1 x2 x,t〉]) C.
-
-lemma in_ctx_swap : ∀x,t,C.〈x,t〉 ∈ C → ∀a,b.〈swap ? a b x,t〉 ∈ ctx_swap_X a b C.
-intros;generalize in match H;elim C;
-[elim (not_in_list_nil ?? H1)
-|simplify;inversion H2;simplify;intros;destruct;simplify;autobatch]
-qed.