Set Implicit Arguments.

Tactic Notation "inv" hyp(A) := inversion A ; subst ; clear A.
Tactic Notation "rdestruct" constr(t) ident(x) := remember t as x ; destruct x.

Notation "'LETOPT' x <== e1 'IN' e2" :=
  (match e1 with Some x => e2 | None => None end)
  (right associativity, at level 60).

Section abstract_Imp.

Variable state : Type.

Definition action : Type := state -> state.
Definition test : Type := state -> bool.

Inductive com : Type :=
| Act : action -> com
| Seq : com -> com -> com
| If : test -> com -> com -> com
| While : test -> com -> com.

Inductive sem : com -> state -> state -> Prop :=
| semAct a s :
  sem (Act a) s (a s)
| semSeq c1 c2 s s' s'' :
  sem c1 s s' ->
  sem c2 s' s'' ->
  sem (Seq c1 c2) s s''
| semIfTrue t c1 c2 s s' :
  t s = true ->
  sem c1 s s' ->
  sem (If t c1 c2) s s'
| semIfFalse t c1 c2 s s' :
  t s = false ->
  sem c2 s s' ->
  sem (If t c1 c2) s s'
| semWhileFalse t c s :
  t s = false ->
  sem (While t c) s s
| semWhileTrue t c s s' s'':
  t s = true ->
  sem c s s' ->
  sem (While t c) s' s'' ->
  sem (While t c) s s''.

Definition evalStep (f : com -> state -> option state)
(c : com) (s : state) : option state :=
match c with
  | Act a => Some (a s)
  | Seq c1 c2 => LETOPT s' <== f c1 s IN f c2 s'
  | If t c1 c2 => if t s then f c1 s else f c2 s
  | While t c' => if t s
    then LETOPT s' <== f c' s IN f c s'
    else Some s
end.

Definition evalN : com -> state -> option state := fun _ _ => None.

Fixpoint eval (n : nat) : com -> state -> option state :=
match n with 0 => evalN | S n' => evalStep (eval n') end.

Definition ole (c c' : state -> option state) : Prop :=
forall s s', c s = Some s' -> c' s = Some s'.

Lemma eval_monotone m n c :
m<=n -> ole (eval m c) (eval n c).

Require Import Omega.

Proof. revert n c.
induction m ; intros n c A s s' ; simpl (eval 0) ; unfold evalN.
congruence.
destruct n. exfalso ; omega.
assert (A1 : m <= n) by omega. clear A.
destruct c ; simpl.
(* a *) now trivial.
(* ; *) rdestruct (eval m c1 s) r ; try congruence.
erewrite (IHm n) ; eauto. now apply IHm ; auto.
(* if *) rdestruct (t s) r ; now firstorder.
(* while *) rdestruct (t s) r ; trivial.
rdestruct (eval m c s) r ; try congruence.
erewrite (IHm n) ; eauto. apply IHm ; trivial. Qed.

Corollary eval_monotone' m n c s s' s'' :
eval m c s = Some s' -> eval n c s = Some s'' -> s' = s''.

Proof. intros A B. assert (C : m<=n \/ n<= m) by omega. destruct C as [C|C].
assert (eval n c s = Some s') by (eapply eval_monotone ; eauto). congruence.
assert (eval m c s = Some s'') by (eapply eval_monotone ; eauto). congruence.
Qed.

Theorem eval_agrees c s s' :
sem c s s' <-> exists n, eval n c s = Some s'.

Proof. split.
(* -> *)
intros A. induction A.
(* a *) exists 1. reflexivity.
(* ; *) destruct IHA1 as [n1 IH1]. destruct IHA2 as [n2 IH2].
exists (S(n1+n2)). simpl.
erewrite eval_monotone with (m:=n1) ; eauto ; try omega.
apply eval_monotone with (m:=n2) ; auto ; omega.
(* if true *)
destruct IHA as [n IH]. exists (S n). simpl. rewrite H. assumption.
(* if false *)
destruct IHA as [n IH]. exists (S n). simpl. rewrite H. assumption.
(* while false *)
exists 1. simpl. rewrite H. reflexivity.
(* while true *)
destruct IHA1 as [n1 IH1]. destruct IHA2 as [n2 IH2].
exists (S(n1+n2)). simpl. rewrite H.
erewrite eval_monotone with (m:=n1) ; eauto ; try omega.
eapply eval_monotone with (m:=n2) ; auto ; omega.
(* <- *)
intros [n A]. revert c s s' A. induction n. intros ; discriminate.
destruct c ; simpl ; intros s s' A ; inv A.
(* a *) now constructor.
(* ; *) rdestruct (eval n c1 s) o ; (eauto using semSeq || congruence).
(* if *) rdestruct (t s) b ; auto using semIfTrue, semIfFalse.
(* while *) rdestruct (t s) b. rdestruct (eval n c s) o ; try congruence.
   now eauto using semWhileTrue.
   inv H0. auto using semWhileFalse. Qed.

Corollary eval_agrees_divergence c s :
~ (exists s', sem c s s') <-> forall n, eval n c s = None.

Proof. split.
intros A n. rdestruct (eval n c s) r ; trivial. exfalso.
   apply A. exists s0. apply eval_agrees. exists n. now trivial.
intros A [s' B]. apply eval_agrees in B. destruct B as [n C].
assert (eval n c s = None) by auto.
congruence. Qed.

Fixpoint iter (n : nat) {X : Type} (f : X -> X) (x : X) : X :=
match n with
| O => x
| S n' => f (iter n' f x)
end.

Goal forall n c s, eval n c s = iter n evalStep evalN c s.

Proof. induction n ; simpl. reflexivity.
(* destruct c needed because of lack of extensionality *)
destruct c ; intros s ; simpl.
(* a *) reflexivity.
(* ; *) rewrite <-IHn. now destruct (eval n c1 s) ; trivial.
(* if *) rewrite IHn, IHn ; reflexivity.
(* while *) rewrite <-IHn. destruct (eval n c s) ; trivial.
rewrite IHn. reflexivity. Qed.

End abstract_Imp.