From 28c71cf03f52e02e25824c9ff5735db2fde5cb14 Mon Sep 17 00:00:00 2001
From: h7x4 <h7x4@nani.wtf>
Date: Thu, 25 Jun 2026 02:27:48 +0900
Subject: [PATCH] chap5: init

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

diff --git a/src/chap5.v b/src/chap5.v
new file mode 100644
index 0000000..68af317
--- /dev/null
+++ b/src/chap5.v
@@ -0,0 +1,390 @@
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import Coq.Lists.ListSet.
+Require Import Coq.Arith.PeanoNat.
+Import ListNotations.
+
+
+Module Chap5.
+  (* 5.1 *)
+  Inductive term : Type :=
+    | Var (name : string)
+    | Lambda (var : string) (body : term)
+    | App (t1 t2 : term).
+
+  Scheme Equality for term.
+
+  Fixpoint substitute (x : string) (s : term) (t : term) : term :=
+    match t with
+    | Var y => if String.eqb x y then s else t
+    | Lambda y body => if String.eqb x y then t else Lambda y (substitute x s body)
+    | App t1 t2 => App (substitute x s t1) (substitute x s t2)
+    end.
+
+  Definition is_value (t : term) : bool :=
+    match t with
+    | Lambda _ _ => true
+    | Var _ => true
+    | App (Var _) _ => true
+    | _ => false
+    end.
+
+  Fixpoint single_step_eval (t : term) : term :=
+    match t with
+    | App (Lambda x body) arg =>
+        if is_value arg
+        then substitute x arg body
+        else App (Lambda x body) (single_step_eval arg)
+
+    | App t1 t2 =>
+        let t1' := single_step_eval t1 in
+        if term_beq t1 t1'
+        then App t1 (single_step_eval t2)
+        else App t1' t2
+
+    | Lambda x body => Lambda x (single_step_eval body)
+
+    | _ => t
+  end.
+
+  Fixpoint multi_step_eval (t : term) (i : nat) : term :=
+    match i, (single_step_eval t) with
+    | O, t' => t'
+    | S i', t' => if (term_eq_dec t t') then t' else multi_step_eval t' i'
+    end.
+
+  Lemma unwrap_multi_step_eval : forall (t : term), forall (i : nat),
+    multi_step_eval t (S i) = multi_step_eval (single_step_eval t) i.
+  Proof.
+    intros t i. simpl. destruct (term_eq_dec t (single_step_eval t)) as [Heq | Hneq].
+    - rewrite <- Heq.
+  Admitted.
+
+
+  (* Notation *)
+  Declare Custom Entry ulc.
+  Notation "<{ t }>" := (t) (t custom ulc at level 99).
+
+  Notation "( x )" := x
+  (in custom ulc, x at level 99).
+
+  Notation "$ x" :=
+    x
+    (in custom ulc at level 0, x constr).
+
+  Notation "'λ' x , t" := (Lambda x t) (in custom ulc at level 90, x constr).
+
+  Notation "t1 . t2" := (App t1 t2) (in custom ulc at level 20, left associativity).
+
+  Notation "x" :=
+    (Var x%string)
+    (in custom ulc at level 0, x constr).
+
+
+  Example single_step_eval_application :
+    single_step_eval <{ (λ "x", "x") . "y" }> = <{ "y" }>.
+  Proof. reflexivity. Qed.
+
+  Example multi_step_eval_application :
+    multi_step_eval <{ (λ "x", "x") . (λ "x", "x") . "y" }> 2 = <{ "y" }>.
+  Proof. reflexivity. Qed.
+
+  (* Church Booleans *)
+  Definition tru : term := <{ (λ "t", (λ "f", "t")) }>.
+  Definition fls : term := <{ λ "t" , λ "f" , "f" }>.
+  Definition test : term := <{ λ "l" , λ "m" , λ "n" , "l" . "m" . "n" }>.
+
+  Example test_tru:
+    multi_step_eval <{ $test . $tru . "x" . "y" }> 100 = Var "x".
+  Proof. reflexivity. Qed.
+
+
+  Definition aand : term := <{ λ "b", λ "c", "b" . "c" . $fls }>.
+  (* 5.2.1 *)
+  Definition oor : term := <{ λ "b", λ "c", "b" . $tru . "c" }>.
+
+  (* Pairs *)
+  Definition ppair : term := <{ λ "f", λ "s", λ "b", "b" . "f" . "s" }>.
+  Definition fst : term := <{ λ "p", "p" . $tru }>.
+  Definition snd : term := <{ λ "p", "p" . $fls }>.
+
+  Example test_pair:
+    multi_step_eval <{ $fst . ($ppair . "v" . "w") }> 100 = Var "v".
+  Proof. reflexivity. Qed.
+
+  (* Church numerals *)
+  Definition zero : term := <{ λ "s", λ "z", "z" }>.
+
+  Fixpoint church_body (n : nat) : term :=
+    match n with
+    | O => Var "z"
+    | S n' => <{ "s" . $church_body n' }>
+    end.
+
+  Definition c (n : nat) : term :=
+    <{ λ "s", λ "z",  $church_body n }>.
+
+  Notation "# n" := (c n) (in custom ulc at level 0, n constr).
+
+  Fixpoint count_apps (s z : string) (t : term) : nat :=
+    match t with
+    | Var z' =>
+        if String.eqb z z' then 0 else 0
+    | App (Var s') t' =>
+        if String.eqb s s'
+        then S(count_apps s z t')
+        else 0
+    | _ => 0
+    end.
+
+  Definition c_to_nat (t : term) : nat :=
+    match t with
+    | Lambda s (Lambda z body) => count_apps s z body
+    | _ => 0
+    end.
+
+  Lemma c_to_nat_0 : c_to_nat zero = 0.
+  Proof. reflexivity. Qed.
+
+  Lemma c_to_nat_1 : c_to_nat (c 1) = 1.
+  Proof. simpl. reflexivity. Qed.
+
+  Lemma c_to_nat_unwrap : forall n,
+    c_to_nat <{ # S n }> = S (c_to_nat <{ # n }>).
+  Proof.
+    intros n. reflexivity.
+  Qed.
+
+  Lemma c_to_nat_correct : forall n, c_to_nat (c n) = n.
+  Proof.
+    intros n. induction n as [| n' IH].
+    - simpl. reflexivity.
+    - simpl. rewrite <- IH.
+  Admitted.
+
+  Definition scc : term := <{ λ "n", λ "s", λ "z", "s" . ("n" . "s" . "z") }>.
+
+  (* 5.2.2 *)
+  Definition scc_2 : term := <{ λ "n", λ "s", λ "z", "s" . ("n" . "s" . "z") }>.
+
+  (* Lemma scc1_matches_scc2 : forall (i : nat),
+    multi_step_eval <{ $scc . $c i }> 100 = multi_step_eval <{ $scc_2 . $c i }> 100.
+  Proof.
+    intros i. simpl. reflexivity.
+  Qed. *)
+
+  Definition plus : term :=
+    <{ λ "m", λ "n", λ "s", λ "z", "m" . "s" . ("n" . "s" . "z") }>.
+
+  Example test_plus:
+    multi_step_eval <{ $plus . # 2 . # 3 }> 100 = <{ # 5 }>.
+  Proof. reflexivity. Qed.
+
+  Definition times : term :=
+    <{ λ "m", λ "n", "m" . ($plus . "n") . "z" }>.
+
+  Example test_times:
+    multi_step_eval <{ $times . # 2 . # 3 }> 100 = <{ # 6 }>.
+  Proof.
+    simpl.
+  Admitted.
+
+  (* 5.2.3 *)
+  Definition times_2 : term :=
+    <{ λ "m", λ "n", λ "s", λ "z", "m" . ("n" . "s") . "z" }>.
+
+  (* 5.2.4 *)
+  Definition power : term :=
+    <{ λ "m", λ "n", "m" . ($times . "n") . ($c 1) }>.
+
+  Definition power2 : term :=
+    <{ λ "m", λ "n", "n" . "m" }>.
+
+  Definition iszro : term :=
+    <{ λ "m", "m" . (λ "x", $fls) . $tru }>.
+
+  Example is_zro_test_0:
+    multi_step_eval <{ $iszro . # 0 }> 100 = tru.
+  Proof. reflexivity. Qed.
+
+  Example is_zro_test_1:
+    multi_step_eval <{ $iszro . # 1 }> 100 = fls.
+  Proof. reflexivity. Qed.
+
+  Example is_zro_test_expr:
+    multi_step_eval <{ $iszro . ($times . # 0 . # 2) }> 100 = tru.
+  Proof.
+    simpl.
+  Admitted.
+
+  Definition zz : term := <{ $ppair . # 0 . # 0 }>.
+  Definition ss : term := <{ λ "p", $ppair . ($snd . "p") . ($scc . ($snd . "p")) }>.
+
+  (*
+    "Apply ss to zz m times, take the first value of the result"
+    (0,0) -> (0,1) -> (1,2) -> (2,3) -> ... -> (_m-1_,m)
+  *)
+  Definition prd : term := <{ λ "m", $fst . ("m" . $ss . $zz) }>.
+
+  (* 5.2.5 *)
+  Definition sub : term :=
+    <{ λ "m", λ "n", "n" . $prd . "m" }>.
+
+  (* Example sub_test_0:
+    multi_step_eval <{ $sub . # 5 . # 3 }> 100 = <{ # 2 }>.
+  Proof. simpl. reflexivity. Qed. *)
+
+  (* 5.2.6 *)
+  (* It takes roughly O(n) steps to calculate prd C(n) *)
+
+  (* 5.2.7 *)
+  Definition c_eq : term :=
+    <{ λ "m", λ "n", ($aand . ($iszro . ($sub . "m" . "n")) . ($iszro . ($sub . "n" . "m"))) }>.
+
+  (* Example c_eq_test_0:
+    multi_step_eval <{ $c_eq . # 0 . # 0 }> 100 = tru.
+  Proof. reflexivity. Qed.
+
+  Example c_eq_test_1:
+    multi_step_eval <{ $c_eq . # 0 . # 1 }> 100 = fls.
+  Proof. reflexivity. Qed. *)
+
+  (* 5.2.8 *)
+
+  Definition l_nil : term := <{ λ "c", λ "n", "n" }>.
+  Definition l_cons : term := <{ λ "h", λ "t", λ "c", λ "n", "c" . "h" . ("t" . "c" . "n") }>.
+  Definition l_isnil : term := <{ λ "l", "l" . (λ "h", λ "t", $fls) . $tru }>.
+  Definition l_head : term := <{ λ "l", "l" . (λ "h", λ "t", "h") . $l_nil }>.
+
+  Definition nn : term := <{ $ppair . $l_nil . $l_nil }>.
+  Definition cc : term := <{ λ "e", λ "p", $ppair . ($snd . "p") . ($l_cons . "e" . ($snd . "p")) }>.
+  Definition tail : term := <{ λ "l", $fst . ("l" . $cc . $nn) }>.
+
+  Definition omega : term := <{ (λ "x", "x" . "x") . (λ "x", "x" . "x") }>.
+
+  Lemma omega_idempotent : forall i, multi_step_eval omega i = omega.
+  Proof.
+    intros i. induction i as [| i' IH].
+    - simpl. reflexivity.
+    - rewrite unwrap_multi_step_eval. simpl. rewrite <- IH. reflexivity.
+  Qed.
+
+  Definition ffix : term := <{ λ "f", (λ "x", "f" . ("x" . "x")) . (λ "x", "f" . ("x" . "x")) }>.
+
+  Definition g : term := <{ λ "fct", λ "n", ($iszro . "n") . ($c 1) . ($times . "n" . ("fct" . ($prd . "n"))) }>.
+  Definition fact : term := <{ $ffix . $g }>.
+
+  (* Example fact_test_3:
+    multi_step_eval <{ $fact . # 3 }> 100 = <{ # 6 }>.
+  Proof. simpl. reflexivity. Qed. *)
+
+  (* 5.2.9 *)
+  (* "test b v w" will eval v and w first due to call-by-value eval order
+     so the naive factorial-in-terms-of-test would not terminate at n = 0.
+     We can fix this by wrapping the v and w in closures that ignore their
+     arguments, so-called "thunks", to force the evaluation order.
+  *)
+  Definition g2 : term := <{
+    λ "fct", λ "n",
+      ($test
+      . ($c_eq . "n" . # 0)
+      . (λ "u", # 1)
+      . (λ "u", $times . "n" . ("fct" . ($prd . "n")))
+      ) . # 0
+  }>.
+  Definition fact2 : term := <{ $ffix . $g2 }>.
+
+  (* 5.2.10 *)
+  Definition churchnat : term := <{
+    $ffix . (λ "cn", λ "n",
+        ($iszro . "n")
+      . # 0
+      . ($scc . ("cn" . ($prd . "n")))
+    )
+  }>.
+
+  (* 5.2.11 *)
+  Definition sumlist : term := <{
+    $ffix . (λ "f", λ "l",
+        ($l_isnil . "l")
+      . # 0
+      . ($plus . ($l_head . "l") . ("f" . ($tail . "l")))
+    )
+  }>.
+
+  (* 5.3.2 *)
+  Fixpoint size (t : term) : nat :=
+    match t with
+    | Var _ => 1
+    | Lambda _ body => 1 + size body
+    | App t1 t2 => size t1 + size t2
+    end.
+
+  Fixpoint free_vars (t : term) : set string :=
+    match t with
+    | Var x => [x]
+    | Lambda x body => set_remove string_dec x (free_vars body)
+    | App t1 t2 => set_union string_dec (free_vars t1) (free_vars t2)
+    end.
+
+  (* 5.3.3 *)
+  Lemma set_remove_length_le : forall (A : Type) (eq_dec : forall x y : A, {x = y} + {x <> y}) (x : A) (s : set A),
+    length (set_remove eq_dec x s) <= length s.
+  Proof.
+    intros A eq_dec x s.
+    induction s as [| y s' IH].
+    - simpl. reflexivity.
+    - simpl. destruct (eq_dec x y) as [Heq | Hneq].
+      + simpl. apply Nat.le_succ_diag_r.
+      + simpl. apply le_n_S. apply IH.
+  Qed.
+
+  Lemma set_union_empty_l : forall (A : Type) (eq_dec : forall x y : A, {x = y} + {x <> y}) (s : set A),
+    set_union eq_dec [] s = s.
+  Proof.
+    intros A eq_dec s.
+    induction s as [| x s' IH].
+    - simpl. reflexivity.
+    - simpl.
+      rewrite IH.
+  Admitted.
+
+  Lemma set_union_length_le : forall (A : Type) (eq_dec : forall x y : A, {x = y} + {x <> y}) (s1 s2 : set A),
+    length (set_union eq_dec s1 s2) <= length s1 + length s2.
+  Proof.
+    intros A eq_dec s1 s2.
+    induction s1 as [| x s1' IH].
+    - simpl. rewrite set_union_empty_l. reflexivity.
+    - simpl. destruct (in_dec eq_dec x s2) as [Hin | Hnotin].
+      + simpl.
+  Admitted.
+
+  Lemma le_sum : forall a b c d : nat, a <= b -> c <= d -> a + c <= b + d.
+  Proof.
+    intros a b c d H1 H2.
+    apply Nat.add_le_mono; assumption.
+  Qed.
+
+  Lemma fv_leq_size : forall t, length (free_vars t) <= size t.
+  Proof.
+    intros t.
+    induction t as [x | x body IH | t1 IH1 t2 IH2].
+    - simpl. reflexivity.
+    - simpl.
+      assert (H : length (set_remove string_dec x (free_vars body)) <= length (free_vars body)).
+      { apply set_remove_length_le. }
+      rewrite H.
+      assert (H2 : length (free_vars body) <= size body).
+      { apply IH. }
+      rewrite H2.
+      apply Nat.le_succ_diag_r.
+    - simpl.
+      assert (H1: length (set_union string_dec (free_vars t1) (free_vars t2)) <= length (free_vars t1) + length (free_vars t2)).
+      { apply set_union_length_le. }
+      rewrite H1.
+      apply le_sum.
+      + apply IH1.
+      + apply IH2.
+  Qed.
+
+End Chap5.