From 7d4574a2ecf11e067b7f13dc9e6b0a3a0d298993 Mon Sep 17 00:00:00 2001 From: h7x4 Date: Wed, 24 Jun 2026 21:36:42 +0900 Subject: [PATCH] Initial commit --- .envrc | 1 + README.md | 5 + flake.lock | 27 +++ flake.nix | 32 ++++ src/chap3.v | 468 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 533 insertions(+) create mode 100644 .envrc create mode 100644 README.md create mode 100644 flake.lock create mode 100644 flake.nix create mode 100644 src/chap3.v diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..3550a30 --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +use flake diff --git a/README.md b/README.md new file mode 100644 index 0000000..42f1794 --- /dev/null +++ b/README.md @@ -0,0 +1,5 @@ +# TaPL proofs + +This repository contains various exercises from the book ["Types and Programming Languages"](https://www.cis.upenn.edu/~bcpierce/tapl/), solved in Rocq. + +I'm pretty new to the entire Rocq ordeal while solving this, so I would not encourage using this as a reference solution. \ No newline at end of file diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..0ee7307 --- /dev/null +++ b/flake.lock @@ -0,0 +1,27 @@ +{ + "nodes": { + "nixpkgs": { + "locked": { + "lastModified": 1781577229, + "narHash": "sha256-lrp67w8AulE9Ks53n27I45ADSzbOCn4H+CNW1Ck8B+8=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "567a49d1913ce81ac6e9582e3553dd90a955875f", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "nixpkgs": "nixpkgs" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..097745c --- /dev/null +++ b/flake.nix @@ -0,0 +1,32 @@ +{ + inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; + + outputs = { self, nixpkgs }: + let + inherit (nixpkgs) lib; + + systems = [ + "x86_64-linux" + "aarch64-linux" + "x86_64-darwin" + "aarch64-darwin" + ]; + + forAllSystems = f: lib.genAttrs systems (system: f system nixpkgs.legacyPackages.${system}); + in { + devShells = forAllSystems (_: pkgs: { + default = pkgs.mkShell { + packages = with pkgs; [ + coq_8_18 + coqPackages_8_18.stdlib + coqPackages_8_18.vsrocq-language-server + ]; + + shellHook = '' + export ROCQPATH="$COQPATH" + unset COQPATH + ''; + }; + }); + }; +} diff --git a/src/chap3.v b/src/chap3.v new file mode 100644 index 0000000..5c803d9 --- /dev/null +++ b/src/chap3.v @@ -0,0 +1,468 @@ +Require Import Arith. +Require Import Coq.Lists.List. +Require Import Coq.Lists.ListSet. +Import ListNotations. + + +Module Chap3. + Module BoolArithExpr. + Inductive term : Type := + | ttrue + | tfalse + | iif (t1 t2 t3 : term). + + Scheme Equality for term. + + Definition is_value (t : term) : Prop := + match t with + | ttrue => True + | tfalse => True + | _ => False + end. + + (* 3.3.1 *) + Fixpoint consts (t:term) : set term := + match t with + | ttrue => [ttrue] + | tfalse => [tfalse] + | iif t1 t2 t3 => consts t1 ++ consts t2 ++ consts t3 + end. + + (* 3.3.2 *) + Fixpoint size (t:term) : Nat.t := + match t with + | ttrue => 1 + | tfalse => 1 + | iif t1 t2 t3 => 1 + size t1 + size t2 + size t3 + end. + + Fixpoint depth (t:term) : Nat.t := + match t with + | ttrue => 1 + | tfalse => 1 + | iif t1 t2 t3 => 1 + (Nat.max (depth t1) (Nat.max (depth t2) (depth t3))) + end. + + (* 3.3.3 *) + Lemma consts_less_than_size : forall t : term, length (consts t) <= size t. + Proof. + intros t. + induction t as [| | t1 IHt1 t2 IHt2 t3 IHt3]. + - reflexivity. + - reflexivity. + - simpl. + rewrite app_length. + rewrite app_length. + rewrite Nat.add_assoc. + rewrite <- Nat.le_succ_diag_r. + apply Nat.add_le_mono. + apply Nat.add_le_mono. + + exact IHt1. + + exact IHt2. + + exact IHt3. + Qed. + + (* 3.5.3 *) + Fixpoint eval_one_step (t:term) : term := + match t with + (* E-IfTrue *) + | iif ttrue t2 t3 => t2 + (* E-IfFalse *) + | iif tfalse t2 t3 => t3 + (* E-If *) + | iif t1 t2 t3 => iif (eval_one_step t1) t2 t3 + (* No rule applies *) + | t => t + end. + + (* 3.5.4 *) + Lemma eval_one_step_determinancy : forall t t1' t2' : term, + eval_one_step t = t1' -> + eval_one_step t = t2' -> + t1' = t2'. + Proof. + destruct t as [| | t1 t2 t3]. + - intros t1' t2' H1 H2. rewrite H1 in H2. exact H2. + - intros t1' t2' H1 H2. rewrite H1 in H2. exact H2. + - intros t1' t2' H1 H2. rewrite H1 in H2. exact H2. + Qed. + + (* 3.5.6 *) + Definition is_normal_form (t:term) : Prop := + eq (eval_one_step t) t. + + (* 3.5.7 *) + Lemma all_values_are_normal_forms : forall t : term, is_value t -> is_normal_form t. + Proof. + intros t H. + destruct t as [| | t1 t2 t3]. + - reflexivity. + - reflexivity. + - contradiction H. + Qed. + + (* 3.5.8 *) + Lemma not_value_not_normal_form : + forall t, + ~ is_value t -> + ~ is_normal_form t. + Proof. + intros t Hv Hnf. + destruct t as [| | t1 t2 t3]. + - apply Hv. exact I. + - apply Hv. exact I. + - unfold is_normal_form in Hnf. + Admitted. + + Lemma all_normal_forms_are_values : forall t : term, + is_normal_form t -> is_value t. + Proof. + intros t Hnf. + Admitted. + + (* 3.5.9 *) + Fixpoint multi_step_eval (t:term) : term := + match t with + (* E-IfTrue *) + | iif ttrue t2 t3 => multi_step_eval t2 + (* E-IfFalse *) + | iif tfalse t2 t3 => multi_step_eval t3 + (* E-If *) + | iif t1 t2 t3 => iif (multi_step_eval t1) t2 t3 + | t => t + end. + + (* 3.5.11 *) + Lemma uniqueness_of_normal_forms : forall t t1' t2' : term, + is_normal_form t1' -> + is_normal_form t2' -> + multi_step_eval t = t1' -> + multi_step_eval t = t2' -> + t1' = t2'. + Proof. + intros t t1' t2' H1 H2 H3 H4. + Admitted. + + (* 3.5.12 *) + Lemma termination_of_evaluation : forall t : term, exists t' : term, + multi_step_eval t = t'. + Proof. + intros t. + Admitted. + End BoolArithExpr. + + + + Module ArithExpr. + Inductive term : Type := + | ttrue + | tfalse + | iif (t1 t2 t3 : term) + | O + | succ (t : term) + | pred (t : term) + | iszero (t : term). + + Scheme Equality for term. + + Fixpoint is_value (t:term) : Prop := + match t with + | ttrue => True + | tfalse => True + | O => True + | succ t1 => is_value t1 + | _ => False + end. + + + (* 3.2.3 *) + Fixpoint term_set (i : nat) : set term := + match i with + | 0 => [] + | S i' => [ttrue; tfalse; O] + ++ map (fun t => succ t) (term_set i') + ++ map (fun t => pred t) (term_set i') + ++ map (fun t => iszero t) (term_set i') + ++ flat_map (fun t1 => + flat_map (fun t2 => + map (fun t3 => iif t1 t2 t3) (term_set i') + ) (term_set i') + ) (term_set i') + end. + + (* 3.2.4 *) + Fixpoint term_set_size (i : nat) : nat := + match i with + | 0 => 0 + | S i' => 3 + + term_set_size i' + + term_set_size i' + + term_set_size i' + + (term_set_size i') * (term_set_size i') * (term_set_size i') + end. + Lemma flat_map_const_length : forall (A B : Type) (f : A -> list B) (l : list A) (n : nat), + (forall x : A, length (f x) = n) -> length (flat_map f l) = n * length l. + Proof. + intros A B f l n H. + induction l as [| x xs IH]. + - simpl. rewrite Nat.mul_0_r. reflexivity. + - simpl. + rewrite app_length. + rewrite H. + rewrite IH. + rewrite Nat.mul_succ_r. + rewrite Nat.add_comm. + reflexivity. + Qed. + + Lemma term_set_size_correct : forall i : nat, length (term_set i) = term_set_size i. + Proof. + intros i. + induction i as [| i' IH]. + - reflexivity. + - simpl. + do 3 apply eq_S. + do 2 rewrite <- Nat.add_assoc. + do 3 ( + rewrite app_length; + rewrite map_length; + rewrite IH; + apply Nat.add_cancel_l + ). + + rewrite flat_map_const_length with (n := length (term_set i') * length (term_set i')). + { rewrite IH. reflexivity. } + intros t1. + rewrite flat_map_const_length with (n := length (term_set i')). + { rewrite IH. reflexivity. } + intros t2. + rewrite map_length. + reflexivity. + Qed. + + (* Compute term_set_size 3. *) + + (* 3.2.5 *) + Lemma term_set_cumulative : forall i : nat, incl (term_set i) (term_set (S i)). + Proof. + intros i t H. + induction i as [| i' IH]. + - simpl in H. contradiction H. + - destruct t as [| | t1 t2 t3 | | t1 | t1 | t1]. + + left. reflexivity. + + right. left. reflexivity. + + do 6 right. + simpl in H. + destruct H as [H | H]. + discriminate H. + destruct H as [H | H]. + discriminate H. + destruct H as [H | H]. + discriminate H. + apply in_or_app. + left. + Admitted. + + (* 3.3.1 *) + Fixpoint consts (t:term) : set term := + match t with + | ttrue => [ttrue] + | tfalse => [tfalse] + | iif t1 t2 t3 => consts t1 ++ consts t2 ++ consts t3 + | O => [O] + | succ t1 => consts t1 + | pred t1 => consts t1 + | iszero t1 => consts t1 + end. + + (* 3.3.2 *) + Fixpoint size (t:term) : Nat.t := + match t with + | ttrue => 1 + | tfalse => 1 + | iif t1 t2 t3 => 1 + size t1 + size t2 + size t3 + | O => 1 + | succ t1 => 1 + size t1 + | pred t1 => 1 + size t1 + | iszero t1 => 1 + size t1 + end. + + Fixpoint depth (t:term) : Nat.t := + match t with + | ttrue => 1 + | tfalse => 1 + | iif t1 t2 t3 => 1 + (Nat.max (depth t1) (Nat.max (depth t2) (depth t3))) + | O => 1 + | succ t1 => 1 + depth t1 + | pred t1 => 1 + depth t1 + | iszero t1 => 1 + depth t1 + end. + + (* 3.3.3 *) + Lemma consts_less_than_size : forall t : term, length (consts t) <= size t. + Proof. + intros t. + induction t as [| | t1 IHt1 t2 IHt2 t3 IHt3 | | t1 IHt1 | t1 IHt1 | t1 IHt1]. + - reflexivity. + - reflexivity. + - simpl. + rewrite app_length. + rewrite app_length. + rewrite Nat.add_assoc. + rewrite <- Nat.le_succ_diag_r. + apply Nat.add_le_mono. + apply Nat.add_le_mono. + + exact IHt1. + + exact IHt2. + + exact IHt3. + - reflexivity. + - simpl. + rewrite <- Nat.le_succ_diag_r. + exact IHt1. + - simpl. + rewrite <- Nat.le_succ_diag_r. + exact IHt1. + - simpl. + rewrite <- Nat.le_succ_diag_r. + exact IHt1. + Qed. + + (* 3.5.3 *) + Fixpoint eval_one_step (t:term) : term := + match t with + (* E-IfTrue *) + | iif ttrue t2 t3 => t2 + (* E-IfFalse *) + | iif tfalse t2 t3 => t3 + (* E-If *) + | iif t1 t2 t3 => iif (eval_one_step t1) t2 t3 + (* E-Succ *) + | succ t1 => succ (eval_one_step t1) + (* E-PredZero *) + | pred O => O + (* E-PredSucc *) + | pred (succ t1) => t1 + (* E-Pred *) + | pred t1 => pred (eval_one_step t1) + (* E-IsZeroZero *) + | iszero O => ttrue + (* E-IsZeroSucc *) + | iszero (succ t1) => tfalse + (* E-IsZero *) + | iszero t1 => iszero (eval_one_step t1) + (* No rule applies *) + | t => t + end. + + (* 3.5.6 *) + Definition is_normal_form (t:term) : Prop := + eq (eval_one_step t) t. + + (* 3.5.7 *) + Lemma all_values_are_normal_forms : forall t : term, is_value t -> is_normal_form t. + Proof. + intros t H. + induction t as [| | t1 _ t2 _ t3 _ | | t1 IHt1 | t1 IHt1 | t1 IHt1]. + - reflexivity. + - reflexivity. + - contradiction H. + - reflexivity. + - simpl. + assert (is_value t1) as H1. + { exact H. } + Admitted. + + (* 3.5.9 *) + Fixpoint multi_step_eval (t:term) : term := + match t with + (* E-IfTrue *) + | iif ttrue t2 t3 => multi_step_eval t2 + (* E-IfFalse *) + | iif tfalse t2 t3 => multi_step_eval t3 + (* E-If *) + | iif t1 t2 t3 => iif (multi_step_eval t1) t2 t3 + (* E-Succ *) + | succ t1 => succ (multi_step_eval t1) + (* E-PredZero *) + | pred O => O + (* E-PredSucc *) + | pred (succ t1) => multi_step_eval t1 + (* E-Pred *) + | pred t1 => pred (multi_step_eval t1) + (* E-IsZeroZero *) + | iszero O => ttrue + (* E-IsZeroSucc *) + | iszero (succ t1) => tfalse + (* E-IsZero *) + | iszero t1 => iszero (multi_step_eval t1) + (* No rule applies *) + | t => t + end. + + (* 3.5.14 (3.5.4) *) + Lemma eval_one_step_determinancy : forall t t1' t2' : term, + eval_one_step t = t1' -> + eval_one_step t = t2' -> + t1' = t2'. + Proof. + destruct t as [| | t1 t2 t3 | | t1 | t1 | t1]. + - intros t1' t2' H1 H2. rewrite H1 in H2. exact H2. + - intros t1' t2' H1 H2. rewrite H1 in H2. exact H2. + - intros t1' t2' H1 H2. rewrite H1 in H2. exact H2. + - intros t1' t2' H1 H2. rewrite H1 in H2. exact H2. + - intros t1' t2' H1 H2. rewrite H1 in H2. exact H2. + - intros t1' t2' H1 H2. rewrite H1 in H2. exact H2. + - intros t1' t2' H1 H2. rewrite H1 in H2. exact H2. + Qed. + + (* 3.5.15 *) + Definition is_stuck (t : term) : Prop := + ~ is_value t /\ is_normal_form t. + + (* 3.5.17 *) + Fixpoint big_step_eval (t : term) : term := + match t with + | iif t1 t2 t3 => + match big_step_eval t1 with + (* B-IfTrue *) + | ttrue => big_step_eval t2 + (* B-IfFalse *) + | tfalse => big_step_eval t3 + | _ => t + end + (* B-Succ *) + | succ t1 => + match big_step_eval t1 with + | O => succ O + | succ t' => succ (succ t') + | pred t' => succ (pred t') + | _ => t + end + | pred t1 => + match big_step_eval t1 with + (* B-PredZero *) + | O => O + (* B-PredSucc *) + | succ t' => t' + | _ => t + end + | iszero t1 => + match big_step_eval t1 with + (* B-IsZeroZero *) + | O => ttrue + (* B-IsZeroSucc *) + | succ t' => tfalse + | _ => t + end + (* B-Value *) + | t => t + end. + + Lemma big_step_eval_equivalence : forall t : term, + big_step_eval t = multi_step_eval t. + Proof. + intros t. + Admitted. + + End ArithExpr. +End Chap3. \ No newline at end of file