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.

Section Relation.
Variable X : Type.

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

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

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

Definition reducible (r : rel) (x : X) : Prop :=
exists y, r x y.

Definition normal (r : rel) (x : X) : Prop :=
~ reducible r x.

Definition decidable (r : rel) : Prop :=
forall x, reducible r x \/ normal r x.

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.

Lemma star_transitive r x y z :
star r x y -> star r y z -> star r x z.
(* using the predicate transitive ruins the lemma for eauto *)

Proof. intros A B. induction A ; eauto using star. Qed.

End Relation.

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''.

Require Import List. (* needed for "::" notation *)

Inductive step : rel (list com * state) :=
| stepA a cs s : step (Act a :: cs, s) (cs, a s)
| stepS c1 c2 cs s : step (Seq c1 c2 :: cs, s) (c1 :: c2 :: cs, s)
| stepIT t c1 c2 cs s : t s = true -> step (If t c1 c2 :: cs, s) (c1 :: cs, s)
| stepIF t c1 c2 cs s : t s = false -> step (If t c1 c2 :: cs, s) (c2 :: cs, s)
| stepWF t c cs s : t s = false -> step (While t c :: cs, s) (cs, s)
| stepWT t c cs s : t s = true -> step (While t c :: cs, s) (c :: While t c :: cs, s).

Lemma sem2step c s s' cs :
sem c s s' -> star step (c::cs, s) (cs, s').

Proof. intros A. revert cs.
induction A ; eauto using star, step, star_transitive. Qed.

Fixpoint sem' cs s s' : Prop :=
match cs with
| nil => s = s'
| c::cr => exists s'', sem c s s'' /\ sem' cr s'' s'
end.

Lemma step2sem r r' :
star step r r' -> fst r' = nil -> sem' (fst r) (snd r) (snd r').

Proof. intros A B. induction A as [r|r r' r''].
rewrite B. reflexivity.
specialize (IHA B). inv H ; simpl in *|-*.
(* a *) exists (a s). now eauto using sem.
(* ; *) destruct IHA as [s1 [C [s2 [D E]]]]. exists s2. now eauto using sem.
(* if true *) destruct IHA as [s1 [C D]]. exists s1. now eauto using sem.
(* if false *) destruct IHA as [s1 [C D]]. exists s1. now eauto using sem.
(* while false *) exists s. now eauto using sem.
(* while true *) destruct IHA as [s1 [C [s2 [D E]]]]. exists s2. now eauto using sem.
Qed.

Theorem step_agrees c s s' :
sem c s s' <-> star step (c::nil,s) (nil,s').

Proof. split ; intros A.
now apply sem2step ; trivial.
apply step2sem in A ; trivial.
cbv in A. destruct A as [s2 [A1 A2]]. subst s2. trivial. Qed.

Goal functional step.

Proof. intros s s' s'' A B. inv A ; inv B ; congruence. Qed.

Goal decidable step.

Proof. intros [cs s]. destruct cs.
right. intros [r A]. now inv A.
left. hnf. destruct c ; eauto using step ;
rdestruct (t s) r ; eauto using step. Qed.

End abstract_Imp.