chap11: progress
This commit is contained in:
+382
-59
@@ -38,7 +38,9 @@ Module Chap11.
|
||||
(** T1 + T2 *)
|
||||
| type_Sum : type -> type -> type
|
||||
(** <l1 : T1, l2 : T2, ..., ln : Tn> *)
|
||||
| type_Variant : list (record_label * type) -> type.
|
||||
| type_Variant : list (record_label * type) -> type
|
||||
(** List[T] *)
|
||||
| type_List : type -> type.
|
||||
|
||||
Definition type_Bool := type_Base "Bool".
|
||||
Definition type_Unit := type_Base "Unit".
|
||||
@@ -101,7 +103,18 @@ Module Chap11.
|
||||
| term_variant_case : term -> list (record_label * varname * term) -> term
|
||||
|
||||
(** fix t *)
|
||||
| term_fix : term -> term.
|
||||
| term_fix : term -> term
|
||||
|
||||
(** nil[T] *)
|
||||
| term_nil : type -> term
|
||||
(** cons[T] t1 t2 *)
|
||||
| term_cons : type -> term -> term -> term
|
||||
(** is_nil[T] t *)
|
||||
| term_is_nil : type -> term -> term
|
||||
(** head[T] t *)
|
||||
| term_head : type -> term -> term
|
||||
(** tail[T] t *)
|
||||
| term_tail : type -> term -> term.
|
||||
|
||||
(* Although we don't have syntax sugar because we omit "Notation",
|
||||
we can simply define a function that looks like a "term_" constructor
|
||||
@@ -139,7 +152,13 @@ Module Chap11.
|
||||
is_value (term_inr v T)
|
||||
| v_variant : forall (l : record_label) (v : term) (T : type),
|
||||
is_value v ->
|
||||
is_value (term_variant l v T).
|
||||
is_value (term_variant l v T)
|
||||
| v_nil : forall (T : type),
|
||||
is_value (term_nil T)
|
||||
| v_cons : forall (T : type) (v1 v2 : term),
|
||||
is_value v1 ->
|
||||
is_value v2 ->
|
||||
is_value (term_cons T v1 v2).
|
||||
|
||||
Inductive is_pattern : term -> Prop :=
|
||||
| p_var : forall (x : string),
|
||||
@@ -220,7 +239,6 @@ Module Chap11.
|
||||
is_free_variable x (term_record_proj t k).
|
||||
(* TODO: expand me, and double check that the above is correct *)
|
||||
|
||||
|
||||
(* In order to generate fresh names, we need to define a function that
|
||||
generates names based on the ones it can already see in the term.
|
||||
This is problematic to do in a normal fixpoint, because we need the
|
||||
@@ -319,6 +337,11 @@ Module Chap11.
|
||||
| term_variant_case t0 cases =>
|
||||
term_variant_case (f t0) (map (fun '(l, x, t) => (l, x, f t)) cases)
|
||||
| term_fix t1 => term_fix (f t1)
|
||||
| term_nil T => term_nil T
|
||||
| term_cons T t1 t2 => term_cons T (f t1) (f t2)
|
||||
| term_is_nil T t1 => term_is_nil T (f t1)
|
||||
| term_head T t1 => term_head T (f t1)
|
||||
| term_tail T t1 => term_tail T (f t1)
|
||||
end.
|
||||
|
||||
Inductive matching : term -> term -> term -> Prop :=
|
||||
@@ -400,17 +423,14 @@ Module Chap11.
|
||||
step (term_tuple_proj t1 n) (term_tuple_proj t1' n)
|
||||
| E_Tuple : forall (t : list term) (tj tj' : term) (j : nat),
|
||||
(* j is bounded by the length of the tuple *)
|
||||
0 <= j < length t ->
|
||||
j < length t ->
|
||||
(* All terms before j are values *)
|
||||
(forall i,
|
||||
1 <= i < j ->
|
||||
i < length t ->
|
||||
is_value (nth i t term_unit)) ->
|
||||
Forall is_value (firstn j t) ->
|
||||
(* j-th element is an evaluatable term *)
|
||||
tj = nth j t term_unit ->
|
||||
step tj tj' ->
|
||||
(* t' is the tuple with the j-th element replaced by tj' *)
|
||||
let t' := List.app (firstn j t) (nth j t term_unit :: (skipn (S j) t)) in
|
||||
let t' := List.app (firstn j t) (tj' :: (skipn (S j) t)) in
|
||||
step (term_tuple t) (term_tuple t')
|
||||
|
||||
| E_ProjRcd : forall (k : record_label) (v : term) (m : list (record_label * term)),
|
||||
@@ -422,12 +442,9 @@ Module Chap11.
|
||||
step (term_record_proj t1 k) (term_record_proj t1' k)
|
||||
| E_Rcd : forall (r : list (string * term)) (tj tj' : term) (j : nat),
|
||||
(* j is bounded by the length of the record *)
|
||||
1 <= j <= length r ->
|
||||
j < length r ->
|
||||
(* All terms before j are values *)
|
||||
(forall i,
|
||||
1 <= i < j ->
|
||||
i < length r ->
|
||||
is_value (snd (nth i r ("", term_unit)))) ->
|
||||
Forall is_value (firstn j (map snd r)) ->
|
||||
(* j-th element is an evaluatable term *)
|
||||
tj = snd (nth j r ("", term_unit)) ->
|
||||
step tj tj' ->
|
||||
@@ -478,7 +495,38 @@ Module Chap11.
|
||||
step (term_fix (term_abs x T1 t2)) (substitute x (term_fix (term_abs x T1 t2)) t2)
|
||||
| E_Fix : forall (t t' : term),
|
||||
step t t' ->
|
||||
step (term_fix t) (term_fix t').
|
||||
step (term_fix t) (term_fix t')
|
||||
|
||||
| E_Cons1 : forall (T : type) (t1 t1' t2 : term),
|
||||
step t1 t1' ->
|
||||
step (term_cons T t1 t2) (term_cons T t1' t2)
|
||||
| E_Cons2 : forall (T : type) (v1 t2 t2' : term),
|
||||
is_value v1 ->
|
||||
step t2 t2' ->
|
||||
step (term_cons T v1 t2) (term_cons T v1 t2')
|
||||
| E_IsNilNil : forall (T : type),
|
||||
step (term_is_nil T (term_nil T)) term_true
|
||||
| E_IsNilCons : forall (T : type) (v1 v2 : term),
|
||||
is_value v1 ->
|
||||
is_value v2 ->
|
||||
step (term_is_nil T (term_cons T v1 v2)) term_false
|
||||
| E_IsNil : forall (T : type) (t t' : term),
|
||||
step t t' ->
|
||||
step (term_is_nil T t) (term_is_nil T t')
|
||||
| E_HeadCons : forall (T : type) (v1 v2 : term),
|
||||
is_value v1 ->
|
||||
is_value v2 ->
|
||||
step (term_head T (term_cons T v1 v2)) v1
|
||||
| E_Head : forall (T : type) (t t' : term),
|
||||
step t t' ->
|
||||
step (term_head T t) (term_head T t')
|
||||
| E_TailCons : forall (T : type) (v1 v2 : term),
|
||||
is_value v1 ->
|
||||
is_value v2 ->
|
||||
step (term_tail T (term_cons T v1 v2)) v2
|
||||
| E_Tail : forall (T : type) (t t' : term),
|
||||
step t t' ->
|
||||
step (term_tail T t) (term_tail T t').
|
||||
|
||||
Inductive has_type : context -> term -> type -> Prop :=
|
||||
| T_Var : forall (Γ : context) (x : string) (T1 : type),
|
||||
@@ -534,7 +582,7 @@ Module Chap11.
|
||||
has_type Γ (term_snd t) T2
|
||||
|
||||
| T_Tuple : forall (Γ : context) (ts : list term) (Ts : list type),
|
||||
(forall t T, In (t, T) (combine ts Ts) -> has_type Γ t T) ->
|
||||
Forall2 (has_type Γ) ts Ts ->
|
||||
has_type Γ (term_tuple ts) (type_Tuple Ts)
|
||||
| T_TupleProj : forall (Γ : context) (t : term) (Ts : list type) (n : nat) (T : type),
|
||||
has_type Γ t (type_Tuple Ts) ->
|
||||
@@ -543,9 +591,7 @@ Module Chap11.
|
||||
has_type Γ (term_tuple_proj t n) T
|
||||
|
||||
| T_Rcd : forall (Γ : context) (m : list (record_label * term)) (Ts : list type),
|
||||
(forall (k : record_label) (v : term) (T : type),
|
||||
In (k, T) (combine (map fst m) Ts) ->
|
||||
has_type Γ v T) ->
|
||||
Forall2 (has_type Γ) (map snd m) Ts ->
|
||||
has_type Γ (term_record m) (type_Record (combine (map fst m) Ts))
|
||||
| T_RcdProj : forall (Γ : context) (t : term) (m : list (record_label * type)) (k : record_label) (T : type),
|
||||
has_type Γ t (type_Record m) ->
|
||||
@@ -582,31 +628,289 @@ Module Chap11.
|
||||
|
||||
| T_Fix : forall (Γ : context) (t1 : term) (T1 : type),
|
||||
has_type Γ t1 (type_Arrow T1 T1) ->
|
||||
has_type Γ (term_fix t1) T1.
|
||||
has_type Γ (term_fix t1) T1
|
||||
|
||||
(* 11.3.2 *)
|
||||
(* Give typing and evaluation rules for wildcard abstractions, and
|
||||
prove that they can be derived from the abbreviation stated above. *)
|
||||
| T_Nil : forall (Γ : context) (T : type),
|
||||
has_type Γ (term_nil T) (type_List T)
|
||||
| T_Cons : forall (Γ : context) (t1 t2 : term) (T : type),
|
||||
has_type Γ t1 T ->
|
||||
has_type Γ t2 (type_List T) ->
|
||||
has_type Γ (term_cons T t1 t2) (type_List T)
|
||||
| T_IsNil : forall (Γ : context) (t : term) (T : type),
|
||||
has_type Γ t (type_List T) ->
|
||||
has_type Γ (term_is_nil T t) type_Bool
|
||||
| T_Head : forall (Γ : context) (t : term) (T : type),
|
||||
has_type Γ t (type_List T) ->
|
||||
has_type Γ (term_head T t) T
|
||||
| T_Tail : forall (Γ : context) (t : term) (T : type),
|
||||
has_type Γ t (type_List T) ->
|
||||
has_type Γ (term_tail T t) (type_List T).
|
||||
|
||||
(* Lemma substitution_noop : forall (Γ : context) (x : string) (v t : term) (T : type),
|
||||
(* NOTE: we have proved these in previous chapters, but they are getting cumbersome
|
||||
to prove with so much stuff around, so we will just assume them for now. *)
|
||||
|
||||
Lemma nth_skipn : forall (A : Type) (l : list A) (n : nat) (d : A),
|
||||
n < length l ->
|
||||
nth n l d :: skipn (S n) l = skipn n l.
|
||||
Proof.
|
||||
intros A l n d Hlen.
|
||||
revert n Hlen.
|
||||
induction l as [| h l IH]; intros n Hlen.
|
||||
- inversion Hlen.
|
||||
- destruct n.
|
||||
+ simpl. reflexivity.
|
||||
+ apply IH.
|
||||
rewrite length_cons in Hlen.
|
||||
rewrite <- Nat.succ_lt_mono in Hlen.
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
Lemma firstn_nth_skipn : forall (A : Type) (l : list A) (n : nat) (d : A),
|
||||
n < length l ->
|
||||
List.app (firstn n l) (nth n l d :: skipn (S n) l) = l.
|
||||
Proof.
|
||||
intros A l n d Hlen.
|
||||
rewrite nth_skipn with (d := d) (l := l) (n := n).
|
||||
- rewrite firstn_skipn with (l := l) (n := n).
|
||||
reflexivity.
|
||||
- assumption.
|
||||
Qed.
|
||||
|
||||
Lemma step_value_stuck : forall (t t' : term),
|
||||
is_value t ->
|
||||
step t t' ->
|
||||
t = t'.
|
||||
Proof.
|
||||
intros t t' Hval Hstep.
|
||||
induction Hstep.
|
||||
all: (
|
||||
try (inversion Hval; subst; auto);
|
||||
try (intuition eauto; subst; reflexivity)
|
||||
).
|
||||
- assert (In (nth j t term_unit) t) as tj_in_t. {
|
||||
apply nth_In.
|
||||
assumption.
|
||||
}
|
||||
pose proof (H3 (nth j t term_unit) tj_in_t) as Htj_val.
|
||||
specialize (IHHstep Htj_val). subst.
|
||||
assert (t = t') as Htuple_eq. {
|
||||
rewrite <- firstn_nth_skipn with (n := j) (l := t) (d := term_unit).
|
||||
- reflexivity.
|
||||
- assumption.
|
||||
}
|
||||
rewrite Htuple_eq.
|
||||
reflexivity.
|
||||
- assert (In (nth j r ("", term_unit)) r) as tj_in_r. {
|
||||
apply nth_In.
|
||||
assumption.
|
||||
}
|
||||
assert (is_value (snd (nth j r ("", term_unit)))) as Htj_val. {
|
||||
apply (H3 (fst (nth j r ("", term_unit))) (snd (nth j r ("", term_unit)))).
|
||||
rewrite <- surjective_pairing.
|
||||
assumption.
|
||||
}
|
||||
specialize (IHHstep Htj_val). subst.
|
||||
assert (r = r') as Hrcd_eq. {
|
||||
rewrite <- firstn_nth_skipn with (n := j) (l := r) (d := ("", term_unit)).
|
||||
- reflexivity.
|
||||
- assumption.
|
||||
}
|
||||
rewrite Hrcd_eq.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Lemma step_deterministic : forall (t t1 t2 : term),
|
||||
step t t1 -> step t t2 -> t1 = t2.
|
||||
Proof.
|
||||
intros t t1' t2' Hstep.
|
||||
generalize dependent t2'.
|
||||
(* induction on the derivation of (t -> t1') *)
|
||||
induction Hstep.
|
||||
all: (
|
||||
intros t2'' Hstep2;
|
||||
try (inversion Hstep2; subst; apply IHHstep in H2; subst; reflexivity);
|
||||
try (inversion Hstep2; subst; apply IHHstep in H3; subst; reflexivity)
|
||||
).
|
||||
Admitted.
|
||||
|
||||
Lemma uniqueness_of_types : forall (Γ : context) (t : term) (T1 T2 : type),
|
||||
has_type Γ t T1 -> has_type Γ t T2 -> T1 = T2.
|
||||
Proof. Admitted.
|
||||
|
||||
Lemma canonical_forms_bool : forall (Γ : context) (t : term) (T : type),
|
||||
is_value t ->
|
||||
has_type Γ t type_Bool ->
|
||||
t = term_true \/ t = term_false.
|
||||
Proof.
|
||||
intros Γ t T Hval Htyp.
|
||||
inversion Htyp; subst; try (inversion Hval; subst; auto).
|
||||
Qed.
|
||||
|
||||
Lemma canonical_forms_unit : forall (Γ : context) (t : term) (T : type),
|
||||
is_value t ->
|
||||
has_type Γ t type_Unit ->
|
||||
t = term_unit.
|
||||
Proof.
|
||||
intros Γ t T Hval Htyp.
|
||||
inversion Htyp; subst; try (inversion Hval; subst; auto).
|
||||
Qed.
|
||||
|
||||
Lemma canonical_forms_arrow : forall (Γ : context) (t : term) (T1 T2 : type),
|
||||
is_value t ->
|
||||
has_type Γ t (type_Arrow T1 T2) ->
|
||||
exists x t1, t = term_abs x T1 t1.
|
||||
Proof.
|
||||
intros Γ t T1 T2 Hval Htyp.
|
||||
inversion Htyp; subst; try (inversion Hval; subst; auto).
|
||||
- exists x, t1.
|
||||
reflexivity.
|
||||
- exists "_", t0.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Lemma canonical_forms_product : forall (Γ : context) (t : term) (T1 T2 : type),
|
||||
is_value t ->
|
||||
has_type Γ t (type_Product T1 T2) ->
|
||||
exists v1 v2, t = term_pair v1 v2 /\ is_value v1 /\ is_value v2.
|
||||
Proof.
|
||||
intros Γ t T1 T2 Hval Htyp.
|
||||
inversion Htyp; subst; try (inversion Hval; subst; auto).
|
||||
exists t1, t2.
|
||||
split; [reflexivity | split; assumption].
|
||||
Qed.
|
||||
|
||||
Lemma canonical_forms_sum : forall (Γ : context) (t : term) (T1 T2 : type),
|
||||
is_value t ->
|
||||
has_type Γ t (type_Sum T1 T2) ->
|
||||
(exists v, t = term_inl v (type_Sum T1 T2) /\ is_value v) \/
|
||||
(exists v, t = term_inr v (type_Sum T1 T2) /\ is_value v).
|
||||
Proof.
|
||||
intros Γ t T1 T2 Hval Htyp.
|
||||
inversion Htyp; subst; try (inversion Hval; subst; auto).
|
||||
- left. exists t0. split; [reflexivity | assumption].
|
||||
- right. exists t0. split; [reflexivity | assumption].
|
||||
Qed.
|
||||
|
||||
Lemma canonical_forms_variant : forall (Γ : context) (t : term) (c : list (record_label * type)),
|
||||
is_value t ->
|
||||
has_type Γ t (type_Variant c) ->
|
||||
exists (l : record_label) (v : term) (T : type),
|
||||
In (l, T) c /\
|
||||
t = term_variant l v (type_Variant c) /\
|
||||
is_value v.
|
||||
Proof.
|
||||
intros Γ t c Hval Htyp.
|
||||
inversion Htyp; subst; try (inversion Hval; subst; auto).
|
||||
exists l, tj, Tj.
|
||||
split; [assumption | split; [reflexivity | assumption]].
|
||||
Qed.
|
||||
|
||||
Lemma canonical_forms_tuple : forall (Γ : context) (t : term) (Ts : list type),
|
||||
is_value t ->
|
||||
has_type Γ t (type_Tuple Ts) ->
|
||||
exists vs, t = term_tuple vs /\ length vs = length Ts /\ (forall v, In v vs -> is_value v).
|
||||
Proof.
|
||||
intros Γ t Ts Hval Htyp.
|
||||
inversion Htyp; subst; try (inversion Hval; subst; auto).
|
||||
exists ts.
|
||||
split.
|
||||
reflexivity.
|
||||
split.
|
||||
- apply Forall2_length in H2.
|
||||
assumption.
|
||||
- assumption.
|
||||
Qed.
|
||||
|
||||
Lemma canonical_forms_record : forall (Γ : context) (t : term) (m : list (record_label * type)),
|
||||
is_value t ->
|
||||
has_type Γ t (type_Record m) ->
|
||||
exists vs, t = term_record vs /\ length vs = length m /\ (forall k v, In (k, v) vs -> is_value v).
|
||||
Proof.
|
||||
intros Γ t m Hval Htyp.
|
||||
inversion Htyp; subst; try (inversion Hval; subst; auto).
|
||||
exists m0.
|
||||
split.
|
||||
reflexivity.
|
||||
split.
|
||||
- apply Forall2_length in H2.
|
||||
rewrite length_combine.
|
||||
rewrite length_map.
|
||||
rewrite <- H2.
|
||||
rewrite length_map.
|
||||
rewrite Nat.min_id.
|
||||
reflexivity.
|
||||
- assumption.
|
||||
Qed.
|
||||
|
||||
Lemma canonical_forms_list : forall (Γ : context) (t : term) (T : type),
|
||||
is_value t ->
|
||||
has_type Γ t (type_List T) ->
|
||||
(t = term_nil T) \/ (exists v1 v2, t = term_cons T v1 v2 /\ is_value v1 /\ is_value v2).
|
||||
Proof.
|
||||
intros Γ t T Hval Htyp.
|
||||
inversion Htyp; subst; try (inversion Hval; subst; auto).
|
||||
right.
|
||||
exists t1, t2.
|
||||
split; [reflexivity | split; assumption].
|
||||
Qed.
|
||||
|
||||
Lemma progress : forall (Γ : context) (t : term) (T : type),
|
||||
has_type Γ t T ->
|
||||
is_value t \/ exists t', step t t'.
|
||||
Proof. Admitted.
|
||||
|
||||
Lemma preservation : forall (Γ : context) (t t' : term) (T : type),
|
||||
has_type Γ t T ->
|
||||
step t t' ->
|
||||
has_type Γ t' T.
|
||||
Proof. Admitted.
|
||||
|
||||
Lemma subst_noop_ih : forall (x : string) (v t t' : term),
|
||||
(~ is_free_variable x t -> substitute x v t = t) ->
|
||||
~ is_free_variable x t' ->
|
||||
(is_free_variable x t -> is_free_variable x t') ->
|
||||
substitute x v t = t.
|
||||
Proof.
|
||||
intros x v t t' IH Hfv Cons.
|
||||
apply IH.
|
||||
intros Hfv'.
|
||||
apply Hfv.
|
||||
apply Cons.
|
||||
exact Hfv'.
|
||||
Qed.
|
||||
|
||||
Lemma substitution_noop : forall (Γ : context) (x : string) (v t : term) (T : type),
|
||||
~ is_free_variable x t ->
|
||||
substitute x v t = t.
|
||||
Proof.
|
||||
intros Γ x v t T Hfv.
|
||||
induction t; simpl in *; try reflexivity.
|
||||
- destruct (String.eqb_spec x s) as [Heq | Hneq].
|
||||
induction t.
|
||||
all: (
|
||||
(* Takes care of values *)
|
||||
try (simpl; reflexivity)
|
||||
).
|
||||
|
||||
(* term_var *)
|
||||
- destruct (String.eqb_spec x v0) as [Heq | Hneq].
|
||||
+ subst.
|
||||
exfalso.
|
||||
apply Hfv.
|
||||
apply FV_Var.
|
||||
+ reflexivity.
|
||||
- assert (substitute x v t1 = t1) as Hsub1.
|
||||
{ apply IHt1. intros Hfv'. apply Hfv. apply FV_App1. exact Hfv'. }
|
||||
assert (substitute x v t2 = t2) as Hsub2.
|
||||
{ apply IHt2. intros Hfv'. apply Hfv. apply FV_App2. exact Hfv'. }
|
||||
rewrite Hsub1, Hsub2.
|
||||
reflexivity.
|
||||
- destruct (String.eqb_spec x s) as [Heq | Hneq].
|
||||
constructor.
|
||||
+ unfold substitute.
|
||||
apply String.eqb_neq in Hneq.
|
||||
rewrite Hneq.
|
||||
reflexivity.
|
||||
|
||||
(* term_app *)
|
||||
- pose proof (subst_noop_ih _ _ _ _ IHt1 Hfv (FV_App1 _ _ _)) as Hsub1.
|
||||
pose proof (subst_noop_ih _ _ _ _ IHt2 Hfv (FV_App2 _ _ _)) as Hsub2.
|
||||
rewrite <- Hsub1 at 2.
|
||||
rewrite <- Hsub2 at 2.
|
||||
constructor.
|
||||
|
||||
(* term_abs *)
|
||||
- simpl.
|
||||
destruct (String.eqb_spec x v0) as [Heq | Hneq].
|
||||
+ subst.
|
||||
reflexivity.
|
||||
+ assert (substitute x v t0 = t0) as Hsub.
|
||||
@@ -621,43 +925,62 @@ Module Chap11.
|
||||
}
|
||||
rewrite Hsub.
|
||||
reflexivity.
|
||||
- assert (substitute x v t1 = t1) as Hsub1.
|
||||
{ apply IHt1. intros Hfv'. apply Hfv. apply FV_If1. exact Hfv'. }
|
||||
assert (substitute x v t2 = t2) as Hsub2.
|
||||
{ apply IHt2. intros Hfv'. apply Hfv. apply FV_If2. exact Hfv'. }
|
||||
assert (substitute x v t3 = t3) as Hsub3.
|
||||
{ apply IHt3. intros Hfv'. apply Hfv. apply FV_If3. exact Hfv'. }
|
||||
|
||||
(* term_if *)
|
||||
- simpl.
|
||||
pose proof (subst_noop_ih _ _ _ _ IHt1 Hfv (FV_If1 _ _ _ _)) as Hsub1.
|
||||
pose proof (subst_noop_ih _ _ _ _ IHt2 Hfv (FV_If2 _ _ _ _)) as Hsub2.
|
||||
pose proof (subst_noop_ih _ _ _ _ IHt3 Hfv (FV_If3 _ _ _ _)) as Hsub3.
|
||||
rewrite Hsub1, Hsub2, Hsub3.
|
||||
reflexivity.
|
||||
- assert (substitute x v t = t) as Hsub.
|
||||
{ apply IHt. intros Hfv'. apply Hfv. apply FV_Ascribe. exact Hfv'. }
|
||||
rewrite Hsub.
|
||||
|
||||
(* term_ascribe *)
|
||||
- pose proof (subst_noop_ih _ _ _ _ IHt Hfv (FV_Ascribe _ _ _)) as Hsub.
|
||||
rewrite <- Hsub at 2.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* term_let *)
|
||||
- destruct (String.eqb_spec x v0) as [Heq | Hneq].
|
||||
Admitted.
|
||||
|
||||
Lemma substitution_preserves_typing : forall (Γ : context) (x : string) (v t : term) (T1 T2 : type),
|
||||
has_type (M.add x T2 Γ) t T1 ->
|
||||
has_type Γ v T2 ->
|
||||
has_type Γ (substitute x v t) T1.
|
||||
Proof.
|
||||
intros Γ x v t T1 T2 Ht Hv.
|
||||
generalize dependent Γ.
|
||||
generalize dependent T1.
|
||||
induction t; intros T1 Γ Ht; simpl in *; inversion Ht; subst; try (econstructor; eauto). *)
|
||||
Proof. Admitted.
|
||||
|
||||
Definition wildcard (t : term) (T : type) : term :=
|
||||
term_app (term_abs "_" T t) (term_unit).
|
||||
(* Lemma step_fv_app_abs : forall (Γ : context) (x : string) (v t : term) (T : type),
|
||||
is_value v ->
|
||||
~ is_free_variable x t ->
|
||||
step (term_app (term_abs x T t) v) v.
|
||||
Proof.
|
||||
intros Γ x v t T Hval Hfv.
|
||||
assert (substitute x v t = v) as Hsub.
|
||||
{
|
||||
apply substitution_noop.
|
||||
assumption.
|
||||
assumption.
|
||||
exact Hfv.
|
||||
}
|
||||
apply E_AppAbs.
|
||||
rewrite <- Hsub at 2. *)
|
||||
|
||||
(* 11.3.2 *)
|
||||
(* Give typing and evaluation rules for wildcard abstractions, and
|
||||
prove that they can be derived from the abbreviation stated above. *)
|
||||
|
||||
Definition term_wildcard (t : term) (T : type) : term :=
|
||||
term_abs "_" T t.
|
||||
|
||||
Lemma wildcard_typing : forall Γ t T,
|
||||
has_type Γ (wildcard t T) (type_Arrow T type_Unit).
|
||||
Proof.
|
||||
Admitted.
|
||||
has_type Γ (term_wildcard t T) (type_Arrow T T).
|
||||
Proof. Admitted.
|
||||
|
||||
Lemma wildcard_evaluation : forall t T,
|
||||
step (wildcard t T) t.
|
||||
step (term_wildcard t T) t.
|
||||
Proof.
|
||||
intros t T.
|
||||
unfold wildcard.
|
||||
unfold term_wildcard.
|
||||
Admitted.
|
||||
|
||||
(* 11.4.1 (1) *)
|
||||
@@ -682,6 +1005,6 @@ Module Chap11.
|
||||
apply T_Var.
|
||||
apply MFacts.add_eq_o.
|
||||
reflexivity.
|
||||
+ exact H.
|
||||
+ exact H.
|
||||
Qed.
|
||||
End Chap11.
|
||||
Reference in New Issue
Block a user