Commit 3ff2c4a2 authored by Martin Clochard's avatar Martin Clochard

example(in_progress): 2wp_gen

parent 29051ec3
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../choice.mlw">
<theory name="Choice" sum="10c4efd79629e9417231ac2d78d9aa7b">
<goal name="WP_parameter choose" expl="VC for choose">
......
......@@ -106,15 +106,15 @@ module Game
('a,'b) -> ('a,'b) -> bool = \x y.
let (a,c) = x in let (b,d) = y in o1 a b /\ o2 c d
(* Two order are chain-compatible by r if for every chain of related pairs,
the supremum is a related pair as well.
(* Two order are chain-compatible by r if for every non-empty chains of
related pairs, the supremum is a related pair as well.
(as we are considering chain-complete orders, the supremum existence
is immediate)
This is a technical condition for the simulation theorem. *)
predicate chain_compatible (o1:'a -> 'a -> bool) (r:'a -> 'b -> bool)
(o2:'b -> 'b -> bool) =
forall ch s1 s2.
chain (oprod o1 o2) ch /\ (forall a b. ch (a,b) -> r a b) /\
forall ch inh s1 s2.
chain (oprod o1 o2) ch /\ ch inh /\ (forall a b. ch (a,b) -> r a b) /\
supremum (oprod o1 o2) ch (s1,s2) -> r s1 s2
predicate step_simulate (g1:game 'a) (r:'a -> 'b -> bool) (g2:game 'b) =
......@@ -130,19 +130,16 @@ end
(* A few properties of strategies on such games.
Proofs in StratProofs. *)
module StratProps
module StratProps "W:non_conservative_extension:N"
use export Game
namespace import Dummy type d end
(* Quantifier inversion between having a uniform strategy and
having strategies for all. *)
axiom have_uniform_winning_strat_alternate_def :
forall g,start win:'a -> bool. game_wf g ->
(have_uniform_winning_strat g start win <->
(forall x. start x -> have_winning_strat g x win))
/\ forall _:d. true
(* Local criterion for winning strategy existence. *)
axiom have_winning_strat_local_criterion :
......@@ -150,12 +147,10 @@ module StratProps
(have_winning_strat g x win <->
win x \/
exists s. g.transition x s /\ have_uniform_winning_strat g s win)
/\ forall _:d. true
(* Simulation theorem: a step simulation extends to a real simulation. *)
axiom simulation : forall g1,r:'a -> 'b -> bool,g2.
game_wf g1 /\ game_wf g2 /\ step_simulate g1 r g2 -> simulate g1 r g2
/\ forall _:d. true
end
......@@ -846,6 +841,9 @@ module StratProofs
by s0 u /\ st.h_proj u
so o1 u a /\ o1 a u
end)
so (let (a,b) = pr in sc.r a b
by exists u. st.h_pair u by u = (sc.basea,sc.baseb)
so sc.sd bs st so subchain op bs.h_pair st.h_pair)
so forall a0 b0 st2. maximum op nst.h_pair (a0,b0) so (a0,b0) = pr ->
let s0 = sc.anga a0 nst.h_proj in
tr_reach sc.sd evl bs st2 /\ sc.sd st2 nst /\
......@@ -1958,7 +1956,7 @@ module StratProofs
exists st. tr_reach sc.sd evl bs st /\
win_at sc.g2 winb angb dmn st.h_total
clone StratProps with type Dummy.d = unit,
clone StratProps with
goal have_uniform_winning_strat_alternate_def,
goal have_winning_strat_local_criterion,
goal simulation
......
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
......@@ -24,7 +24,7 @@ module IterateCommon
end
(* Proof of iterate axioms in IterateProof module. *)
module Iterates
module Iterates "W:non_conservative_extension:N"
use import order.Order
use import order.Chain
......@@ -32,14 +32,11 @@ module Iterates
use import order.Wf
use export IterateCommon
namespace import Dummy type d end
(* tr_reach is a chain, and there are no
tr_reach element between any z and its 'sucessor' f z. *)
axiom tr_reach_separated : forall o f,x y z:'a.
order o /\ inflationary o f /\ tr_reach o f x y /\ tr_reach o f x z ->
separator o f z y
/\ forall _:d. true
(* For chain-complete orders, there is a maximum tr_reach element,
which is a fixpoint of the growth function
......@@ -50,29 +47,24 @@ module Iterates
order o /\ inflationary o f /\ chain_complete o ->
f (fixpoint_above o f x) = fixpoint_above o f x /\
maximum o (tr_reach o f x) (fixpoint_above o f x)
/\ forall _:d. true
axiom tr_reach_fixpoint : forall o f,x y:'a.
order o /\ inflationary o f /\ f y = y /\ tr_reach o f x y ->
maximum o (tr_reach o f x) y
/\ forall _:d. true
(* transifinite reachability relation is compatible with the base order. *)
axiom tr_reach_compare : forall o f,x y:'a.
preorder o /\ inflationary o f /\ tr_reach o f x y -> o x y
/\ forall _:d. true
(* transfinite reachability relation is transitive. *)
axiom tr_reach_transitive : forall o f,x y z:'a.
preorder o /\ inflationary o f ->
tr_reach o f x y /\ ("induction" tr_reach o f y z) -> tr_reach o f x z
/\ forall _:d. true
(* the set of reachable states from a given one is well-founded
for the base order relation. *)
axiom tr_reach_wf : forall o f,x:'a.
order o /\ inflationary o f -> wf (restricted_lower o f x)
/\ forall _:d. true
end
......@@ -161,7 +153,7 @@ module IterateProof
acc (restricted_lower o f x) z
by exists a. ch a /\ not o a z so separator o f a z so o z a)
clone Iterates with type Dummy.d = unit,
clone Iterates with
function fixpoint_above = fixpoint_above,
goal tr_reach_separated,
goal tr_reach_maximum,
......@@ -202,41 +194,34 @@ end
(* Special shape of iterates: chain extension.
This module contain the machinery to build chain iterates.
Proofs in ChainExtensionProof. *)
module ChainExtension
module ChainExtension "W:non_conservative_extension:N"
use import order.Order
use import order.Chain
use import order.Mono
use export ChainExtensionCommon
namespace import Dummy type d end
(* subchain ordering is a chain-complete order for transitive relations. *)
axiom subchain_order : forall o:'a -> 'a -> bool.
transitive o -> order (subchain o)
/\ forall _:d. true
axiom subchain_complete : forall o:'a -> 'a -> bool,ch.
chain (subchain o) ch -> supremum (subchain o) ch (subchain_completion ch)
/\ forall _:d. true
axiom subchain_completion_chain : forall o:'a -> 'a -> bool,ch.
chain (subchain o) ch /\ (forall x. ch x -> chain o x) ->
chain o (subchain_completion ch)
/\ forall _:d. true
axiom extends_inflationary : forall o:'a -> 'a -> bool,f.
ub_builder o f -> inflationary (subchain o) (extends_ch o f)
/\ forall _:d. true
axiom extends_preserve_chain : forall o:'a -> 'a -> bool,f ch.
ub_builder o f /\ chain o ch /\ reflexive o ->
chain o (extends_ch o f ch)
/\ forall _:d. true
axiom reach_only_chains : forall o:'a -> 'a -> bool,f ch1 ch2.
ub_builder o f /\ chain o ch1 /\ reach_ch o f ch1 ch2 /\
reflexive o -> chain o ch2
/\ forall _:d. true
end
......@@ -278,7 +263,7 @@ module ChainExtensionProof
by forall o1 f1 b1 x. o1 = o /\ f1 = f /\ b1 = ch1 ->
("induction" tr_reach (subchain o1) (extends_ch o1 f1) b1 x) -> chain o1 x
clone ChainExtension with type Dummy.d = unit,
clone ChainExtension with
goal subchain_order,
goal subchain_complete,
goal subchain_completion_chain,
......
......@@ -2,24 +2,24 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../transfinite.mlw">
<theory name="IterateCommon" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Iterates" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="IterateProof" sum="7110fa6c95abf2834680e9aea777adf9">
<theory name="IterateProof" sum="749a80e0893a304d15f90fcfd59ecdd2">
<goal name="tr_reach_compare">
<transf name="induction_pr">
<goal name="tr_reach_compare.1" expl="1.">
<proof prover="2" steplimit="1"><result status="valid" time="0.00" steps="9"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="tr_reach_compare.2" expl="2.">
<proof prover="2" steplimit="1"><result status="valid" time="0.01" steps="38"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="38"/></proof>
</goal>
<goal name="tr_reach_compare.3" expl="3.">
<proof prover="2" steplimit="1"><result status="valid" time="0.01" steps="26"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
</transf>
</goal>
......@@ -326,18 +326,18 @@
</theory>
<theory name="ChainExtension" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ChainExtensionProof" sum="eb25cf3911502cbbab86e46f7256e871">
<theory name="ChainExtensionProof" sum="fcf81d2518ca60cb2f06e6d92c1f1a0c">
<goal name="WP_parameter ext" expl="VC for ext">
<transf name="split_goal_wp">
<goal name="WP_parameter ext.1" expl="1. assertion">
<transf name="inline_goal">
<goal name="WP_parameter ext.1.1" expl="1. assertion">
<proof prover="2" steplimit="1"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter ext.2" expl="2. postcondition">
<proof prover="2" steplimit="1"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
</transf>
</goal>
......
(* Zorn's lemma: any chain-bounded (not even complete)
order has a maximal element. *)
module Zorn
namespace import Dummy type d end
module Zorn "W:non_conservative_extension:N"
use import order.Order
use import order.Chain
......@@ -11,7 +9,6 @@ module Zorn
(* Proof in ZornProof module. *)
axiom zorn_lemma : forall o:'a -> 'a -> bool.
preorder o /\ chain_bounded o -> exists y. maximal o y
/\ forall _:d. true
end
......@@ -48,21 +45,18 @@ module ZornProof
so forall x. o witness x -> o x witness
by not strict_upper_bound o fix x
clone Zorn with type Dummy.d = unit, goal zorn_lemma
clone Zorn with goal zorn_lemma
end
(* Consequence of Zorn's lemma: well-ordering theorem. *)
module WellOrder
module WellOrder "W:non_conservative_extension:N"
use import order.Wf
namespace import Dummy type d end
predicate well_order_witness (x y:'a)
axiom well_order_exists : well_order (well_order_witness:'a -> 'a -> bool)
/\ forall _:d. true
end
......@@ -185,7 +179,7 @@ module WellOrderProof
predicate witness (x y:'a) = choice well_order x y
meta rewrite_def predicate witness
clone WellOrder with type Dummy.d = unit,
clone WellOrder with
predicate well_order_witness = witness,
goal well_order_exists
......
......@@ -2,12 +2,12 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../zorn.mlw">
<theory name="Zorn" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ZornProof" sum="0e970e51c81a73c1c9027c6d998611a7">
<theory name="ZornProof" sum="ec60b3936ceac8b7c7e3c840622f551a">
<goal name="choose_ub_builder">
<proof prover="1"><result status="valid" time="0.36"/></proof>
</goal>
......@@ -42,7 +42,7 @@
</theory>
<theory name="WellOrder" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="WellOrderProof" sum="81be3f5db7a9225b73e9d0bac8e2c489">
<theory name="WellOrderProof" sum="95b5475e469c614aa865e019736a6061">
<goal name="completion_well_ordered">
<transf name="split_goal_wp">
<goal name="completion_well_ordered.1" expl="1.">
......@@ -214,7 +214,7 @@
<proof prover="2"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="well_order_proof.3" expl="3.">
<proof prover="2" steplimit="1"><result status="valid" time="0.05" steps="17"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="17"/></proof>
</goal>
<goal name="well_order_proof.4" expl="4.">
<proof prover="2"><result status="valid" time="0.01" steps="18"/></proof>
......@@ -232,7 +232,7 @@
<proof prover="2"><result status="valid" time="0.03" steps="59"/></proof>
</goal>
<goal name="well_order_proof.9" expl="9.">
<proof prover="2" steplimit="1"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
</transf>
</goal>
......
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