(* Projet Coq - WP - MPRI 2.7.1 *)

(***** Partie 1 : definition de While ****************************************)

Require Import ZArith.BinInt.
Require Import FunctionalExtensionality.
Require Import Omega.
Import Z.

Definition Var := nat.
Definition Mem := Var -> Z.
Definition Expr:= Mem -> Z.

Inductive SynAssert : Type:=
| ATop: SynAssert
| ABot: SynAssert
| ANeg: SynAssert -> SynAssert
| AAnd: SynAssert -> SynAssert -> SynAssert
| AOr: SynAssert -> SynAssert -> SynAssert
| AImplies: SynAssert -> SynAssert -> SynAssert
| AExpr: Expr -> SynAssert
| AForall: Var -> SynAssert -> SynAssert
| AExists: Var -> SynAssert -> SynAssert
| ASubstZ: Var -> Z -> SynAssert -> SynAssert
| ASubstE: Var -> Expr -> SynAssert -> SynAssert.

Inductive Instr : Type :=
| skip: Instr
| abort: Instr
| assign: Var -> Expr -> Instr
| seq: Instr -> Instr -> Instr
| ifelse: Expr -> Instr -> Instr -> Instr
| while: SynAssert -> Expr -> Instr -> Instr.

Definition ifonly (exp: Expr) (inst: Instr) : Instr :=
  ifelse exp inst skip.

(***** CPO *******************************************************************)

Fixpoint nat_eq x y :=
  match x, y with
  | 0, 0 => true
  | 0, S _ => false
  | S _, 0 => false
  | S x0, S y0 => nat_eq x0 y0
  end.

Definition Sequence (S: Type) := nat -> S.

Inductive cpo (T: Type): Type :=
| CpoError: (cpo T)
| CpoElem: T -> (cpo T).

Definition cpo_leq: forall (T: Type), cpo T -> cpo T -> Prop :=
  fun T x y => match x, y with
  | CpoError _, _ => True
  | CpoElem _ x0, CpoElem _ y0 => x0 = y0
  | _, _ => False
  end.
Arguments cpo_leq {T} _ _.
Infix "cpo<=" := cpo_leq (at level 100).

Definition is_chain: forall (T: Type), Sequence (cpo T) -> Prop :=
  fun T chain => forall (n: nat), (chain n) cpo<= (chain (S n)).
Arguments is_chain {T} _.

Definition is_lub_of: forall (T: Type), Sequence (cpo T) -> cpo T -> Prop :=
  fun T chain elt => forall (n: nat), (chain n) cpo<= elt.
Arguments is_lub_of {T} _ _.

Axiom find_lub: forall (T: Type), Sequence (cpo T) -> cpo T.
Arguments find_lub {T} _.

Axiom find_lub_correct:
  forall (T: Type), forall (chain: Sequence (cpo T)),
  is_chain chain -> is_lub_of chain (find_lub chain).
Arguments find_lub_correct {T} {chain} _.

Axiom lub_is_first_correct:
  forall (T: Type), forall (n: nat), forall (chain: Sequence (cpo T)),
  is_chain chain
  -> chain n = CpoError T
  -> chain (S n) <> CpoError T
  -> find_lub chain = chain (S n).
(***** Interpretation ********************************************************)

Definition subst: Mem -> Var -> Z -> Mem :=
  fun (m: Mem) (v: Var) (z: Z) (v2: Var) =>
    if nat_eq v v2 then z else m v2.
Notation "m [ x <- z ]" := (subst m x z) (at level 50, left associativity).

Definition MemCpo := cpo Mem.
Definition MemError := CpoError Mem.
Definition MemElem := CpoElem Mem.

Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
  match mem with
  | CpoError _ => MemError
  | CpoElem _ mem0 =>
    match inst with
    | skip => MemElem mem0
    | abort => MemError
    | assign v e => (MemElem (mem0 [v <- (e mem0)]))
    | seq instr1 instr2 => interp instr2 (interp instr1 (MemElem mem0))
    | ifelse guard instrIf instrElse =>
      if ((guard mem0) =? 0) % Z
        then interp instrElse mem
        else interp instrIf mem
    | while _ guard body =>
      let fix while_chain (mem: MemCpo) (n: nat): MemCpo :=
        match n with
        | 0 => mem
        | S m =>
          match while_chain (MemElem mem0) m with
          | CpoError _ => MemError
          | CpoElem _ submem =>
            if ((guard submem) =? 0) % Z
              then interp body (MemElem submem)
              else mem
          end
        end
      in find_lub (fun n =>
        match while_chain (MemElem mem0) n with
        | CpoError _ => MemError
        | CpoElem _ submem =>
          if ((guard submem) =? 0) % Z
            then MemError
            else MemElem submem
        end)
    end
  end.

Fixpoint nth_iterate (instr: Instr) (n: nat) : Instr :=
  match n with
  | 0 => skip
  | S m => seq (nth_iterate instr m) instr
  end.

Definition satisfies_expr (mem: MemCpo) (expr: Expr) : Prop := match mem with
| CpoError _ => False
| CpoElem _ mem0 => (expr mem0 <> 0) % Z
end.
Infix "|=e" := satisfies_expr (at level 32).

Definition expr_neg (expr: Expr) : Expr :=
  fun mem => match expr mem with
  | 0%Z => 1%Z
  | _ => 0%Z
  end.

Lemma certain_termination_exists assert body guard mem :
  interp (while assert guard body) mem <> MemError ->
    exists n: nat,
      interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard.
Proof.
  intros noError.
Admitted.

Lemma certain_termination_exists_minimal assert body guard mem :
  interp (while assert guard body) mem <> MemError ->
    exists n: nat,
      (forall p: nat, p < n ->
        interp (nth_iterate (ifonly guard body) p) mem |=e guard)
     /\ interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard.
Proof.
  intros not_error.
Admitted.

Lemma unfold_one_iter (s: Instr) (m: Mem) (n: nat):
  interp (nth_iterate s (S n)) (MemElem m)
  = interp s (interp (nth_iterate s n) (MemElem m)).
Proof.
  simpl; congruence.
Qed.

Lemma bool_prop_contradict {x: Z}:
  (x <> 0)%Z -> (x =? 0)%Z = true -> False.
Proof.
  intros diff equ. apply diff.
  unfold eqb in equ; destruct x; simpl; trivial;
    exfalso; apply (Bool.Bool.diff_false_true); assumption.
Qed.

Lemma before_n_useless_guard {body guard n mem}:
  (forall p, p < n
    -> (interp (nth_iterate (ifonly guard body) p) mem) |=e guard)
  -> forall p, p <= n ->
    (interp (nth_iterate body p) mem)
    = (interp (nth_iterate (ifonly guard body) p) mem).
Proof.
  intros matchGuard p infN.
  induction p.
  - unfold nth_iterate; trivial.
  - assert (p < n). omega. assert (p <= n). omega.
    apply IHp in H0 as IHp0.
    destruct mem eqn:mRel; [simpl; trivial | ].
    fold MemElem; rewrite (unfold_one_iter body m p);
      rewrite (unfold_one_iter (ifonly guard body) m p).
    fold MemElem in IHp0; rewrite IHp0.
    remember (interp (nth_iterate body p) (MemElem m))
      as stepMem eqn:stepMemRel.
    remember (interp (nth_iterate (ifonly guard body) p) (MemElem m))
      as fancyStepMem eqn:fancyStepMemRel.
    specialize matchGuard with p.
    apply matchGuard in H as matchGuardP.
    fold MemElem in matchGuardP.
    rewrite <- fancyStepMemRel in matchGuardP.
    rewrite <- IHp0 in matchGuardP.
    destruct fancyStepMem.
    * destruct body; simpl; trivial.
    * unfold satisfies_expr in matchGuardP.
      destruct (guard m0 =? 0)%Z eqn:guardRel.
      + rewrite IHp0 in matchGuardP.
        exfalso; apply (bool_prop_contradict matchGuardP guardRel).
      + unfold ifonly; simpl; rewrite guardRel; congruence.
Qed.

Lemma certain_termination assert body guard mem :
  interp (while assert guard body) mem <> MemError ->
    exists n: nat,
      (interp (nth_iterate body n) mem) |=e (expr_neg guard)
     /\ (forall p, p < n -> (interp (nth_iterate body p) mem) |=e guard)
     /\ interp (while assert guard body) mem = interp (nth_iterate body n) mem.
Proof.
  intros notError.
  destruct (certain_termination_exists_minimal assert body guard mem) as [n];
    trivial.
  destruct H as [beforeN atN].
  exists n.
  split; [|split].
  - assert (n <= n). omega. rewrite (before_n_useless_guard beforeN n H).
    assumption.
  - intros p infN. assert (p <= n). omega.
    rewrite (before_n_useless_guard beforeN p H ).
    apply beforeN; trivial.
  - admit.
Admitted.

(***** Validite, prouvabilite pour Hoare *************************************)

Definition Assert := Mem -> Prop.
Delimit Scope assert with assert.

Definition assertTop : Assert := fun _ => True.
Definition assertBot : Assert := fun _ => False.

Definition assertNot : Assert -> Assert :=
  fun orig mem => ~ (orig mem).
Notation "~ x" := (assertNot x) (at level 75, right associativity) : assert.
Definition assertAnd : Assert -> Assert -> Assert :=
  fun x1 x2 mem => (x1 mem) /\ (x2 mem).
Infix "/\" := assertAnd : assert.
Definition assertOr : Assert -> Assert -> Assert :=
  fun x1 x2 mem => (x1 mem) \/ (x2 mem).
Infix "\/" := assertOr : assert.
Definition assertImpl : Assert -> Assert -> Assert :=
  fun x1 x2 => (~x1 \/ x2) % assert.
Infix "->" := assertImpl : assert.
Definition assertForall : Var -> Assert -> Assert :=
  fun ident asser mem => forall (z: Z), asser (mem [ident <- z]).
Notation "\-/ x" := (assertForall x) (at level 90, no associativity) : assert.
Definition existsForall : Var -> Assert -> Assert :=
  fun ident asser mem => exists (z: Z), asser (mem [ident <- z]).
Notation "'exists' x" := (existsForall x)
  (at level 87, no associativity): assert.
Definition assertMemForall : Assert -> Assert :=
  fun asser mem => forall (mem: Mem), asser mem.
Notation "'\-/m' x" := (assertMemForall x)
  (at level 90, no associativity): assert.
Definition existsMemForall : Assert -> Assert :=
  fun asser mem => exists (mem: Mem), asser mem.
Notation "'exists_m' x" := (existsMemForall x)
  (at level 87, no associativity): assert.

Definition substAssert : Assert -> Var -> Z -> Assert :=
  fun asser ident val mem => asser (mem [ident <- val]).
Notation "a [[ x <- z ]]" := (substAssert a x z)
  (at level 50, left associativity).
Definition substAssertExpr : Assert -> Var -> Expr -> Assert :=
  fun asser ident expr mem => asser (mem [ident <- (expr mem)]).
Notation "a [[ x <- 'expr' z ]]" := (substAssertExpr a x z)
  (at level 50, left associativity).

Definition assertOfExpr : Expr -> Assert :=
  fun expr mem => (expr mem <> 0)%Z.

Definition assertImplLogical (a1 a2: Assert): Prop :=
  forall (m: Mem), (a1 m) -> (a2 m).


(***** Hoare provability *****************************************************)

Reserved Notation "|- [| x |] y [| z |]" (at level 30).

Inductive hoare_provability : Assert -> Instr -> Assert -> Prop :=
  | H_skip: forall pre, hoare_provability pre skip pre
  | H_abort: forall pre, forall post, hoare_provability pre abort post
  | H_assign: forall post, forall (x: Var), forall (e: Expr),
    (|- [| post [[ x <- expr e ]] |] (assign x e) [| post |]) % assert
  | H_conseq:
    forall pre, forall post,
    forall pre', forall post',
    forall s,
    (|- [| pre' |] s [| post' |]) % assert ->
      (assertImplLogical pre pre') ->
      (assertImplLogical post' post) ->
      (|- [| pre |] s [| post |]) % assert
  | H_seq:
    forall pre, forall mid, forall post, forall s1, forall s2,
    (|- [|pre|] s1 [|mid|]) % assert ->
      (|- [|mid|] s2 [|post|]) % assert ->
      (|- [|pre|] (seq s1 s2) [|post|]) % assert
  | H_if:
    forall pre, forall post, forall expr, forall sIf, forall sElse,
    (|- [| pre /\ (assertOfExpr expr) |] sIf [| post |]) % assert ->
      (|- [| pre /\ ~(assertOfExpr expr) |] sElse [| post |]) % assert ->
      (|- [| pre |] (ifelse expr sIf sElse) [| post |]) % assert
  | H_while:
    forall inv assert expr sBody,
    (|- [| inv /\ (assertOfExpr expr) |] sBody [| inv |]) % assert ->
      (|- [| inv |] (while assert expr sBody)
          [| inv /\ ~ (assertOfExpr expr) |]) % assert
where "|- [| pre  |] instr  [| post |]" :=
    (hoare_provability pre instr post) : assert.

(***** Hoare: provability implies consequence ********************************)

Definition conseq_or_bottom (y: Assert) (m: MemCpo) :=
  match m with
  | CpoError _ => True
  | CpoElem _ m0 => y m0
  end.

Definition hoare_consequence (pre: Assert) (instr: Instr) (post: Assert) :=
  forall mem: Mem,
  (pre mem) -> (conseq_or_bottom post (interp instr (MemElem mem))).

Notation "|= [| pre  |] instr  [| post |]" :=
    (hoare_consequence pre instr post) (at level 30): assert.

Lemma weaken_in_conseq:
  forall a1, forall a2, forall m,
  assertImplLogical a1 a2 -> conseq_or_bottom a1 m ->
    conseq_or_bottom a2 m.
Proof.
  intros a1 a2 m impl conseq. destruct m.
  - apply conseq.
  - simpl. unfold assertImplLogical in impl. apply (impl m). apply conseq.
Qed.

Lemma interp_of_error (s: Instr):
  interp s (MemError) = MemError.
Proof.
  unfold MemError. destruct s; cbv; trivial.
Qed.

Lemma conseq_or_bottom_is_conseq (y: Assert) (m: Mem) :
  conseq_or_bottom y (MemElem m) -> y m.
Proof.
  intros src; unfold conseq_or_bottom; simpl; trivial.
Qed.

Lemma error_leads_to_no_success s:
  forall m, interp s MemError <> MemElem m.
Proof.
  intros mem. unfold interp; destruct s; simpl ;
    unfold MemElem; unfold MemError; congruence.
Qed.

Lemma expr_neg_consistency (expr: Expr):
  forall mem, expr_neg expr mem <> 0%Z -> (~ assertOfExpr expr)%assert mem.
Proof.
  intros mem. intros src.
  unfold assertNot. unfold assertOfExpr. destruct (expr mem) eqn:exprRel.
  + congruence.
  + elimtype False.
    unfold expr_neg in src; rewrite exprRel in src. apply src.
    congruence.
  + elimtype False.
    unfold expr_neg in src; rewrite exprRel in src. apply src.
    congruence.
Qed.

Lemma Sn_noerror_n_noerror (n: nat) (s: Instr) (sMem: Mem) (m: Mem):
  interp (nth_iterate s (S n)) (MemElem sMem)  = MemElem m
  -> exists m0, interp (nth_iterate s n) (MemElem sMem) = MemElem m0
     /\ interp s (MemElem m0) = MemElem m.
Proof.
  intro HSn.
  destruct (interp (nth_iterate s n) (MemElem sMem)) eqn:nRel.
  - rewrite (unfold_one_iter s sMem n) in HSn.
    rewrite nRel in HSn. apply error_leads_to_no_success in HSn.
    elimtype False. apply HSn.
  - exists m0; unfold MemElem. split.
    * trivial.
    * rewrite <- nRel; simpl. apply HSn.
Qed.


Lemma greater_n_noerror (n1 n2: nat) (s: Instr) (sMem: Mem) (m: Mem):
  n1 < n2
  -> interp (nth_iterate s n2) (MemElem sMem) = MemElem m
  -> exists m0, interp (nth_iterate s n1) (MemElem sMem) = MemElem m0.
Proof.
  intros nRel eventuallySound.
  assert (forall nDecr, nDecr <= n2 - n1 ->
    exists m0,
    interp (nth_iterate s (n2 - nDecr)) (MemElem sMem) = MemElem m0).
    * intros mDecr mDecrRel. induction mDecr.
      + exists m.
        assert (n2 = n2 - 0).
        { unfold Nat.sub. destruct n2; trivial. }
        { rewrite <- H. assumption. }
      + assert (mDecr <= n2 - n1).
        { omega. }
        { elim (IHmDecr H). intros memNext memNextRel.
          elim (Sn_noerror_n_noerror (n2 - (S mDecr)) s sMem memNext).
          intros memNow [memNowRel memNowInterp].
          exists memNow. apply memNowRel.
          assert (S (n2 - S mDecr) = n2 - mDecr). omega.
          rewrite H0. apply memNextRel.
        }
    * assert (n2 - n1 <= n2 - n1). omega. elim (H (n2 - n1) H0).
      intros memRes memResRel. exists memRes.
      assert (n2 - (n2 - n1) = n1). omega. rewrite H1 in memResRel.
      assumption.
Qed.

Lemma unwrap_CpoElem (T: Type) :
  forall m1 m2, CpoElem T m1 = CpoElem T m2 -> m1 = m2.
Proof.
  intros m1 m2 cpoEq. congruence.
Qed.

Theorem hoare_provability_implies_consequence :
  forall (pre: Assert), forall (s: Instr), forall (post: Assert),
  ( |- [| pre |] s [| post |] ) % assert
      -> ( |= [| pre |] s [| post |] ) % assert.
Proof.
  intros pre instr post. intros deduction.
  induction deduction; intros mem preInMem.
  - exact preInMem.
  - simpl; trivial.
  - exact preInMem.
  - apply (weaken_in_conseq post' post (interp s (MemElem mem)) H0).
    apply IHdeduction. apply H. exact preInMem.
  - simpl; destruct (interp s1 (MemElem mem)) eqn:mRel.
    * fold MemError. rewrite (interp_of_error s2); simpl; trivial.
    * apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
      specialize IHdeduction1 with mem as IH1_mem.
      rewrite mRel in IH1_mem. apply IH1_mem. assumption.
  - simpl; destruct (expr mem =? 0)%Z eqn:branchEqn.
    * apply (IHdeduction2 mem). unfold assertOfExpr.
      unfold assertAnd. split.
      + assumption.
      + unfold assertNot. rewrite <- Z.eqb_eq. congruence.
    * apply (IHdeduction1 mem). unfold assertOfExpr.
      unfold assertAnd. split.
      + assumption.
      + rewrite <- Z.eqb_eq. congruence.
  - unfold conseq_or_bottom.
    destruct (interp (while assert expr sBody) (MemElem mem)) eqn:interpRel.
    * trivial.
    * elim (certain_termination assert sBody expr (MemElem mem)).
      intros n [lastIter [notLastIter isWhile] ].
      rewrite isWhile in interpRel.
      destruct n.
      {
        simpl in lastIter. simpl in interpRel; unfold MemElem in interpRel.
        unfold assertAnd. apply (unwrap_CpoElem Mem) in interpRel. split.
        { rewrite interpRel in preInMem; assumption. }
        { apply expr_neg_consistency; rewrite <- interpRel; assumption. }
      }
      unfold assertAnd; split.
      + apply conseq_or_bottom_is_conseq. unfold MemElem.
        rewrite <- interpRel.
        assert (forall n1, n1 <= (S n) ->
          conseq_or_bottom inv
            (interp (nth_iterate sBody n1) (MemElem mem))).
        { induction n1.
          { intros obvious. simpl. assumption. }
          { intros order; simpl.
            unfold hoare_consequence in IHdeduction.
            assert (n1 < S n) as nOrder. omega.
            elim (greater_n_noerror n1 (S n) sBody mem m nOrder interpRel).
            intros memN relMemN.
            specialize (IHdeduction memN) as IHmem.
            rewrite relMemN.
            apply IHmem.
            unfold assertAnd; split.
            { rewrite relMemN in IHn1; unfold MemElem in IHn1.
              apply IHn1. omega.
            }
            { unfold assertOfExpr.
              specialize (notLastIter n1).
              rewrite relMemN in notLastIter.
              unfold satisfies_expr in notLastIter; simpl in notLastIter.
              apply notLastIter. assumption.
            }
          }
        }
        {
          apply H. omega.
        }
      + unfold assertNot; unfold assertOfExpr. rewrite interpRel in lastIter.
        unfold satisfies_expr in lastIter.
        unfold expr_neg in lastIter.
        destruct (expr m); simpl; congruence.
      + rewrite interpRel; unfold MemError; congruence.
Qed.

(***** Syntactic assertion interpretation ************************************)

Fixpoint aInterp (src: SynAssert): Assert :=
  fun (mem: Mem) => match src with
  | ATop => True
  | ABot => False
  | ANeg x => ~ (aInterp x mem)
  | AAnd x y => (aInterp x mem) /\ (aInterp y mem)
  | AOr x y => (aInterp x mem) \/ (aInterp y mem)
  | AImplies x y => (~ (aInterp x mem)) \/ (aInterp y mem)
  | AExpr exp => exp mem <> 0%Z
  | AForall v x => forall (z: Z), aInterp x (mem [v <- z])
  | AExists v x => exists (z: Z), aInterp x (mem [v <- z])
  | ASubstZ v z x => aInterp x (mem [v <- z])
  | ASubstE v e x => aInterp x (mem [v <- (e mem)])
  end.

(***** Weakest precondition **************************************************)

Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with
| skip => cond
| abort => assertTop
| assign x expr => (cond [[ x <- expr expr ]])
| seq s1 s2 => wp s1 (wp s2 cond)
| ifelse guard sIf sElse =>
    ((assertOfExpr guard -> wp sIf cond)
     /\ (~ (assertOfExpr guard) -> wp sElse cond)) % assert
| while assert guard body => assertBot
end.

Lemma assertImplElim {a b: Assert} :
  forall (m: Mem), (assertImpl a b) m -> a m -> b m.
Proof.
  intros mem impl pa.
  unfold assertImpl in impl; unfold assertOr in impl.
  destruct impl.
  * elimtype False. unfold assertNot in H. apply (H pa).
  * assumption.
Qed.

Lemma assertImplSelf (a: Assert) :
  assertImplLogical a a.
Proof.
  unfold assertImplLogical. intros mem x. assumption.
Qed.

Lemma preBottomIsCorrect {instr post}:
  (|= [|assertBot|] instr [|post|]) % assert.
Proof.
  unfold hoare_consequence. intros mem.
  unfold assertBot.
  intros F; exfalso; exact F.
Qed.

Lemma leftWeaken {instr post}:
  forall pre,
  (|- [|pre|] instr [|post|])%assert
  -> (|- [|assertBot|] instr [|post|])%assert.
Proof.
  intros pre orig.
  apply (H_conseq
    assertBot post
    pre post).
  - assumption.
  - unfold assertImplLogical. intros mem.
    unfold assertBot. intros F; exfalso; assumption.
  - apply (assertImplSelf post).
Qed.

Lemma assertBotAndStuff {res}:
  forall assert, assertImplLogical (assertBot /\ assert)%assert (res).
Proof.
  intros assert. unfold assertImplLogical. unfold assertBot. unfold assertAnd.
  intros mem [F _]. exfalso. assumption.
Qed.

Lemma preBottomIsProvable {instr post}:
  (|- [|assertBot|] instr [|post|]) % assert.
Proof.
  revert post.
  induction instr; intros post.
  * apply (leftWeaken post); apply (H_skip post).
  * apply (H_abort assertBot post).
  * apply (leftWeaken (post [[ v <- expr e]])%assert ).
    apply (H_assign post v e).
  * specialize IHinstr2 with post; specialize IHinstr1 with assertBot.
    apply (H_seq assertBot assertBot post).
    assumption. assumption.
  * apply (H_if assertBot post e instr1 instr2).
    - apply (H_conseq
        (assertBot /\ assertOfExpr e)%assert post
        assertBot post).
      + apply IHinstr1.
      + apply (assertBotAndStuff (assertOfExpr e)).
      + apply (assertImplSelf post).
    - apply (H_conseq
        (assertBot /\ ~ assertOfExpr e)%assert post
        assertBot post).
      + apply IHinstr2.
      + apply (assertBotAndStuff (assertNot (assertOfExpr e))).
      + apply (assertImplSelf post).
  * apply (H_conseq
      assertBot post
      assertBot (assertBot /\ ~ (assertOfExpr e))%assert).
    - apply (H_while assertBot s e instr).
      apply (H_conseq
        (assertBot /\ assertOfExpr e)%assert assertBot
        assertBot assertBot).
      + apply IHinstr.
      + apply (assertBotAndStuff (assertOfExpr e)).
      + apply assertImplSelf.
    - apply assertImplSelf.
    - apply assertBotAndStuff.
Qed.

Theorem wp_correctness_provable (instr: Instr) :
  forall post,
    ( |- [| wp instr post |] instr [| post |] ) % assert.
Proof.
  induction instr; intros post; simpl.
  * apply (H_skip post).
  * apply (H_abort assertTop post).
  * apply (H_assign post v e).
  * remember (wp instr2 post) as mid eqn:midRel.
    remember (wp instr1 mid) as pre eqn:preRel.
    specialize IHinstr2 with post.
    specialize IHinstr1 with mid.
    rewrite <- midRel in IHinstr2; rewrite <- preRel in IHinstr1.
    apply (H_seq pre mid post instr1 instr2).
    assumption. assumption.
  * remember ((assertOfExpr e -> wp instr1 post)
              /\ (~ assertOfExpr e -> wp instr2 post)) % assert
      as pre eqn:preRel.
    apply (H_if pre post e instr1 instr2).
    - apply (H_conseq
        (pre /\ assertOfExpr e)%assert post
        (wp instr1 post) post instr1
        (IHinstr1 post)).
      + rewrite preRel. unfold assertImplLogical.
        intros mem. intros [ [disjunctIf disjunctElse] isIf].
        apply (assertImplElim mem disjunctIf isIf).
      + apply (assertImplSelf post).
    - apply (H_conseq
        (pre /\ ~ assertOfExpr e)%assert post
        (wp instr2 post) post instr2
        (IHinstr2 post)).
      + rewrite preRel. unfold assertImplLogical.
        intros mem. intros [ [disjunctIf disjunctElse] isElse].
        apply (assertImplElim mem disjunctElse isElse).
      + apply (assertImplSelf post).
  * apply preBottomIsProvable.
Qed.

Theorem wp_correctness (instr: Instr) :
  forall post,
    ( |= [| wp instr post |] instr [| post |] ) % assert.
Proof.
  intros post.
  apply hoare_provability_implies_consequence.
  apply wp_correctness_provable.
Qed.

(***** Assertions syntaxiques -- proprietes **********************************)

Fixpoint wps (instr: Instr) (asser: SynAssert) : SynAssert := match instr with
| skip => asser
| abort => ATop
| assign x expr => ASubstE x expr asser
| seq s1 s2 => wps s1 (wps s2 asser)
| ifelse guard sIf sElse =>
    AAnd
      (AImplies (AExpr guard) (wps sIf asser))
      (AImplies (ANeg (AExpr guard)) (wps sElse asser))
| while assert guard body => ABot
end.

Lemma aInterpConsistent (instr: Instr):
  forall post, aInterp (wps instr post) = wp instr (aInterp post).
Proof.
  induction instr; intros post; simpl; trivial.
  * (* sequence *)
    rewrite <- (IHinstr2 post).
    rewrite (IHinstr1 (wps instr2 post)).
    congruence.
  * (* if/else *)
    rewrite <- (IHinstr2 post).
    rewrite <- (IHinstr1 post).
    unfold assertAnd; unfold assertImpl; unfold assertOfExpr; unfold assertOr;
      unfold assertNot; simpl.
    apply functional_extensionality; intros mem; simpl. congruence.
Qed.

Theorem wps_correctness (instr: Instr):
  forall post,
    ( |= [| aInterp (wps instr post) |] instr [| aInterp post |] ) % assert.
Proof.
  intro post.
  rewrite (aInterpConsistent instr).
  apply wp_correctness.
Qed.

(* vim: ts=2 sw=2
*)