Set Implicit Arguments.

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.

Inductive star (r : rel) : rel :=
| starR x : star r x x
| starS x y z : r x y -> star r y z -> star r x z.
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''.

Inductive exp : Type :=
| Actn : action -> exp
| Test : test -> exp
| Comp : exp -> exp -> exp
| Plus : exp -> exp -> exp
| Star : exp -> exp.

Fixpoint den (e : exp) (s s' : state) : Prop :=
match e with
| Actn a => a s = s'
| Test t => t s = true /\ s = s'
| Comp e1 e2 => exists s0, den e1 s s0 /\ den e2 s0 s'
| Plus e1 e2 => den e1 s s' \/ den e2 s s'
| Star e => star (den e) s s'
end.

Goal forall a1 a2, (exists s, a1 s <> a2 s) ->
~ functional (den (Plus (Actn a1) (Actn a2))).

Proof. cbv. firstorder. Qed.

Definition negt : test -> test := fun t s => negb (t s).

Fixpoint compile (c : com) : exp :=
match c with
| Act a => Actn a
| Seq c1 c2 => Comp (compile c1) (compile c2)
| If t c1 c2 => Plus (Comp (Test t) (compile c1))
                     (Comp (Test (negt t)) (compile c2))
| While t c' => Comp (Star (Comp (Test t) (compile c'))) (Test (negt t))
end.

Lemma negteq t s :
t s = false <-> negt t s = true.

Proof. cbv. firstorder ; destruct (t s) ; congruence. Qed.

Theorem correctness c :
req (sem c) (den (compile c)).

Proof. split.
(* -> *)
intros s s' A. induction A ; firstorder using negteq.
(* WhileFalse *) simpl. now firstorder using negteq, star.
(* WhileTrue *) subst ; simpl. exists s'' ; firstorder. now eauto using star.
 (* <- *)
induction c ; simpl ; intros s s' A.
(* a *) rewrite <- A. now constructor.
(* ; *) now firstorder ; eauto using sem.
(* if *) firstorder.
   subst x. now eauto using sem.
   subst x. now firstorder using sem, negteq.
(* while *) firstorder. subst. induction H.
   now firstorder using semWhileFalse, negteq.
   firstorder. subst x. eauto using semWhileTrue. Qed.

End abstract_Imp.