(* Projet Coq - WP - MPRI 2.7.1 *)

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

Require Import ZArith.BinInt.
Import Z.

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

Inductive Instr : Type :=
| skip: Instr
| abort: Instr
| assign: Var -> Expr -> Instr
| seq: Instr -> Instr -> Instr
| ifelse: Expr -> Instr -> Instr -> Instr
| while: 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} _.

(***** 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 instrIf mem
                else interp instrElse 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.

(***** 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 : Assert -> Assert -> Prop :=
    fun a1 a2 => 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, forall expr, forall sBody,
        (|- [| inv /\ (assertOfExpr expr) |] sBody [| inv |]) % assert ->
            (|- [| inv |] (while 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.

Theorem hoare_provability_implies_consequence :
    forall (pre: Assert), forall (s: Instr), forall (post: Assert),
    ( |- [| pre |] s [| post |] ) % assert
            -> ( |= [| pre |] s [| post |] ) % assert.
Proof.
    (* TODO *)
Admitted.