(* Hoare logic in Coq *)

Require Export Arith Omega. 
Ltac sinv h := (inversion h; clear h; subst).  (* a useful tactic *)

(** Syntax of IMP *)

(* Identifiers / Locations *)
Inductive loc : Type := 
  Loc : nat -> loc.

Definition beq_loc l1 l2 :=
  match (l1, l2) with
    (Loc n1, Loc n2) => beq_nat n1 n2
  end.

Theorem beq_loc_refl : forall i,
  true = beq_loc i i.
Proof.
  intros. destruct i.
  unfold beq_loc. apply beq_nat_refl. Qed.

(* Arithmetic expressions *) 
Inductive aexp : Type := 
  | ANum : nat -> aexp
  | AId : loc -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp.

(* Boolean expressions *)
Inductive bexp : Type := 
  | BTrue : bexp
  | BFalse : bexp
  | BEq : aexp -> aexp -> bexp
  | BLe : aexp -> aexp -> bexp
  | BNot : bexp -> bexp
  | BAnd : bexp -> bexp -> bexp
  | BOr : bexp -> bexp -> bexp.

(* Commands *)
Inductive com : Type :=
  | CSkip : com
  | CAss : loc -> aexp -> com
  | CSeq : com -> com -> com
  | CIf : bexp -> com -> com -> com
  | CWhile : bexp -> com -> com.


(** Semantics of IMP *)

(* States *)
Definition state := loc -> nat.

Definition initial_state : state := fun _ => 0.

Definition update (st : state) (X:loc) (n : nat) :=
  fun Y => if beq_loc X Y then n else st Y.

Theorem update_eq : forall n X st,
  (update st X n) X = n.
Proof.
  intros n V st.
  unfold update.
  destruct V. unfold beq_loc.
  rewrite <- beq_nat_refl.
  reflexivity.
Qed.

Theorem update_neq : forall n1 n2 X1 X2 st,
  st X1 = n1 ->
  beq_loc X2 X1 = false ->
  (update st X2 n2) X1 = n1.
Proof.
  intros n1 n2 X1 X2 st H1 H2. 
  unfold update. rewrite H2. assumption. 
Qed. 

(* interpretation of arithmetic expressions *)
Fixpoint aeval (e : aexp) (st : state) {struct e} : nat :=
  match e with
  | ANum n => n
  | AId i => st i
  | APlus a1 a2 => plus (aeval a1 st) (aeval a2 st)
  | AMinus a1 a2 => minus (aeval a1 st) (aeval a2 st)
  | AMult a1 a2 => mult (aeval a1 st) (aeval a2 st)
  end.

(* interpretation of boolean expressions *)

Fixpoint ble_nat (n m : nat) {struct n} : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => ble_nat n' m'
      end
  end.

Fixpoint beval (e : bexp) (st : state) {struct e} : bool :=
  match e with 
  | BTrue => true
  | BFalse => false
  | BEq a1 a2 => beq_nat (aeval a1 st) (aeval a2 st)
  | BLe a1 a2 => ble_nat (aeval a1 st) (aeval a2 st)
  | BNot b1 => negb (beval b1 st)
  | BAnd b1 b2 => andb (beval b1 st) (beval b2 st)
  | BOr b1 b2 => orb (beval b1 st) (beval b2 st)
  end.

(* evaluation of commands *) 
Inductive ceval : com -> state -> state -> Prop :=
  | CESkip : forall st,
      ceval CSkip st st
  | CEAss : forall st a X,
      ceval (CAss X a) st (update st X (aeval a st))
  | CESeq : forall c1 c2 st st' st'',
      ceval c1 st st' -> 
      ceval c2 st' st'' ->
      ceval (CSeq c1 c2) st st'' 
  | CEIfTrue : forall st st' b1 c1 c2,
      beval b1 st = true ->
      ceval c1 st st' ->
      ceval (CIf b1 c1 c2) st st'
  | CEIfFalse : forall st st' b1 c1 c2,
      beval b1 st = false ->
      ceval c2 st st' ->
      ceval (CIf b1 c1 c2) st st'
  | CEWhileEnd : forall b1 st c1,
      beval b1 st = false ->
      ceval (CWhile b1 c1) st st
  | CEWhileLoop : forall st st' st'' b1 c1,
      beval b1 st = true ->
      ceval c1 st st' ->
      ceval (CWhile b1 c1) st' st'' ->
      ceval (CWhile b1 c1) st st''. 

(* Assertions *)
Definition assn := state -> Prop.

(* Embedding bexp in Prop *)
Definition bassn b : assn :=
  fun st => beval b st = true.

Lemma bexp_eval_true : forall b st,
  beval b st = true -> (bassn b) st.
Proof.
  intros b st Hbe. unfold bassn. assumption. 
Qed.

Lemma bexp_eval_false : forall b st,
  beval b st = false -> ~ ((bassn b) st).
Proof.
  intros b st Hbe contra.
  unfold bassn in contra.
  rewrite -> contra in Hbe. inversion Hbe. 
Qed.

(* Hoare triples *)
Definition hoare_triple (p:assn) (c:com) (q:assn) : Prop :=
  forall st st', 
       ceval c st st' -> p st -> q st'.

Notation "{{ p }} c {{ q }}" := (hoare_triple p c q) (at level 90).
Hint Unfold hoare_triple. 

(* Proof rule for skip *)
Theorem hoare_skip : forall p,
     {{p}} CSkip {{p}}.
Proof.
  unfold hoare_triple. intros p st st' H HP. sinv H. assumption. 
Qed.

(* Proof rule for assignment *)
Theorem hoare_asgn : forall p X a,
  {{ fun st => p(update st X (aeval a st)) }} (CAss X a) {{p}}.
Proof.
  unfold hoare_triple.
  intros p V a st st' HE HP.
  sinv HE. assumption. 
Qed. 

(* Proof rule for sequencing *)
Theorem hoare_seq : forall p q r c1 c2,
     {{r}} c2 {{q}}
  -> {{p}} c1 {{r}}
  -> {{p}} CSeq c1 c2 {{q}}.
Proof.
  unfold hoare_triple.
  intros p q r c1 c2 H1 H2 st st' H12 Pre. sinv H12.
  apply (H1 st'0 st'); try assumption.
  apply (H2 st st'0); try assumption. Qed.

(* Proof rule for conditionals *)
Theorem hoare_if : forall p q b c1 c2,
  {{fun st => p st /\ bassn b st}} c1 {{q}} ->
  {{fun st => p st /\ ~(bassn b st)}} c2 {{q}} ->
  {{p}} (CIf b c1 c2) {{q}}.
Proof with auto.
  unfold hoare_triple.
  intros p q b c1 c2 HTrue HFalse st st' HE HP. sinv HE. 
(* Case b is true *)
    apply (HTrue st st')...
(* Case b is false *)
    apply (HFalse st st')...
    split... apply bexp_eval_false... 
Qed.

(* Proof rule for loops *)
Theorem hoare_while : forall p b c,
  {{fun st => p st /\ bassn b st}} c {{p}} ->
  {{p}} (CWhile b c) {{fun st => p st /\ ~ (bassn b st)}}.
Proof with auto.
  unfold hoare_triple.
  intros p b c Hhoare st st' He HP.
  (* we reason by induction on He, since the hypothesis of the 
      evaluation rule for loops contains the loop again. See the lecture
      notes for a pen-and-paper proof *)
  remember (CWhile b c) as wcom.
  induction He; try (sinv Heqwcom).
(* Case b is false *)
    split... apply bexp_eval_false in H...
(* Case b is true *) 
    destruct IHHe2 as [HP' Hbfalse']...
    apply (Hhoare st st')...
Qed. 

(* Consequence rules *)
Theorem hoare_consequence : forall (p p' q q' : assn) c,
  {{p'}} c {{q'}} ->
  (forall st, p st -> p' st) ->
  (forall st, q' st -> q st) ->
  {{p}} c {{q}}.
Proof with auto.
  unfold hoare_triple. 
  intros p p' q q' c Hht HPP' HQ'Q.
  intros st st' Hc HP.
  apply HQ'Q. apply (Hht st st')... 
Qed. 

Theorem hoare_consequence_pre : forall (p p' q : assn) c,
  {{p'}} c {{q}} ->
  (forall st, p st -> p' st) ->
  {{p}} c {{q}}.
Proof with auto.
  intros p p' q c Hhoare Himp.
  apply hoare_consequence with (p' := p') (q' := q)...
Qed. 

Theorem hoare_consequence_post : forall (p q q' : assn) c,
  {{p}} c {{q'}} ->
  (forall st, q' st -> q st) ->
  {{p}} c {{q}}.
Proof with auto.
  intros p q q' c Hhoare Himp.
  apply hoare_consequence with (p' := p) (q' := q')...
Qed. 




(** Exercise 10.2(a) conjunction rule *)
Theorem hoare_conjunction : 


(** Exercise 10.2(a) conjunction rule *)
Theorem hoare_disjunction :