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.

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.

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.

Lemma star_expansive r :
rle r (star r).

Proof. hnf. eauto using star. Qed.
Lemma star_right r x y z :
star r x y -> r y z -> star r x z.

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 :=
| Skip : com
| Act : action -> com
| Seq : com -> com -> com
| If : test -> com -> com -> com
| While : test -> com -> com.

Inductive sem : com -> state -> state -> Prop :=
| semSkip s : sem Skip s s
| 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 step : rel (com * state) :=
| stepA a s :
  step (Act a, s) (Skip, a s)
| stepSS c s :
  step (Seq Skip c, s) (c, s)
| stepSD c1 c1' c2 s s' :
  step (c1, s) (c1', s') ->
  step (Seq c1 c2, s) (Seq c1' c2, s')
| stepIT t c1 c2 s :
  t s = true ->
  step (If t c1 c2, s) (c1, s)
| stepIF t c1 c2 s :
  t s = false ->
  step (If t c1 c2, s) (c2, s)
| stepWF t c s :
  t s = false ->
  step (While t c, s) (Skip, s)
| stepWT t c s :
  t s = true ->
  step (While t c, s) (Seq c (While t c), s).

Lemma step_adjoin r r' c' :
star step r r' ->
star step (Seq (fst r) c', snd r) (Seq (fst r') c', (snd r')).

Proof. intros A. induction A. now apply starR.
destruct x as [c s]. destruct y as [c1 s1].
eauto using star, step. Qed.

Lemma step_adjoin_skip c s s' c' :
star step (c,s) (Skip,s') -> star step (Seq c c',s) (c',s').

Proof. intros A.
apply step_adjoin with (c':=c') in A. simpl in A.
eauto using star_right, stepSS. Qed.

Lemma sem_step c s s' :
sem c s s' -> star step (c, s) (Skip, s').

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

Lemma step_compatible c c' s s' s'' :
step (c,s) (c',s') -> sem c' s' s'' -> sem c s s''.

Proof. revert c' s''.
induction c ; intros c' s'' A B ; inv A ; inv B ;
(* we have 25 cases now *) eauto using sem. Qed.

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

Proof. intros A B.
induction A as [[c s]|[c s] [c' s'] r''] ; simpl in *|-*.
rewrite B. now apply semSkip.
eauto using step_compatible. Qed.

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

Proof. split. now apply sem_step.
intros A. apply step2sem in A ; auto. Qed.

Goal functional step.

Proof. intros r r' r'' A B. revert r'' B.
induction A ; intros r'' B ; inv B ; try congruence.
inv H3. inv A. apply IHA in H3. congruence. Qed.

Lemma skip_eq c :
c = Skip \/ c <> Skip.

Proof. destruct c ; auto ; right ; intros A ; inversion A. Qed.

Lemma progress c s :
c <> Skip -> reducible step (c,s).

Proof with now eauto using step. intros A. hnf. induction c.
(* Skip *) congruence.
(* a *) trivial...
(* ; *) destruct (skip_eq c1). subst...
    destruct (IHc1 H) as [[c' s'] B]...
(* if *) rdestruct (t s) b.
    destruct (skip_eq c1). subst...
    destruct (IHc1 H) as [[c' s'] B]...
    destruct (skip_eq c2). subst...
    destruct (IHc2 H) as [[c' s'] B]...
(* while *) rdestruct (t s) b.
    destruct (skip_eq c). subst...
    destruct (IHc H) as [[c' s'] B]...
    trivial...
Qed.

Lemma step_normal c s :
normal step (c,s) <-> c = Skip.

Proof. split ; intros A.
destruct (skip_eq c). now trivial.
exfalso. apply A. apply progress ; assumption.
(* <- *) subst. intros [r A]. inversion A. Qed.

Goal decidable step.

Proof. intros [c s]. destruct (skip_eq c).
right. apply step_normal. assumption.
left. apply progress. assumption. Qed.

End abstract_Imp.