Commit da34dca3 authored by Martin Clochard's avatar Martin Clochard
Browse files

examples(wip): 2wp_gen

parent 2411344a
SHELL=/bin/bash
REPLAY=why3 replay -L .
MLW=base choice ho_set ho_rel fn order transfinite game
MLW=base choice ho_set ho_rel fn order transfinite game game_fmla
replay:
@exe() { echo "$$0 $$@"; "$$@"; };\
......
......@@ -2,13 +2,13 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../base.mlw">
<theory name="Fun" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="FunExt" sum="74d4af5538daa9eb9ddee6284a05e5bf">
<goal name="WP_parameter extensional" expl="VC for extensional">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
<theory name="FunCategory" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -19,34 +19,34 @@
<goal name="ext.1" expl="1.">
<transf name="inline_goal">
<goal name="ext.1.1" expl="1.">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</transf>
</goal>
<goal name="ext.2" expl="2.">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
</transf>
</goal>
<goal name="assoc">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="neutral">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="FunExt.extensionality">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="FunCategory.assoc">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="FunCategory.neutral">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</theory>
<theory name="Set" sum="8dc39e2ae96fd0498b0d50bb47f235eb">
<goal name="sext_is_ext">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
</theory>
<theory name="Rel" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -63,66 +63,66 @@
<goal name="extensionality">
<transf name="split_goal_wp">
<goal name="extensionality.1" expl="1.">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="extensionality.2" expl="2.">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="extensionality.3" expl="3.">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
</transf>
</goal>
<goal name="assoc">
<transf name="compute_specified">
<goal name="assoc.1" expl="1.">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
</transf>
</goal>
<goal name="reverse_antimorphism">
<proof prover="0"><result status="valid" time="0.01" steps="27"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
<goal name="reverse_antimorphism_id">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="reverse_involution">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="neutral">
<transf name="compute_specified">
<goal name="neutral.1" expl="1.">
<proof prover="0"><result status="valid" time="0.00" steps="14"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
</transf>
</goal>
<goal name="RelExt.extensionality">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="RelCategory.assoc">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="RelCategory.reverse_antimorphism">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="RelCategory.reverse_antimorphism_id">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="RelCategory.reverse_involution">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="RelCategory.neutral">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
</theory>
<theory name="SubsetOrder" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="SetProofs" sum="0be5aa0fe01aa313571b5c5ef55cb77b">
<goal name="anti_subset">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="SubsetOrder.subset_order">
<proof prover="0"><result status="valid" time="0.02" steps="65"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="65"/></proof>
</goal>
</theory>
<theory name="Image" sum="d41d8cd98f00b204e9800998ecf8427e">
......
......@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../choice.mlw">
<theory name="Choice" sum="7c1ca533a0ae37f3bd6e59347ceef0bd">
<goal name="WP_parameter choose" expl="VC for choose">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="WP_parameter choose_if" expl="VC for choose_if">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
</file>
......
......@@ -7,5 +7,7 @@
</theory>
<theory name="Category" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Image" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
</file>
</why3session>
......@@ -1993,123 +1993,3 @@ module StratProofs
end
(*
lemma absurdity : forall sc:section 'a 'b,dmn.
section_hypothesis sc ->
let evl = evolve sc dmn in
let bs = basic sc in
let st = fixpoint_above sc.sd evl bs in
let angb = sim_angel sc in
let winb = rel_map sc.r sc.win in
(forall x. st.h_total x -> not winb x) /\
not win_at sc.g2 winb angb dmn st.h_total ->
false
by let o1 = sc.g1.progress in let o2 = sc.g2.progress in
let op = oprod o1 o2 in
let pr = sup op st.h_pair in
let (a,b) = pr in
let nst = evl st in
tr_reach sc.sd evl bs st
so coherent sc dmn st
so maximum sc.sd (tr_reach sc.sd evl bs) st
so if not maximum op st.h_pair pr
then nst.h_pair pr so chain op st.h_pair
so (exists y. supremum op st.h_pair y)
so supremum op st.h_pair pr
so upper_bound op st.h_pair pr so false
else let s0 = sc.anga a st.h_proj in
if st.i_dmn s0 <> None \/ not sc.g1.transition a s0
then (* This is the point where we use the fact that
'a-angel must win. *)
let dmna = \x. match st.i_dmn x with
| None -> default
| Some a -> a
end
in
compat st.i_dmn dmna
so reconstructed sc st dmna
so (forall x. st.h_proj x -> not (sc.win x
so exists y. st.h_pair (x,y) so sc.r x y
so rel_map_witness sc.r sc.win y x so winb y
so st.h_total y))
so (maximum o1 st.h_proj a by forall u. st.h_proj u ->
o1 u a by exists v. st.h_pair (u,v) so op (u,v) (a,b))
so supremum o1 st.h_proj a
so a = sup o1 st.h_proj
so (sc.g1.transition a s0 -> dmna s0 = a /\ s0 (dmna s0)
by match st.i_dmn s0 with
| None -> false
| Some u -> s0 u /\ u = a
end)
so let nxt = strat_next sc.g1 sc.anga dmna in
nxt st.h_proj = a
so pext (extends_ch o1 nxt st.h_proj) st.h_proj
so maximum (subchain o1)
(tr_reach (subchain o1) (extends_ch o1 nxt) ((=) sc.basea))
st.h_proj
so (not win_against sc.g1 sc.basea sc.win sc.anga dmna
by forall ch. reach_ch o1 nxt ((=) sc.basea) ch ->
win_at sc.g1 sc.win sc.anga dmna ch -> false
by exists x. maximum o1 ch x /\
(sc.win x \/ let a = sc.anga x ch in sc.g1.transition x a /\
not a (dmna a))
so not (sc.win x so subchain o1 ch st.h_proj so st.h_proj x)
so supremum o1 ch x
so x = sup o1 ch
so nxt ch = x
so ext (extends_ch o1 nxt ch) ch
so maximum (subchain o1)
(tr_reach (subchain o1) (extends_ch o1 nxt) ((=) sc.basea))
ch
so ch = st.h_proj
so false)
so not winning_strat sc.g1 sc.basea sc.win sc.anga
so false
else false by let target = rel_map sc.r s0 in
let bl = sup o2 st.h_local in
if target bl
then let al = choice (rel_map_witness sc.r s0 bl) in
nst.i_dmn s0 = Some al so false
else let iang = iangel sc b target in
let nxt = strat_next sc.g2 iang dmn in
nst.h_local = extends_ch o2 nxt st.h_local
so if win_at sc.g2 winb angb dmn st.h_total then true else
not (nst.h_local = st.h_local
so locally_winning sc dmn st
so reach_ch o2 nxt ((=) b) st.h_local
so maximum (subchain o2)
(tr_reach (subchain o2) (extends_ch o2 nxt) ((=) b))
st.h_local
so (not win_against sc.g2 b target iang dmn
by forall ch. reach_ch o2 nxt ((=) b) ch ->
win_at sc.g2 target iang dmn ch -> false
by exists x. maximum o2 ch x /\
(target x \/ let a = iang x ch in sc.g2.transition x a /\
not a (dmn a))
so (supremum o2 st.h_local bl
by exists y. supremum o2 st.h_local y)
so not (target x so subchain o2 ch st.h_local so st.h_local x
so maximum o2 st.h_local x
so supremum o2 st.h_local x
so x = bl)
so supremum o2 ch x
so x = sup o2 ch
so nxt ch = x
so ext (extends_ch o2 nxt ch) ch
so maximum (subchain o2)
(tr_reach (subchain o2) (extends_ch o2 nxt) ((=) b))
ch
so ch = st.h_local
so x = bl
so maximum o2 st.h_total bl
so maximal_witness sc st.h_total st dmn
so any_max_witness sc st.h_total st
so st = choice (any_max_witness sc st.h_total)
so iang bl ch = angb bl st.h_total)
so not winning_strat sc.g2 b target iang
so sc.r a b
so exists ang. winning_strat sc.g2 b target ang)
so false
end*)
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -79,27 +79,24 @@ module Fmla
(* Game formulae: predicates over games. *)
type fmla 'a = game 'a -> bool
(* Valid game formulae: formula increasing with respect to the subgame
relationship (Kripke semantics for intuitionistic logic) *)
predicate is_fmla (f:fmla 'a) = forall g1 g2. subgame g1 g2 /\ f g1 -> f g2
predicate is_fmla (f:fmla 'a) =
forall g g2. subgame g g2 /\ f g -> f g2
(* `P enforce Q` mean that from a state in P, we have a winning
strategy to reach a state in Q. *)
function enforce (p q:set 'a) : fmla 'a =
\g. have_uniform_winning_strat g p q
function enforce (p q:set 'a) : fmla 'a = \g. have_uniform_winning_strat g p q
(* Higher-order lifting of enforce: \u. enforce (p u) (q u) *)
function u_enforce (p q:rel 'b 'a) : 'b -> fmla 'a =
\b. enforce (p b) (q b)
(* Intuitionistic arrow. *)
function arrow (f1 f2:fmla 'a) : fmla 'a =
\g. forall g2. subgame g g2 /\ game_wf g2 /\ f1 g2 -> f2 g2
(* Intuitionistic implication (Kripke interpretation) *)
predicate arrow (f1 f2:fmla 'a) (g:game 'a) =
forall g2. subgame g g2 /\ game_wf g2 /\ f1 g2 -> f2 g2
(* Universal quantifiers (restricted and general) *)
function b_universal (s:'b -> bool) (p:'b -> fmla 'a) : fmla 'a =
\g. forall y. s y -> p y g
predicate b_universal (s:'b -> bool) (p:'b -> fmla 'a) (g:game 'a) =
forall y. s y -> p y g
function universal (p:'b -> fmla 'a) : fmla 'a = b_universal all p
(* Conjonction. Could also be deduced from
......@@ -179,39 +176,37 @@ module FmlaRules "W:non_conservative_extension:N" (* => FmlaRulesProof *)
use import game.Game
use export Fmla
(* Formula builders indeed build formulas. *)
(* Formula builders indeed build formulas *)
axiom enforce_fmla : forall p q:set 'a. is_fmla (enforce p q)
axiom arrow_fmla : forall f1 f2:fmla 'a. is_fmla (arrow f1 f2)
axiom b_universal_fmla : forall s:'b -> bool,f:'b -> fmla 'a.
axiom b_universal_fmla : forall s:set 'b,f:'b -> fmla 'a.
(forall x. s x -> is_fmla (f x)) -> is_fmla (b_universal s f)
(*axiom universal_fmla : forall f:'b -> fmla 'a.
(forall x. is_fmla (f x)) -> is_fmla (universal f)
axiom existential_fmla : forall f:'b -> fmla 'a.
(forall x. is_fmla (f x)) -> is_fmla (existential f)*)
axiom arrow_fmla : forall f1 f2:fmla 'a. is_fmla (arrow f1 f2)
axiom conj_fmla : forall f1 f2:fmla 'a. is_fmla f1 /\ is_fmla f2 ->
is_fmla (conj f1 f2)
axiom ordering_fmla : forall o:erel 'a. is_fmla (ordering o)
(* Weakening rule. *)
axiom enforce_monotonic : forall c,p1 p2 q1 q2:set 'a. is_fmla c ->
axiom enforce_monotonic : forall c,p1 p2 q1 q2:set 'a.
subset p2 p1 /\ holds c (enforce p1 q1) /\ subset q1 q2 ->
holds c (enforce p2 q2)
axiom enforce_does_progress : forall c o x,q:set 'a. is_fmla c ->
axiom enforce_does_progress : forall c o x,q:set 'a.
holds c (enforce ((=) x) q) /\ holds c (ordering o) ->
holds c (enforce ((=) x) (inter q (o x)))
axiom sequence : forall c,p q r:set 'a. is_fmla c ->
axiom sequence : forall c,p q r:set 'a.
holds c (enforce p q) /\ holds c (enforce q r) -> holds c (enforce p r)
(* Continuation rule: to prove that P enforce Q, we may take as
hypothesis that Q enforce False. *)
axiom kont_intro : forall c,p q:set 'a. is_fmla c ->
holds (conj c (enforce q none)) (enforce p q) -> holds c (enforce p q)
axiom kont_intro : forall c,p q:set 'a.
holds c (arrow (enforce q none) (enforce p q)) ->
holds c (enforce p q)
(* External precondition rule: to prove that P enforce Q,
it is enough to prove that forall x. (=) x enforce Q.
(the other way around is obvious by weakening) *)
axiom external_pre : forall c,p q:set 'a. is_fmla c ->
axiom external_pre : forall c,p q:set 'a.
(forall y. p y -> holds c (enforce ((=) y) q)) -> holds c (enforce p q)
(* Transfinite loop rule:
......@@ -222,7 +217,6 @@ module FmlaRules "W:non_conservative_extension:N" (* => FmlaRulesProof *)
prove that Inv enforce False.
(we can derive rules with real postcondition from this one + Kont). *)
axiom trampoline : forall c go,i:rel 'b 'a,o:erel 'b.
is_fmla c ->
holds c (universal (u_enforce i (later o i))) /\
holds c (ordering go) /\ order o /\
(forall ch f inh y. chain o ch /\ supremum go (image f ch) y /\
......@@ -231,10 +225,8 @@ module FmlaRules "W:non_conservative_extension:N" (* => FmlaRulesProof *)
holds c (enforce ((=) y) (later_limit o i ch))) ->
holds c (universal (u_enforce i (const none)))
(* Standard abstraction rule of intuitionistic logic. *)
axiom abstraction : forall c f1 f2:fmla 'a.
is_fmla c /\ is_fmla f1 /\ is_fmla f2 ->
holds c (arrow f1 f2) <-> holds (conj c f1) f2
is_fmla c -> holds c (arrow f1 f2) <-> holds (conj c f1) f2
(* TODO: rewrite vertical fixpoint
(* Vertical fixpoint rule (or transfinite call-stack rule):
......@@ -323,8 +315,8 @@ module FmlaRulesProof
But any run of P enforce Q in this modified game
can be mapped as is to a P enforce Q run in the initial game,
so we're done. *)
lemma kont_intro : forall c,p q:'a -> bool. is_fmla c ->
holds (conj c (enforce q none)) (enforce p q) ->
lemma kont_intro : forall c,p q:'a -> bool.
holds c (arrow (enforce q none) (enforce p q)) ->
holds c (enforce p q)
by forall g. game_wf g /\ c g ->
have_uniform_winning_strat g p q
......@@ -449,7 +441,7 @@ module FmlaRulesProof
This version relax a lot the limit requirements by using
version 1 with specific invariants and ordering
(subchain ordering with injective product) *)
lemma better_trampoline : forall c go o,i:rel 'b 'a. is_fmla c ->
lemma better_trampoline : forall c go o,i:rel 'b 'a.
holds c (universal (u_enforce i (later o i))) /\
holds c (ordering go) /\ order o /\
(forall ch inh y. chain (iprod o go) ch /\ supremum go (image snd ch) y /\
......@@ -571,7 +563,6 @@ module FmlaRulesProof
monotone-function-based criterion imply the one based on
injective product. *)
lemma trampoline : forall c go,i:rel 'b 'a,o.
is_fmla c ->
holds c (universal (u_enforce i (later o i))) /\
holds c (ordering go) /\ order o /\
(forall ch f inh y. chain o ch /\ supremum go (image f ch) y /\
......@@ -611,11 +602,11 @@ module FmlaRulesProof
lemma conj_fmla : forall f1 f2:fmla 'a. is_fmla f1 /\ is_fmla f2 ->
is_fmla (conj f1 f2)
lemma sequence : forall c,p q r:set 'a. is_fmla c ->
lemma sequence : forall c,p q r:set 'a.
holds c (enforce p q) /\ holds c (enforce q r) -> holds c (enforce p r)
by forall g. game_wf g /\ c g -> enforce p r g
by let go = g.progress in
let c' = conj c (ordering go) in
let c' = conj (enforce p q) (conj (enforce q r) (ordering go)) in
holds c' (enforce p r)
by let c'' = conj c' (enforce r none) in
(holds c'' (enforce p r) by subset none r)
......@@ -631,7 +622,6 @@ module FmlaRulesProof
subset (i (n+1)) (later (<=) i n)))
)
/\ holds c'' (ordering go)
/\ is_fmla c''
/\ (forall ch f inh. chain (<=) ch /\ ch inh /\
monotone_on ch (<=) f go /\
(forall x. ch x -> i x (f x)) -> (exists x. maximum (<=) ch x)
......@@ -640,404 +630,1139 @@ module FmlaRulesProof
|| (ch 1 so maximum (<=) ch 1)
|| (ch 0 so maximum (<=) ch 0))
(* Abstraction rule (basically come from subgame being a preorder) *)
lemma open_abstraction : forall c f1 f2:fmla 'a.
holds c (arrow f1 f2) -> holds (conj c f1) f2
lemma close_abstraction : forall c f1 f2:fmla 'a. is_fmla c ->
holds (conj c f1) f2 -> holds c (arrow f1 f2)
(* TODO: recursion theorem. *)
(* Re-thinking recursion theorem: the context dependency completely
kills the stack-of-strategy proof. However, it also opens
a vast spectrum of usages for this combinator, notably cps.
And actually, cps seems to be the right way to carry out the proof.
Indeed, since we carry a dependent context, we can in particular
fit a continuation inside.
In that setup (and simplifying out the extra state for readability),
the theorem rewrite as:
If:
C |- forall x. (forall y > x. phi y => ((=) y) enforce False) =>
phi x => ((=) x) enforce False
Forall X non-empty chain, C |- (forall y in X. phi y) -> phi (sup X)
C |- phi x_0
Then:
C |- ((=) x_0) enforce False
The proof of this theorem is rather special.
First, we reduce to C being cone(G) for some G such that C(G).
Then, we use the transfinite loop rule with the extra state
being... a stack of game (really !)
At the bottom of the stack sits G.
But G does not allows ((=) x0) enforce False directly.
The only way to do that is to use the recursion hypothesis,
but for this we need (forall y > x. phi y -> ((=) y) enforce False).
Then, we could add to G extra to-empty transitions for y such that
phi holds in G... but that a priori does NOT yield a game where
(forall y > x. phi y -> ((=) y) enforce False) holds, because there
could be MORE values for which phi holds now (thankfully, there
cannot be less because phi is subgame-monotonic)
===> We can define a transfinite process of saturation that
add to-empty transitions as needed, and eventually reach a fixpoint
G_{fix}. For this game, we know that ((=) x_0) enforce False
holds. However,
it might be that the last transition we takes (for exiting) does not
exists in G ! Then, there exists G_{\alpha} in the saturation process
that was responsible for the introduction of that y->False transition
(not present in G_{\alpha} but is in G_{\alpha^+}). For this
game, we need to prove y->False. But we can achieve this by using
the fixpoint hypothesis for that y. Then we saturate again, adding
a layer to the stack (which is now {<x_0|G>,<y|G_{\alpha}>}).
However, there are now two kinds of transition in G_{\alpha} that are
wrong... in fact that's not a problem as we can just cut out to
the right layer.
So let's sum up:
- State is a well-founded injective chain of pairs <state|game>,
with <x_0|G> being the bottom of the chain,
and where each successor pair (<x|G_x>,<y|G_y>) verify
that G_y is obtained by x-saturation of G_x
- Each pair <x|G> in the stack has G |- phi(x)
- Each limit pair (limit if forall x < l. exists z: x < z < l,
e.g not successor) is the supremum of its lower pairs.
Which gives the state invariants. Now, we also need to define
an ordering between such stacks:
S_0 <= S_1 if, with P being the largest common prefix of (S_0,S_1)
(S_0 = P ++ X, S_1 = P ++ Y, X and Y differ from the bottom.
P exists since S_0/S_1 are well-founded),
we have that:
- Y is empty => X is empty as well
- Forall <y|_> in Y, y is above any element of X
- If Y and X have minimum elements <y|G_y> and <x|G_x> with x = y,
and P have maximum element <z|G_z>, then G_y is strictly lower than
G_x in the z-saturation of G_z. Note that by the above definition,
if P <> S_0, then P necessarily have a maximum.
(this implies P <> S_1 as well. If P had no maximum,
then the limit would be the minimum of S_0 and S_1, and P would
not be the lcp) *)
(* Some definitions/simple lemmas to prove the cps recursion theorem.
The cps recursion theorem is (with simplified extra state):
If
C is cone(G) for a given game
C |- forall x. (forall y > x. ctx y => (=) y enforce False) =>
phi x => (=) x enforce False)
(forall X non-empty chain, C |- (forall x in X. phi x) => phi (sup x))
C |- phi x_0
Then
C |- (=) x_0 enforce False *)
(* There is a (trivial) formula corresponding to the cone
generated by a game (more importantly, this is indeed a formula. *)
lemma cone_fmla : forall g:game 'a. is_fmla (subgame g)
(* Regroup parameters. *)
(* From that point on, the goal is to prove the
'crude recursion theorem'.
If we have:
- An ordered set B
- A non-empty-chain-stable precondition on (B,Game-support) chains
- Q a (B,input)-dependent postcondition only
- Forall X non-empty (B,game-support) chain,
Gamma |- forall X. (forall Y strict super-chain of X =>
P Y enforce exists y in Y. Q Y) =>
P X enforce exists x in X. Q x
- Gamma |- Q X_0 enforce False
Then, Gamma |- P X_0 enforce False
Initially, we even restrict Gamma to a singleton. *)
(* Regroup parameters *)
type section 'a 'b = {
(* Base game *)
gm : game 'a;
(* Progression order *)
(* Progression order *)
bo : erel 'b;
(* Dependent context for ((=) x) enforce False *)
ctx : 'b -> 'a -> fmla 'a;
(* Base points. *)
bs_a : 'a;
bs_b : 'b;
(* Precondition *)
pr : set (set ('b,'a));
(* Postcondition *)
ps : rel ('b,'a) 'a;
}
(* The basic arrow we intend to prove by recursion. *)
function rcps_impl (sc:section 'a 'b) (x:'b) (y:'a) : fmla 'a =
arrow (sc.ctx x y) (enforce ((=) y) none)
(* Recursive hypothesis. *)
function rcps_hyp (sc:section 'a 'b) (x:'b) : fmla 'a =
b_universal (lower sc.bo x) (\x. universal (rcps_impl sc x))
(* chain-complete ordering on game transitions. *)
type trans 'a = 'a -> set (set 'a)
predicate tro (t1 t2:trans 'a) = forall x. subset (t1 x) (t2 x)
function tro_complete (s:set (trans 'a)) : trans 'a =
\x z. exists u. s u /\ u x z
lemma tro_fully_complete :
let o = (tro:erel (trans 'a)) in
(order o by antisymetric o by forall x y. o x y /\ o y x ->
ext x y by (forall u. sext (x u) (y u)))
&& (forall s. let cpl = tro_complete s in
supremum o s cpl
by upper_bound o s cpl
/\ forall u. upper_bound o s u -> o cpl u
by forall x y. cpl x y -> u x y
by exists v. s v /\ v x y so o v u)
&& chain_complete o
&& (forall s x. supremum o s x -> x = tro_complete s)
(* Saturation process: If we have a game that satisfy
[ctx x] for a recursive layer x, we need to be able to
create a game that satisfy the recursive hypothesis
[forall y > x. (ctx y) => (from y) enforce False]
We do so by adding necessary transitions step-by-step,
e.g taking all y > x such that [ctx y] holds in the game and
additing respective y -> {} transitions.
After a step, the modified game might not satisfy