(*** Hoare Logic : Assignment 09 ***) Set Implicit Arguments. Tactic Notation "inv" hyp(A) := inversion A ; subst ; clear A. 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 assn : Type := state -> Prop. Definition Hoare (P : assn) (c : com) (Q : assn) : Prop := forall s s', P s -> sem c s s' -> Q s'. Inductive hoare : assn -> com -> assn -> Prop := | hoareAct a Q : hoare (fun s => Q (a s)) (Act a) Q | hoareS c1 c2 P Q R : hoare P c1 R -> hoare R c2 Q -> hoare P (Seq c1 c2) Q | hoareIf t c1 c2 P Q : hoare (fun s => P s /\ t s = true) c1 Q -> hoare (fun s => P s /\ t s = false) c2 Q -> hoare P (If t c1 c2) Q | hoareWhile t c P : hoare (fun s => P s /\ t s = true) c P -> hoare P (While t c) (fun s => P s /\ t s = false) | hoareConsequence c (P P' Q Q' : assn) : hoare P c Q -> (forall s, P' s -> P s) -> (forall s, Q s -> Q' s) -> hoare P' c Q'. (*** Exercise 9.9 ***) Goal forall P Q, Hoare P div Q. Admitted. Goal forall P Q, hoare P div Q. Admitted. End abstract_Imp.