|
|
@ -74,11 +74,16 @@ Proof.
|
|
|
|
all: naive_solver.
|
|
|
|
all: naive_solver.
|
|
|
|
Qed.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(* values are values *)
|
|
|
|
Lemma is_val_of_val v : is_val (of_val v).
|
|
|
|
Lemma is_val_of_val v : is_val (of_val v).
|
|
|
|
Proof.
|
|
|
|
Proof.
|
|
|
|
|
|
|
|
destruct v; simpl; done.
|
|
|
|
|
|
|
|
Restart.
|
|
|
|
apply is_val_spec. rewrite to_of_val. eauto.
|
|
|
|
apply is_val_spec. rewrite to_of_val. eauto.
|
|
|
|
Qed.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Definition is_val_val := is_val_of_val.
|
|
|
|
|
|
|
|
|
|
|
|
(* A small tactic that simplifies handling values. *)
|
|
|
|
(* A small tactic that simplifies handling values. *)
|
|
|
|
Ltac simplify_val :=
|
|
|
|
Ltac simplify_val :=
|
|
|
|
repeat match goal with
|
|
|
|
repeat match goal with
|
|
|
@ -86,15 +91,9 @@ Ltac simplify_val :=
|
|
|
|
| H: is_val ?e |- _ => destruct (proj1 (is_val_spec e) H) as (? & ?); clear H
|
|
|
|
| H: is_val ?e |- _ => destruct (proj1 (is_val_spec e) H) as (? & ?); clear H
|
|
|
|
end.
|
|
|
|
end.
|
|
|
|
|
|
|
|
|
|
|
|
(* values are values *)
|
|
|
|
(* we tell eauto to use the lemma is_val_of_val *)
|
|
|
|
Lemma is_val_val (v: val): is_val (of_val v).
|
|
|
|
|
|
|
|
Proof.
|
|
|
|
|
|
|
|
destruct v; simpl; done.
|
|
|
|
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(* we tell eauto to use the lemma is_val_val *)
|
|
|
|
|
|
|
|
#[global]
|
|
|
|
#[global]
|
|
|
|
Hint Immediate is_val_val : core.
|
|
|
|
Hint Immediate is_val_of_val : core.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** ** Operational Semantics *)
|
|
|
|
(** ** Operational Semantics *)
|
|
|
@ -125,7 +124,7 @@ Definition subst' (mx : binder) (es : expr) : expr → expr :=
|
|
|
|
the left side can only be reduced once the right
|
|
|
|
the left side can only be reduced once the right
|
|
|
|
side is fully evaluated (i.e., is a value). *)
|
|
|
|
side is fully evaluated (i.e., is a value). *)
|
|
|
|
Inductive step : expr → expr → Prop :=
|
|
|
|
Inductive step : expr → expr → Prop :=
|
|
|
|
| StepBeta x e e' :
|
|
|
|
| StepBeta x e e' :
|
|
|
|
is_val e' →
|
|
|
|
is_val e' →
|
|
|
|
step (App (Lam x e) e') (subst' x e' e)
|
|
|
|
step (App (Lam x e) e') (subst' x e' e)
|
|
|
|
| StepAppL e1 e1' e2 :
|
|
|
|
| StepAppL e1 e1' e2 :
|
|
|
|