diff --git a/examples/in_progress/2wp_gen/base.mlw b/examples/in_progress/2wp_gen/base.mlw index c7d9789ba2a5a4259c71412365748e7bddc93451..c42eba12c86e48fcc190d18d96cc77e820af5ad3 100644 --- a/examples/in_progress/2wp_gen/base.mlw +++ b/examples/in_progress/2wp_gen/base.mlw @@ -95,6 +95,16 @@ module Set end +(* Some usual big operators on sets. *) +module SetBigOps + + use import Set + + function bigunion (c:set (set 'a)) : set 'a = \x. exists s. c s /\ s x + function biginter (c:set (set 'a)) : set 'a = \x. forall s. c s -> s x + +end + (* Basic definition on relations-as-arrows *) module Rel diff --git a/examples/in_progress/2wp_gen/base/why3session.xml b/examples/in_progress/2wp_gen/base/why3session.xml index 2be9fd135138a342257d39c12d8b80e398ac7378..a5b9d6f82adc5cd33e09eb2f8120d202ae43fa95 100644 --- a/examples/in_progress/2wp_gen/base/why3session.xml +++ b/examples/in_progress/2wp_gen/base/why3session.xml @@ -2,13 +2,13 @@ - + - + @@ -19,36 +19,38 @@ - + - + - + - + - + - + - + - + + + @@ -63,66 +65,66 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/in_progress/2wp_gen/choice/why3session.xml b/examples/in_progress/2wp_gen/choice/why3session.xml index b3ee6b7838f717093f4b9efa4c1adcc4fe5073ef..1c9c57e5660bc5b95514c849ca4d5765dbc12763 100644 --- a/examples/in_progress/2wp_gen/choice/why3session.xml +++ b/examples/in_progress/2wp_gen/choice/why3session.xml @@ -2,14 +2,14 @@ - + - + - + diff --git a/examples/in_progress/2wp_gen/game.mlw b/examples/in_progress/2wp_gen/game.mlw index 9954f41470d5574779fe23ba5e0f136860be3622..f3288a2237f2fc8b067a48394f03ec4d183438e2 100644 --- a/examples/in_progress/2wp_gen/game.mlw +++ b/examples/in_progress/2wp_gen/game.mlw @@ -1,6 +1,6 @@ (* Asymetric angel vs demon perfect information games on - chain-complete orders. + quasi-chain-complete orders. Angel and demon reflect respectively existential and universal behavior. Definition mostly intended for angel possibility results, @@ -38,11 +38,11 @@ module Game the set of states he has to choose in. *) type demon 'a = set 'a -> 'a - (* Game well-formed: as stated above, order is chain-complete + (* Game well-formed: as stated above, order is quasi chain-complete and transition respect progression (loosely: there may be loops) *) predicate game_wf (g:game 'a) = - order g.progress /\ chain_complete g.progress /\ + order g.progress /\ q_chain_complete g.progress /\ forall x s y. g.transition x s /\ s y -> g.progress x y (* Describe a step in the game, as the next element in function @@ -199,6 +199,7 @@ module DmnReachProofs use import DmnReachCommon use import fn.Fun use import ho_set.Set + use import ho_set.SetBigOps use import order.Chain use import order.WfChain use import order.LimUniq @@ -263,11 +264,11 @@ module DmnReachProofs same_choices g ang ch0 dmn1 dmn2) by order sb so dmn_witness g ang b ((=) b) dmn2 /\ - (same_choices g ang ((=) b) dmn1 dmn2 - by forall ch0 x. sb ch0 ((=) b) /\ maximum o ch0 x /\ - ch0 <> ((=) b) -> false - by if ch0 b then sext ch0 ((=) b) else sext ch0 none) - /\ (forall ch0. dmn_witness g ang b ch0 dmn1 /\ + ("stop_split" same_choices g ang ((=) b) dmn1 dmn2 + by forall ch0 x. sb ch0 ((=) b) /\ maximum o ch0 x /\ + ch0 <> ((=) b) -> false + by if ch0 b then sext ch0 ((=) b) else sext ch0 none) + /\ ("stop_split" forall ch0. dmn_witness g ang b ch0 dmn1 /\ dmn_witness g ang b ch0 dmn2 /\ same_choices g ang ch0 dmn1 dmn2 /\ sb (xt1 ch0) ch -> (dmn_witness g ang b (xt1 ch0) dmn2 /\ @@ -275,7 +276,8 @@ module DmnReachProofs by ("case_split" if xt1 ch0 = ch0 then true else let x = sup o ch0 in if not ch0 x - then (sext (xt1 ch0) (xt2 ch0) by st1 ch0 = st2 ch0) + then "stop_split" + (sext (xt1 ch0) (xt2 ch0) by st1 ch0 = st2 ch0) /\ forall ch1 x1. sb ch1 (xt1 ch0) /\ maximum o ch1 x1 /\ ch1 <> (xt1 ch0) -> dmn1 (ang x1 ch1) = dmn2 (ang x1 ch1) @@ -284,9 +286,11 @@ module DmnReachProofs by dmn_witness g ang b (xt1 ch0) dmn1 so dmn_witness g ang b ch1 dmn1 so separator sb xt1 ch0 ch1) - else let a = ang x ch0 in + else + let a = ang x ch0 in if dmn1 a = dmn2 a - then (sext (xt1 ch0) (xt2 ch0) by st1 ch0 = st2 ch0) + then "stop_split" + (sext (xt1 ch0) (xt2 ch0) by st1 ch0 = st2 ch0) so forall ch1 x1. sb ch1 (xt1 ch0) /\ maximum o ch1 x1 /\ ch1 <> xt1 ch0 -> dmn1 (ang x1 ch1) = dmn2 (ang x1 ch1) @@ -296,7 +300,8 @@ module DmnReachProofs by dmn_witness g ang b (xt1 ch0) dmn1 so dmn_witness g ang b ch1 dmn1 else x1 = x - else false + else "stop_split" + false by (not same_choices g ang ch dmn1 dmn2 by sb ch0 ch /\ ch0 <> ch /\ maximum o ch0 x) so st1 ch0 = dmn1 a @@ -304,7 +309,7 @@ module DmnReachProofs so not (dmn1 a = x so sext ch0 (xt1 ch0)) so st1 ch0 <> st2 ch0 so if not dmn_witness g ang b ch dmn2 then true else - false by if xt2 ch0 = ch0 + "stop_split" false by if xt2 ch0 = ch0 then false by maximum sb (tr_reach sb xt2 ((=) b)) ch0 so sb ch ch0 so sb ch0 ch else false by dmn_witness g ang b (xt2 ch0) dmn2 @@ -320,7 +325,8 @@ module DmnReachProofs so antisymetric o ) by chain o ch0 so xt1 ch0 = add ch0 (st1 ch0) so xt2 ch0 = add ch0 (st2 ch0)) - /\ (forall chh y. supremum sb chh y /\ chain sb chh /\ chh ((=) b) /\ + /\ ("stop_split" + forall chh y. supremum sb chh y /\ chain sb chh /\ chh ((=) b) /\ (forall x. chh x /\ sb x ch -> dmn_witness g ang b x dmn2 /\ same_choices g ang x dmn1 dmn2) -> sb y ch -> @@ -379,11 +385,11 @@ module DmnReachProofs let dmn_x = \x. choice (dmn_witness g ang b x) in (forall x. chh x -> dmn_witness g ang b x (dmn_x x) by exists dmn. dmn_witness g ang b x dmn) - so ch = subchain_completion chh + so ch = bigunion chh so order sb so let p0 = \ch0 s. sb ch0 s /\ ch0 <> s /\ chh s in let sub_wit = \ch0. choice (p0 ch0) in - (forall ch0. sb ch0 ch /\ ch0 <> ch -> + ("stop_split" forall ch0. sb ch0 ch /\ ch0 <> ch -> let s = sub_wit ch0 in sb ch0 s /\ ch0 <> s /\ chh s by (exists s. subset ch0 s /\ ch0 <> s /\ chh s so sb ch0 s so p0 ch0 s) @@ -400,7 +406,7 @@ module DmnReachProofs let dmn_l = \s. let ch0 = choice (ch_by s) in let db = dmn_x (sub_wit ch0) in db s in - (forall ch1. chh ch1 -> dmn_witness g ang b ch1 dmn_l + ("stop_split" forall ch1. chh ch1 -> dmn_witness g ang b ch1 dmn_l by let dmn = dmn_x ch1 in same_choices g ang ch1 dmn dmn_l by forall ch0 x. sb ch0 ch1 /\ maximum o ch0 x /\ @@ -536,6 +542,7 @@ module StratProofs use import order.LimUniq use import fn.Fun use import ho_set.Set + use import ho_set.SetBigOps use import transfinite.Iterates use import transfinite.ChainExtension @@ -582,7 +589,7 @@ module StratProofs (have_winning_strat g x win <-> win x \/ exists s. g.transition x s /\ have_uniform_winning_strat g s win) (* First implication. *) - by (have_winning_strat g x win -> not win x -> + by ("stop_split" have_winning_strat g x win -> not win x -> exists s. g.transition x s /\ have_uniform_winning_strat g s win by let ex = (=) x in exists ang. winning_strat g x win ang /\ s = ang x ex @@ -600,16 +607,16 @@ module StratProofs winning_strat g y win ang2 by forall dmn2. win_against g y win ang2 dmn2 by let dmn = update dmn2 s y in - (let st = step g ang dmn in + ("stop_split" let st = step g ang dmn in let st2 = step g ang2 dmn2 in let xt = extends_ch o st in let xt2 = extends_ch o st2 in - let ey = ((=) y) in + let ey = (=) y in exists ch2. reach_ch o st2 ey ch2 /\ win_at g win ang2 dmn2 ch2 by if win y then ch2 = ey so maximum o ey y else exists ch. reach_ch o st ex ch /\ win_at g win ang dmn ch /\ ch2 = remove ch x - so (forall ch0. reach_ch o st ex ch0 -> + so ("stop_split" forall ch0. reach_ch o st ex ch0 -> let c = add (remove ch0 x) x in c = ch0 by sext c ch0 by ch0 x by sb ex ch0) so (order o /\ transitive o /\ order sb /\ inflationary sb xt) @@ -619,7 +626,8 @@ module StratProofs ch0 <> ex -> reach_ch o st2 ey (remove ch0 x)) by let exy = add ex y in (* case Reach_succ *) - (forall ch0. reach_ch o st ex ch0 /\ (ch0 <> ex -> + ("stop_split" + forall ch0. reach_ch o st ex ch0 /\ (ch0 <> ex -> reach_ch o st2 ey (remove ch0 x)) -> reach_ch o st2 ey (remove (xt ch0) x) by "case_split" @@ -634,8 +642,9 @@ module StratProofs by chain o ch0 so chain o rx so xt ch0 = add ch0 (st ch0) /\ xt2 rx = add rx (st2 rx) - so (st2 rx = st ch0 - by let u = sup o ch0 in + so ("stop_split" st2 rx = st ch0 + by (ch0 y by subset exy ch0) + so let u = sup o ch0 in supremum o ch0 u so (supremum o rx u by upper_bound o rx u /\ forall v. @@ -645,11 +654,11 @@ module StratProofs by t <> x || (o x y /\ o y v by rx y by sb exy ch0)) so u = sup o rx - so (ch0 y by subset exy ch0) so o y u so ((ch0 u <-> rx u) by u <> x) so let a = ang u ch0 in a = ang2 u rx - so (g.transition u a -> dmn a = dmn2 a by (a = s -> + so ("stop_split" + g.transition u a -> dmn a = dmn2 a by (a = s -> o u y so sb exy ch0 so (forall v. ch0 v /\ not exy v -> false by exy y so o y v so o v u so o v y so y = v) @@ -669,7 +678,8 @@ module StratProofs so subset exy ch0 so o y (st ch0) so o x y so not o y x so not o (st ch0) x) /\ (* case Reach_chain. *) - (forall chh ch0. chain sb chh /\ supremum sb chh ch0 /\ + ("stop_split" + forall chh ch0. chain sb chh /\ supremum sb chh ch0 /\ chh ex /\ ch0 <> ex /\ (forall u. chh u -> reach_ch o st ex u /\ (u <> ex -> reach_ch o st2 ey (remove u x))) -> @@ -687,7 +697,7 @@ module StratProofs by a = ey || b = ey || ( sb (add a x) (add b x) \/ sb (add b x) (add a x))) so supremum sb chh2 (remove ch0 x) - by (forall bd. upper_bound sb chh2 bd -> + by ("stop_split" forall bd. upper_bound sb chh2 bd -> sb (remove ch0 x) bd by o x y so not o y x so sb ey bd so (upper_bound sb chh (add bd x) @@ -702,7 +712,7 @@ module StratProofs so ch0 = add (remove ch0 x) x so (not bd x by ey y /\ not ey x) so not remove ch0 x x) - /\ (upper_bound sb chh2 (remove ch0 x) + /\ ("stop_split" upper_bound sb chh2 (remove ch0 x) by forall u. chh2 u -> sb u (remove ch0 x) by add (remove ch0 x) x = ch0 so not remove ch0 x x so not u x so @@ -728,10 +738,10 @@ module StratProofs by win_against g x win ang dmn )) /\ (* Inverse implications. *) - (win x -> have_winning_strat g x win + ("stop_split" win x -> have_winning_strat g x win by forall dmn. win_against g x win witness dmn by win_at g win witness dmn ((=) x) - by maximum o ((=) x) x) /\ forall s. g.transition x s + by maximum o ((=) x) x) /\ "stop_split" forall s. g.transition x s /\ have_uniform_winning_strat g s win -> have_winning_strat g x win by exists ang. uniform_winning_strat g s win ang @@ -744,8 +754,7 @@ module StratProofs let ey = ((=) y) in if not s y then win_at g win ang2 dmn ex by maximum o ex x - else - let st = step g ang dmn in + else let st = step g ang dmn in let st2 = step g ang2 dmn in let xt = extends_ch o st in let xt2 = extends_ch o st2 in @@ -766,10 +775,12 @@ module StratProofs reach_ch o st2 ex (add ch0 x)) by let exy = add ey x in (* case Reach_base. *) - (reach_ch o st2 ex exy by sext (xt2 ex) exy by st2 ex = y + ("stop_split" + reach_ch o st2 ex exy by sext (xt2 ex) exy by st2 ex = y by x = sup o ex by supremum o ex x) /\ (* case Reach_succ. *) - (forall ch0. reach_ch o st ey ch0 /\ + ("stop_split" + forall ch0. reach_ch o st ey ch0 /\ reach_ch o st2 ex (add ch0 x) /\ sb ey ch0 -> reach_ch o st2 ex (add (xt ch0) x) by (not (ch0 x so not ey x so o y x)) @@ -796,19 +807,21 @@ module StratProofs so sext (add (xt ch0) x) (xt2 (add ch0 x)) ) /\ (* case Reach_chain. *) - (forall chh ch0. chain sb chh /\ supremum sb chh ch0 /\ + ("stop_split" + forall chh ch0. chain sb chh /\ supremum sb chh ch0 /\ chh ey /\ (forall u. chh u -> reach_ch o st ey u /\ reach_ch o st2 ex (add u x)) -> reach_ch o st2 ex (add ch0 x) by let chh2 = \ch. ch = ex \/ (ch x /\ chh (remove ch x)) in (supremum sb chh2 (add ch0 x) - by (upper_bound sb chh2 (add ch0 x) + by ("stop_split" upper_bound sb chh2 (add ch0 x) by forall v. chh2 v -> subchain o v (add ch0 x) by (forall z. ch0 z -> o x z by sb ey ch0 so o y z) so v = ex || let rv = remove v x in sb rv ch0 so sext (add rv x) v - ) /\ forall ch1. upper_bound sb chh2 ch1 -> + ) /\ "stop_split" + forall ch1. upper_bound sb chh2 ch1 -> sb (add ch0 x) ch1 by let r1 = remove ch1 x in sb ex ch1 so subset ex ch1 @@ -822,7 +835,7 @@ module StratProofs so sext (remove (add u x) x) u so chh2 (add u x) so sb (add u x) ch1) - so (chain sb chh2 + so ("stop_split" chain sb chh2 by (forall u. chh2 u -> sb ex u by u = ex || forall z. u z -> o x z by chh (remove u x) @@ -883,9 +896,9 @@ module StratProofs (with_prefix s2.h_pair s1 -> subchain o2 s1.h_local s2.h_local) function sorder_completion (ch:state 'a 'b -> bool) : state 'a 'b = - let hp = subchain_completion (image h_pair ch) in - let ht = subchain_completion (image h_total ch) in - let hl = subchain_completion (image h_local (with_prefix_in ch hp)) in + let hp = bigunion (image h_pair ch) in + let ht = bigunion (image h_total ch) in + let hl = bigunion (image h_local (with_prefix_in ch hp)) in { h_pair = hp; h_total = ht; h_local = hl } @@ -932,7 +945,7 @@ module StratProofs order o1 /\ order o2 -> let sd = sorder o1 o2 in chain sd ch -> let op = rprod o1 o2 in - let hp = subchain_completion (image h_pair ch) in + let hp = bigunion (image h_pair ch) in let pref = with_prefix_in ch hp in (chain (subchain op) (image h_pair ch) by forall a b. image h_pair ch a /\ image h_pair ch b -> @@ -965,11 +978,11 @@ module StratProofs let cpl = sorder_completion ch in supremum sd ch cpl by - let hp = subchain_completion (image h_pair ch) in - let ht = subchain_completion (image h_total ch) in + let hp = bigunion (image h_pair ch) in + let ht = bigunion (image h_total ch) in let pref = with_prefix_in ch hp in let local = image h_local pref in - let hl = subchain_completion local in + let hl = bigunion local in let (op,sb) = (rprod o1 o2,subchain o2) in supremum (subchain op) (image h_pair ch) hp /\ supremum sb (image h_total ch) ht @@ -1028,6 +1041,16 @@ module StratProofs h_total = ((=) sc.baseb); h_local = ((=) sc.baseb) } + (* Very simple invariants on state: historics are + chains, and mostly non-empty. *) + predicate correct (sc:section 'a 'b) (st:state 'a 'b) = + let o1 = sc.g1.progress in let o2 = sc.g2.progress in + chain (rprod o1 o2) st.h_pair /\ chain o2 st.h_local /\ + chain o2 st.h_total /\ + st.h_pair (sc.basea,sc.baseb) /\ + st.h_total sc.baseb /\ + (forall a b. maximum (rprod o1 o2) st.h_pair (a,b) -> st.h_local b) + (* Paired evolution of state: simulate steps in 'a game by picking a winning imitation strategy on 'b game, and carrying out a step in 'a game once this strategy terminates @@ -1035,7 +1058,7 @@ module StratProofs function evolve (sc:section 'a 'b) (dmn:demon 'b) (st:state 'a 'b) : state 'a 'b = let o1 = sc.g1.progress in let o2 = sc.g2.progress in - if not (chain (rprod o1 o2) st.h_pair /\ chain o2 st.h_local) + if not (correct sc st) then st else let pr = sup (rprod o1 o2) st.h_pair in let b = snd pr in @@ -1072,12 +1095,12 @@ module StratProofs sc.sd st nx by "case_split" let o1 = sc.g1.progress in let o2 = sc.g2.progress in - chain (rprod o1 o2) st.h_pair /\ chain o2 st.h_local -> + correct sc st -> let pr = sup (rprod o1 o2) st.h_pair in let b = snd pr in if not maximum (rprod o1 o2) st.h_pair pr then (supremum o2 st.h_total b -> - chain_complete (rprod o1 o2) + q_chain_complete (rprod o1 o2) so supremum (rprod o1 o2) st.h_pair pr so subchain (rprod o1 o2) st.h_pair nx.h_pair so subchain o2 st.h_total nx.h_total @@ -1145,9 +1168,7 @@ module StratProofs history *) predicate coherent (sc:section 'a 'b) (dmn:demon 'b) (st:state 'a 'b) = let o1 = sc.g1.progress in let o2 = sc.g2.progress in - chain (rprod o1 o2) st.h_pair /\ - chain o2 st.h_total /\ - chain o2 st.h_local /\ + correct sc st /\ (forall a b. st.h_pair (a,b) -> sc.r a b) /\ dmn_reach sc.g1 sc.anga sc.basea st.h_proj /\ (forall pr. maximum (rprod o1 o2) st.h_pair pr -> @@ -1178,7 +1199,7 @@ module StratProofs by forall x. bs.h_proj x -> x = sc.basea by exists y. bs.h_pair y /\ fst y = x) so (* Case Reach_base *) - (coherent sc dmn bs + ("stop_split" coherent sc dmn bs by (dmn_reach sc.g1 sc.anga sc.basea bs.h_proj by reach_ch o1 (step sc.g1 sc.anga witness) bs.h_proj bs.h_proj) /\ (forall pr. supremum op bs.h_pair pr -> bs.h_pair pr @@ -1190,7 +1211,7 @@ module StratProofs by (sc.sd bs st2 so antisymetric sc.sd) ) /\ (* Case Reach_succ *) - (forall st. tr_reach sc.sd evl bs st /\ + ("stop_split" forall st. tr_reach sc.sd evl bs st /\ coherent sc dmn st -> let nst = evl st in coherent sc dmn nst by "case_split" @@ -1211,12 +1232,12 @@ module StratProofs so maximum op nst.h_pair pr so (forall pr2. maximum op nst.h_pair pr2 -> sup o2 nst.h_local = b = sup o2 nst.h_total) - so (let (a,b) = pr in sc.r a b + so ("stop_split" let (a,b) = pr in sc.r a b by chain_compatible o1 sc.r o2 /\ 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 subset bs.h_pair st.h_pair) - so (forall st2. tr_reach sc.sd evl bs st2 /\ + so ("stop_split" forall st2. tr_reach sc.sd evl bs st2 /\ sc.sd st2 nst /\ st2.h_pair <> nst.h_pair -> forall a. st2.h_total a -> (exists b c. nst.h_pair (b,c) /\ o2 a c) @@ -1225,7 +1246,7 @@ module StratProofs so (st.h_total a by subchain o2 st2.h_total st.h_total so subset st2.h_total st.h_total) so o2 a b) - so (dmn_reach sc.g1 sc.anga sc.basea nst.h_proj + so ("stop_split" dmn_reach sc.g1 sc.anga sc.basea nst.h_proj by if nst.h_proj = st.h_proj then true else let ba = (=) sc.basea in @@ -1272,7 +1293,8 @@ module StratProofs so nst.h_pair = add st.h_pair (al,bl) so nst.h_total = add st.h_total bl so nst.h_local = ((=) bl) - so (upper_bound op st.h_pair (al,bl) by forall u. + so ("stop_split" + upper_bound op st.h_pair (al,bl) by forall u. st.h_pair u -> op u (al,bl) by let (a0,b0) = u in op (a0,b0) pr so o1 a0 a so s0 al so o1 a al @@ -1281,33 +1303,34 @@ module StratProofs so maximum op nst.h_pair (al,bl) so maximum o2 nst.h_total bl so maximum o2 nst.h_local bl so sup o2 nst.h_total = bl = sup o2 nst.h_local - so (forall pr. supremum op nst.h_pair pr /\ + so ("stop_split" forall pr. supremum op nst.h_pair pr /\ not maximum op nst.h_pair pr -> false by pr = (al,bl)) - so (forall st2. tr_reach sc.sd evl bs st2 /\ + so ("stop_split" forall st2. tr_reach sc.sd evl bs st2 /\ sc.sd st2 nst /\ st2.h_pair <> nst.h_pair -> forall a. st2.h_total a -> (exists b c. nst.h_pair (b,c) /\ o2 a c) by subchain o2 st2.h_total nst.h_total so subset st2.h_total nst.h_total so nst.h_total a so o2 a bl) - so (dmn_reach sc.g1 sc.anga sc.basea nst.h_proj + so ("stop_split" dmn_reach sc.g1 sc.anga sc.basea nst.h_proj by (sext nst.h_proj (add st.h_proj al) - by (forall x. nst.h_proj x -> + by ("stop_split" forall x. nst.h_proj x -> add st.h_proj al x by image fst nst.h_pair x so exists y. nst.h_pair y /\ fst y = x so if y = (al,bl) then true else st.h_pair y so image fst st.h_pair x so st.h_proj x) - /\ (forall x. add st.h_proj al x -> nst.h_proj x + /\ ("stop_split" + forall x. add st.h_proj al x -> nst.h_proj x by image fst nst.h_pair x by if x = al then nst.h_pair (al,bl) else image fst st.h_pair x so exists y. st.h_pair y /\ fst y = x so nst.h_pair y)) - so (maximum o1 st.h_proj a + so ("stop_split" maximum o1 st.h_proj a by (st.h_proj a by st.h_pair (a,b)) /\ upper_bound o1 st.h_proj a by forall u. st.h_proj u -> @@ -1332,7 +1355,7 @@ module StratProofs so (maximum o2 nst.h_local nx by upper_bound o2 st.h_local nx) so sup o2 nst.h_total = nx = sup o2 nst.h_local - so (forall st2. tr_reach sc.sd evl bs st2 /\ + so ("stop_split" forall st2. tr_reach sc.sd evl bs st2 /\ sc.sd st2 nst /\ st2.h_pair <> nst.h_pair -> forall a. st2.h_total a -> (exists b c. nst.h_pair (b,c) /\ o2 a c) @@ -1342,61 +1365,65 @@ module StratProofs else nst = st ) /\ (* Case Reach_chain *) + "stop_split" forall chh st. chain sc.sd chh /\ chh bs /\ supremum sc.sd chh st /\ (forall u. chh u -> tr_reach sc.sd evl bs u /\ coherent sc dmn u) -> coherent sc dmn st by let pref = with_prefix_in chh st.h_pair in st = sorder_completion chh (* Chains+demon-reach. *) - so (chain op st.h_pair + so ("stop_split" chain op st.h_pair by chain sbp (image h_pair chh) - so st.h_pair = subchain_completion (image h_pair chh) + so st.h_pair = bigunion (image h_pair chh) so supremum sbp (image h_pair chh) st.h_pair so (forall x. image h_pair chh x -> chain (rprod o1 o2) x)) - so (chain o2 st.h_total + so ("stop_split" chain o2 st.h_total by chain sb (image h_total chh) so supremum sb (image h_total chh) st.h_total so (forall x. image h_total chh x -> chain o2 x)) - so (chain o2 st.h_local + so ("stop_split" chain o2 st.h_local by chain (subchain o2) (image h_local pref) so supremum (subchain o2) (image h_local pref) st.h_local so (forall x. image h_local pref x -> chain o2 x by exists y. chh y /\ y.h_local = x)) - so (dmn_reach sc.g1 sc.anga sc.basea st.h_proj + so ("stop_split" dmn_reach sc.g1 sc.anga sc.basea st.h_proj by chain (subchain o1) (image h_proj chh) so (let s = image h_proj chh in supremum (subchain o1) s st.h_proj - by sext st.h_proj (subchain_completion s) - by (forall x. st.h_proj x -> subchain_completion s x - by image fst st.h_pair x - so exists y. st.h_pair y /\ fst y = x - so exists hp. image h_pair chh hp /\ hp y - so exists u. chh u /\ u.h_pair = hp - so s u.h_proj /\ u.h_proj x - ) /\ forall x. subchain_completion s x -> st.h_proj x - by exists prj. s prj /\ prj x - so exists st2. chh st2 /\ st2.h_proj = prj - so image fst st2.h_pair x - so exists y. st2.h_pair y /\ fst y = x - so image h_pair chh st2.h_pair so st.h_pair y) + by sext st.h_proj (bigunion s) + by ("stop_split" forall x. st.h_proj x -> bigunion s x + by image fst st.h_pair x + so exists y. st.h_pair y /\ fst y = x + so exists hp. image h_pair chh hp /\ hp y + so exists u. chh u /\ u.h_pair = hp + so s u.h_proj /\ u.h_proj x + ) /\ "stop_split" forall x. bigunion s x -> st.h_proj x + by exists prj. s prj /\ prj x + so exists st2. chh st2 /\ st2.h_proj = prj + so image fst st2.h_pair x + so exists y. st2.h_pair y /\ fst y = x + so image h_pair chh st2.h_pair so st.h_pair y) so (forall x. image h_proj chh x -> dmn_reach sc.g1 sc.anga sc.basea x by exists y. chh y /\ y.h_proj = x so coherent sc dmn y) so image h_proj chh ((=) sc.basea)) so dmn_reach sc.g1 sc.anga sc.basea st.h_proj + so (st.h_total sc.baseb + by bs.h_total sc.baseb /\ image h_total chh bs.h_total) (* The limit correlation falls by bi-domination. *) - so (forall pr. maximum op st.h_pair pr -> + so ("stop_split" forall pr. maximum op st.h_pair pr -> let loc = sup o2 st.h_local in let tot = sup o2 st.h_total in loc = tot /\ - (maximum o2 st.h_local loc <-> maximum o2 st.h_total tot) - by ((exists st3. pref st3) + (maximum o2 st.h_local loc <-> maximum o2 st.h_total tot) /\ + (let (_,b) = pr in st.h_local b) + by ("stop_split" (exists st3. pref st3) by exists hp. image h_pair chh hp /\ hp pr so exists st2. chh st2 /\ st2.h_pair = hp so sc.sd st2 st so sbp hp st.h_pair so (forall x. st.h_pair x -> not (not hp x so op pr x so op x pr)) so sext hp st.h_pair so pref st2) so exists st3. pref st3 - so (forall u. st.h_total u -> + so ("stop_split" forall u. st.h_total u -> (exists st2. pref st2 /\ st2.h_total u) by exists s0. image h_total chh s0 /\ s0 u so exists st2. chh st2 /\ st2.h_total = s0 @@ -1404,33 +1431,49 @@ module StratProofs \/ (sc.sd st3 st2 so sc.sd st2 st so sbp st2.h_pair st.h_pair so sbp st3.h_pair st2.h_pair so pref st2)) - so supremum o2 st.h_total tot /\ supremum o2 st.h_local loc + so ("stop_split" let (_,b) = pr in st.h_local b + by exists h0. image h_pair chh h0 /\ h0 pr + so exists st0. chh st0 /\ st0.h_pair = h0 + so (subchain op h0 st.h_pair by sc.sd st0 st) + so (sext h0 st.h_pair by forall x. st.h_pair x -> + not (not h0 x so op pr x so op x pr so x = pr)) + so with_prefix h0 st0 + so image h_local (with_prefix_in chh h0) st0.h_local + so st0.h_local b by coherent sc dmn st0) + so supremum o2 st.h_total tot + so supremum o2 st.h_local loc so (loc = tot by sext (upper_bound o2 st.h_local) (upper_bound o2 st.h_total) - by (forall u v. upper_bound o2 st.h_local u /\ st.h_total v -> + by ("stop_split" forall u v. + upper_bound o2 st.h_local u /\ st.h_total v -> o2 v u by exists st2. pref st2 /\ st2.h_total v so coherent sc dmn st2 so supremum o2 st2.h_total (sup o2 st2.h_total) - so supremum o2 st2.h_local (sup o2 st2.h_local) + so (supremum o2 st2.h_local (sup o2 st2.h_local) + by let (_,b) = pr in st2.h_local b) so sup o2 st2.h_total = sup o2 st2.h_local so o2 v (sup o2 st2.h_total) so sc.sd st2 st so subset st2.h_local st.h_local so upper_bound o2 st2.h_local u so o2 (sup o2 st2.h_local) u) - /\ (forall u v. upper_bound o2 st.h_total u /\ st.h_local v -> + /\ ("stop_split" forall u v. + upper_bound o2 st.h_total u /\ st.h_local v -> o2 v u by exists s0. image h_local pref s0 /\ s0 v so exists st2. pref st2 /\ st2.h_local = s0 so coherent sc dmn st2 - so supremum o2 st2.h_total (sup o2 st2.h_total) - so supremum o2 st2.h_local (sup o2 st2.h_local) + so (supremum o2 st2.h_total (sup o2 st2.h_total) + by st2.h_total sc.baseb) + so (supremum o2 st2.h_local (sup o2 st2.h_local) + by let (_,b) = pr in st2.h_local b) so sup o2 st2.h_total = sup o2 st2.h_local so o2 v (sup o2 st2.h_local) so sc.sd st2 st so subset st2.h_total st.h_total so upper_bound o2 st2.h_total u so o2 (sup o2 st2.h_total) u)) - so (maximum o2 st.h_total tot -> maximum o2 st.h_local tot + so ("stop_split" + maximum o2 st.h_total tot -> maximum o2 st.h_local tot by exists st2. pref st2 /\ st2.h_total tot so sc.sd st2 st so subset st2.h_total st.h_total so subset st2.h_local st.h_local @@ -1438,7 +1481,8 @@ module StratProofs so maximum o2 st2.h_total tot so (maximum o2 st2.h_local tot by st2.h_pair = st.h_pair) so st.h_local tot) - /\ (maximum o2 st.h_local loc -> maximum o2 st.h_total loc + /\ ("stop_split" + maximum o2 st.h_local loc -> maximum o2 st.h_total loc by exists s0. image h_local pref s0 /\ s0 loc so exists st2. pref st2 /\ st2.h_local = s0 so sc.sd st2 st so subset st2.h_total st.h_total @@ -1448,19 +1492,21 @@ module StratProofs so (maximum o2 st2.h_total loc by st2.h_pair = st.h_pair) so st.h_total loc)) (* Related pairs + total above paired. *) - so (forall a b. st.h_pair (a,b) -> sc.r a b /\ st.h_total b + so ("stop_split" + forall a b. st.h_pair (a,b) -> sc.r a b /\ st.h_total b by exists s0. image h_pair chh s0 /\ s0 (a,b) so exists st2. chh st2 /\ st2.h_pair = s0 so st2.h_total b so st.h_total b by sc.sd st2 st so subset st2.h_total st.h_total) (* paired above previous totals. *) - so (forall st2. tr_reach sc.sd evl bs st2 /\ + so ("stop_split" + forall st2. tr_reach sc.sd evl bs st2 /\ sc.sd st2 st /\ st2.h_pair <> st.h_pair -> forall a. st2.h_total a -> (exists b c. st.h_pair (b,c) /\ o2 a c) by not ext st2.h_pair st.h_pair so subset st2.h_pair st.h_pair so exists x. st.h_pair x /\ not st2.h_pair x - so st.h_pair = subchain_completion (image h_pair chh) + so st.h_pair = bigunion (image h_pair chh) so exists hp. image h_pair chh hp /\ hp x so exists st3. chh st3 /\ st3.h_pair = hp so separator sc.sd evl st2 st3 so not sbp st3.h_pair st2.h_pair @@ -1471,15 +1517,16 @@ module StratProofs ) (* If limit paired history get a supremum which is not a max, then it is a supremum of total history. *) - so (forall a b. supremum op st.h_pair (a,b) /\ not st.h_pair (a,b) -> + so ("stop_split" forall a b. + supremum op st.h_pair (a,b) /\ not st.h_pair (a,b) -> supremum o2 st.h_total b - by (forall u. upper_bound o2 st.h_total u -> o2 b u + by ("stop_split" forall u. upper_bound o2 st.h_total u -> o2 b u by op (a,b) (a,u) by upper_bound op st.h_pair (a,u) by forall x. st.h_pair x -> op x (a,u) by let (c,d) = x in op x (a,b) so o1 c a so st.h_total d so o2 d u) - /\ (upper_bound o2 st.h_total b + /\ ("stop_split" upper_bound o2 st.h_total b by forall u. st.h_total u -> o2 u b by exists ht. image h_total chh ht /\ ht u so exists st2. chh st2 /\ st2.h_total = ht @@ -1490,6 +1537,8 @@ module StratProofs so transitive o2 so o2 w b by op (v,w) (a,b)) ) + so (let pr0 = (sc.basea,sc.baseb) in st.h_pair pr0 + by bs.h_pair pr0 /\ image h_pair chh bs.h_pair) (* Unicity of maximal witness for a given total history. @@ -1514,7 +1563,8 @@ module StratProofs so let o1 = sc.g1.progress in let o2 = sc.g2.progress in let op = rprod o1 o2 in let pr = sup op st3.h_pair in - supremum op st3.h_pair pr + (supremum op st3.h_pair pr by st3.h_pair (sc.basea,sc.baseb) + /\ q_chain_complete op) so let (a,b) = pr in a = fst pr /\ b = snd pr so if not maximum op st3.h_pair pr @@ -1538,8 +1588,11 @@ module StratProofs = add st3.h_local sp1 /\ (ev2 st3).h_local = extends_ch o2 stp2 st3.h_local = add st3.h_local sp2 - so supremum o2 st3.h_local bl - /\ supremum o2 st3.h_total (sup o2 st3.h_total) + so (supremum o2 st3.h_local bl + /\ supremum o2 st3.h_total (sup o2 st3.h_total) + by q_chain_complete o2 + /\ st3.h_total sc.baseb + /\ st3.h_local b) so bl = sup o2 st3.h_total so antisymetric o2 so (* Either the step was already there, in case ev1 stutter, @@ -1602,7 +1655,7 @@ module StratProofs by (* Case Reach_succ: For most cases, unrolling def of evolve is enough. Evolve corresponds either to 0 or 1 step in total history. *) - (forall st. tr_reach sc.sd evl bs st /\ + ("stop_split" forall st. tr_reach sc.sd evl bs st /\ reach_ch o2 stp ((=) sc.baseb) st.h_total -> let nst = evl st in reach_ch o2 stp ((=) sc.baseb) nst.h_total @@ -1627,7 +1680,11 @@ module StratProofs not s0 a /\ sc.g1.transition a s0 so let target = related sc.r s0 in let bl = sup o2 st.h_local in - supremum o2 st.h_total bl /\ supremum o2 st.h_local bl + (supremum o2 st.h_total bl /\ supremum o2 st.h_local bl + by q_chain_complete o2 + /\ st.h_total sc.baseb + /\ st.h_local b + ) so upper_bound o2 st.h_total bl /\ o2 b bl /\ not target bl so let iang = iangel sc b target in let stp' = step sc.g2 iang dmn in @@ -1635,7 +1692,7 @@ module StratProofs (* Tricky part: the following equality holds because the current state is a/the maximal witness for the current total history. *) - so (stp' st.h_local = stp st.h_total + so ("stop_split" stp' st.h_local = stp st.h_total by let n' = stp' st.h_local in n' <> bl so st.h_local bl @@ -1659,7 +1716,7 @@ module StratProofs ) so upper_bound o2 st.h_total (stp st.h_total) ) - /\ (* Case Reach_chain. *) + /\ "stop_split" (* Case Reach_chain. *) forall ch st. chain sc.sd ch /\ supremum sc.sd ch st /\ ch bs /\ (forall u. ch u -> reach_ch o2 stp ((=) sc.baseb) u.h_total) -> @@ -1715,13 +1772,14 @@ module StratProofs by let o1 = sc.g1.progress in let o2 = sc.g2.progress in let op = rprod o1 o2 in (* Case Reach_base *) - (locally_winning sc dmn bs by + ("stop_split" locally_winning sc dmn bs by (sup op bs.h_pair = (sc.basea,sc.baseb) by maximum op bs.h_pair (sc.basea,sc.baseb) by reflexive op) /\ forall x. bs.h_local x -> maximum o2 bs.h_local x) /\ (* Case Reach_succ *) - (forall st. coherent sc dmn st /\ locally_winning sc dmn st -> + ("stop_split" + forall st. coherent sc dmn st /\ locally_winning sc dmn st -> let nst = evl st in locally_winning sc dmn nst by "case_split" let pr = sup op st.h_pair in let a = fst pr in let b = snd pr in @@ -1745,7 +1803,7 @@ module StratProofs so related_w sc.r s0 bl al1) so related_w sc.r s0 bl al) so nst.h_pair = add st.h_pair (al,bl) /\ nst.h_local = ((=) bl) - so (maximum op nst.h_pair (al,bl) + so ("stop_split" maximum op nst.h_pair (al,bl) by upper_bound op st.h_pair (al,bl) by forall u. st.h_pair u -> op u (al,bl) by let (a0,b0) = u in op (a0,b0) pr @@ -1757,7 +1815,7 @@ module StratProofs else let stp = step sc.g2 (iangel sc b target) dmn in nst.h_pair = st.h_pair /\ nst.h_local = extends_ch o2 stp st.h_local - so forall y. nst.h_local y /\ target y -> + so "stop_split" forall y. nst.h_local y /\ target y -> maximum o2 nst.h_local y by if st.h_local y then false @@ -1766,7 +1824,7 @@ module StratProofs else y = stp st.h_local so upper_bound o2 (st.h_local) y so upper_bound o2 (nst.h_local) y ) - /\ (* Case Reach_chain *) + /\ "stop_split" (* Case Reach_chain *) forall ch st. chain sc.sd ch /\ supremum sc.sd ch st /\ ch bs /\ (forall u. ch u -> tr_reach sc.sd evl bs u /\ locally_winning sc dmn u) -> @@ -1780,7 +1838,8 @@ module StratProofs let pref = with_prefix_in ch st.h_pair in let imp = image h_local pref in st = sorder_completion ch - so (forall x. st.h_local x /\ target x -> maximum o2 st.h_local x + so ("stop_split" forall x. st.h_local x /\ target x -> + maximum o2 st.h_local x by forall y. st.h_local y -> o2 y x by exists hl. imp hl /\ hl y so exists sty. pref sty /\ sty.h_local = hl @@ -1790,9 +1849,13 @@ module StratProofs so stxy.h_pair = st.h_pair so locally_winning sc dmn stxy so maximum o2 stxy.h_local x) - by (sc.sd stx sty so sty.h_local x by subset stx.h_local sty.h_local) - \/ (sc.sd sty stx so stx.h_local y by subset sty.h_local stx.h_local)) - /\ (let stp = step sc.g2 (iangel sc b target) dmn in + by (sc.sd stx sty so sty.h_local x + by subset stx.h_local sty.h_local + by subchain o2 stx.h_local sty.h_local) + \/ (sc.sd sty stx so stx.h_local y + by subset sty.h_local stx.h_local + by subchain o2 sty.h_local stx.h_local)) + /\ ("stop_split" let stp = step sc.g2 (iangel sc b target) dmn in reach_ch o2 stp ((=) b) st.h_local by tr_reach sc.sd evl bs st so coherent sc dmn st @@ -1811,7 +1874,7 @@ module StratProofs so let sb = subchain o2 in supremum sb imp st.h_local so supremum sb chh st.h_local - by (upper_bound sb chh st.h_local + by ("stop_split" upper_bound sb chh st.h_local by forall u. chh u -> sb u st.h_local by "case_split" if imp u then true else u = (=) b @@ -1824,7 +1887,7 @@ module StratProofs so imp st0.h_local so sb st0.h_local st.h_local) by (exists st0. pref st0) - by subchain_completion (image h_pair ch) pr + by bigunion (image h_pair ch) pr so exists hp. image h_pair ch hp /\ hp pr so exists st2. ch st2 /\ st2.h_pair = hp so (sext st2.h_pair st.h_pair @@ -1873,7 +1936,7 @@ module StratProofs (forall x. maximum o2 ch x /\ g20.transition x (angb x ch) -> dmn (angb x ch) = x) /\ lose_at g20 angb rwin ch - so (xt ch = ch by ext (xt ch) ch by ch (stp ch) + so ("stop_split" xt ch = ch by ext (xt ch) ch by ch (stp ch) by exists x. let a = angb x ch in maximum o2 ch x /\ (not g20.transition x a \/ a x) so x = sup o2 ch so stp ch = x @@ -1890,7 +1953,7 @@ module StratProofs so maximum sb (tr_reach sb xt ((=) y)) ch so subchain o2 stl.h_total ch (* Preliminary: check that there are no past winner for h_proj. *) - so (forall x. stl.h_proj x -> not (win0 x + so ("stop_split" forall x. stl.h_proj x -> not (win0 x so image fst stl.h_pair x so exists y. stl.h_pair y /\ fst y = x so let (_,y) = y in @@ -1904,11 +1967,11 @@ module StratProofs let pr = sup op stl.h_pair in let a = fst pr in let b = snd pr in (* Safe-guards holds. *) - chain op stl.h_pair /\ chain o2 stl.h_local + correct sc stl so (* Fixpoint can't be at a 'add supremum' step, otherwise it would not be a fixpoint. *) if not maximum op stl.h_pair pr - then chain_complete op + then q_chain_complete op so supremum op stl.h_pair pr so supremum o2 stl.h_total b so stl.h_pair = add stl.h_pair pr so false else let s0 = sc.anga a stl.h_proj in @@ -1920,12 +1983,15 @@ module StratProofs else let target = related sc.r s0 in let bl = sup o2 stl.h_local in (* Other safe-guards holds. *) - (supremum o2 stl.h_local bl /\ supremum o2 stl.h_total bl - by chain_complete o2 + ("stop_split" + supremum o2 stl.h_local bl /\ supremum o2 stl.h_total bl + by q_chain_complete o2 + so stl.h_local b /\ stl.h_total sc.baseb so (exists bl0. supremum o2 stl.h_local bl0) /\ (exists bl1. supremum o2 stl.h_total bl1)) so upper_bound o2 stl.h_total bl - so (o2 b bl by op (a,b) (a,bl) by upper_bound op stl.h_pair (a,bl) + so ("stop_split" + o2 b bl by op (a,b) (a,bl) by upper_bound op stl.h_pair (a,bl) by forall u. stl.h_pair u -> op u (a,bl) by let (v,w) = u in op (v,w) (a,b) so o1 v a so stl.h_total w so o2 w bl) @@ -1968,7 +2034,7 @@ module StratProofs the case where the demon fail. Then, the run is maximal => it also corresponds to the losing run, which is absurd. *) - (angb bl stl.h_total = an + ("stop_split" angb bl stl.h_total = an by (maximal_witness sc stl.h_total stl dmn by maximum sc.sd (tr_reach sc.sd evl bs) stl) so any_max_witness sc stl.h_total stl @@ -1992,4 +2058,3 @@ module StratProofs goal simulation end - diff --git a/examples/in_progress/2wp_gen/game/why3session.xml b/examples/in_progress/2wp_gen/game/why3session.xml index 5e2ddbbb6f7d96e694868f8477455b9749ae3240..f0e60fc43cd371b241c6577b5afcf136344e17aa 100644 --- a/examples/in_progress/2wp_gen/game/why3session.xml +++ b/examples/in_progress/2wp_gen/game/why3session.xml @@ -2,388 +2,380 @@ - - - - - - + + + + + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - + - - + + - + - + - - + + - + - + - - + + @@ -391,365 +383,373 @@ - - + + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -758,7 +758,7 @@ - + @@ -769,7 +769,7 @@ - + @@ -780,7 +780,7 @@ - + @@ -789,2389 +789,2679 @@ - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + - - + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - + + - - + + - - + + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - + + + - - + + + + + + - - - - - + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - + + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + + + + + + + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + - - + + - - + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + + + + - - + + - - + + - - + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - - - - - - - - + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -3179,36 +3469,36 @@ - + - + - + - - + + - + - + - - + + - + - + - - + + @@ -3216,193 +3506,208 @@ - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + + - + - + - - + + - + - + - - + + - + - + - - + + @@ -3410,550 +3715,609 @@ - - + + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - + + + + - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - - + + - + - + - - + + - + - + - - + + @@ -3961,329 +4325,327 @@ - - + + - + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - + - + diff --git a/examples/in_progress/2wp_gen/game/why3shapes.gz b/examples/in_progress/2wp_gen/game/why3shapes.gz index 9394a72100a6435ddbb7654eb5907b9a4510f925..b8047ccf3089100b674037e53f65a4cf0f8eb8b2 100644 Binary files a/examples/in_progress/2wp_gen/game/why3shapes.gz and b/examples/in_progress/2wp_gen/game/why3shapes.gz differ diff --git a/examples/in_progress/2wp_gen/game_fmla.mlw b/examples/in_progress/2wp_gen/game_fmla.mlw index fcc3134c92d4c99a381436d04f06670a06d304bb..0477900295084fd059dcc21d9a05a5cc83554881 100644 --- a/examples/in_progress/2wp_gen/game_fmla.mlw +++ b/examples/in_progress/2wp_gen/game_fmla.mlw @@ -62,7 +62,7 @@ module SubgameProof have_winning_strat g2 x (related (=) s) by g2.transition x s) - clone Subgame with lemma trivial_subgame_indeed + clone Subgame with goal trivial_subgame_indeed end @@ -73,6 +73,7 @@ module Fmla use import ho_set.Set use import ho_rel.Rel use import fn.Fun + use import fn.Image use import game.Game use import Subgame @@ -121,49 +122,32 @@ module Fmla predicate later_limit (o:erel 'b) (i:rel 'b 'a) (ch:set 'b) (y:'a) = exists x. i x y /\ upper_bound o ch x - (* TODO: recreate values for transfinite call-stack rule, - commented for now. *) - (* type v_data 'a 'b = { - (* Underlying game ordering. *) - v_go : 'a -> 'a -> bool; - (* Extra order for the stack. *) - v_so : 'b -> 'b -> bool; - (* Initial stack. *) - v_s0 : ('a,'b) -> bool; - (* Precondition for calling on a given stack. - The location is the stack supremum on first component. *) - v_pr : (('a,'b) -> bool) -> bool; - (* Postcondition: some element in the stack satisfy the postcondition - at the given point. *) - v_pst : 'a -> ('a,'b) -> bool; - } - function v_prod (vd:v_data 'a 'b) : ('a,'b) -> ('a,'b) -> bool = - \x y. oprod vd.v_go vd.v_so x y - predicate v_data_valid (vd:v_data 'a 'b) = - order vd.v_so /\ - chain vd.v_prod vd.v_s0 /\ - forall stack. - chain vd.v_prod stack /\ - subchain vd.v_prod vd.v_s0 stack /\ - (forall x. not maximum vd.v_prod stack x) /\ - (forall rstack. - subchain vd.v_prod vd.v_s0 rstack /\ subchain vd.v_prod rstack stack /\ - rstack <> stack -> vd.v_pr rstack) -> - vd.v_pr stack - predicate v_pre (vd:v_data 'a 'b) (stack:('a,'b) -> bool) (x:'a) = - vd.v_pr stack /\ chain vd.v_prod stack /\ - supremum vd.v_go (proj1 stack) x - predicate v_post (vd:v_data 'a 'b) (stack:('a,'b) -> bool) (x:'a) = - exists y. stack y /\ vd.v_pst x y - function v_enf (vd:v_data 'a 'b) : (('a,'b) -> bool) -> fmla 'a = - u_enforce (v_pre vd) (v_post vd) - function v_hrec (vd:v_data 'a 'b) (s:('a,'b) -> bool) : fmla 'a = - universal (\s'. arrow (lift (subchain vd.v_prod s s' /\ s <> s')) - (v_enf vd s')) - function v_hfix (vd:v_data 'a 'b) : fmla 'a = - universal (\s. arrow (conj (lift (subchain vd.v_prod vd.v_s0 s)) - (v_hrec vd s)) - (v_enf vd s))*) + (* Condition for transfinite loop limit case. *) + predicate step_limit (c:fmla 'a) (o:erel 'b) (go:erel 'a) (i:rel 'b 'a) = + forall ch f inh. chain o ch /\ monotone_on ch o f go /\ ch inh /\ + (forall x. not maximum o ch x) /\ (forall x. ch x -> i x (f x)) -> + holds c (enforce (supremum go (image f ch)) (later_limit o i ch)) + + (* Express that the precondition is taken with respect to higher + state. For transfinite recursion rule. *) + predicate higher (o:erel 'b) (p:rel 'b 'a) (x:'b) (y:'b) (z:'a) = + o x y /\ x <> y /\ p y z + + (* Variation of higher in limit case. *) + predicate higher_limit (o:erel 'b) (p:rel 'b 'a) (ch:set 'b) (y:'b) (z:'a) = + upper_bound o ch y /\ p y z + + (* Postcondition for recursion limit case. *) + predicate post_limit (q:rel 'b 'a) (ch:set 'b) (y:'a) = + exists x. ch x /\ q x y + + (* Fixpoint condition for recursion limit case. *) + predicate fix_limit (c:fmla 'a) (o:erel 'b) (go:erel 'a) (p q:rel 'b 'a) = + forall ch inh f. ch inh /\ monotone_on ch o f go /\ chain o ch /\ + (forall x. not maximum o ch x) /\ (forall x. ch x -> p x (f x)) -> + holds c (arrow (universal (u_enforce (higher_limit o p ch) q)) + (enforce (supremum go (image f ch)) (post_limit q ch))) + end module FmlaRules "W:non_conservative_extension:N" (* => FmlaRulesProof *) @@ -218,30 +202,22 @@ module FmlaRules "W:non_conservative_extension:N" (* => FmlaRulesProof *) (we can derive rules with real postcondition from this one + Kont). *) axiom 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 /\ - (forall ch f inh y. chain o ch /\ supremum go (image f ch) y /\ - monotone_on ch o f go /\ ch inh /\ - (forall x. not maximum o ch x) /\ (forall x. ch x -> i x (f x)) -> - holds c (enforce ((=) y) (later_limit o i ch))) -> + holds c (ordering go) /\ order o /\ step_limit c o go i -> holds c (universal (u_enforce i (const none))) axiom abstraction : forall c f1 f2:fmla 'a. 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): - If, knowing that from any valid higher stack we can reach a point in - which the post is satisfied for some point of the stack, - then we can reach a point in which an element of the current stack - satisfy the post, plus some continuity condition on the precondition, - then we can have the same enforcement without the higher-stack - hypothesis (e.g a fixpoint) *) - axiom vertical_fix : forall c,vd:v_data 'a 'b. - is_fmla c -> - holds c (v_hfix vd) /\ - holds c (ordering vd.v_go) /\ - v_data_valid vd -> - holds c (v_enf vd vd.v_s0)*) + axiom modus_ponens : forall c f1 f2:fmla 'a. + holds c (arrow f1 f2) /\ holds c f1 -> holds c f2 + + axiom recursion : forall c o go,p q:rel 'b 'a. + holds c (ordering go) /\ order o /\ + (forall x. + holds c (arrow (universal (u_enforce (higher o p x) q)) + (enforce (p x) (q x)))) /\ + fix_limit c o go p q -> + holds c (universal (u_enforce p q)) end @@ -249,6 +225,7 @@ module FmlaRulesProof use import option.Option use import ho_set.Set + use import ho_set.SetBigOps use import ho_rel.RelSet use import ho_rel.Prod use import fn.Fun @@ -376,8 +353,8 @@ module FmlaRulesProof let tr = \x. (=) (nx x) in let g2 = { progress = op; transition = tr } in let strt = (=) (x,y) in - game_wf g2 - so (have_uniform_winning_strat g2 strt none + (game_wf g2 by forall x s y. tr x s /\ s y -> op x y by nx x y) + so ("stop_split" have_uniform_winning_strat g2 strt none by have_winning_strat g2 (x,y) none by let ang = \x _. nx x in not (not winning_strat g2 (x,y) none ang @@ -385,7 +362,7 @@ module FmlaRulesProof so let r = \x y. let (a,b) = x in b = y /\ i a b in (simulate g2 r g by step_simulate g2 r g - by (forall x s y. tr x s /\ r x y -> + by ("stop_split" forall x s y. tr x s /\ r x y -> have_winning_strat g y (related r s) by let (xx,_) = x in (have_winning_strat g y (inter (later o i xx) (go y)) @@ -395,12 +372,14 @@ 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) - /\ (chain_compatible op r go + /\ ("stop_split" chain_compatible op r go by forall chp inhp xp yp. chain (rprod op go) chp /\ chp inhp /\ (forall x y. chp (x,y) -> r x y) /\ supremum (rprod op go) chp (xp,yp) -> let ch = image fst chp in - supremum op ch xp + let (inh,_) = inhp in + ch inh + so supremum op ch xp 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 @@ -467,11 +446,11 @@ module FmlaRulesProof so order o_ch /\ chain_complete o_ch (* Can carry out steps for i_ch. Case disjunction between regular and limit steps. *) - so (holds c (universal (u_enforce i_ch (later o_ch i_ch))) + so ("stop_split" holds c (universal (u_enforce i_ch (later o_ch i_ch))) by forall ch. holds c (enforce (i_ch ch) (later o_ch i_ch ch)) by (exists ys. i_ch ch ys so let ch1 = image fst ch in let ch2 = image snd ch in - (forall xn yn. + ("stop_split" forall xn yn. upper_bound go ch2 yn /\ upper_bound o ch1 xn /\ i xn yn /\ not ch1 xn -> later o_ch i_ch ch yn @@ -487,7 +466,7 @@ module FmlaRulesProof maximum go ch'2 yn by ch'2 yn /\ forall u. ch'2 u -> go u yn by u = yn \/ ch2 u) so (exists xs. maximum o ch1 xs - so (maximum ip ch (xs,ys) + so ("stop_split" maximum ip ch (xs,ys) by exists p. ch p /\ fst p = xs so let (xs,yp) = p in (maximum ip ch p @@ -518,25 +497,26 @@ module FmlaRulesProof so not (ch1 xn so maximum o ch1 xn)) ) || sext (i_ch ch) none) (* Chain compatibility. *) - so (forall chh inhh chs y. chain op chh /\ supremum op chh (chs,y) + 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 = subchain_completion ch1 + 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 (forall u. ch3 u -> go u 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) - /\ forall u. upper_bound go ch3 u -> go y 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 @@ -564,11 +544,7 @@ module FmlaRulesProof injective product. *) lemma trampoline : forall c go,i:rel 'b 'a,o. 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 /\ - monotone_on ch o f go /\ ch inh /\ - (forall x. not maximum o ch x) /\ (forall x. ch x -> i x (f x)) -> - holds c (enforce ((=) y) (later_limit o i ch))) -> + holds c (ordering go) /\ order o /\ step_limit c o go i -> holds c (universal (u_enforce i (const none))) by forall ch inh y. chain (iprod o go) ch /\ supremum go (image snd ch) y /\ @@ -578,6 +554,10 @@ module FmlaRulesProof by let ch2 = image fst ch in let wit = \x z. ch (x,z) in let f = \x. choice (wit x) in + holds c (enforce (supremum go (image f ch2)) + (later_limit o i (image fst ch))) + /\ subset ((=) y) (supremum go (image f ch2)) + by (chain o ch2 by forall x y. ch2 x /\ ch2 y -> o x y \/ o y x by exists a. ch a /\ fst a = x so exists b. ch b /\ fst b = y so let ((_,_),(_,_)) = (a,b) in iprod o go a b \/ iprod o go b a) @@ -621,8 +601,7 @@ module FmlaRulesProof (holds c'' (enforce (i n) (i (n+1))) /\ subset (i (n+1)) (later (<=) i n))) ) - /\ holds c'' (ordering go) - /\ (forall ch f inh. chain (<=) ch /\ ch inh /\ + /\ (step_limit c'' (<=) go i by 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) by (forall x. ch x -> 0 <= x <= 2) @@ -630,8 +609,8 @@ module FmlaRulesProof || (ch 1 so maximum (<=) ch 1) || (ch 0 so maximum (<=) ch 0)) - (* From that point on, the goal is to prove the - 'crude recursion theorem'. + (* From that point on, the goal is to prove the recursion theorem, + starting by the 'crude recursion theorem'. If we have: - An ordered set B - A non-empty-chain-stable precondition on (B,Game-support) chains @@ -640,8 +619,7 @@ module FmlaRulesProof 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 + Then, Gamma |- P X_0 enforce Q X_0 Initially, we even restrict Gamma to a singleton. *) (* Regroup parameters *) @@ -761,12 +739,12 @@ module FmlaRulesProof lemma clex_order : forall o1 o2 r:erel 'a. clex_valid o1 o2 r -> let o = clex o1 o2 r in order o - by (antisymetric o + by ("stop_split" antisymetric o by forall a b. o a b /\ o b a /\ a <> b -> false by not subchain o1 a b so not subchain o1 b a so antisymetric o2) - /\ (transitive o + /\ ("stop_split" transitive o by forall a b c. o a b /\ o b c -> o a c by if a = b || b = c then true else if subchain o1 a b @@ -794,29 +772,29 @@ module FmlaRulesProof else if o1 xb yb then clex_witness o1 o2 r a c xp xa xb by yp xb so subset yp b so subset yp c so b xb so c xb - so (forall y. c y /\ o1 y xa -> xp y + so ("stop_split" forall y. c y /\ o1 y xa -> xp y by if o1 y xb then xp y by yp y else false by chain o1 c so o1 xb y so o1 xb xa) so subchain o1 xp c by subchain o1 xp yp - by (forall x. xp x -> yp x + by ("stop_split" forall x. xp x -> yp x by b x so o1 x xb so o1 x yb so x <> yb) - so (forall x y. xp x /\ yp y /\ not xp y -> o1 x y + so ("stop_split" forall x y. xp x /\ yp y /\ not xp y -> o1 x y by o1 x xb so if o1 xb y then true else false by chain o1 b so b y so o1 y xb so y <> xb) else (o1 yb xb by chain o1 b) so clex_witness o1 o2 r a c yp yb yc by xp yb so subset xp b so subset xp a so a yb so b yb - so (forall y. a y /\ o1 y yc -> yp y + so ("stop_split" forall y. a y /\ o1 y yc -> yp y by if o1 y yb then yp y by xp y else false by chain o1 a so o1 yb y so o1 yb yc) so subchain o1 yp a by subchain o1 yp xp - by (forall x. yp x -> xp x + by ("stop_split" forall x. yp x -> xp x by b x so o1 x yb so o1 x xb so x <> xb) - so (forall x y. yp x /\ xp y /\ not yp y -> o1 x y + so ("stop_split" forall x y. yp x /\ xp y /\ not yp y -> o1 x y by o1 x yb so if o1 yb y then true else false by chain o1 b so b y so o1 y yb so y <> yb) ) @@ -967,18 +945,20 @@ module FmlaRulesProof so is_stack sc stk so is_frame sc f so transitive (lframe sc) /\ transitive go /\ antisymetric go - so (* Lengthy internal lemma for step case of trampoline rule: + so (* Internal lemma for step case of trampoline rule: if we execute any frame in the stack (and cut the stack at the associated level), then we go to a later stack. This lemma covers both natural step case and return chaining case. *) - (forall f0 y z. stk f0 /\ maximum go f0.hstr y /\ f0.angl y f0.hstr z /\ + ("stop_split" + forall f0 y z. stk f0 /\ maximum go f0.hstr y /\ f0.angl y f0.hstr z /\ go x z /\ not rc_post sc f0.keys y -> later o i stk z by let nf = { f0 with hstr = add f0.hstr z } in let nstk = \f2. (stk f2 /\ lframe sc f2 f0 /\ f2 <> f0) \/ f2 = nf in let mg = mgame sc f0.keys in (* Preservation of frame invariant. *) - (is_frame sc nf /\ maximum go nf.hstr z /\ nf.hstr <> f0.hstr + ("stop_split" + is_frame sc nf /\ maximum go nf.hstr z /\ nf.hstr <> f0.hstr by let s = f0.angl y f0.hstr in not (not mg.transition y s \/ s y so lose_at mg f0.angl (rc_post sc f0.keys) f0.hstr) @@ -988,11 +968,11 @@ module FmlaRulesProof maximum go nf.hstr x by not (x <> z so f0.hstr x so maximum go f0.hstr x)) ) - so (maximum (lframe sc) nstk nf + so ("stop_split" maximum (lframe sc) nstk nf by forall f1. nstk f1 -> lframe sc f1 nf by f1 = nf || (stk f1 so lframe sc f1 f0)) (* Preservation of stack invariant. *) - so (is_stack sc nstk + so ("stop_split" is_stack sc nstk by (wf_chain (lframe sc) nstk by let pstk = remove nstk nf in subset pstk stk @@ -1014,7 +994,7 @@ module FmlaRulesProof so nstk <> stk so rframe sc f0 nf (* Progression. *) - so (lstack sc stk nstk + so ("stop_split" lstack sc stk nstk by let p = \f2. stk f2 /\ lframe sc f2 f0 /\ f2 <> f0 in clex_witness (lframe sc) (rframe sc) (later_frame sc) stk nstk p f0 nf @@ -1047,7 +1027,7 @@ module FmlaRulesProof not (not mg.transition x s so lose_at mg f.angl (rc_post sc f.keys) f.hstr) so if g.transition x s - then (* Normal execution, just runs top frame. *) + then (* Normal execution, just runs top frame via internal lemma. *) have_uniform_winning_strat g s (later o i stk) by forall y. s y -> later o i stk y else (* The transition does not exists in the original game, @@ -1078,11 +1058,11 @@ module FmlaRulesProof so lframe sc f nf (* Put it at the top of the stack. *) so let nstk = add stk nf in - (maximum (lframe sc) nstk nf + ("stop_split" maximum (lframe sc) nstk nf by forall f0. nstk f0 -> lframe sc f0 nf by f0 = nf || (stk f0 so lframe sc f0 f)) - so (is_stack sc nstk + so ("stop_split" is_stack sc nstk by forall f0 y. nstk f0 /\ rc_post sc f0.keys y /\ go f0.strt y -> (exists fr x. chain_to sc nstk fr f0 x y) by if f0 <> nf @@ -1104,20 +1084,32 @@ module FmlaRulesProof so c x /\ c y so o x y so o y x so x = y)) || (subchain o a b) - (* We can also carry out limit steps of trampoline as expected. *) + (* We can also carry out limit steps of trampoline as expected. + The (lengthy) proof is based on the following dichotomy: + - Either there is a largest eventually stable prefix. Then, + we can recover an ordered sequence of frames at the same + level that corresponds to the same state in the game as the + complete sequence of stacks. We get a valid limit state by taking + the limit of those frames. + - Either there is no such prefix. Then, the supremum of eventually + stable prefixes is a non-empty maxless stack and an upper bound of + of all prefixes. We get a valid limit state by adding an extra + frame on top of that maxless stack. *) lemma rc_as_trampoline_limit : forall sc:section 'a 'b. rc_section sc -> let o = lstack sc in let i = rc_inv sc in let go = sc.gm.progress in let c = (=) sc.gm in - forall chh loc inh x. chain o chh /\ supremum go (image loc chh) x /\ - monotone_on chh o loc go /\ chh inh /\ + step_limit c o go i + by forall chh loc inh. chain o chh /\ monotone_on chh o loc go /\ chh inh /\ (forall x. not maximum o chh x) /\ (forall x. chh x -> i x (loc x)) -> - holds c (enforce ((=) x) (later_limit o i chh)) + holds c (enforce (supremum go (image loc chh)) (later_limit o i chh)) by forall g. c g -> - have_uniform_winning_strat g ((=) x) (later_limit o i chh) + have_uniform_winning_strat g (supremum go (image loc chh)) + (later_limit o i chh) by g = sc.gm - so have_winning_strat g x (later_limit o i chh) + so forall x. supremum go (image loc chh) x -> + have_winning_strat g x (later_limit o i chh) by later_limit o i chh x by (* Introduce the notion of eventually stable prefixes. *) let lf = lframe sc in @@ -1126,7 +1118,7 @@ module FmlaRulesProof forall s1. chh s1 /\ lstack sc s0 s1 -> sbf p s1 in transitive sbf /\ transitive lf /\ antisymetric lf /\ transitive go (* Eventually stable prefixes form a chain. *) - so (chain sbf evp + so ("stop_split" chain sbf evp by forall p1 p2. evp p1 /\ evp p2 -> (sbf p1 p2 \/ sbf p2 p1) by exists s0. chh s0 /\ @@ -1137,7 +1129,7 @@ module FmlaRulesProof by (lstack sc s0 s1 /\ s3 = s1) \/ (lstack sc s1 s0 /\ s3 = s0) ) (* Eventually stable prefixes are stacks. *) - so (forall p. evp p -> is_stack sc p + so ("stop_split" forall p. evp p -> is_stack sc p by exists s0. chh s0 /\ (forall s2. chh s2 /\ lstack sc s0 s2 -> sbf p s2) so subchain lf p s0 @@ -1150,9 +1142,9 @@ module FmlaRulesProof ) so transitive o /\ transitive go (* In particular, they have a supremum which is also a stack. *) - so let limp = subchain_completion evp in + so let limp = bigunion evp in supremum sbf evp limp - so (is_stack sc limp + so ("stop_split" is_stack sc limp by forall f y. limp f /\ rc_post sc f.keys y /\ go f.strt y -> (exists fr x. chain_to sc limp fr f x y) by exists p. evp p /\ p f @@ -1173,7 +1165,7 @@ module FmlaRulesProof (* Such a right-above-limp element must exists, otherwise limp=stkr would be maximal. *) not (not (exists x. mins x) - so (forall s2. chh s2 /\ lstack sc stkr s2 -> s2 = limp + so ("stop_split" forall s2. chh s2 /\ lstack sc stkr s2 -> s2 = limp by sext s2 limp by sbf limp s2 so forall x. s2 x -> not (not limp x so diff s2 limp x so subset (diff s2 limp) s2 @@ -1186,7 +1178,7 @@ module FmlaRulesProof so lstack sc stkr s2)) (* Local lemma: if two stacks after stkr have a maximal common prefix, then limp is included in that prefix. *) - so (forall s2 s3 pi x. + so ("stop_split" forall s2 s3 pi x. lstack sc stkr s2 /\ lstack sc stkr s3 /\ chh s2 /\ chh s3 /\ max_cprefix_by lf pi s2 s3 x -> sbf limp pi by if subchain lf limp pi then true else false @@ -1196,7 +1188,7 @@ module FmlaRulesProof ) (* Local lemma: if two stacks have a maximal common prefix, then the cut implies a minimum. *) - so (forall s2 s3 pi x. + so ("stop_split" forall s2 s3 pi x. max_cprefix_by lf pi s2 s3 x /\ chh s3 -> minimum lf (diff s3 pi) x by subset pi s3 @@ -1207,7 +1199,7 @@ module FmlaRulesProof could not have been the maximum stable prefix. *) so let rf = rframe sc in transitive rf /\ antisymetric rf - so (forall x. maximum rf mins x -> false + so ("stop_split" forall x. maximum rf mins x -> false by let prf = add limp x in exists s0. chh s0 /\ lstack sc stkr s0 /\ minimum lf (diff s0 limp) x @@ -1241,7 +1233,7 @@ module FmlaRulesProof so sbf prf limp so limp x) (* The right-above-lim elements indeed form a chain. The relation is induced by the chain structure of chh. *) - so (forall x y. mins x /\ mins y -> rf x y \/ rf y x + so ("stop_split" forall x y. mins x /\ mins y -> rf x y \/ rf y x by (forall x sx y sy. chh sx /\ chh sy /\ lstack sc stkr sx /\ lstack sc sx sy /\ minimum lf (diff sx limp) x /\ minimum lf (diff sy limp) y -> @@ -1269,7 +1261,7 @@ module FmlaRulesProof so exists stk0. chh stk0 /\ minimum lf (diff stk0 limp) fr0 /\ lstack sc stkr stk0 (* All min frames are valid frames. *) - so (forall fr. mins fr -> is_frame sc fr + so ("stop_split" forall fr. mins fr -> is_frame sc fr by exists stk. chh stk /\ minimum lf (diff stk limp) fr so is_stack sc stk by i stk (loc stk)) (* Introduce the chain of frame historics to prove the @@ -1278,28 +1270,29 @@ module FmlaRulesProof let e0 = (=) fr0.strt in let ehstrs = add hstrs e0 in let mg = mgame sc fr0.keys in - (forall x. ehstrs x -> - (dmn_reach mg fr0.angl fr0.strt x so subchain go e0 x) + ("stop_split" forall x. ehstrs x -> + (dmn_reach mg fr0.angl fr0.strt x && subchain go e0 x) by if x = e0 then reach_ch go (step mg fr0.angl witness) e0 e0 else exists frx. mins frx /\ frx.hstr = x so (rf fr0 frx \/ rf frx fr0)) so subchain go e0 fr0.hstr - so (chain (subchain go) ehstrs by forall x y. ehstrs x /\ ehstrs y -> + so ("stop_split" + chain (subchain go) ehstrs by forall x y. ehstrs x /\ ehstrs y -> subchain go x y \/ subchain go y x by if x = e0 \/ y = e0 then true else exists fr1. mins fr1 /\ fr1.hstr = x so exists fr2. mins fr2 /\ fr2.hstr = y so rf fr1 fr2 \/ rf fr2 fr1) - so let sp = subchain_completion ehstrs in + so let sp = bigunion ehstrs in supremum (subchain go) ehstrs sp so dmn_reach mg fr0.angl fr0.strt sp (* Prove that the current state (x) is indeed the supremum of the limit history. To achieve this, use the fact that cuts carry out global progression via later_frame. *) - so (supremum go sp x - by (upper_bound go sp x + so ("stop_split" supremum go sp x + by ("stop_split" upper_bound go sp x by forall y. sp y -> go y x by (exists fr. fr.hstr y /\ mins fr so exists stk. chh stk /\ minimum lf (diff stk limp) fr @@ -1324,7 +1317,7 @@ module FmlaRulesProof which is located after y. However, finding those stacks formally is rather inelegant. *) - by (forall y. image loc chh y -> go y ub + by ( "stop_split" forall y. image loc chh y -> go y ub by (exists stk fr. chh stk /\ lstack sc stkr stk /\ go y (loc stk) /\ minimum lf (diff stk limp) fr so go (loc stk) ub @@ -1388,7 +1381,7 @@ module FmlaRulesProof ) (* Complete sp with x as to have a maximum in history. *) so let csp = add sp x in - (dmn_reach mg fr0.angl fr0.strt csp + ("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 @@ -1399,7 +1392,8 @@ module FmlaRulesProof so maximum go csp x (* Prove that the obtained limit historic does satisfy the postcondition-maximum criterion for frame validity. *) - so (forall z. csp z /\ rc_post sc fr0.keys z -> maximum go csp z + so ("stop_split" + forall z. csp z /\ rc_post sc fr0.keys z -> maximum go csp z by if z = x then true else false by maximum go sp z by (forall y. sp y -> go y z @@ -1428,7 +1422,7 @@ module FmlaRulesProof (* Limit frame is above any mins frame. In particular, since mins has no maximum it is strictly above any mins frame. *) - so (forall fr. mins fr -> rf fr frl + so ("stop_split" forall fr. mins fr -> rf fr frl by rf fr fr0 \/ rf fr0 fr so ehstrs fr.hstr so subchain go fr.hstr sp so subchain go sp csp so subchain go fr.hstr csp @@ -1442,7 +1436,7 @@ module FmlaRulesProof (maximum lf stkl frl by forall u. stkl u -> lf u frl by if u = frl then true else limp u so lf u fr0 /\ u <> fr0) - so (is_stack sc stkl + so ("stop_split" is_stack sc stkl by forall fr y. stkl fr /\ rc_post sc fr.keys y /\ go fr.strt y -> (exists fr2 x. chain_to sc stkl fr2 fr x y) by (is_stack sc stk0 by i stk0 (loc stk0)) @@ -1459,7 +1453,7 @@ module FmlaRulesProof so (i stkl x by is_stack_top sc stkl frl x) (* There is one last thing to prove in order to establish later_limit: that stkl is indeed an upper bound of ch. *) - so (upper_bound o chh stkl by (forall stk. chh stk -> + so ("stop_split" upper_bound o chh stkl by (forall stk. chh stk -> lstack sc stk stkl by (lstack sc stk stkr -> lstack sc stkr stkl) ) @@ -1507,7 +1501,7 @@ module FmlaRulesProof (forall p. evp p -> exists s0. chh s0 && (sbf p s0 by forall s2. chh s2 /\ lstack sc s0 s2 -> sbf p s2)) (* limp is upper bound. *) - so (upper_bound o chh limp + so ("stop_split" upper_bound o chh limp by forall stk. chh stk -> o stk limp by exists stk2. chh stk2 /\ lstack sc stk stk2 /\ not sbf limp stk2 so o stk2 limp @@ -1532,7 +1526,7 @@ module FmlaRulesProof stk2 p1 pi f1 f2 ) (* limp does not have a maximum. *) - so (forall fr. limp fr -> not (maximum lf limp fr + so ("stop_split" forall fr. limp fr -> not (maximum lf limp fr so exists p. evp p /\ p fr so sext p limp by forall x. limp x -> not (not p x so subchain lf p limp so lf fr x so lf x fr so x = fr))) @@ -1542,7 +1536,7 @@ module FmlaRulesProof so exists inh_fr. limp inh_fr (* The supremum of the so-build stack is exactly x. *) so (supremum go (image strt limp) x - by (forall ub. upper_bound go (image strt limp) ub -> + by ("stop_split" forall ub. upper_bound go (image strt limp) ub -> go x ub by upper_bound go (image loc chh) ub by forall a. image loc chh a -> go a ub @@ -1570,7 +1564,7 @@ module FmlaRulesProof so (go b fr4.strt by upper_bound go fr3.hstr fr4.strt) so image strt limp fr4.strt so go fr4.strt ub - ) /\ (forall y. image strt limp y -> go y x + ) /\ ("stop_split" forall y. image strt limp y -> go y x by exists fr. limp fr /\ fr.strt = y so exists p. evp p /\ p fr so exists stk. chh stk /\ sbf p stk @@ -1592,14 +1586,14 @@ module FmlaRulesProof so let op = rprod sc.bo go in let sbp = subchain op in let allk = image keys limp in - (chain sbp allk by forall k1 k2. allk k1 /\ allk k2 -> + ("stop_split" chain sbp allk by forall k1 k2. allk k1 /\ allk k2 -> (sbp k1 k2 \/ sbp k2 k1) by exists f1. limp f1 /\ f1.keys = k1 so exists f2. limp f2 /\ f2.keys = k2 so (lf f1 f2 \/ lf f2 f1)) - so let ksup = subchain_completion allk in + so let ksup = bigunion allk in supremum sbp allk ksup - so (supremum go (image snd ksup) x + so ("stop_split" supremum go (image snd ksup) x by (upper_bound go (image snd ksup) x by forall y. image snd ksup y -> go y x by exists z. ksup z /\ snd z = y @@ -1638,7 +1632,7 @@ module FmlaRulesProof (is_frame sc nf by reach_ch go (step mg' ang witness) ((=) x) ((=) x)) so (* Put it at the top of the stack. *) let lstk = add limp nf in - (maximum lf lstk nf by forall fr. lstk fr -> lf fr nf + ("stop_split" maximum lf lstk nf by forall fr. lstk fr -> lf fr nf by fr = nf || (limp fr so allk fr.keys so sbp fr.keys ksup so chain lf limp @@ -1654,7 +1648,7 @@ module FmlaRulesProof so upper_bound go fr.hstr fr2.strt so (go fr2.strt x by image strt limp fr2.strt) )) - so (is_stack sc lstk + so ("stop_split" is_stack sc lstk by forall f y. lstk f /\ rc_post sc f.keys y /\ go f.strt y -> (exists fr x. chain_to sc lstk fr f x y) by (exists f2. limp f2 /\ lf f2 f /\ @@ -1700,7 +1694,7 @@ module FmlaRulesProof by forall x. rc_pre sc ch0 x -> holds c2 (enforce ((=) x) none) by let pst = \inp x. sc.ps inp x /\ not ch0 inp in let sc2 = { sc with gm = g2; ps = pst } in - (rc_section sc2 + ("stop_split" rc_section sc2 by forall ch. arrow (rc_hyp sc2 ch) (rc_enf sc2 ch) g2 by forall g3. subgame g2 g3 /\ game_wf g3 /\ rc_hyp sc2 ch g3 -> rc_enf sc2 ch g3 @@ -1710,6 +1704,7 @@ module FmlaRulesProof by forall ch'. lower sbp ch ch' -> rc_enf sc ch' g3 by holds c3 (rc_enf sc2 ch') so subset (rc_post sc2 ch') (rc_post sc ch') + so subset (rc_pre sc ch') (rc_pre sc2 ch') so holds c3 (rc_enf sc ch')) so (rc_enf sc ch g3 by subgame sc.gm g3) so holds c3 (rc_enf sc ch) @@ -1750,13 +1745,250 @@ module FmlaRulesProof so holds c2 (enforce (i stk) none) so i stk x - (* TODO: apply the crude recursion theorem to derive - a variation that does not use chains. *) - + lemma 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) + lemma modus_ponens : forall c f1 f2:fmla 'a. + holds c (arrow f1 f2) /\ holds c f1 -> holds c f2 + predicate ifix_limit (c:fmla 'a) (o:erel 'b) (go:erel 'a) (p q:rel 'b 'a) = + (forall ch inh. ch inh /\ chain (iprod o go) ch /\ + (forall x. not maximum o (image fst ch) x) /\ + (forall x y. ch (x,y) -> p x y) -> + let ch1 = image fst ch in let ch2 = image snd ch in + holds c (arrow (universal (u_enforce (higher_limit o p ch1) q)) + (enforce (supremum go ch2) (post_limit q ch1)))) + (* Derive a variant of recursion theorem that does not use chains + except for limit. *) + lemma better_recursion : forall c o go,p q:rel 'b 'a. + holds c (ordering go) /\ order o /\ + (forall x. + holds c (arrow (universal (u_enforce (higher o p x) q)) + (enforce (p x) (q x)))) /\ + ifix_limit c o go p q -> + holds c (universal (u_enforce p q)) + by forall g. c g /\ game_wf g -> universal (u_enforce p q) g + by let cg = subgame g in + cg g /\ is_fmla cg + so + let ip = iprod o go in + let op = rprod ip go in + let sbp = subchain op in + let pre = \ch. + chain op ch /\ + (exists x. ch x) /\ + (forall x y z. ch ((x,y),z) -> p x y /\ y = z) in + let pst = \z y. let ((x,_),_) = z in q x y in + let sc = { + gm = g; + bo = ip; + pr = pre; + ps = pst; + } in + (rc_section sc + by ("stop_split" + forall chh inh chs. chain sbp chh /\ chh inh /\ + supremum sbp chh chs /\ (forall ch. chh ch -> sc.pr ch) -> sc.pr chs + by chs = bigunion chh + so (forall x y z. chs ((x,y),z) -> p x y /\ y = z + by exists ch0. chh ch0 /\ ch0 ((x,y),z)) + so (exists x. inh x so chs x) + so chain op chs + ) /\ ("stop_split" forall ch. arrow (rc_hyp sc ch) (rc_enf sc ch) sc.gm + by holds cg (arrow (rc_hyp sc ch) (rc_enf sc ch)) + by let c2 = conj cg (rc_hyp sc ch) in + (is_fmla c2 by is_fmla (rc_hyp sc ch) + by forall ch. is_fmla (rc_enf sc ch)) + so holds c2 (rc_enf sc ch) + by forall y. rc_pre sc ch y -> + holds c2 (enforce ((=) y) (rc_post sc ch)) + by (* Technical: in the crude variant, the higher + enforcement requires that the next state is after the + one for the lower one, while the variant we prove has + no such constraint. To re-enable it, we introduce a + 'continuation' for element not beyond y in the context, + using enforce_does_progress and kont_intro lemma. *) + let q0 = \x. rc_post sc ch x \/ not go y x in + let q1 = inter q0 (go y) in + (holds c2 (enforce ((=) y) q1) /\ subset q1 (rc_post sc ch)) + by holds c2 (enforce ((=) y) q0) + by holds c2 (arrow (enforce q0 none) (enforce ((=) y) q0)) + by let c3 = conj c2 (enforce q0 none) in + holds c3 (enforce ((=) y) q0) + by let chi = image fst ch in + let chc = image fst chi in + let chg = image snd chi in + (* Lemma: for all x strictly above chc, + 'enforce (p x) (q x)' holds in c3. Will be used in + both future cases. *) + ("stop_split" forall x. upper_bound o chc x /\ not chc x -> + holds c3 (enforce (p x) (q x)) + by forall z. p x z -> holds c3 (enforce ((=) z) (q x)) + by (* Discard not(y < z) by continuation. *) + if not go y z + then subset ((=) z) q0 + so holds c3 (enforce q0 none) + else let nw = ((x,z),z) in + let nch = add ch nw in + ("stop_split" holds c3 (enforce ((=) z) (rc_post sc nch)) + by ("stop_split" upper_bound op ch nw + by forall u. ch u -> op u nw + by let ((a,b),c) = u in b = c + so (go c z by go c y by image snd ch c) + so (o a x /\ a <> x by chc a by chi (a,b)) + ) + so (lower sbp ch nch + by not (ch nw so chi (x,z) so chc x) + so not (sbp nch ch so subset nch ch so sext ch nch) + so sbp ch nch) + so holds c3 (b_universal (lower sbp ch) (rc_enf sc)) + so holds c3 (rc_enf sc nch) + so subset ((=) z) (rc_pre sc nch) + by rc_pre sc nch z + by (maximum op nch nw by reflexive op) + so chain op nch + so (forall a b c. nch ((a,b),c) -> + p a b /\ b = c by ch ((a,b),c) || (a = x /\ b = z /\ c = z)) + so sc.pr nch + so supremum go (image snd nch) z + ) /\ ("stop_split" holds c3 (enforce (rc_post sc nch) (q x)) + by forall z. rc_post sc nch z -> + holds c3 (enforce ((=) z) (q x)) + by exists v. nch v /\ pst v z + so if ch v + then subset ((=) z) q0 + so holds c3 (enforce q0 none) + else v = nw so q x z + ) + ) + (* Invoke different hypothesis depending on whether + ch has a maximum. *) + so if (exists u. maximum op ch u) + then exists u. maximum op ch u + so let ((x0,y0),z0) = u in + z0 = y /\ y0 = z0 + so subset ((=) y) (p x0) + so subset (q x0) (rc_post sc ch) + so "stop_split" holds c3 (enforce (p x0) (q x0)) + by let unv = universal (u_enforce (higher o p x0) q) in + holds c3 (arrow unv (enforce (p x0) (q x0))) + so holds c3 unv + by forall x. holds c3 (enforce (higher o p x0 x) (q x)) + by forall z. higher o p x0 x z -> + holds c3 (enforce ((=) z) (q x)) + by subset ((=) z) (p x) + so holds c3 (enforce (p x) (q x)) + 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) + 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)) + else + (* Prove that chi satisfy the hypothesis + expected for the limit enforcement. *) + ("stop_split" forall x. not (maximum o chc x + so exists p0. chi p0 /\ fst p0 = x + so exists p1. ch p1 /\ fst p1 = p0 + so let ((_,y),z) = p1 in y = z + so maximum op ch p1 + by forall u. ch u -> if op u p1 then true else false + by let ((a,b) as v,c) = u in + p a b /\ b = c + so order op so op p1 u so ip p0 v so o x a so a <> x + so chi v so chc a so o a x)) + so exists inh. ch inh + so let ((x_,_) as p_,_) = inh in (chc x_ by chi p_) + so chain ip chi + so (forall x y. chi (x,y) -> p x y + by exists p0. ch p0 /\ fst p0 = (x,y)) + so let unv = universal (u_enforce (higher_limit o p chc) q) in + let enf = enforce (supremum go chg) (post_limit q chc) in + holds c (arrow unv enf) + so holds c3 (arrow unv enf) + so ("stop_split" subset ((=) y) (supremum go chg) + by sext chg (image snd ch) + by (forall x. chg x -> image snd ch x + by exists p. chi p /\ snd p = x + so exists p2. ch p2 /\ fst p2 = p + so snd p2 = x by let ((_,a),b) = p2 in a = b + ) /\ (forall x. image snd ch x -> chg x + by exists p. ch p /\ snd p = x + so let ((_,a) as p2 ,b) = p in a = b + so (chi p2 by fst p = p2) so snd p2 = a)) + so ("stop_split" subset (post_limit q chc) q0 + by forall z. post_limit q chc z -> q0 z + by rc_post sc ch z + by exists x. chc x /\ q x z + so exists p. chi p /\ fst p = x + so exists p2. ch p2 /\ fst p2 = p + so (pst p2 z by let ((a,_),_) = p2 in q a z)) + so "stop_split" holds c3 enf + by holds c3 unv + by forall x. holds c3 (enforce (higher_limit o p chc x) (q x)) + by forall z. higher_limit o p chc x z -> + holds c3 (enforce ((=) z) (q x)) + by subset ((=) z) (p x) + so holds c3 (enforce (p x) (q x)) + by upper_bound o chc x + so not (chc x so maximum o chc x) + ) + ) + so forall x. u_enforce p q x g by enforce (p x) (q x) g + by holds cg (enforce (p x) (q x)) + by forall y. p x y -> holds cg (enforce ((=) y) (q x)) + by let ch0 = (=) ((x,y),y) in + rc_enf sc ch0 g + so holds cg (enforce (rc_pre sc ch0) (rc_post sc ch0)) + so (subset ((=) y) (rc_pre sc ch0) + by (supremum go (image snd ch0) y + by order go /\ image snd ch0 = (=) y + by sext (image snd ch0) ((=) y) + by snd ((x,y),y) = y + ) + so chain op ch0 + so ch0 ((x,y),y) + so forall a b c. ch0 ((a,b),c) -> p a b /\ b = c + ) + so subset (rc_post sc ch0) (q x) + (* Now we can prove the exported variant of recursion theorem. *) + lemma recursion : forall c o go,p q:rel 'b 'a. + holds c (ordering go) /\ order o /\ + (forall x. + holds c (arrow (universal (u_enforce (higher o p x) q)) + (enforce (p x) (q x)))) /\ + fix_limit c o go p q -> + holds c (universal (u_enforce p q)) + by ifix_limit c o go p q + by forall ch inh. ch inh /\ chain (iprod o go) ch /\ + (forall x. not maximum o (image fst ch) x) /\ + (forall x y. ch (x,y) -> p x y) -> + let ch1 = image fst ch in let ch2 = image snd ch in + holds c (arrow (universal (u_enforce (higher_limit o p ch1) q)) + (enforce (supremum go ch2) (post_limit q ch1))) + by let wit = \x z. ch (x,z) in + let f = \x. choice (wit x) in + (ch2 = image f ch1 by sext ch2 (image f ch1) + by (forall y. ch2 y -> image f ch1 y + by exists z. ch z /\ snd z = y + so let (x,_) = z in ch (x,f x) + so y = f x by (iprod o go z (x,f x) \/ iprod o go (x,f x) z) + ) /\ (forall y. image f ch1 y -> ch2 y + by exists x. ch1 x /\ f x = y + so exists z. ch z /\ fst z = x + so let (_,_) = z in snd (x,y) = y + )) + so (forall x. ch1 x -> p x (f x)) + so (chain o ch1 by forall x y. ch1 x /\ ch1 y -> o x y \/ o y x + by exists a. ch a /\ fst a = x so exists b. ch b /\ fst b = y + so let ((_,_),(_,_)) = (a,b) in iprod o go a b \/ iprod o go b a) + so (monotone_on ch1 o f go by forall x y. ch1 x /\ ch1 y /\ o x y -> + let a = (x,f x) in let b = (y,f y) in + ch a /\ ch b so iprod o go a b \/ (x = y by iprod o go b a)) + so let (a,_) = inh in ch1 a clone FmlaRules with goal enforce_fmla, goal b_universal_fmla, @@ -1769,8 +2001,8 @@ module FmlaRulesProof goal external_pre, goal kont_intro, goal trampoline, - goal abstraction - (* TODO: goal vertical_fix *) + goal abstraction, + goal modus_ponens, + goal recursion end - diff --git a/examples/in_progress/2wp_gen/game_fmla/why3session.xml b/examples/in_progress/2wp_gen/game_fmla/why3session.xml index 7e909fceaafef3e87791f1a94a2b8edadb8dc168..1b8084025ea91276e5599c751723c0d3678de69e 100644 --- a/examples/in_progress/2wp_gen/game_fmla/why3session.xml +++ b/examples/in_progress/2wp_gen/game_fmla/why3session.xml @@ -2,15 +2,15 @@ - - - - + + + + - + @@ -20,10 +20,10 @@ - + - + @@ -32,68 +32,68 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -103,10 +103,10 @@ - + - + @@ -115,118 +115,118 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -237,7 +237,7 @@ - + @@ -248,1098 +248,1149 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + + + + + - + - + - + - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + - + - + - + - + - + - + - - - - - + + + + + + + + + + + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -1350,10 +1401,10 @@ - + - + @@ -1362,2254 +1413,3013 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + + + + + + + + + + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - + - + + + + + + + + + + + + + + + + + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + + + + + + + + + + + + + + + + + + + + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - - + + - - + + - - + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - - + + + + + + + + + + + + + + + + + + - - + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + + + + + + + + + + + + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + + + + + + + - - + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + - - + + - - - - - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + diff --git a/examples/in_progress/2wp_gen/game_fmla/why3shapes.gz b/examples/in_progress/2wp_gen/game_fmla/why3shapes.gz index 5010b4f06a9f492a14e27004b7394d6bb42faabd..c62e7fc4d1406c213d1360665c1bc9f1e3dddf91 100644 Binary files a/examples/in_progress/2wp_gen/game_fmla/why3shapes.gz and b/examples/in_progress/2wp_gen/game_fmla/why3shapes.gz differ diff --git a/examples/in_progress/2wp_gen/ho_set.mlw b/examples/in_progress/2wp_gen/ho_set.mlw index a800994d26c678d3099ecbc086afb2118f742ccc..15d7975323bb9a551935c362e7186b6cb3407a04 100644 --- a/examples/in_progress/2wp_gen/ho_set.mlw +++ b/examples/in_progress/2wp_gen/ho_set.mlw @@ -1,3 +1,4 @@ module Set use export base.Set end -module SubsetOrder use export base.SubsetOrder end \ No newline at end of file +module SubsetOrder use export base.SubsetOrder end +module SetBigOps use export base.SetBigOps end \ No newline at end of file diff --git a/examples/in_progress/2wp_gen/ho_set/why3session.xml b/examples/in_progress/2wp_gen/ho_set/why3session.xml index 3d780429aeb39f6069ef3bcda913a8108ace90d7..7188d04b182cb4954be4719ee67e1a02d3d131aa 100644 --- a/examples/in_progress/2wp_gen/ho_set/why3session.xml +++ b/examples/in_progress/2wp_gen/ho_set/why3session.xml @@ -7,5 +7,7 @@ + + diff --git a/examples/in_progress/2wp_gen/order.mlw b/examples/in_progress/2wp_gen/order.mlw index a09a6e56bb20ef61e95b5989a2e1eb695fd2ac97..bc81269d4dcad8841d92646885ff7327371874b7 100644 --- a/examples/in_progress/2wp_gen/order.mlw +++ b/examples/in_progress/2wp_gen/order.mlw @@ -92,13 +92,14 @@ module Chain predicate chain_complete (o:erel 'a) = forall s. chain o s -> exists y. supremum o s y + (* quasi-chain-complete = all non-empty chains admit supremum. *) + predicate q_chain_complete (o:erel 'a) = + forall s inh. chain o s /\ s inh -> exists y. supremum o s y + predicate subchain (o:erel 'a) (s1 s2:set 'a) = subset s1 s2 /\ forall x y. s1 x /\ s2 y /\ not s1 y -> o x y - function subchain_completion (c:set (set 'a)) : set 'a = - \x. exists s. c s /\ s x - predicate wf_chain (o:erel 'a) (s:set 'a) = forall s2. subset s2 s /\ (exists x. s2 x) -> exists y. minimum o s2 y @@ -162,13 +163,14 @@ end module SubChain "W:non_conservative_extension:N" (* => SubChainProof *) use export Chain + use import ho_set.SetBigOps axiom subchain_complete_order : forall o:erel 'a. transitive o -> order (subchain o) /\ chain_complete (subchain o) axiom subchain_completion : forall o:erel 'a,ch. chain (subchain o) ch -> - supremum (subchain o) ch (subchain_completion ch) + supremum (subchain o) ch (bigunion ch) axiom chain_subchain_completion : forall o:erel 'a,ch x. chain (subchain o) ch /\ (forall x. ch x -> chain o x) /\ @@ -183,6 +185,7 @@ end module SubChainProof use import ho_set.SubsetOrder + use import ho_set.SetBigOps use import Chain lemma subchain_antisymetric : forall o:erel 'a. @@ -192,7 +195,7 @@ module SubChainProof transitive o -> order (subchain o) lemma subchain_completion : forall o:erel 'a,ch. - let u = subchain_completion ch in + let u = bigunion ch in let sb = subchain o in chain sb ch -> supremum sb ch u @@ -211,7 +214,7 @@ module SubChainProof chain (subchain o) ch /\ (forall x. ch x -> chain o x) /\ supremum (subchain o) ch x -> chain o x - by x = subchain_completion ch + by x = bigunion ch so forall u v. x u /\ x v -> o u v \/ o v u by exists wu. ch wu /\ wu u so exists wv. ch wv /\ wv v @@ -222,7 +225,7 @@ module SubChainProof chain (subchain o) ch /\ (forall x. ch x -> wf_chain o x) /\ supremum (subchain o) ch x -> wf_chain o x - by x = subchain_completion ch + by x = bigunion ch so forall s2 y. s2 y /\ subset s2 x -> (exists z. minimum o s2 z) by exists wy. ch wy /\ wy y @@ -347,4 +350,13 @@ module ProductChain so exists y. supremum o2 (image snd ch) y so supremum (rprod o1 o2) ch (x,y) + lemma prod_q_chain_complete : forall o1:erel 'a,o2:erel 'b. + order o1 /\ order o2 /\ q_chain_complete o1 /\ q_chain_complete o2 -> + q_chain_complete (rprod o1 o2) + by forall ch inh. chain (rprod o1 o2) ch /\ ch inh -> + let (a,b) = inh in image fst ch a /\ image snd ch b + so exists x. supremum o1 (image fst ch) x + so exists y. supremum o2 (image snd ch) y + so supremum (rprod o1 o2) ch (x,y) + end \ No newline at end of file diff --git a/examples/in_progress/2wp_gen/order/why3session.xml b/examples/in_progress/2wp_gen/order/why3session.xml index 0d4add148c29f1bcaa7f9df261e65159d1c4eaf4..5e08450aebda69e346040f51002e0eb7067503c5 100644 --- a/examples/in_progress/2wp_gen/order/why3session.xml +++ b/examples/in_progress/2wp_gen/order/why3session.xml @@ -2,128 +2,128 @@ - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -132,7 +132,7 @@ - + @@ -143,383 +143,405 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/in_progress/2wp_gen/order/why3shapes.gz b/examples/in_progress/2wp_gen/order/why3shapes.gz index b560c11db6ca7d3f9f7e37fd9a559172b8f6d941..913f4e0ff11899f239f797e33e8afe33dee465df 100644 Binary files a/examples/in_progress/2wp_gen/order/why3shapes.gz and b/examples/in_progress/2wp_gen/order/why3shapes.gz differ diff --git a/examples/in_progress/2wp_gen/transfinite.mlw b/examples/in_progress/2wp_gen/transfinite.mlw index fd31e2f855d70716deca1ee590edf5d2659b36d3..de01698e072f5726ad57ef1fdcec8b4e30f07420 100644 --- a/examples/in_progress/2wp_gen/transfinite.mlw +++ b/examples/in_progress/2wp_gen/transfinite.mlw @@ -37,7 +37,7 @@ module Iterates "W:non_conservative_extension:N" (* => IterateProof *) function fixpoint_above (o:'a -> 'a -> bool) (f:'a -> 'a) 'a : 'a axiom tr_reach_maximum : forall o f,x:'a. - order o /\ inflationary o f /\ chain_complete o -> + order o /\ inflationary o f /\ q_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) @@ -109,11 +109,12 @@ module IterateProof sup o (tr_reach o f u) lemma fixpoint_max_proof : forall o f,u:'a. - order o /\ chain_complete o /\ inflationary o f -> + order o /\ q_chain_complete o /\ inflationary o f -> (forall x y. tr_reach o f u x /\ tr_reach o f u y -> separator o f x y && (o x y \/ o y x)) && chain o (tr_reach o f u) && let y = fixpoint_above o f u in - maximum o (tr_reach o f u) y && (f y = y by o (f y) y /\ o y (f y)) + (maximum o (tr_reach o f u) y by tr_reach o f u u) + && (f y = y by o (f y) y /\ o y (f y)) lemma fixpoint_is_max_proof : forall o f,x y:'a. order o /\ inflationary o f /\ tr_reach o f x y /\ f y = y -> diff --git a/examples/in_progress/2wp_gen/transfinite/why3session.xml b/examples/in_progress/2wp_gen/transfinite/why3session.xml index 641e0ed7a58cc1f393d1526f7a5b81e32fee2a92..dd506008d5ce1400477d2ad7434a1388fccd1bd8 100644 --- a/examples/in_progress/2wp_gen/transfinite/why3session.xml +++ b/examples/in_progress/2wp_gen/transfinite/why3session.xml @@ -2,36 +2,36 @@ - - - - + + + + - + - + - + - + @@ -44,7 +44,7 @@ - + @@ -55,7 +55,7 @@ - + @@ -68,7 +68,7 @@ - + @@ -81,25 +81,25 @@ - + - + - + - + - + - + - + @@ -108,7 +108,7 @@ - + @@ -119,7 +119,7 @@ - + @@ -130,7 +130,7 @@ - + @@ -143,32 +143,35 @@ - + - + - + - + - + - + - + + + + - + @@ -177,7 +180,7 @@ - + @@ -188,7 +191,7 @@ - + @@ -199,7 +202,7 @@ - + @@ -208,75 +211,75 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -285,7 +288,7 @@ - + @@ -296,7 +299,7 @@ - + @@ -307,7 +310,7 @@ - + @@ -316,17 +319,17 @@ - + - + - + @@ -335,10 +338,10 @@ - + - + @@ -347,24 +350,24 @@ - + - + - + - + - + - + @@ -373,21 +376,21 @@ - + - + - + @@ -396,69 +399,69 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -471,7 +474,7 @@ - + @@ -482,7 +485,7 @@ - + @@ -493,7 +496,7 @@ - + @@ -502,7 +505,7 @@ - + @@ -515,7 +518,7 @@ - + @@ -526,7 +529,7 @@ - + @@ -537,7 +540,7 @@ - + @@ -546,80 +549,80 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -628,7 +631,7 @@ - + @@ -639,7 +642,7 @@ - + @@ -650,7 +653,7 @@ - + @@ -661,22 +664,22 @@ - + - + - + - + - + - + diff --git a/examples/in_progress/2wp_gen/transfinite/why3shapes.gz b/examples/in_progress/2wp_gen/transfinite/why3shapes.gz index 3a672b42ffff87fecf7dffd9dc96ac8bbfd156ed..0145ab777712d6e61e357a7defb1be53048668ea 100644 Binary files a/examples/in_progress/2wp_gen/transfinite/why3shapes.gz and b/examples/in_progress/2wp_gen/transfinite/why3shapes.gz differ