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

chap5: init

Browse Source
This commit is contained in:
Oystein Kristoffer Tveit
2026-06-25 02:27:48 +09:00
parent 7d4574a2ec
commit 28c71cf03f
1 changed files with 390 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/chap5.v
+390
View File
@@ -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.