Commit 07b93033 authored by Martin Clochard's avatar Martin Clochard

examples/in_progress(wip): 2wp_gen, cont'd

parent c8bbcd4b
(* TODO: complete. *)
module Base
meta compute_max_steps 0x1_000_000
function f (x:('a,'b)) : 'a = let (x,_) = x in x
meta rewrite_def function f
function s (x:('a,'b)) : 'b = let (_,x) = x in x
meta rewrite_def function s
end
(* Decomposition of quantification statements by destructuring
the argument structure. This is intended to be used by compute alone,
so the definitions/lemmas are kept away from the provers sight. *)
module Quant "W:non_conservative_extension:N"
use import HighOrd
type structure
predicate quant_structure bool structure (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
axiom forall_default : forall p:'a -> bool.
quant_structure true def p <-> forall y. p y
axiom exists_default : forall p:'a -> bool.
quant_structure false 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
axiom quant_structure_pair : forall b s1 s2,p:('a,'b) -> bool.
quant_structure b (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
axiom forall_cond : forall s1 s2,p:('a,bool) -> bool.
quant_structure true (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 s1 (\x. p (x,true)) \/
quant_structure false s2 (\x. p (x,false))
meta rewrite prop forall_cond
meta rewrite prop exists_cond
meta remove_prop prop forall_cond
meta remove_prop prop exists_cond
end
module QuantImpl
use import HighOrd
type structure = int
constant def : int = 0
function 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) = ()
clone Quant with type structure = structure,
predicate quant_structure = quant_structure,
val quant_structure_def = quant_structure_def,
function def = def,
goal forall_default,
goal exists_default,
function pair = pair,
goal quant_structure_pair,
function cond = pair,
goal forall_cond,
goal exists_cond
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<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">
</theory>
<theory name="Quant" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="QuantImpl" sum="345cdf6d746cb7346db087793c271275">
<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>
<goal name="Quant.forall_default">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="Quant.exists_default">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="Quant.quant_structure_pair">
<proof prover="0"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="Quant.forall_cond">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="Quant.exists_cond">
<proof prover="0"><result status="valid" time="0.03"/></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>
</theory>
</file>
</why3session>
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
module SubgameCommon
use import game.Game
use import ho_set.Set
(* Notion of game inclusion: the larger game simulate the smaller one,
using the same ordering support. *)
predicate subgame (g1 g2:game 'a) =
simulate g1 (=) g2 /\ g1.progress = g2.progress
(* Trivial game inclusion: the smaller game transitions are included
in the larger one. *)
predicate trivial_subgame (g1 g2:game 'a) =
g1.progress = g2.progress /\
forall x. subset (g1.transition x) (g2.transition x)
end
module Subgame "W:non_conservative_extension:N" (* => SubgameProof *)
use import game.Game
use export SubgameCommon
axiom trivial_subgame_indeed : forall g1 g2:game 'a.
game_wf g1 /\ game_wf g2 /\ trivial_subgame g1 g2 -> subgame g1 g2
end
module SubgameProof
use import game.Game
use import SubgameCommon
use import ho_set.Set
use import ho_rel.RelSet
use import ho_rel.Prod
use import game.StratProps
use import order.LimUniq
use import order.Product
use import order.Chain
use import fn.Fun
use import fn.Image
lemma rel_map_equal : forall s:set 'a.
related (=) s = s by sext (related (=) s) s
lemma ax : forall g1 g2:game 'a.
game_wf g1 /\ game_wf g2 /\ trivial_subgame g1 g2 ->
subgame g1 g2 by step_simulate g1 (=) g2
by let o1 = g1.progress in let o2 = g2.progress in
(chain_compatible o1 (=) o2
by forall ch inh s1 s2.
chain (rprod o1 o2) ch /\ ch inh /\ (forall a b. ch (a,b) -> a = b)
/\ supremum (rprod o1 o2) ch (s1,s2) -> s1 = s2
by supremum o1 (image fst ch) s1
so supremum o2 (image snd ch) s2
so sext (image fst ch) (image snd ch)
by forall x. (image fst ch x <-> image snd ch x)
by (image fst ch x <-> ch (x,x)) /\ (image snd ch x <-> ch (x,x))
)
/\ (forall x s. g1.transition x s ->
have_winning_strat g2 x (related (=) s)
by g2.transition x s)
clone Subgame with goal trivial_subgame_indeed
end
module Fmla
use import order.Chain
......@@ -75,7 +8,6 @@ module Fmla
use import fn.Fun
use import fn.Image
use import game.Game
use import Subgame
(* Game formulae: predicates over games. *)
type fmla 'a = game 'a -> bool
......@@ -158,7 +90,7 @@ module FmlaRules "W:non_conservative_extension:N" (* => FmlaRulesProof *)
use import fn.Image
use import order.Chain
use import game.Game
use export Fmla
use import Fmla
(* Formula builders indeed build formulas *)
axiom enforce_fmla : forall p q:set 'a. is_fmla (enforce p q)
......@@ -242,11 +174,10 @@ module FmlaRulesProof
use import game.StratProps
use import transfinite.Iterates
use import transfinite.ChainExtension
use import Subgame
use import Fmla
lemma rel_map_equal : forall s:set 'a.
related (=) s = s by sext (related (=) s) s
(*lemma rel_map_equal : forall s:set 'a.
related (=) s = s by sext (related (=) s) s*)
(* prepare for enforce_monotonic: postcondition side. *)
lemma pre_monotonic : forall g x,q1 q2:set 'a.
......@@ -333,17 +264,24 @@ module FmlaRulesProof
(* Transfinite loop rule, version 1.
(it is weak in the sense that it imposes
few properties on the I-chain and requires a very strong property,
namely the supremum to satisfy the invariant)
few properties on the I-chain and requires very strong properties,
namely that the second supremum always exists and
satisfy the invariant when the first one do exists)
Under the hood, the transfinite loop rule is an immediate application
of the simulation theorem based on fully demonic games.
Consider the fully demonic game of I-state with progression relation
being the product order. Then, we requires exactly the hypothesis
needed to have a simulation from this game to the current game. *)
predicate chain_compatible (o1:erel 'a) (r:rel 'a 'b) (o2:erel 'b) =
forall ch inh s2.
chain (rprod o1 o2) ch /\ ch inh /\ (forall a b. ch (a,b) -> r a b) /\
supremum o2 (image snd ch) s2 ->
exists s1. supremum o1 (image fst ch) s1 /\ r s1 s2
lemma crude_trampoline : forall c go,i:rel 'b 'a,o:erel 'b.
holds c (universal (u_enforce i (later o i))) /\
holds c (ordering go) /\ order o /\ chain_complete o /\
holds c (ordering go) /\ order o /\
chain_compatible o i go ->
holds c (universal (u_enforce i (const none)))
by forall g. game_wf g /\ c g -> forall x.
......@@ -351,6 +289,7 @@ module FmlaRulesProof
by forall y. i x y -> have_winning_strat g y none
by let op = rprod o go in
order op
so g.progress = go
so let nx = \x y. let (a,b) = x in let (c,d) = y in
go b d /\ a <> c /\ o a c /\ i c d in
let tr = \x. (=) (nx x) in
......@@ -375,27 +314,29 @@ module FmlaRulesProof
by forall z. later o i xx z /\ go y z ->
related r s z by exists xz. i xz z /\ o xx xz /\ xx <> xz
so s (xz,z) /\ r (xz,z) z)
/\ ("stop_split" chain_compatible op r go
by forall chp inhp xp yp. chain (rprod op go) chp /\ chp inhp /\
/\ ("stop_split" limit_compatible op r g
by forall chp inhp s2. chain (rprod op go) chp /\ chp inhp /\
(forall x y. chp (x,y) -> r x y) /\
supremum (rprod op go) chp (xp,yp) ->
supremum go (image snd chp) s2 ->
let ch = image fst chp in
let (inh,_) = inhp in
ch inh
so supremum op ch xp
(exists s1. supremum op ch s1 /\ r s1 s2)
by let (inh,_) = inhp in
ch inh
so chain op ch
so (forall x y. ch (x,y) -> i x y
by exists z. chp z /\ fst z = (x,y))
so let (a,b) = xp in let (u,_) = inhp in ch u so i a b
so b = yp
by let ch1 = image snd ch in let ch2 = image snd chp in
supremum go ch1 b /\ supremum go (image snd chp) yp
so sext ch1 ch2
by (forall x. ch1 x -> ch2 x by exists y. ch y /\ snd y = x
so exists z. chp z /\ fst z = y so
let ((_,b),_) = z in ch2 (snd z) so snd z = b)
/\ (forall x. ch2 x -> ch1 x by exists y. chp y /\ snd y = x
so ch (fst y) so ch1 (snd (fst y)) so
let ((_,_),c) = y in snd (fst y) = c)
so (sext (image snd ch) (image snd chp)
by (forall x. image snd ch x -> image snd chp x
by exists u. ch u /\ snd u = x
so exists v. chp v /\ fst v = u
so let ((_,_),a) = v in x = a)
/\ (forall x. image snd chp x -> image snd ch x
by exists u. chp u /\ snd u = x
so let ((a,b),_) = u in ch (a,b) so b = x
))
so supremum go (image snd ch) s2
so exists s1. supremum o (image fst ch) s1 /\ i s1 s2
so supremum op ch (s1,s2) /\ r (s1,s2) s2
))
so (related r strt y)
so (sext (related r none) none)
......@@ -500,36 +441,37 @@ module FmlaRulesProof
so not (ch1 xn so maximum o ch1 xn))
) || sext (i_ch ch) none)
(* Chain compatibility. *)
so ("stop_split"
forall chh inhh chs y. chain op chh /\ supremum op chh (chs,y)
/\ chh inhh /\ (forall x y. chh (x,y) -> i_ch x y) ->
i_ch chs y
by let ch1 = image fst chh in let ch2 = image snd chh in
supremum o_ch ch1 chs /\ chain o_ch ch1 /\
supremum go ch2 y /\ chain go ch2
so chs = bigunion ch1
so (chain ip chs by forall x. ch1 x -> chain ip x)
so let (ch0,_) = inhh in
(exists u. chs u by exists v. ch0 v /\ u = v so ch1 ch0)
so (let ch3 = image snd chs in
supremum go ch3 y
by ("stop_split" forall u. ch3 u -> go u y
by exists v. chs v /\ snd v = u
so exists s0. ch1 s0 /\ s0 v
so exists w. chh w /\ fst w = s0
so let (_,a) = w in (go a y by op w (chs,y))
so supremum go (image snd s0) a /\ image snd s0 u)
/\ "stop_split" forall u. upper_bound go ch3 u -> go y u
by forall a. ch2 a -> go a u
by exists b. chh b /\ snd b = a
so let (b,_) = b in
supremum go (image snd b) a
so upper_bound go (image snd b) u
by forall u0. image snd b u0 -> go u0 u
by exists v0. b v0 /\ snd v0 = u0
so ch3 u0 by ch1 b)
so (forall y z. chs (y,z) -> i y z
by exists ch. ch1 ch /\ ch (y,z) so exists a. chh a /\ fst a = ch)
so ("stop_split" chain_compatible o_ch i_ch go
by forall chh inhh y.
let ch1 = image fst chh in let ch2 = image snd chh in
chain op chh /\ chh inhh /\
(forall x y. chh (x,y) -> i_ch x y) /\
supremum go ch2 y ->
exists chs. supremum o_ch ch1 chs /\ i_ch chs y
by chs = bigunion ch1
so (chain ip chs by forall x. ch1 x -> chain ip x)
so let (ch0,_) = inhh in
(exists u. chs u by exists v. ch0 v /\ u = v so ch1 ch0)
so supremum o_ch ch1 chs
so (forall y z. chs (y,z) -> i y z
by exists ch. ch1 ch /\ ch (y,z) so exists a. chh a /\ fst a = ch)
so (let ch3 = image snd chs in
supremum go ch3 y
by ("stop_split" forall u. ch3 u -> go u y
by exists v. chs v /\ snd v = u
so exists s0. ch1 s0 /\ s0 v
so exists w. chh w /\ fst w = s0
so let (_,a) = w in (go a y by ch2 a)
so supremum go (image snd s0) a /\ image snd s0 u)
/\ "stop_split" forall u. upper_bound go ch3 u -> go y u
by forall a. ch2 a -> go a u
by exists b. chh b /\ snd b = a
so let (b,_) = b in
supremum go (image snd b) a
so upper_bound go (image snd b) u
by forall u0. image snd b u0 -> go u0 u
by exists v0. b v0 /\ snd v0 = u0
so ch3 u0 by ch1 b)
)
so holds c (universal (u_enforce i_ch (const none)))
so forall y. i x y -> have_winning_strat g y none
......@@ -1384,14 +1326,7 @@ module FmlaRulesProof
)
(* Complete sp with x as to have a maximum in history. *)
so let csp = add sp x in
("stop_split" dmn_reach mg fr0.angl fr0.strt csp
by if sp x then sext csp sp else
exists dmn. let st = step mg fr0.angl dmn in
reach_ch go st ((=) fr0.strt) csp
by reach_ch go st ((=) fr0.strt) sp
so (st sp = x by sup go sp = x)
so extends_ch go st sp = csp
)
dmn_reach mg fr0.angl fr0.strt csp
so maximum go csp x
(* Prove that the obtained limit historic does satisfy
the postcondition-maximum criterion for frame validity. *)
......@@ -1885,7 +1820,9 @@ module FmlaRulesProof
by (* Prove that we are above. *)
"stop_split" upper_bound o chc x /\ not chc x
by maximum o chc x0
by maximum ip chi (x0,y)
by chi (x0,y)
so (maximum ip chi (x0,y) by upper_bound ip chi (x0,y))
so chc x0
so (forall x. chc x -> o x x0
by exists p. chi p /\ fst p = x
so let (_,b) = p in ip (x,b) (x0,y))
......
This source diff could not be displayed because it is too large. You can view the blob instead.
module WpCommon
use import ho_set.Set
use import ho_rel.Rel
use import order.Ordered
use import fn.Image
use import game.Game
use import game_fmla.Fmla
use import compute_elts.Quant
(* An enforcement object (type enforce 'a 'i 'o) represents a theorem
shaped as
|- forall x Q. Gamma(x) => < f(Q,x) -> exists y. Q(y) >
Here, the f(Q,x) mapping represent a regular backward predicate
transformer (as obtained by wp calculus).
A context can be represented as an arbitrary
collection of regular < P -> Q > enforcements.
For practical reasons, this collection is a set of sets
(this makes hypothesis membership tests true membership tests,
while the other option requires to handles subset tests through
compute)
It is kept on two forms: As a minimal context (logging everything
that was used as axiom), and as its dual from (monotonic predicate
describing the contexts containing the used axiom).
The first form is useful for internal proofs, while the second
one is much more practical externally to manage hypothesis
membership checks.
Note that for practical reasons, the contexts should be able
to refer to the same variables as the predicate transformer.
Finally, the enforcement box also refer the underlying game
ordering, which is necessary for obtaining limit theorems,
and for practical reason, we keep a validity predicate on the
underlying states (which is intended to be satisfied by just every
state we consider)
*)
type context 'a = set (set (set 'a,set 'a))
type enforce 'a 'i 'o = {
(* Underlying order. *)
game_order : erel 'a;
(* Valid states. *)
game_valid : set 'a;
(* Context, minimal form. *)
ctx_minima : 'i -> context 'a;
(* Context, dual form. *)
ctx_predic : rel 'i (context 'a);
(* Predicate transformer. *)
transformp : rel 'o 'a -> rel 'i 'a;
(* Structure for making universal quantifications
on the input variables ('i) *)
input_strt : structure;
(* Structure for making universal quantifications
on the game variables ('a) *)
game_strt : structure;
}
predicate same_context (e1 e2:enforce 'a 'i 'o) =
e1.game_order = e2.game_order /\
e1.game_valid = e2.game_valid /\
e1.ctx_minima = e2.ctx_minima /\
e1.ctx_predic = e2.ctx_predic /\
e1.input_strt = e2.input_strt /\
e1.game_strt = e2.game_strt
(* Represents members of the contexts, as:
(forall x. < P x -> exists y. Q x y >) formulas.
Those are analog to procedure calls. *)
type enf_hyp 'a 'i 'o = (rel 'i 'a,'i -> 'a -> rel 'o 'a)
end
module Wp "W:non_conservative_extension:N" (* Definitions in WpImpl *)
(* TODO: exported stuff goes here *)
end
module WpImpl
use import WpCommon
use import ho_set.Set
use import ho_set.SetBigOps
use import ho_rel.Rel
use import ho_rel.Prod
use import ho_rel.RelSet
use import order.Ordered
use import order.Chain
use import fn.Fun
use import fn.Image
use import game.Game
use import game.StratProps
use import game_fmla.Fmla
use import game_fmla.FmlaRules
use import compute_elts.Quant
(* Lifting of postcondition with extra return values *)
function e_lift (q:rel 'a 'b) : set 'b = \y. exists x. q x y
(* Transform a 'forall x. < P x -> exists y. Q x y >' context element
into a set of pre-post pairs. *)
function enf_hyp_token (h:enf_hyp 'a 'i 'o) : set (set 'a,set 'a) =
let (hp,hq) = h in
\pr. let (p0,q0) = pr in
exists x xs. p0 = inter (hp x) ((=) xs) /\ q0 = e_lift (hq x xs)
(* Define a specific membership predicate for hypothesis,
so as to be able to define non-intrusive computation rules *)
predicate enf_hyp_mem (h:enf_hyp 'a 'i 'o) (ctx:context 'a) =
ctx (enf_hyp_token h)
function pre_post_fmla (r:rel 'a 'd) (pq:(set 'a,set 'a)) : fmla 'd =
let (p,q) = pq in enforce (related r p) (related r q)
function sing_kont_fmla (x:'d) : fmla 'd = enforce ((=) x) none
function ctx_fmla (r:rel 'a 'd) (ctx:context 'a) : fmla 'd =
b_universal (bigunion ctx) (pre_post_fmla r)
predicate invalid_sup_witness (r:rel 'a 'd) (o1:erel 'a) (o2:erel 'd) (sp:'d)
(ch:set ('a,'d)) (inh:('a,'d)) =
chain (rprod o1 o2) ch /\ ch inh /\ supremum o2 (image snd ch) sp /\
(forall x y. ch (x,y) -> r x y) /\
(forall sp0. supremum o1 (image fst ch) sp0 -> not r sp0 sp)
predicate invalid_sup (r:rel 'a 'd) (o1:erel 'a) (o2:erel 'd) (sp:'d) =
exists ch inh. invalid_sup_witness r o1 o2 sp ch inh
function vld_fmla (r:rel 'a 'd) (o1:erel 'a) (o2:erel 'd) : fmla 'd =
b_universal (invalid_sup r o1 o2) sing_kont_fmla
predicate eqv (s:set 'a) (x y:'a) = x = y /\ s x
predicate valid_proj (e:enforce 'a 'i 'o) (r:rel 'a 'd) (o:erel 'd) =
(forall x y. r x y -> e.game_valid x) /\
(forall x y u v. r x y /\ r u v /\ o y v -> e.game_order x u)
predicate enforce_inv (e:enforce 'a 'i 'o) =
let o = e.game_order in
order o /\
(forall x ctx. e.ctx_predic x ctx <-> subset (e.ctx_minima x) ctx) /\
forall x q ctx. e.ctx_predic x ctx ->
let r = eqv e.game_valid in
let c = conj (ctx_fmla r ctx) (conj (vld_fmla r o o) (ordering o)) in
let p2 = related r (e.transformp q x) in
let q2 = related r (e_lift q) in
holds c (enforce p2 q2)
(* Very important lemma: in the invariant, we fixed the game support
type to be 'd = 'a, as well as we fixed the order and the relation.
However, this will still holds for ANY support type 'd and order
with a validity-compatible relation that maps ordering relation backward.
Note: monotonicity condition come from the fact that
if (x -> Q) is in context, what is truly implied is
(x -> \y. Q y /\ y >= x). However, related(\y. Q y /\ y >= x)
is a priori not a superset of \y. related(Q) y /\ y >= x'...
the condition on the ordering relation is the simplest way
to guarantee this.
Method:
1) build a canonical game satisfying the context
2) Show the relation induce simulation from the canonical game
to the 'd-one.
This lemma will be used to switch between game supports.
TODO: need to devise tools to carry out switching correctly on
context, as it is non-trivial. We may need to enforce
usage of a very particular kind of explicit contexts...
but they cannot be explicited for obvious typing reasons ! *)
lemma enforce_inv_reinforced : forall e:enforce 'a 'i 'o. enforce_inv e ->
let oe = e.game_order in
forall x q ctx rd,od:erel 'd. valid_proj e rd od /\ e.ctx_predic x ctx ->
let c = conj (ctx_fmla rd ctx) (conj (vld_fmla rd oe od) (ordering od)) in
let p0 = e.transformp q x in let q0 = e_lift q in
let pd = related rd p0 in let qd = related rd q0 in
holds c (enforce pd qd)
by forall gd. game_wf gd /\ c gd -> have_uniform_winning_strat gd pd qd
by let re = eqv e.game_valid in
let ctx0 = \p q. (exists p0 q0. bigunion ctx (p0,q0) /\
p = related re p0 /\ q = related re q0) \/
(exists sp. invalid_sup re oe oe sp /\
p = (=) sp /\ q = none)
in
let tr = \x s. exists p q. ctx0 p q /\ p x /\ s = inter q (oe x) in
let ge = { progress = oe; transition = tr } in
game_wf ge
(* Preliminary: related by re then rd is equivalent to relate
directly by rd *)
so ("stop_split" forall s. related rd (related re s) = related rd s
by let rds = related rd s in let res = related re s in
let rdes = related rd res in
sext rdes rds
by (forall x. rdes x -> rds x)
/\ (forall x. rds x -> rdes x
by exists y. s y /\ rd y x so res y by re y y)
)
(* All pre-post implied by the context are validated by ge
(the canonical game associated to the theorem) *)
so ("stop_split" forall p q. ctx0 p q -> enforce p q ge
by forall x. p x -> have_winning_strat ge x q
by let s = inter q (oe x) in
subset s q /\ tr x s)
(* Hence the context is validated by ge, and so the final
pre/post holds. *)
so let ce = conj (ctx_fmla re ctx) (conj (vld_fmla re oe oe) (ordering oe))
in ("stop_split" ce ge
by ctx_fmla re ctx ge
/\ (vld_fmla re oe oe ge)
/\ ordering oe ge
)
so let pe = related re p0 in let qe = related re q0 in
(enforce pe qe ge by holds ce (enforce pe qe))
(* To conclude, it remains only to notice that rd
induce a step-by-step simulation from ge to gd. *)
so step_simulate ge rd gd
by ("stop_split" limit_compatible oe rd gd
by forall ch inh sd. chain (rprod oe od) ch /\ ch inh /\
(forall a b. ch (a,b) -> rd a b) /\ supremum od (image snd ch) sd ->
(have_winning_strat gd sd none
\/ exists se. supremum oe (image fst ch) se /\ rd se sd)
by if invalid_sup rd oe od sd
then have_winning_strat gd sd none
by enforce ((=) sd) none gd
else not invalid_sup_witness rd oe od sd ch inh
so exists se. supremum oe (image fst ch) se /\ rd se sd
)
/\ "stop_split" forall x y s. tr x s /\ rd x y ->
(* Out of the two transition possibility, the invalid
supremum one is unfeasible as this supremum may not be related. *)
have_winning_strat gd y (related rd s)
by exists p q. ctx0 p q /\ p x /\ s = inter q (oe x)
so (false by exists sp. invalid_sup re oe oe sp /\
p = (=) sp /\ q = none so exists ch inh.
invalid_sup_witness re oe oe sp ch inh
so image fst ch = image snd ch
by sext (image fst ch) (image snd ch)
by (forall x. image fst ch x <-> ch (x,x))
/\ (forall x. image snd ch x <-> ch (x,x))
)
\/ (exists p0 q0. bigunion ctx (p0,q0) /\
p = related re p0 /\ q = related re q0
so enforce (related rd p0) (related rd q0) gd
so let cd = subgame gd in
holds cd (enforce (related rd p0) (related rd q0))
so let qr = related rd q in
(holds cd (enforce ((=) y) qr)
by subset ((=) y) (related rd p0))
so holds cd (enforce ((=) y) (inter qr (od y)))
so (holds cd (enforce ((=) y) (related rd s))
by subset (inter qr (od y)) (related rd s)
)
so have_uniform_winning_strat gd ((=) y) (related rd s)
)
function enf_transf (p:rel 'i 'a) (q:'i -> 'a -> rel 'o 'a) :
rel 'o 'a -> rel 'i 'a =
\q1 x xs. p x xs && forall y ys. q x xs y ys -> q1 y ys
predicate enforce_inv_enf_transf (p:rel 'i 'a)
(e:enforce 'a 'i 'o)
(q:'i -> 'a -> rel 'o 'a) =
let o = e.game_order in
let r = eqv e.game_valid in
order o /\
(forall x ctx. e.ctx_predic x ctx <-> subset (e.ctx_minima x) ctx) /\
forall x ctx xs. e.ctx_predic x ctx ->
let c = conj (ctx_fmla r ctx) (conj (vld_fmla r o o) (ordering o)) in
e.game_valid xs /\ p x xs ->
let qr = related r (e_lift (q x xs)) in
holds c (enforce ((=) xs) qr)
(* Special traduction of invariant when the predicate transformer
is derivable from a hoare triplet. *)
lemma enforce_inv_on_enf_transf : forall e:enforce 'a 'i 'o,p q.
e.transformp = enf_transf p q ->
enforce_inv e -> enforce_inv_enf_transf p e q
by forall x ctx xs. e.ctx_predic x ctx ->
let r = eqv e.game_valid in let o = e.game_order in
let c = conj (ctx_fmla r ctx) (conj (vld_fmla r o o) (ordering o)) in
e.game_valid xs /\ p x xs ->
let qr = related r (e_lift (q x xs)) in
holds c (enforce ((=) xs) qr)
by let p1 = e.transformp (q x xs) x in
let p2 = related r p1 in
holds c (enforce p2 qr)
so subset ((=) xs) p2 by r xs xs
(* Also useful: this traduction is an equivalence. *)
lemma enforce_inv_from_enf_transf : forall e:enforce 'a 'i 'o,p q.
e.transformp = enf_transf p q /\ enforce_inv_enf_transf p e q ->
enforce_inv e
by let o = e.game_order in let r = eqv e.game_valid in
forall x q0 ctx. e.ctx_predic x ctx ->
let c = conj (ctx_fmla r ctx) (conj (vld_fmla r o o) (ordering o)) in
let p2 = related r (e.transformp q0 x) in
let q2 = related r (e_lift q0) in