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 normal (r : rel) (x : X) : Prop := ~ exists y, r x y. Definition functional (r : rel) : Prop := forall s s' s'', r s s' -> r s s'' -> s'=s''. Inductive star (r : rel) : rel := | starR s : star r s s | starS s s' s'' : r s s' -> star r s' s'' -> star r s s''. Lemma star_transitive r x y z : star r x y -> star r y z -> star r x z. Proof. intros A B. induction A ; 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. Implicit Arguments functional [X]. Implicit Arguments star [X]. Implicit Arguments normal [X]. 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. Admitted. Lemma step_adjoin_skip c s s' c' : star step (c,s) (Skip,s') -> star step (Seq c c',s) (c',s'). Proof. Admitted. Lemma sem_step c s s' : sem c s s' -> star step (c, s) (Skip, s'). Proof. intros A. induction A. Admitted. 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. Admitted. 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 *|-*. Admitted. Theorem step_agrees c s s' : sem c s s' <-> star step (c,s) (Skip,s'). Proof. Admitted. 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 -> exists r, step (c,s) r. Proof with now eauto using step. intros A. 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. End abstract_Imp.