468 lines
12 KiB
V
468 lines
12 KiB
V
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. |