Require Import Bool.
Require Import ZArith.
Require Import IMPSyntax.
Require Import IMPSemantics.
Ltac ecea := econstructor; eauto.
Ltac erep := repeat ecea.
Lemma can_eval:
forall h e,
exists i, eval h e i.
Proof.
intros; induction e.
- erep.
- erep.
- destruct IHe1; destruct IHe2.
take apart IH before eauto
erep.
Qed.
Lemma can_step:
forall s,
s <> Nop ->
forall h, exists h´, exists s´, step h s h´ s´.
Proof.
intros; induction s.
- congruence.
- destruct (can_eval h e). erep.
- destruct (isNop s1) eqn:?.
+ apply isNop_ok in Heqb; subst. erep.
+ destruct IHs1.
* intro; subst. discriminate.
* destruct H0; erep.
- destruct (can_eval h e).
destruct (Z_eq_dec 0 x).
+ ecea; ecea; eapply step_cond_false; eauto.
+ erep.
- destruct (can_eval h e).
destruct (Z_eq_dec 0 x).
+ ecea; ecea; eapply step_while_false; eauto.
+ erep.
Qed.
Definition diverges (s: stmt) : Prop :=
forall h n,
exists h´, exists s´,
step_n h s n h´ s´.
Definition furnace : stmt :=
while 1 {{ Nop }}.
Qed.
Lemma can_step:
forall s,
s <> Nop ->
forall h, exists h´, exists s´, step h s h´ s´.
Proof.
intros; induction s.
- congruence.
- destruct (can_eval h e). erep.
- destruct (isNop s1) eqn:?.
+ apply isNop_ok in Heqb; subst. erep.
+ destruct IHs1.
* intro; subst. discriminate.
* destruct H0; erep.
- destruct (can_eval h e).
destruct (Z_eq_dec 0 x).
+ ecea; ecea; eapply step_cond_false; eauto.
+ erep.
- destruct (can_eval h e).
destruct (Z_eq_dec 0 x).
+ ecea; ecea; eapply step_while_false; eauto.
+ erep.
Qed.
Definition diverges (s: stmt) : Prop :=
forall h n,
exists h´, exists s´,
step_n h s n h´ s´.
Definition furnace : stmt :=
while 1 {{ Nop }}.
stupid auto indent
Ltac zex x := exists x.
Lemma warming_up:
diverges furnace.
Proof.
unfold diverges. intros.
induction n.
- zex h. zex furnace. constructor.
- destruct IHn as [h´ [s´ H]].
Lemma warming_up:
diverges furnace.
Proof.
unfold diverges. intros.
induction n.
- zex h. zex furnace. constructor.
- destruct IHn as [h´ [s´ H]].
hmm, need to add next step to the *end*
Abort.
Lemma step_n_r:
forall h1 s1 n h2 s2 h3 s3,
step_n h1 s1 n h2 s2 ->
step h2 s2 h3 s3 ->
step_n h1 s1 (S n) h3 s3.
Proof.
intros. induction H.
- econstructor; eauto.
constructor.
- econstructor; eauto.
Qed.
Lemma warming_up:
diverges furnace.
Proof.
unfold diverges. intros.
induction n.
- zex h. zex furnace. constructor.
- destruct IHn as [h´ [s´ H]].
Lemma step_n_r:
forall h1 s1 n h2 s2 h3 s3,
step_n h1 s1 n h2 s2 ->
step h2 s2 h3 s3 ->
step_n h1 s1 (S n) h3 s3.
Proof.
intros. induction H.
- econstructor; eauto.
constructor.
- econstructor; eauto.
Qed.
Lemma warming_up:
diverges furnace.
Proof.
unfold diverges. intros.
induction n.
- zex h. zex furnace. constructor.
- destruct IHn as [h´ [s´ H]].
just need to show that s' can take one more step we know everything but Nop can step... hmmm, do not know much about h' s' need stronger IH !
Abort.
Lemma warming_up:
forall h n,
exists h´, exists s´,
step_n h furnace n h´ s´ /\
s´ <> Nop.
Proof.
intros. induction n.
- zex h. zex furnace.
split.
+ constructor.
+ discriminate.
- destruct IHn as [h´ [s´ [Hs Hn]]].
destruct (can_step s´ Hn h´) as [h´´ [s´´ HS]].
zex h´´; zex s´´. split.
+ eapply step_n_r; eauto.
+
Lemma warming_up:
forall h n,
exists h´, exists s´,
step_n h furnace n h´ s´ /\
s´ <> Nop.
Proof.
intros. induction n.
- zex h. zex furnace.
split.
+ constructor.
+ discriminate.
- destruct IHn as [h´ [s´ [Hs Hn]]].
destruct (can_step s´ Hn h´) as [h´´ [s´´ HS]].
zex h´´; zex s´´. split.
+ eapply step_n_r; eauto.
+
ugh, don't know enough about s'' ! IH still too weak
Abort.
Lemma warming_up:
forall h n,
exists h´,
step_n h furnace n h´ furnace.
Proof.
intros. induction n.
- zex h. constructor.
- destruct IHn as [h´ IH].
eexists. eapply step_n_r; eauto.
Lemma warming_up:
forall h n,
exists h´,
step_n h furnace n h´ furnace.
Proof.
intros. induction n.
- zex h. constructor.
- destruct IHn as [h´ IH].
eexists. eapply step_n_r; eauto.
stuck! furnance doesn't step to itself! IH too strong!!!
Abort.
Definition furnace´ : stmt :=
Nop ;; while 1 {{ Nop }}.
Lemma warming_up:
forall h n,
exists h´,
step_n h furnace n h´ furnace \/
step_n h furnace n h´ furnace´.
Proof.
intros. induction n.
- zex h. left. constructor.
- destruct IHn as [h´ [IH | IH]].
+ eexists. right.
eapply step_n_r; eauto.
unfold furnace´.
econstructor; eauto.
econstructor; eauto.
omega.
+ eexists. left.
eapply step_n_r; eauto.
unfold furnace´.
econstructor; eauto.
Qed.
Definition furnace´ : stmt :=
Nop ;; while 1 {{ Nop }}.
Lemma warming_up:
forall h n,
exists h´,
step_n h furnace n h´ furnace \/
step_n h furnace n h´ furnace´.
Proof.
intros. induction n.
- zex h. left. constructor.
- destruct IHn as [h´ [IH | IH]].
+ eexists. right.
eapply step_n_r; eauto.
unfold furnace´.
econstructor; eauto.
econstructor; eauto.
omega.
+ eexists. left.
eapply step_n_r; eauto.
unfold furnace´.
econstructor; eauto.
Qed.
Finally IH is strong enough!
Now prove our original goal as a special case.
Lemma full_blast:
diverges furnace.
Proof.
unfold diverges; intros.
pose proof (warming_up h n).
destruct H as [h´ [H1 | H2]].
- erep.
- erep.
Qed.
diverges furnace.
Proof.
unfold diverges; intros.
pose proof (warming_up h n).
destruct H as [h´ [H1 | H2]].
- erep.
- erep.
Qed.
This page has been generated by coqdoc