Initial commit
This commit is contained in:
@@ -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.
|
||||
Generated
+27
@@ -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
|
||||
}
|
||||
@@ -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
|
||||
'';
|
||||
};
|
||||
});
|
||||
};
|
||||
}
|
||||
+468
@@ -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.
|
||||
Reference in New Issue
Block a user