mpri-funcprog-project/coq/LambdaCalculusBigStep.v

535 lines
15 KiB
Coq
Raw Normal View History

2017-09-28 10:36:07 +02:00
Require Import List.
Require Import MyTactics.
Require Import Sequences.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusFreeVars.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusReduction.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* A big-step call-by-value semantics. *)
Inductive bigcbv : term -> term -> Prop :=
| BigcbvValue:
forall v,
is_value v ->
bigcbv v v
| BigcbvApp:
forall t1 t2 u1 v2 v,
bigcbv t1 (Lam u1) ->
bigcbv t2 v2 ->
bigcbv u1.[v2/] v ->
bigcbv (App t1 t2) v
| BigcbvLet:
forall t1 t2 v1 v,
bigcbv t1 v1 ->
bigcbv t2.[v1/] v ->
bigcbv (Let t1 t2) v
.
Hint Constructors bigcbv : bigcbv.
(* The tactic [invert_bigcbv] looks for a hypothesis of the form [bigcbv t v]
and inverts it. *)
Ltac invert_bigcbv :=
pick bigcbv invert;
try solve [ false; eauto 3 with obvious ].
(* -------------------------------------------------------------------------- *)
(* If [bigcbv t v] holds, then [v] must be a value. *)
Lemma bigcbv_is_value:
forall t v,
bigcbv t v ->
is_value v.
Proof.
induction 1; eauto.
Qed.
Hint Resolve bigcbv_is_value : is_value obvious.
(* -------------------------------------------------------------------------- *)
(* If [t] evaluates to [v] according to the big-step semantics,
then [t] reduces to [v] according to the small-step semantics. *)
Lemma bigcbv_star_cbv:
forall t v,
bigcbv t v ->
star cbv t v.
Proof.
(* A detailed proof: *)
induction 1.
(* BigcbvValue *)
{ eapply star_refl. }
(* BigcbvApp *)
{ eapply star_trans. obvious.
eapply star_trans. obvious.
eapply star_step. obvious.
eauto. }
(* BigcbvLet *)
{ eapply star_trans. obvious.
eapply star_step. obvious.
eauto. }
Restart.
(* A much shorter proof: *)
induction 1; eauto 6 with sequences obvious.
Qed.
(* Conversely, if [t] reduces to [v] in the small-step semantics,
then [t] evaluates to [v] in the big-step semantics. *)
Lemma cbv_bigcbv_bigcbv:
forall t1 t2,
cbv t1 t2 ->
forall v,
bigcbv t2 v ->
bigcbv t1 v.
Proof.
(* A detailed proof: *)
induction 1; intros; subst; try solve [ false; tauto ].
(* BetaV *)
{ econstructor; eauto with bigcbv. }
(* LetV *)
{ econstructor; eauto with bigcbv. }
(* AppL *)
{ invert_bigcbv. eauto with bigcbv. }
(* AppR *)
{ invert_bigcbv. eauto with bigcbv. }
(* LetL *)
{ invert_bigcbv. eauto with bigcbv. }
Restart.
(* A shorter proof: *)
induction 1; intros; subst; try solve [ false; tauto
| econstructor; eauto with bigcbv
| invert_bigcbv; eauto with bigcbv
].
Qed.
Lemma star_cbv_bigcbv:
forall t v,
star cbv t v ->
is_value v ->
bigcbv t v.
Proof.
induction 1; eauto using cbv_bigcbv_bigcbv with bigcbv.
Qed.
(* In conclusion, we have the following equivalence: *)
Theorem star_cbv_bigcbv_eq:
forall t v,
(star cbv t v /\ is_value v) <-> bigcbv t v.
Proof.
split; intros; unpack;
eauto using star_cbv_bigcbv, bigcbv_star_cbv with is_value.
Qed.
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* A big-step call-by-value semantics with explicit environments. *)
(* A closure is a pair of a term and an environment. A cvalue [cv] must be a
closure, as we have no other forms of values. An environment [e] is a list
of cvalues. *)
(* We break the mutual induction between [cvalue] and [cenv] by inlining the
definition of [cenv] into the definition of [cvalue]. *)
(* CVALUE *)
Inductive cvalue :=
| Clo: {bind term} -> list cvalue -> cvalue.
Definition cenv :=
list cvalue.
(* CVALUE *)
(* This dummy cvalue is passed below as an argument to [nth], but is really
irrelevant, as the condition [x < length e] ensures that the dummy cvalue
is never used. *)
Definition dummy_cvalue : cvalue :=
Clo (Var 0) nil.
(* The judgement [ebigcbv e t cv] means that, under the environment [e], the
term [t] evaluates to [cv]. *)
Inductive ebigcbv : cenv -> term -> cvalue -> Prop :=
| EBigcbvVar:
forall e x cv,
(* The variable [x] must be in the domain of [e]. *)
x < length e ->
(* This allows us to safely look up [e] at [x]. *)
cv = nth x e dummy_cvalue ->
ebigcbv e (Var x) cv
| EBigcbvLam:
forall e t,
(* The free variables of [t] must be less than or equal to [length e]. *)
(forall cv, fv (length (cv :: e)) t) ->
(* This allows us to build a closure that is indeed closed. *)
ebigcbv e (Lam t) (Clo t e)
| EBigcbvApp:
forall e e' t1 t2 u1 cv2 cv,
(* Evaluate [t1] to a closure, *)
ebigcbv e t1 (Clo u1 e') ->
(* evaluate [t2] to a value, *)
ebigcbv e t2 cv2 ->
(* and evaluate the function body, in a suitable environment. *)
ebigcbv (cv2 :: e') u1 cv ->
ebigcbv e (App t1 t2) cv
| EBigcbvLet:
forall e t1 t2 cv1 cv,
(* Evaluate [t1] to a value, *)
ebigcbv e t1 cv1 ->
(* and evaluate [t2] under a suitable environment. *)
ebigcbv (cv1 :: e) t2 cv ->
ebigcbv e (Let t1 t2) cv
.
Hint Constructors ebigcbv : ebigcbv.
(* -------------------------------------------------------------------------- *)
(* To explain what the above semantics means, and to prove that it is
equivalent to the big-step semantics, we first define a function that
decodes a cvalue into a value. *)
(* Ideally, the function [decode] should be defined by the equation:
decode (Clo t e) = (Lam t).[decode_cenv e]
where the auxiliary function [decode_cenv] maps [decode] over the
environment [e], and converts the result to a substitution, that
is, a function of type [term -> term]:
decode_cenv e = fun x => nth x (map decode e) (decode dummy_cvalue)
The definitions below are a bit more awkward (as Coq does not support
mutual induction very well), but mean the same thing. *)
Definition dummy_value : term :=
Lam (Var 0).
Fixpoint decode (cv : cvalue) : term :=
match cv with
| Clo t e =>
(Lam t).[fun x => nth x (map decode e) dummy_value]
end.
(* I am not even sure why this definition is accepted by Coq? *)
Definition decode_cenv e :=
fun x => nth x (map decode e) (decode dummy_cvalue).
(* The first equation in the above comment is satisfied, as shown by
the following lemma. The second equation in the above comment is
satisfied too, by definition. *)
Lemma decode_eq:
forall t e,
decode (Clo t e) = (Lam t).[decode_cenv e].
Proof.
reflexivity.
Qed.
(* This equation is useful, too. *)
Lemma decode_cenv_Var_eq:
forall x e,
(Var x).[decode_cenv e] = decode (nth x e dummy_cvalue).
Proof.
intros. asimpl. unfold decode_cenv. rewrite map_nth. eauto.
Qed.
(* The tactic [decode] rewrites using the above two equations. *)
Hint Rewrite decode_eq decode_cenv_Var_eq : decode.
Ltac decode := autorewrite with decode in *.
(* We make [decode] opaque, so its definition is not unfolded by Coq. *)
Opaque decode.
(* [decode cv] is always a value. *)
Lemma is_value_decode:
forall cv,
is_value (decode cv).
Proof.
intros. destruct cv. decode. asimpl. tauto.
Qed.
Lemma is_value_decode_cenv:
forall x e,
is_value (Var x).[decode_cenv e].
Proof.
intros. decode. eauto using is_value_decode.
Qed.
Local Hint Resolve is_value_decode is_value_decode_cenv : is_value obvious.
(* A composition of two substitutions is the same thing as one substitution. *)
Lemma decode_cenv_cons:
forall t e cv,
t.[up (decode_cenv e)].[decode cv/] = t.[decode_cenv (cv :: e)].
Proof.
intros. autosubst. (* wonderful *)
Qed.
(* The tactic [nonvalue_eq_decode] closes a subgoal when there is a hypothesis
of the form [_ = decode_cenv e x], where the left-hand side of the equation
clearly is not a value. This is a contradiction. *)
Ltac nonvalue_eq_decode :=
match goal with
| heq: _ = decode_cenv ?e ?x |- _ =>
assert (hv: is_value (decode_cenv e x)); [
solve [ obvious ]
| rewrite <- heq in hv; false; is_value ]
end.
(* -------------------------------------------------------------------------- *)
(* If [t] evaluates to [cv] under environment [e],
then, in the big-step semantics,
the term [t.[decode_cenv e]] evaluates to the value [decode cv]. *)
Lemma ebigcbv_bigcbv:
forall e t cv,
ebigcbv e t cv ->
bigcbv t.[decode_cenv e] (decode cv).
Proof.
induction 1; intros; subst.
(* EBigcbvVar *)
{ decode. econstructor. obvious. }
(* EBigcbvLam *)
{ econstructor. obvious. }
(* EBigcbvApp *)
{ decode.
asimpl. econstructor; eauto.
asimpl. eauto. }
(* EBigcbvLet *)
{ asimpl. econstructor; eauto.
asimpl. eauto. }
Qed.
(* A simplified corollary, where [t] is closed and is therefore evaluated
under the empty environment. *)
Lemma ebigcbv_bigcbv_nil:
forall t cv,
ebigcbv nil t cv ->
closed t ->
bigcbv t (decode cv).
Proof.
intros.
replace t with t.[decode_cenv nil] by eauto using closed_unaffected.
eauto using ebigcbv_bigcbv.
Qed.
(* -------------------------------------------------------------------------- *)
(* The converse statement: if in the big-step semantics, the term
[t.[decode_cenv e]] evaluates to the value [decode cv], then [t] evaluates
to [cv] under environment [e]. *)
(* This proof does not work (and, in fact, the statement is wrong). A failed
proof attempt reveals two problems... *)
Lemma bigcbv_ebigcbv_failed:
forall e t cv,
bigcbv t.[decode_cenv e] (decode cv) ->
ebigcbv e t cv.
Proof.
inversion 1; intros; subst.
(* BigcbvValue *)
{ (* [t] must be a variable or a lambda-abstraction. *)
destruct t; [ | | false; is_value | false; is_value ].
(* Case: [t] is a variable. *)
{ econstructor.
(* Here, we have two subgoals, neither of which can be proved. *)
{ (* Problem 1: we are unable to prove [x < length e]. In order
to establish such a property, we would have to express the
hypothesis that the free variables of [t] are in the domain
of the environment [e]. And, for this hypothesis to be
inductive, we have to further require every closure in
the environment [e] to satisfy a similar condition. *)
admit. }
{ (* Problem 2: we have [decode cv1 = decode cv2], and the goal
is [cv1 = cv2]. This goal cannot be proved, as the function
[decode] is not injective: multiple closures represent the
same lambda-abstraction. *)
decode.
admit. }
Abort.
(* -------------------------------------------------------------------------- *)
(* In order to fix the above failed statement, we need to express the
following well-formedness invariant: whenever a closure [Clo t e] is
constructed, the free variables of the term [t] are in the domain of the
environment [env], and, recursively, every value in [e] is well-formed. *)
Inductive wf_cvalue : cvalue -> Prop :=
| WfCvalue:
forall t e,
(forall cv, fv (length (cv :: e)) t) ->
wf_cenv e ->
wf_cvalue (Clo t e)
with wf_cenv : cenv -> Prop :=
| WfCenv:
forall e,
Forall wf_cvalue e ->
wf_cenv e.
(* The following trivial lemmas (which repeat the definition) are provided as
hints for [eauto with wf_cvalue]. *)
Lemma use_wf_cvalue_1:
forall t e cv,
wf_cvalue (Clo t e) ->
fv (length (cv :: e)) t.
Proof.
inversion 1; eauto.
Qed.
Lemma use_wf_cvalue_2:
forall t e,
wf_cvalue (Clo t e) ->
wf_cenv e.
Proof.
inversion 1; eauto.
Qed.
Lemma prove_wf_cenv_nil:
wf_cenv nil.
Proof.
econstructor. eauto.
Qed.
Lemma prove_wf_cenv_cons:
forall cv e,
wf_cvalue cv ->
wf_cenv e ->
wf_cenv (cv :: e).
Proof.
inversion 2; intros; subst.
econstructor.
econstructor; eauto.
Qed.
Hint Resolve
use_wf_cvalue_1 use_wf_cvalue_2 prove_wf_cenv_nil prove_wf_cenv_cons
: wf_cvalue.
(* The following lemma states that the invariant is preserved by [ebigcbv].
That is, if the term [t] is successfully evaluated in the well-formed
environment [e] to a cvalue [cv], then [cv] is well-formed. *)
Lemma ebigcbv_wf_cvalue:
forall e t cv,
ebigcbv e t cv ->
wf_cenv e ->
wf_cvalue cv.
Proof.
induction 1; intros; subst.
(* EBigcbvVar *)
{ pick wf_cenv invert. rewrite Forall_forall in *. eauto using nth_In. }
(* EBigcbvLam *)
{ econstructor; eauto. }
(* EBigcbvApp *)
{ eauto 6 with wf_cvalue. }
(* EBigcbvLet *)
{ eauto 6 with wf_cvalue. }
Qed.
Hint Resolve ebigcbv_wf_cvalue : wf_cvalue.
(* -------------------------------------------------------------------------- *)
(* We can now make an amended statement: if in the big-step semantics, the
term [t.[decode_cenv e]] evaluates to a value [v], if the environment [e]
is well-formed, and if the free variables of [t] are in the domain of [e],
then under environment [e] the term [t] evaluates to some cvalue [cv] such
that [decode cv] is [v]. *)
Lemma bigcbv_ebigcbv:
forall te v,
bigcbv te v ->
forall t e,
te = t.[decode_cenv e] ->
fv (length e) t ->
wf_cenv e ->
exists cv,
ebigcbv e t cv /\ decode cv = v.
Proof.
induction 1; intros; subst.
(* BigcbvValue *)
{ (* [t] must be a variable or a lambda-abstraction. *)
destruct t; [ | | false; is_value | false; is_value ]; fv.
(* Case: [t] is a variable. *)
{ eexists; split. econstructor; eauto. decode. eauto. }
(* Case: [t] is a lambda-abstraction. *)
{ eexists; split. econstructor; eauto. reflexivity. }
}
(* BigcbvApp *)
{ (* [t] must be an application. *)
destruct t;
match goal with h: _ = _ |- _ => asimpl in h end;
[ nonvalue_eq_decode | false; congruence | | false; congruence ].
fv. unpack.
(* The equality [App _ _ = App _ _] can be simplified. *)
injections. subst.
(* Exploit two of the induction hypotheses (forward). *)
edestruct IHbigcbv1; eauto. unpack. clear IHbigcbv1.
edestruct IHbigcbv2; eauto. unpack. clear IHbigcbv2.
(* If [decode cv] is [Lam _], then [cv] must be a closure. This should
be a lemma. Because (here) every cvalue is a closure, it is trivial. *)
match goal with h: decode ?cv = Lam _ |- _ =>
destruct cv as [ t' e' ];
rewrite decode_eq in h;
asimpl in h;
injections; subst
end.
(* Now, exploit the third induction hypothesis (forward). *)
edestruct IHbigcbv3; eauto using decode_cenv_cons with wf_cvalue.
unpack. clear IHbigcbv3.
(* The result follows. *)
eauto with ebigcbv.
}
(* BigcbvLet *)
{ (* [t] must be a [Let] construct. *)
destruct t;
match goal with h: _ = _ |- _ => asimpl in h end;
[ nonvalue_eq_decode | false; congruence | false; congruence | ].
fv. unpack.
injections. subst.
(* Exploit the induction hypotheses (forward). *)
edestruct IHbigcbv1; eauto. unpack. clear IHbigcbv1.
edestruct IHbigcbv2; eauto using decode_cenv_cons with wf_cvalue.
unpack. clear IHbigcbv2.
(* The result follows. *)
eauto with ebigcbv.
}
Qed.
(* A simplified corollary, where [t] is closed and is therefore evaluated
under the empty environment. *)
Lemma bigcbv_ebigcbv_nil:
forall t v,
bigcbv t v ->
closed t ->
exists cv,
ebigcbv nil t cv /\ decode cv = v.
Proof.
intros. eapply bigcbv_ebigcbv; eauto with wf_cvalue.
rewrite closed_unaffected by eauto. reflexivity.
Qed.