Commit 031e19ef authored by Martin Clochard's avatar Martin Clochard

2wp_gen: cont'd

parent 07b93033
SHELL=/bin/bash
REPLAY=why3 replay -L .
MLW=base choice ho_set ho_rel fn order transfinite game game_fmla
REPLAY=why3 replay -L . -f
MLW=base choice ho_set ho_rel fn order transfinite game game_fmla transition
replay:
@exe() { echo "$$0 $$@"; "$$@"; };\
......
(* TODO: complete. *)
(* TODO: complete.... if feasible. *)
module Base
......@@ -9,6 +9,9 @@ module Base
meta rewrite_def function f
function s (x:('a,'b)) : 'b = let (_,x) = x in x
meta rewrite_def function s
predicate (-->) (x y:'a) = "rewrite" (x = y)
meta rewrite_def predicate (-->)
end
......@@ -18,37 +21,48 @@ end
module Quant "W:non_conservative_extension:N"
use import HighOrd
use import int.Int
type structure
predicate quant_structure bool structure (p:'a -> bool)
type qstructure 'a
predicate quant_structure bool (qstructure 'a) (p:'a -> bool)
val ghost quant_structure_def (_:'a -> bool) : unit
ensures { forall b s,p:'a -> bool.
quant_structure b s p <-> if b then forall y. p y else exists y. p y }
constant def : structure
(* Unstructured quantification. *)
constant q_def : qstructure 'a
axiom forall_default : forall p:'a -> bool.
quant_structure true def p <-> forall y. p y
quant_structure true q_def p <-> forall y. p y
axiom exists_default : forall p:'a -> bool.
quant_structure false def p <-> exists y. p y
quant_structure false q_def p <-> exists y. p y
meta rewrite prop forall_default
meta rewrite prop exists_default
meta remove_prop prop forall_default
meta remove_prop prop exists_default
function pair structure structure : structure
(* Unit quantification. *)
constant q_unit : qstructure unit
axiom quant_structure_unit : forall b p.
quant_structure b q_unit p <-> p ()
meta rewrite prop quant_structure_unit
meta remove_prop prop quant_structure_unit
(* Splitting pairs *)
function q_pair (qstructure 'a) (qstructure 'b) : qstructure ('a,'b)
axiom quant_structure_pair : forall b s1 s2,p:('a,'b) -> bool.
quant_structure b (pair s1 s2) p <->
quant_structure b (q_pair s1 s2) p <->
quant_structure b s1 (\x. quant_structure b s2 (\y. p (x,y)))
meta rewrite prop quant_structure_pair
meta remove_prop prop quant_structure_pair
function cond structure structure : structure
(* Boolean casing *)
function q_cond (qstructure 'a) (qstructure 'a) : qstructure ('a,bool)
axiom forall_cond : forall s1 s2,p:('a,bool) -> bool.
quant_structure true (cond s1 s2) p <->
quant_structure true (q_cond s1 s2) p <->
quant_structure true s1 (\x. p (x,true)) /\
quant_structure true s2 (\x. p (x,false))
axiom exists_cond : forall s1 s2,p:('a,bool) -> bool.
quant_structure false (cond s1 s2) p <->
quant_structure false (q_cond s1 s2) p <->
quant_structure false s1 (\x. p (x,true)) \/
quant_structure false s2 (\x. p (x,false))
meta rewrite prop forall_cond
......@@ -56,29 +70,61 @@ module Quant "W:non_conservative_extension:N"
meta remove_prop prop forall_cond
meta remove_prop prop exists_cond
(* Integer casing *)
function q_range int int (qstructure int) : qstructure int
predicate q_range_structure bool (qstructure int) int int int (int -> bool)
axiom quant_structure_range : forall b s n m,p:int -> bool.
quant_structure b (q_range n m s) p <-> q_range_structure b s n n m p
axiom forall_range_structure : forall s n l m,p:int -> bool.
q_range_structure true s n l m p =
if l = m then quant_structure true s (\x. not(n <= x < m) -> p x)
else p l /\ q_range_structure true s n (l+1) m p
axiom exists_range_structure : forall s n l m,p:int -> bool.
q_range_structure false s n l m p =
if l = m then quant_structure false s (\x. not(n <= x < m) /\ p x)
else p l \/ q_range_structure false s n (l+1) m p
meta rewrite prop quant_structure_range
meta rewrite prop forall_range_structure
meta rewrite prop exists_range_structure
meta remove_prop prop quant_structure_range
meta remove_prop prop forall_range_structure
meta remove_prop prop exists_range_structure
end
module QuantImpl
use import HighOrd
use import int.Int
type structure = int
constant def : int = 0
function pair 'a 'b : int = 0
type qstructure 'a = int
constant q_def : int = 0
function q_pair 'a 'b : int = 0
predicate quant_structure (b:bool) 'b (p:'a -> bool) =
if b then forall x. p x else exists x. p x
let ghost quant_structure_def (_:'b) = ()
function q_range 'a 'b 'c : int = 0
predicate q_range_structure (b:bool) 'a (n i m:int) (p:int -> bool) =
if b then forall x. not(n <= x < i) -> p x
else exists x. not (n <= x < i) /\ p x
clone Quant with type structure = structure,
clone Quant with type qstructure = qstructure,
predicate quant_structure = quant_structure,
val quant_structure_def = quant_structure_def,
function def = def,
function q_def = q_def,
goal forall_default,
goal exists_default,
function pair = pair,
function q_unit = q_def,
goal quant_structure_unit,
function q_pair = q_pair,
goal quant_structure_pair,
function cond = pair,
function q_cond = q_pair,
goal forall_cond,
goal exists_cond
goal exists_cond,
function q_range = q_range,
predicate q_range_structure = q_range_structure,
goal quant_structure_range,
goal forall_range_structure,
goal exists_range_structure
end
......@@ -4,12 +4,13 @@
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../compute_elts.mlw" expanded="true">
<theory name="Base" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../compute_elts.mlw">
<theory name="Base" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Quant" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Quant" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="QuantImpl" sum="345cdf6d746cb7346db087793c271275">
<theory name="QuantImpl" sum="43b1dc380e604d26ccd15795dd6d972d">
<goal name="WP_parameter quant_structure_def" expl="VC for quant_structure_def">
<proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
......@@ -19,6 +20,9 @@
<goal name="Quant.exists_default">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="Quant.quant_structure_unit">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="Quant.quant_structure_pair">
<proof prover="0"><result status="valid" time="0.18"/></proof>
</goal>
......@@ -28,6 +32,15 @@
<goal name="Quant.exists_cond">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="Quant.quant_structure_range">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="Quant.forall_range_structure">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Quant.exists_range_structure">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Quant.WP_parameter Quant quant_structure_def" expl="VC for Quant quant_structure_def">
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
......
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment