From c72976d072e1eb4fc6022f30b768bf7601c06308 Mon Sep 17 00:00:00 2001
From: h7x4 <h7x4@nani.wtf>
Date: Mon, 6 Jul 2026 18:00:24 +0900
Subject: [PATCH] chap11: progress

---
 src/chap11.v | 441 ++++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 382 insertions(+), 59 deletions(-)

diff --git a/src/chap11.v b/src/chap11.v
index 4982e4e..eae7928 100644
--- a/src/chap11.v
+++ b/src/chap11.v
@@ -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.
\ No newline at end of file