Set Implicit Arguments.

Tactic Notation "inv" hyp(A) := inversion A ; subst ; clear A.

Section Relation.
Variable X : Type.

Definition rel : Type := X -> X -> Prop.

Definition functional (r : rel) : Prop :=
forall x y z, r x y -> r x z -> y=z.

Definition rle (r r' : rel) : Prop :=
forall x y, r x y -> r' x y.

Definition req (r r' : rel) : Prop :=
rle r r' /\ rle r' r.

End Relation.

Section abstract_Imp.

Variable state : Type.

Definition action : Type := state -> state.

Definition test : Type := state -> bool.
Definition TRUE : test := fun _ => true.
Definition FALSE : test := fun _ => false.

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

Definition skip : com := Act (fun s => s).
Definition div : com := While TRUE skip.

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 terminates c s : Prop := exists s', sem c s s'.

(* forall c s, terminates c s \/ ~terminates c s 
is not provable without assumptions since termination 
is undecidable. *)

Lemma sem_functional c :
functional (sem c).

Proof. intros s s' s'' A. revert s''.
induction A ; intros s0 B ; inv B ; auto ; try congruence.
(* ; *) assert (s' = s'0) by auto. subst. now auto.
(* while true *) assert (s' =s'0) by auto. subst. auto. Qed.

Definition cle c c' : Prop := rle (sem c) (sem c').
Definition ceq c c' : Prop := req (sem c) (sem c').

Goal forall c c',
ceq c c' <-> forall s s', sem c s s' <-> sem c' s s'.

Proof. firstorder. Qed.

Goal forall c,
ceq (Seq skip c) c.

Proof. split ; intros s s' A.
inv A. inv H1. assumption.
cbv. eauto using sem. Qed.

Goal forall c1 c2 c3,
ceq (Seq c1 (Seq c2 c3)) (Seq (Seq c1 c2) c3).

Proof. split ; intros s s' A ; inv A.
inv H4. eauto using sem.
inv H1. eauto using sem. Qed.

Goal forall c1 c2,
ceq (If TRUE c1 c2) c1.

Proof. split ; intros s s' A.
inv A ; auto. discriminate.
eauto using sem. Qed.

Goal forall c,
ceq (While FALSE c) skip.

Proof. split ; intros s s' A.
inv A. now constructor. discriminate.
inv A. apply semWhileFalse. reflexivity. Qed.

Goal forall t c,
ceq (While t c) (If t (Seq c (While t c)) skip).

Proof. split ; intros s s' A.
inv A. apply semIfFalse. assumption. now constructor.
       apply semIfTrue. assumption. econstructor ; eassumption.
inv A. inv H5. eauto using sem.
       inv H5. eauto using sem. Qed.

Lemma div_terminates s :
~ terminates div s.

Proof. intros [s' A].
remember div as c. induction A ; inv Heqc.
discriminate. auto. Qed.

Goal (exists s : state, True) -> ~ ceq skip div.

Proof. intros [s _] A. apply div_terminates with (s:=s). exists s.
apply A. constructor. Qed.

Goal forall c c',
(forall s, terminates c s) -> cle c c' -> ceq c c'.

Proof. intros c c' A B. split. assumption.
intros s s' C. destruct (A s) as [s'' D].
assert (s' = s'') by (eapply sem_functional ; eauto).
congruence. Qed.

Definition monotone (f : com -> com) : Prop :=
forall c c', cle c c' -> cle (f c) (f c').

Lemma monotone_compatible (f : com -> com) c c' :
monotone f -> ceq c c' -> ceq (f c) (f c').

Proof. firstorder. Qed.

Lemma monotone_while t : monotone (While t).

Proof. intros c c' A s s' B.
remember (While t c) as r ; induction B ; inv Heqr.
apply semWhileFalse ; assumption.
eapply semWhileTrue ; eauto. Qed.

Lemma while_compatible t c c' :
ceq c c' -> ceq (While t c) (While t c').

Proof. apply monotone_compatible, monotone_while. Qed.

Fixpoint optimize (f : com -> com) (c : com) : com :=
match c with
| Act a => f (Act a)
| Seq c c' => f (Seq (optimize f c) (optimize f c'))
| If t c c' => f (If t (optimize f c) (optimize f c'))
| While t c => f (While t (optimize f c))
end.

Theorem optimization1 (f : com -> com) :
(forall c, cle c (f c)) ->
 forall c, cle c (optimize f c).

Proof.
intros A c. induction c ; simpl ; intros s s' B ; apply A ; inv B.
now apply semAct.
now eapply semSeq ; eauto.
now apply semIfTrue ; auto.
now apply semIfFalse ; auto.
now apply semWhileFalse ; assumption.
eapply semWhileTrue ; eauto. revert H5. apply monotone_while ; auto. Qed.

Theorem optimization2 (f : com -> com) :
(forall c, cle (f c) c) ->
 forall c, cle (optimize f c) c.

Proof.
intros A c. induction c ; simpl ; intros s s' B ; apply A in B ; inv B.
now apply semAct.
now eapply semSeq ; eauto.
now apply semIfTrue ; auto.
now apply semIfFalse ; auto.
now apply semWhileFalse ; assumption.
eapply semWhileTrue ; eauto. revert H5. apply monotone_while ; auto. Qed.

Theorem optimization3 (f : com -> com) :
(forall c, ceq (f c) c) ->
 forall c, ceq (optimize f c) c.

Proof. intros A c. split.
now apply optimization2 ; firstorder.
apply optimization1 ; firstorder. Qed.

End abstract_Imp.