Implement most operators on assertions

wp.v

@@ -5,7 +5,7 @@
 Require Import ZArith.BinInt.
 Import Z.
 
-Parameter Var: Type.
+Definition Var := nat.
 Definition Mem := Var -> Z.
 Definition Expr:= Mem -> Z.
 
@@ -16,3 +16,140 @@ Inductive Instr : Type :=
 | 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).