oysteikt/tapl-proofs
0
0
Fork 0
Code Issues Pull Requests Activity

chap11: progress

Browse Source
This commit is contained in:
Oystein Kristoffer Tveit
2026-07-06 18:00:24 +09:00
parent 8ef7eb87b3
commit 55adee0ba0
1 changed files with 529 additions and 157 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/chap11.v
+529 -157
View File
@@ -6,11 +6,12 @@ From Stdlib Require Import
FSets.FMapList
FSets.FMapFacts
Structures.OrderedTypeEx
Structures.OrderedType
Nat
Arith
Compare_dec
Lia.
Import ListNotations.
Require Import Recdef.
Open Scope string_scope.
@@ -21,14 +22,88 @@ Module Chap11.
and adapted to fit the contents from the book.
*)
Definition varname := string.
Inductive varname : Type :=
| varname_nat : nat -> varname
| varname_unused : varname.
Scheme Equality for varname.
Module Varname_as_OT <: OrderedType.
Definition t := varname.
Definition eq := @eq t.
Definition lt (x y : t) := match x, y with
| varname_nat n1, varname_nat n2 => n1 < n2
| varname_unused, varname_nat _ => True
| varname_nat _, varname_unused => False
| varname_unused, varname_unused => False
end.
Definition eq_refl := @eq_refl t.
Definition eq_sym := @eq_sym t.
Definition eq_trans := @eq_trans t.
Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Parameter compare : forall x y : t, Compare lt eq x y.
Parameter eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
End Varname_as_OT.
(* Module Varname_as_OT_Facts := OrderedTypeFacts Varname_as_OT. *)
Definition varname_eqb (x y : varname) : bool :=
match x, y with
| varname_nat n1, varname_nat n2 => Nat.eqb n1 n2
| varname_unused, varname_unused => true
| _, _ => false
end.
Lemma varname_eqb_spec s1 s2 : Bool.reflect (s1 = s2) (varname_eqb s1 s2).
Proof.
destruct s1, s2; simpl.
Admitted.
Lemma varname_eqb_neq : forall (x y : varname),
varname_eqb x y = false <-> ~ Varname_as_OT.eq x y.
Proof.
intros x y. split; intros H.
- destruct x, y; simpl in *; try discriminate; try congruence.
apply Nat.eqb_neq in H. congruence.
- destruct x, y; simpl in *; try reflexivity; try congruence.
apply Nat.eqb_neq. congruence.
Qed.
Fixpoint repeat_string (s : string) (n : nat) : string :=
match n with
| 0 => ""
| S n' => s ++ repeat_string s n'
end.
Definition varname_to_string (v : varname) : string :=
match v with
| varname_nat n => "x" ++ repeat_string "'" n
| varname_unused => "_"
end.
Fixpoint max_varname (s : set varname) : nat :=
match s with
| [] => 0
| varname_nat n :: s' => Nat.max n (max_varname s')
| varname_unused :: s' => max_varname s'
end.
Definition fresh_varname (s : set varname) : varname :=
varname_nat (S (max_varname s)).
Definition typename := string.
Definition record_label := string.
Inductive type : Type :=
(** T1 -> T2 *)
| type_Arrow : type -> type -> type
(** ArbitraryType *)
| type_Base : string -> type
| type_Base : typename -> type
(** T1 x T2 *)
| type_Product : type -> type -> type
(** {T1, T2, ..., Tn} *)
@@ -38,13 +113,15 @@ 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".
Module M := FMapList.Make(String_as_OT).
Module MFacts := FMapFacts.WFacts_fun String_as_OT M.
Module M := FMapList.Make(Varname_as_OT).
Module MFacts := FMapFacts.WFacts_fun Varname_as_OT M.
Definition context := M.t type.
Definition empty_ctx : context := @M.empty type.
@@ -101,19 +178,30 @@ 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
to simulate it *)
Definition term_seq (t1 t2 : term) : term :=
term_app (term_abs "_" type_Unit t2) t1.
term_app (term_abs varname_unused type_Unit t2) t1.
Definition term_letrec (x : string) (T1 : type) (t1 : term) (t2 : term) : term :=
Definition term_letrec (x : varname) (T1 : type) (t1 : term) (t2 : term) : term :=
term_let x (term_fix (term_abs x T1 t1)) t2.
Inductive is_value : term -> Prop :=
| v_abs : forall (x : string) (T2 : type) (t1 : term),
| v_abs : forall (x : varname) (T2 : type) (t1 : term),
is_value (term_abs x T2 t1)
| v_true :
is_value term_true
@@ -139,20 +227,25 @@ 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),
| p_var : forall (x : varname),
is_pattern (term_var x)
| p_pattern_bind : forall (t1 t2 t3 : term),
is_pattern t1 ->
is_pattern (term_pattern_bind t1 t2 t3).
(* Before we continue with evaluation and typing rules,
we need substitution. After chapter 6, it seems like tapl
assumes that our substitution function is capture-avoiding,
so this is a requirement *)
Inductive is_free_variable : string -> term -> Prop :=
(* This denotes whether a variable is free in a term.
That is, there is no closure in t that will eventually
replace the variable *)
Inductive is_free_variable : varname -> term -> Prop :=
| FV_Var : forall x,
is_free_variable x (term_var x)
@@ -220,78 +313,51 @@ 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
function to have a measure that is strictly decreasing.
In this implementation, we append primes to x until we find an emtpy
one. Our strictly decreasing measure is the max count of primes of any
'x' in the set of free variables.
*)
Fixpoint repeat_n (x : string) (n : nat) : string :=
match n with
| 0 => x
| S n' => x ++ repeat_n x n'
Fixpoint varnames (t : term) : (set varname) :=
match t with
| term_var y => [y]
| term_abs y T t1 => set_union varname_eq_dec [y] (varnames t1)
| term_app t1 t2 => set_union varname_eq_dec (varnames t1) (varnames t2)
| term_true => []
| term_false => []
| term_unit => []
| term_if t1 t2 t3 => set_union varname_eq_dec (varnames t1) (set_union varname_eq_dec (varnames t2) (varnames t3))
| term_ascribe t1 T => varnames t1
| term_let y t1 t2 => set_union varname_eq_dec [y] (set_union varname_eq_dec (varnames t1) (varnames t2))
| term_pair t1 t2 => set_union varname_eq_dec (varnames t1) (varnames t2)
| term_fst t1 => varnames t1
| term_snd t1 => varnames t1
| term_tuple ts => fold_left (fun acc t => set_union varname_eq_dec acc (varnames t)) ts []
| term_tuple_proj t n => varnames t
| term_record m => fold_left (fun acc kv => set_union varname_eq_dec acc (varnames (snd kv))) m []
| term_record_proj t k => varnames t
| term_pattern_bind p t1 t2 => set_union varname_eq_dec (varnames p) (set_union varname_eq_dec (varnames t1) (varnames t2))
| term_inl t1 T => varnames t1
| term_inr t1 T => varnames t1
| term_case t0 T x t1 y t2 => set_union varname_eq_dec (varnames t0) (set_union varname_eq_dec [x] (set_union varname_eq_dec (varnames t1) (set_union varname_eq_dec [y] (varnames t2))))
| term_variant l t1 T => varnames t1
| term_variant_case t0 cases => set_union varname_eq_dec (varnames t0) (fold_left (fun acc case => let '(l, x, t) := case in set_union varname_eq_dec acc (set_union varname_eq_dec [x] (varnames t))) cases [])
| term_fix t1 => varnames t1
| term_nil T => []
| term_cons T t1 t2 => set_union varname_eq_dec (varnames t1) (varnames t2)
| term_is_nil T t1 => varnames t1
| term_head T t1 => varnames t1
| term_tail T t1 => varnames t1
end.
Fixpoint max_key_len (xs : list (string * type)) : nat :=
match xs with
| [] => 0
| (k, _) :: xs' =>
Nat.max (String.length k) (max_key_len xs')
end.
Lemma fresh_varname_not_free : forall (t : term) (x : varname),
fresh_varname (varnames t) = x <-> ~ is_free_variable x t.
Proof. Admitted.
Definition decrement_key (k : string) : option string :=
match String.length k with
| 0 => None
| 1 => None
| S n => Some (String.substring 0 n k)
end.
(* Function fresh_var
(Γ : context)
{measure max_key_len (M.elements Γ)}
: string :=
if M.mem "x" Γ then
let
reduced_keys : context := M.remove "x" (filtermap (fun '(k, _) => decrement_key k) (M.elements Γ))
in
fresh_var reduced_keys
else
"x".
Proof. *)
(* Function fresh_varname
(x : string)
(s : set string)
{measure max_varname_size s}
: string :=
match s with
| [] => x
| y :: ys =>
if String.eqb x y
then fresh_varname (x ++ "'") (decrease_varname_sizes ys)
else fresh_varname x ys
end.
Proof.
intros x s y ys.
- unfold decrease_varname_sizes.
lia. *)
Fixpoint substitute (x : string) (s : term) (t : term) : term :=
Fixpoint substitute (x : varname) (s : term) (t : term) : term :=
let f := fun t => substitute x s t in
match t with
| term_var y =>
if String.eqb x y
| term_var y =>
if varname_eqb x y
then s
else t
| term_abs y T t1 =>
if String.eqb x y
| term_abs y T t1 =>
if varname_eqb x y
then t
else term_abs y T (f t1)
| term_app t1 t2 => term_app (f t1) (f t2)
@@ -301,7 +367,7 @@ Module Chap11.
| term_if t1 t2 t3 => term_if (f t1) (f t2) (f t3)
| term_ascribe t1 T => term_ascribe (f t1) T
| term_let y t1 t2 =>
if String.eqb x y
if varname_eqb x y
then term_let y (f t1) t2
else term_let y (f t1) (f t2)
| term_pair t1 t2 => term_pair (f t1) (f t2)
@@ -319,11 +385,16 @@ 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 :=
(** match(x, 5) -> [x -> 5] *)
| M_Var : forall (x : string) (v : term),
| M_Var : forall (x : varname) (v : term),
is_pattern (term_var x) ->
matching (term_var x) v (substitute x v (term_var x)).
(** match({x, y}, {5, true}) -> [x -> 5, y -> true]
@@ -339,12 +410,12 @@ Module Chap11.
step t2 t2' ->
step (term_app v1 t2) (term_app v1 t2')
| E_AppAbs : forall (x : string) (T : type) (t v : term),
| E_AppAbs : forall (x : varname) (T : type) (t v : term),
is_value v ->
step (term_app (term_abs x T t) v) (substitute x v t)
| E_Wildcard : forall (t1 t2 : term),
step (term_app (term_abs "_" type_Unit t1) t2) t1
step (term_app (term_abs varname_unused type_Unit t1) t2) t1
| E_IfTrue : forall (t1 t2 : term),
step (term_if term_true t1 t2) t1
@@ -361,10 +432,10 @@ Module Chap11.
step t t' ->
step (term_ascribe t T) (term_ascribe t' T)
| E_LetV : forall (x : string) (v t2 : term),
| E_LetV : forall (x : varname) (v t2 : term),
is_value v ->
step (term_let x v t2) (substitute x v t2)
| E_Let : forall (x : string) (t1 t1' t2 : term),
| E_Let : forall (x : varname) (t1 t1' t2 : term),
step t1 t1' ->
step (term_let x t1 t2) (term_let x t1' t2)
@@ -400,17 +471,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)),
@@ -420,14 +488,11 @@ Module Chap11.
| E_Proj' : forall (t1 t1' : term) (k : record_label),
step t1 t1' ->
step (term_record_proj t1 k) (term_record_proj t1' k)
| E_Rcd : forall (r : list (string * term)) (tj tj' : term) (j : nat),
| E_Rcd : forall (r : list (record_label * 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' ->
@@ -447,13 +512,13 @@ Module Chap11.
step t1 t1' ->
step (term_pattern_bind p t1 t2) (term_pattern_bind p t1' t2)
| E_CaseInl : forall (v t1 t2 : term) (T : type) (x y : string),
| E_CaseInl : forall (v t1 t2 : term) (T : type) (x y : varname),
is_value v ->
step (term_case (term_inl v T) T x t1 y t2) (substitute x v t1)
| E_CaseInr : forall (v t1 t2 : term) (T : type) (x y : string),
| E_CaseInr : forall (v t1 t2 : term) (T : type) (x y : varname),
is_value v ->
step (term_case (term_inr v T) T x t1 y t2) (substitute y v t2)
| E_Case : forall (t t' t1 t2 : term) (T : type) (x y : string),
| E_Case : forall (t t' t1 t2 : term) (T : type) (x y : varname),
step t t' ->
step (term_case t T x t1 y t2) (term_case t' T x t1 y t2)
| E_Inl : forall (t t' : term) (T : type),
@@ -463,7 +528,7 @@ Module Chap11.
step t t' ->
step (term_inr t T) (term_inr t' T)
| E_CaseVariant : forall (Γ : context) (lj xj : record_label) (vj tj : term) (T : type) (c : list (record_label * varname * term)),
| E_CaseVariant : forall (Γ : context) (lj : record_label) (xj : varname) (vj tj : term) (T : type) (c : list (record_label * varname * term)),
is_value vj ->
In (lj, xj, tj) c ->
step (term_variant_case (term_variant lj vj T) c) (substitute xj vj tj)
@@ -474,18 +539,49 @@ Module Chap11.
step t t' ->
step (term_variant l t T) (term_variant l t' T)
| E_FixBeta : forall (x : string) (T1 : type) (t2 : term),
| E_FixBeta : forall (x : varname) (T1 : type) (t2 : term),
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),
| T_Var : forall (Γ : context) (x : varname) (T1 : type),
M.find x Γ = Some T1 ->
has_type Γ (term_var x) T1
| T_Abs : forall (Γ : context) (x : string) (T1 T2 : type) (t1 : term),
| T_Abs : forall (Γ : context) (x : varname) (T1 T2 : type) (t1 : term),
has_type (M.add x T1 Γ) t1 T2 ->
has_type Γ (term_abs x T1 t1) (type_Arrow T1 T2)
@@ -510,13 +606,13 @@ Module Chap11.
| T_Wildcard : forall (Γ : context) (t : term) (T : type),
has_type Γ t T ->
has_type Γ (term_abs "_" T t) (type_Arrow T type_Unit)
has_type Γ (term_abs varname_unused T t) (type_Arrow T type_Unit)
| T_Ascribe : forall (Γ : context) (t : term) (T : type),
has_type Γ t T ->
has_type Γ (term_ascribe t T) T
| T_Let : forall (Γ : context) (x : string) (t1 t2 : term) (T1 T2 : type),
| T_Let : forall (Γ : context) (x : varname) (t1 t2 : term) (T1 T2 : type),
has_type Γ t1 T1 ->
has_type (M.add x T1 Γ) t2 T2 ->
has_type Γ (term_let x t1 t2) T2
@@ -534,7 +630,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 +639,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) ->
@@ -558,7 +652,7 @@ Module Chap11.
| T_Inr : forall (Γ : context) (t : term) (T1 T2 : type),
has_type Γ t T2 ->
has_type Γ (term_inr t (type_Sum T1 T2)) (type_Sum T1 T2)
| T_Case : forall (Γ : context) (t0 t1 t2 : term) (x1 x2 : string) (T1 T2 T : type),
| T_Case : forall (Γ : context) (t0 t1 t2 : term) (x1 x2 : varname) (T1 T2 T : type),
has_type Γ t0 (type_Sum T1 T2) ->
has_type (M.add x1 T1 Γ) t1 T ->
has_type (M.add x2 T2 Γ) t2 T ->
@@ -582,31 +676,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 varname_unused, 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 : varname) (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 : varname) (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 (varname_eq_dec 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 varname_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 (varname_eqb_spec x v0) as [Heq | Hneq].
+ subst.
reflexivity.
+ assert (substitute x v t0 = t0) as Hsub.
@@ -621,43 +973,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.
reflexivity.
Qed.
Lemma substitution_preserves_typing : forall (Γ : context) (x : string) (v t : term) (T1 T2 : type),
(* term_ascribe *)
- pose proof (subst_noop_ih _ _ _ _ IHt Hfv (FV_Ascribe _ _ _)) as Hsub.
rewrite <- Hsub at 2.
reflexivity.
(* term_let *)
- destruct (varname_eqb_spec x v0) as [Heq | Hneq].
Admitted.
Lemma substitution_preserves_typing : forall (Γ : context) (x : varname) (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 : varname) (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 varname_unused 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) *)
@@ -665,7 +1036,8 @@ Module Chap11.
Prove that the “official” typing and evaluation rules given here
correspond to your definition in a suitable sense. *)
Definition ascribe' (t : term) (T : type) : term :=
term_app (term_abs "x" T (term_var "x")) (t).
let x := fresh_varname (varnames t) in
term_app (term_abs x T (term_var x)) (t).
Lemma ascribe'_typing : forall Γ t T,
has_type Γ (ascribe' t T) T <-> has_type Γ t T.
@@ -682,6 +1054,6 @@ Module Chap11.
apply T_Var.
apply MFacts.add_eq_o.
reflexivity.
+ exact H.
+ exact H.
Qed.
End Chap11.