From 354c7643f4064ce1b671c2b7c09096e8eade75b8 Mon Sep 17 00:00:00 2001
From: h7x4 <h7x4@nani.wtf>
Date: Tue, 30 Jun 2026 23:00:01 +0900
Subject: [PATCH] chap11: init

---
 src/chap11.v | 481 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 481 insertions(+)
 create mode 100644 src/chap11.v

diff --git a/src/chap11.v b/src/chap11.v
new file mode 100644
index 0000000..54e3c30
--- /dev/null
+++ b/src/chap11.v
@@ -0,0 +1,481 @@
+From Stdlib Require Import
+  Strings.String
+  Lists.List
+  Lists.ListSet
+  FSets.FMapInterface
+  FSets.FMapList
+  FSets.FMapFacts
+  Structures.OrderedTypeEx
+  Nat
+  Arith
+  Lia.
+Import ListNotations.
+Require Import Recdef.
+
+Open Scope string_scope.
+
+Module Chap11.
+  (*
+    NOTE: a lot of the definitions of stlc done here were
+          taken from https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html
+          and adapted to fit the contents from the book.
+  *)
+
+  Definition varname := string.
+
+  Inductive type : Type :=
+    | type_Arrow : type -> type -> type
+    | type_Base : string -> type
+    | type_Product : type -> type -> type
+    | type_Tuple : list type -> type.
+
+
+  Definition type_Bool := type_Base "Bool".
+  Definition type_Unit := type_Base "Unit".
+
+  Inductive term : Type :=
+    | term_var : varname -> term
+    | term_app : term -> term -> term
+    | term_abs : varname -> type -> term -> term
+    | term_true : term
+    | term_false : term
+    | term_if : term -> term -> term -> term
+    | term_unit : term
+    | term_ascribe : term -> type -> term
+    | term_let : varname -> term -> term -> term
+    | term_pair : term -> term -> term
+    | term_fst : term -> term
+    | term_snd : term -> term
+    | term_tuple : list term -> term
+    | term_tuple_proj : term -> nat -> 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.
+
+  Module M := FMapList.Make(String_as_OT).
+  Module MFacts := FMapFacts.WFacts_fun String_as_OT M.
+  Definition context := M.t type.
+  Definition empty_ctx : context := @M.empty type.
+
+  Inductive value : term -> Prop :=
+    | v_abs : forall (x : string) (T2 : type) (t1 : term),
+        value (term_abs x T2 t1)
+    | v_true :
+        value term_true
+    | v_false :
+        value term_false
+    | v_unit :
+        value term_unit
+    | v_pair : forall (v1 v2 : term),
+        value v1 ->
+        value v2 ->
+        value (term_pair v1 v2)
+    | v_tuple : forall (vs : list term),
+        (forall v, In v vs -> value v) ->
+        value (term_tuple vs).
+
+  (* 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 :=
+    | FV_Var : forall x,
+        is_free_variable x (term_var x)
+
+    | FV_App1 : forall x t1 t2,
+        is_free_variable x t1 ->
+        is_free_variable x (term_app t1 t2)
+    | FV_App2 : forall x t1 t2,
+        is_free_variable x t2 ->
+        is_free_variable x (term_app t1 t2)
+
+    | FV_Abs : forall x y T1 t1,
+        y <> x ->
+        is_free_variable x t1 ->
+        is_free_variable x (term_abs y T1 t1)
+
+    | FV_If1 : forall x t1 t2 t3,
+        is_free_variable x t1 ->
+        is_free_variable x (term_if t1 t2 t3)
+    | FV_If2 : forall x t1 t2 t3,
+        is_free_variable x t2 ->
+        is_free_variable x (term_if t1 t2 t3)
+    | FV_If3 : forall x t1 t2 t3,
+        is_free_variable x t3 ->
+        is_free_variable x (term_if t1 t2 t3)
+
+    | FV_Ascribe : forall x T1 t1,
+        is_free_variable x t1 ->
+        is_free_variable x (term_ascribe t1 T1)
+
+    | FV_Let : forall x y t1 t2,
+        y <> x ->
+        is_free_variable x t1 ->
+        is_free_variable x (term_let y t1 t2)
+    | FV_Let2 : forall x y t1 t2,
+        y <> x ->
+        is_free_variable x t2 ->
+        is_free_variable x (term_let y t1 t2)
+
+    | FV_Pair1 : forall x t1 t2,
+        is_free_variable x t1 ->
+        is_free_variable x (term_pair t1 t2)
+    | FV_Pair2 : forall x t1 t2,
+        is_free_variable x t2 ->
+        is_free_variable x (term_pair t1 t2)
+
+    | FV_Fst : forall x t1,
+        is_free_variable x t1 ->
+        is_free_variable x (term_fst t1)
+    | FV_Snd : forall x t1,
+        is_free_variable x t1 ->
+        is_free_variable x (term_snd t1)
+
+    | FV_Tuple : forall x ts,
+        (forall t, In t ts -> is_free_variable x t) ->
+        is_free_variable x (term_tuple ts)
+    | FV_TupleProj : forall x t n,
+        is_free_variable x t ->
+        is_free_variable x (term_tuple_proj t n).
+
+
+  (* 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'
+    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.
+
+  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 :=
+    match t with
+    | term_var y =>
+        if String.eqb x y
+          then s
+          else t
+    | term_abs y T t1 =>
+        if String.eqb x y
+          then t
+          else term_abs y T (substitute x s t1)
+    | term_app t1 t2 =>
+        term_app (substitute x s t1) (substitute x s t2)
+    | term_true =>
+        term_true
+    | term_false =>
+        term_false
+    | term_unit =>
+        term_unit
+    | term_if t1 t2 t3 =>
+        term_if (substitute x s t1) (substitute x s t2) (substitute x s t3)
+    | term_ascribe t1 T =>
+        term_ascribe (substitute x s t1) T
+    | term_let y t1 t2 =>
+        if String.eqb x y
+          then term_let y (substitute x s t1) t2
+          else term_let y (substitute x s t1) (substitute x s t2)
+    | term_pair t1 t2 =>
+        term_pair (substitute x s t1) (substitute x s t2)
+    | term_fst t1 =>
+        term_fst (substitute x s t1)
+    | term_snd t1 =>
+        term_snd (substitute x s t1)
+    | term_tuple ts =>
+        term_tuple (map (substitute x s) ts)
+    | term_tuple_proj t n =>
+        term_tuple_proj (substitute x s t) n
+    end.
+
+  Inductive step : term -> term -> Prop :=
+    | E_App1 : forall t1 t1' t2,
+          step t1 t1' ->
+          step (term_app t1 t2) (term_app t1' t2)
+    | E_App2 : forall v1 t2 t2',
+          value v1 ->
+          step t2 t2' ->
+          step (term_app v1 t2) (term_app v1 t2')
+
+    | E_AppAbs : forall x T t v,
+          value v ->
+          step (term_app (term_abs x T t) v) (substitute x v t)
+
+    | E_Wildcard : forall t1 t2,
+          step (term_app (term_abs "_" type_Unit t1) t2) t1
+
+    | E_IfTrue : forall t1 t2,
+        step (term_if term_true t1 t2) t1
+    | E_IfFalse : forall t1 t2,
+        step (term_if term_false t1 t2) t2
+    | E_If : forall t1 t1' t2 t3,
+        step t1 t1' ->
+        step (term_if t1 t2 t3) (term_if t1' t2 t3)
+
+    | E_Ascribe : forall v T,
+        value v ->
+        step (term_ascribe v T) v
+    | E_Ascribe1 : forall t t' T,
+        step t t' ->
+        step (term_ascribe t T) (term_ascribe t' T)
+
+    | E_LetV : forall x v t2,
+        value v ->
+        step (term_let x v t2) (substitute x v t2)
+    | E_Let : forall x t1 t1' t2,
+        step t1 t1' ->
+        step (term_let x t1 t2) (term_let x t1' t2)
+
+    | E_PairBeta1 : forall v1 v2,
+        value v1 ->
+        value v2 ->
+        step (term_fst (term_pair v1 v2)) v1
+    | E_PairBeta2 : forall v1 v2,
+        value v1 ->
+        value v2 ->
+        step (term_snd (term_pair v1 v2)) v2
+    | E_Proj1 : forall t1 t1',
+        step t1 t1' ->
+        step (term_fst t1) (term_fst t1')
+    | E_Proj2 : forall t1 t1',
+        step t1 t1' ->
+        step (term_snd t1) (term_snd t1')
+    | E_Pair1 : forall t1 t1' t2,
+        step t1 t1' ->
+        step (term_pair t1 t2) (term_pair t1' t2)
+    | E_Pair2 : forall v1 t2 t2',
+        value v1 ->
+        step t2 t2' ->
+        step (term_pair v1 t2) (term_pair v1 t2')
+
+    | E_ProjTuple :
+        forall vs n,
+          (forall v, In v vs -> value v) ->
+          n < length vs ->
+          step (term_tuple_proj (term_tuple vs) n) (nth n vs term_unit)
+    | E_Proj : forall t1 t1' n,
+        step t1 t1' ->
+        step (term_tuple_proj t1 n) (term_tuple_proj t1' n)
+    | E_Tuple : forall ts ts' n,
+        (forall i, i < n -> i < length ts -> value (nth i ts term_unit)) ->
+        (step (nth n ts term_unit) (nth n ts' term_unit)) ->
+        ts' = List.app (firstn n ts) ((nth n ts' term_unit) :: (skipn (S n) ts)) ->
+        step (term_tuple ts) (term_tuple ts').
+
+  Inductive has_type : context -> term -> type -> Prop :=
+    | T_Var : forall (Γ : context) (x : string) (T1 : type),
+        M.find x Γ = Some T1 ->
+        has_type Γ (term_var x) T1
+
+    | T_Abs : forall (Γ : context) (x : string) (T1 T2 : type) (t1 : term),
+        has_type (M.add x T1 Γ) t1 T2 ->
+        has_type Γ (term_abs x T1 t1) (type_Arrow T1 T2)
+
+    | T_App : forall (Γ : context) (t1 t2 : term) (T1 T2 : type),
+        has_type Γ t1 (type_Arrow T2 T1) ->
+        has_type Γ t2 T2 ->
+        has_type Γ (term_app t1 t2) T1
+
+    | T_True : forall Γ,
+        has_type Γ term_true type_Bool
+    | T_False : forall Γ,
+        has_type Γ term_false type_Bool
+
+    | T_If : forall t1 t2 t3 T1 Γ,
+        has_type Γ t1 type_Bool ->
+        has_type Γ t2 T1 ->
+        has_type Γ t3 T1 ->
+        has_type Γ (term_if t1 t2 t3) T1
+
+    | T_Unit : forall Γ,
+        has_type Γ term_unit type_Unit
+
+    | T_Wildcard : forall Γ t T,
+        has_type Γ t T ->
+        has_type Γ (term_abs "_" T t) (type_Arrow T type_Unit)
+
+    | T_Ascribe : forall Γ t T,
+        has_type Γ t T ->
+        has_type Γ (term_ascribe t T) T
+
+    | T_Let : forall Γ x t1 t2 T1 T2,
+        has_type Γ t1 T1 ->
+        has_type (M.add x T1 Γ) t2 T2 ->
+        has_type Γ (term_let x t1 t2) T2
+
+    | T_Pair : forall Γ t1 t2 T1 T2,
+        has_type Γ t1 T1 ->
+        has_type Γ t2 T2 ->
+        has_type Γ (term_pair t1 t2) (type_Product T1 T2)
+
+    | T_Proj1 : forall Γ t T1 T2,
+        has_type Γ t (type_Product T1 T2) ->
+        has_type Γ (term_fst t) T1
+    | T_Proj2 : forall Γ t T1 T2,
+        has_type Γ t (type_Product T1 T2) ->
+        has_type Γ (term_snd t) T2
+
+    | T_Tuple : forall Γ ts Ts,
+        (forall t T, In (t, T) (combine ts Ts) -> has_type Γ t T) ->
+        has_type Γ (term_tuple ts) (type_Tuple Ts)
+    | T_Proj : forall Γ t Ts n T,
+        has_type Γ t (type_Tuple Ts) ->
+        n < length Ts ->
+        nth_error Ts n = Some T ->
+        has_type Γ (term_tuple_proj t n) T.
+
+  (* 11.3.2 *)
+  (* Give typing and evaluation rules for wildcard abstractions, and
+     prove that they can be derived from the abbreviation stated above. *)
+
+  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].
+      + 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].
+      + subst.
+        reflexivity.
+      + assert (substitute x v t0 = t0) as Hsub.
+        {
+          apply IHt.
+          intros Hfv'.
+          apply Hfv.
+          apply FV_Abs.
+          - symmetry.
+            exact Hneq.
+          - exact Hfv'.
+        }
+        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'. }
+      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),
+      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).
+
+  Definition wildcard (t : term) (T : type) : term :=
+    term_app (term_abs "_" T t) (term_unit).
+
+  Lemma wildcard_typing : forall Γ t T,
+    has_type Γ (wildcard t T) (type_Arrow T type_Unit).
+  Proof.
+  Admitted.
+
+  Lemma wildcard_evaluation : forall t T,
+    step (wildcard t T) t.
+  Proof.
+    intros t T.
+    unfold wildcard.
+  Admitted.
+
+  (* 11.4.1 (1) *)
+  (* Show how to formulate ascription as a derived form.
+     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).
+
+  Lemma ascribe'_typing : forall Γ t T,
+    has_type Γ (ascribe' t T) T <-> has_type Γ t T.
+  Proof.
+    intros Γ t T.
+    split.
+    - intros H.
+      inversion H; subst.
+      inversion H3; subst.
+      exact H5.
+    - intros H.
+      apply T_App with (T2 := T).
+      + apply T_Abs.
+        apply T_Var.
+        apply MFacts.add_eq_o.
+        reflexivity.
+      + exact H.
+  Qed.
+End Chap11.
\ No newline at end of file