transfinite.mlw 11.8 KB
 Martin Clochard committed Jan 25, 2016 1 2 3 4 5 6 7 8 `````` (* Definition and lemmas about the transfinite sequence generated by an inflationary function on a chain-complete order. *) module IterateCommon use import order.Chain `````` Martin Clochard committed Feb 22, 2016 9 10 `````` (* Transfinite reachability of an inflationary function in chain-complete orders. *) `````` Martin Clochard committed Jan 25, 2016 11 12 13 14 15 16 17 18 19 20 21 22 `````` inductive tr_reach ('a -> 'a -> bool) ('a -> 'a) (_ _:'a) = | Reach_base : forall o f,x:'a. tr_reach o f x x | Reach_succ : forall o f,x y:'a. tr_reach o f x y -> tr_reach o f x (f y) | Reach_chain : forall o f x c,y:'a. chain o c /\ c x /\ (forall y. c y -> tr_reach o f x y) /\ supremum o c y -> tr_reach o f x y predicate separator (o:'a -> 'a -> bool) (f:'a -> 'a) (base x:'a) = o x base \/ o (f base) x end `````` Martin Clochard committed Feb 22, 2016 23 ``````module Iterates "W:non_conservative_extension:N" (* => IterateProof *) `````` Martin Clochard committed Jan 25, 2016 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 `````` use import order.Chain use export IterateCommon (* tr_reach is a chain, and there are no tr_reach element between any z and its 'sucessor' f z. *) axiom tr_reach_separated : forall o f,x y z:'a. order o /\ inflationary o f /\ tr_reach o f x y /\ tr_reach o f x z -> separator o f z y (* For chain-complete orders, there is a maximum tr_reach element, which is a fixpoint of the growth function (the fixpoint part is the Bourbaki-Witt theorem) *) function fixpoint_above (o:'a -> 'a -> bool) (f:'a -> 'a) 'a : 'a axiom tr_reach_maximum : forall o f,x:'a. `````` Martin Clochard committed Mar 14, 2016 40 `````` order o /\ inflationary o f /\ q_chain_complete o -> `````` Martin Clochard committed Jan 25, 2016 41 42 43 `````` f (fixpoint_above o f x) = fixpoint_above o f x /\ maximum o (tr_reach o f x) (fixpoint_above o f x) `````` Martin Clochard committed Feb 22, 2016 44 `````` (* Transfinite chain stop at the first encountered fixpoint. *) `````` Martin Clochard committed Jan 25, 2016 45 46 47 48 49 50 51 52 53 54 55 56 57 `````` axiom tr_reach_fixpoint : forall o f,x y:'a. order o /\ inflationary o f /\ f y = y /\ tr_reach o f x y -> maximum o (tr_reach o f x) y (* transifinite reachability relation is compatible with the base order. *) axiom tr_reach_compare : forall o f,x y:'a. preorder o /\ inflationary o f /\ tr_reach o f x y -> o x y (* transfinite reachability relation is transitive. *) axiom tr_reach_transitive : forall o f,x y z:'a. preorder o /\ inflationary o f -> tr_reach o f x y /\ ("induction" tr_reach o f y z) -> tr_reach o f x z `````` Martin Clochard committed Feb 22, 2016 58 `````` (* the set of reachable states from a given one is a well-founded chain `````` Martin Clochard committed Jan 25, 2016 59 60 `````` for the base order relation. *) axiom tr_reach_wf : forall o f,x:'a. `````` Martin Clochard committed Feb 22, 2016 61 62 `````` order o /\ inflationary o f -> wf_chain o (tr_reach o f x) && chain o (tr_reach o f x) `````` Martin Clochard committed Jan 25, 2016 63 64 65 66 67 `````` end module IterateProof `````` Martin Clochard committed Feb 22, 2016 68 69 70 `````` use import ho_set.Set use import order.WfChain use import order.LimUniq `````` Martin Clochard committed Jan 25, 2016 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 `````` use import choice.Choice use import IterateCommon lemma tr_reach_compare : forall o f,x y:'a. preorder o /\ inflationary o f -> ("induction" tr_reach o f x y) -> o x y predicate near_all_separator (o:'a -> 'a -> bool) (f:'a -> 'a) (u a:'a) = tr_reach o f u a /\ forall c b. tr_reach o f u c /\ tr_reach o f u b /\ o c a /\ not o a c -> separator o f c b (* Any element <= a is a separator. *) predicate all_separator (o:'a -> 'a -> bool) (f:'a -> 'a) (u a:'a) = tr_reach o f u a /\ forall c b. tr_reach o f u c /\ tr_reach o f u b /\ o c a -> separator o f c b lemma separation : forall o f,u base:'a. order o /\ inflationary o f /\ near_all_separator o f u base -> (forall o1 f1 u1 x. o1 = o /\ f1 = f /\ u1 = u -> ("induction" tr_reach o1 f1 u1 x) -> separator o f base x) lemma all_separation : forall o,f,u:'a. order o /\ inflationary o f -> (forall o1 f1 u1 x. o1 = o /\ f1 = f /\ u1 = u -> ("induction" tr_reach o1 f1 u1 x) -> all_separator o f u x) by (forall a. all_separator o f u a -> near_all_separator o f u (f a) by forall c b. o c (f a) /\ not o (f a) c /\ tr_reach o f u c /\ tr_reach o f u b -> separator o f c b by separator o f a c) /\ forall ch a. ch u /\ (forall y. ch y -> all_separator o f u y) /\ chain o ch /\ supremum o ch a -> near_all_separator o f u a by forall c b. o c a /\ not o a c /\ tr_reach o f u c /\ tr_reach o f u b -> separator o f c b by exists x. ch x /\ not o x c so separator o f x c function fixpoint_above (o:'a -> 'a -> bool) (f:'a -> 'a) (u:'a) : 'a = `````` Martin Clochard committed Feb 22, 2016 109 `````` sup o (tr_reach o f u) `````` Martin Clochard committed Jan 25, 2016 110 111 `````` lemma fixpoint_max_proof : forall o f,u:'a. `````` Martin Clochard committed Mar 14, 2016 112 `````` order o /\ q_chain_complete o /\ inflationary o f -> `````` Martin Clochard committed Jan 25, 2016 113 114 115 `````` (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 `````` Martin Clochard committed Mar 14, 2016 116 117 `````` (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)) `````` Martin Clochard committed Jan 25, 2016 118 119 120 121 `````` 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 -> maximum o (tr_reach o f x) y `````` Martin Clochard committed Feb 22, 2016 122 123 124 `````` by (forall o1 f1 x1 y1. o1 = o /\ f1 = f /\ x1 = x -> "induction" tr_reach o1 f1 x1 y1 -> o y1 y) by forall c x. supremum o c x /\ upper_bound o c y -> o x y `````` Martin Clochard committed Jan 25, 2016 125 126 `````` predicate all_acc (o:'a -> 'a -> bool) (f:'a -> 'a) (x:'a) (y:'a) = `````` Martin Clochard committed Feb 22, 2016 127 128 `````` forall z. tr_reach o f x z /\ o z y -> acc_on (lower o) (tr_reach o f x) z `````` Martin Clochard committed Jan 25, 2016 129 `````` `````` Martin Clochard committed Feb 22, 2016 130 `````` lemma tr_reach_wf : forall o f,x:'a. `````` Martin Clochard committed Jan 25, 2016 131 `````` order o /\ inflationary o f -> `````` Martin Clochard committed Feb 22, 2016 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 `````` let s = tr_reach o f x in wf_chain o s by (chain o s by forall x y. s x /\ s y -> o x y \/ o y x by separator o f x y) /\ let lo = lower o in let a = all_acc o f x in wf_on lo s by (forall o1 f1 x1 y. o1 = o /\ f1 = f /\ x1 = x -> ("induction" tr_reach o1 f1 x1 y) -> a y) by (forall y. s y /\ a y -> a (f y) by forall z. s z /\ o z (f y) -> acc_on lo s z by "case_split" (o z y || (z = f y so forall z. s z /\ lo z (f y) -> acc_on lo s z by o z y by separator o f y z)) by separator o f y z) /\ forall c y. chain o c /\ c x /\ (forall y. c y -> s y /\ a y) /\ supremum o c y -> a y by forall z. s z /\ lo z y -> acc_on lo s z by (exists t. c t /\ o z t) || (false by upper_bound o c z by forall t. c t -> separator o f t z) lemma add_chain : forall o f x y c,z:'a. preorder o /\ inflationary o f /\ c y /\ chain o c /\ (forall t. c t -> tr_reach o f x t) /\ supremum o c z /\ tr_reach o f x y -> tr_reach o f x z by chain o (add c x) so supremum o (add c x) z by sext (upper_bound o (add c x)) (upper_bound o c) `````` Martin Clochard committed Jan 25, 2016 160 `````` `````` Martin Clochard committed Feb 08, 2016 161 `````` clone Iterates with `````` Martin Clochard committed Jan 25, 2016 162 163 164 165 166 167 168 169 170 171 172 173 `````` function fixpoint_above = fixpoint_above, goal tr_reach_separated, goal tr_reach_maximum, goal tr_reach_fixpoint, goal tr_reach_compare, goal tr_reach_transitive, goal tr_reach_wf end module ChainExtensionCommon `````` Martin Clochard committed Jun 21, 2016 174 `````` use import option.Option `````` Martin Clochard committed Jan 25, 2016 175 `````` use import Iterates `````` Martin Clochard committed Feb 22, 2016 176 `````` use import ho_set.Set `````` Martin Clochard committed Jun 21, 2016 177 `````` use import ho_rel.Rel `````` Martin Clochard committed Jan 25, 2016 178 179 `````` use import order.Chain `````` Martin Clochard committed Jun 21, 2016 180 `````` type ub_builder 'a = set 'a -> option 'a `````` Martin Clochard committed Jan 25, 2016 181 `````` `````` Martin Clochard committed Jun 21, 2016 182 183 184 185 186 `````` predicate ub_builder (o:erel 'a) (f:ub_builder 'a) = forall ch. chain o ch -> match f ch with | None -> true | Some u -> upper_bound o ch u end `````` Martin Clochard committed Jan 25, 2016 187 `````` `````` Martin Clochard committed Jun 21, 2016 188 189 190 191 192 193 194 `````` function extends_ch (o:erel 'a) (f:ub_builder 'a) (ch:set 'a) : set 'a = if chain o ch then match f ch with | None -> ch | Some u -> add ch u end else ch predicate reach_ch (o:erel 'a) (f:ub_builder 'a) (x y:set 'a) = `````` Martin Clochard committed Jan 25, 2016 195 196 197 198 199 200 `````` tr_reach (subchain o) (extends_ch o f) x y end (* Special shape of iterates: chain extension. `````` Martin Clochard committed Feb 22, 2016 201 `````` This module contain the machinery to build chain iterates. *) `````` Martin Clochard committed Feb 08, 2016 202 ``````module ChainExtension "W:non_conservative_extension:N" `````` Martin Clochard committed Feb 22, 2016 203 `````` (* => ChainExtensionProof *) `````` Martin Clochard committed Jan 25, 2016 204 `````` `````` Martin Clochard committed Jun 21, 2016 205 `````` use import ho_rel.Rel `````` Martin Clochard committed Feb 22, 2016 206 `````` use import order.SubChain `````` Martin Clochard committed Jan 25, 2016 207 208 `````` use export ChainExtensionCommon `````` Martin Clochard committed Jun 21, 2016 209 `````` axiom extends_inflationary : forall o:erel 'a,f. `````` Martin Clochard committed Jan 25, 2016 210 211 `````` ub_builder o f -> inflationary (subchain o) (extends_ch o f) `````` Martin Clochard committed Jun 21, 2016 212 `````` axiom extends_preserve_chains : forall o:erel 'a,f ch. `````` Martin Clochard committed Jan 25, 2016 213 `````` ub_builder o f /\ chain o ch /\ reflexive o -> `````` Martin Clochard committed Feb 22, 2016 214 215 `````` chain o (extends_ch o f ch) `````` Martin Clochard committed Jun 21, 2016 216 `````` axiom extends_preserve_wf_chains : forall o:erel 'a,f ch. `````` Martin Clochard committed Feb 22, 2016 217 218 `````` ub_builder o f /\ wf_chain o ch /\ reflexive o -> wf_chain o (extends_ch o f ch) `````` Martin Clochard committed Jan 25, 2016 219 `````` `````` Martin Clochard committed Jun 21, 2016 220 `````` axiom reach_only_chains : forall o:erel 'a,f ch1 ch2. `````` Martin Clochard committed Jan 25, 2016 221 222 223 `````` ub_builder o f /\ chain o ch1 /\ reach_ch o f ch1 ch2 /\ reflexive o -> chain o ch2 `````` Martin Clochard committed Jun 21, 2016 224 `````` axiom reach_only_wf_chains : forall o:erel 'a,f ch1 ch2. `````` Martin Clochard committed Feb 22, 2016 225 226 227 `````` ub_builder o f /\ wf_chain o ch1 /\ reach_ch o f ch1 ch2 /\ reflexive o -> wf_chain o ch2 `````` Martin Clochard committed Jun 21, 2016 228 `````` axiom reach_ch_interval : forall o:erel 'a,f ch1 chm ch2. `````` Martin Clochard committed Feb 22, 2016 229 230 231 232 `````` ub_builder o f /\ reach_ch o f ch1 ch2 /\ order o /\ subchain o ch1 chm /\ subchain o chm ch2 -> reach_ch o f ch1 chm `````` Martin Clochard committed Jan 25, 2016 233 234 235 236 ``````end module ChainExtensionProof `````` Martin Clochard committed Jun 21, 2016 237 `````` use import option.Option `````` Martin Clochard committed Feb 22, 2016 238 `````` use import ho_set.SubsetOrder `````` Martin Clochard committed Jun 21, 2016 239 `````` use import ho_rel.Rel `````` Martin Clochard committed Feb 22, 2016 240 241 `````` use import order.SubChain use import order.WfChain `````` Martin Clochard committed Jan 25, 2016 242 243 244 245 `````` use import choice.Choice use import Iterates use import ChainExtensionCommon `````` Martin Clochard committed Jun 21, 2016 246 247 248 249 250 `````` lemma extends_inflationary : forall o:erel 'a,f. let xt = extends_ch o f in ub_builder o f -> inflationary (subchain o) xt lemma extends_preserve_chains : forall o:erel 'a,f ch. `````` Martin Clochard committed Jan 25, 2016 251 252 253 `````` ub_builder o f /\ chain o ch /\ reflexive o -> chain o (extends_ch o f ch) `````` Martin Clochard committed Jun 21, 2016 254 `````` lemma extends_preserve_wf_chains : forall o:erel 'a,f ch. `````` Martin Clochard committed Feb 22, 2016 255 256 257 258 259 260 261 262 263 264 265 266 `````` ub_builder o f /\ wf_chain o ch /\ reflexive o -> wf_chain o (extends_ch o f ch) by let nx = extends_ch o f ch in forall s2 y. s2 y /\ subset s2 nx -> (exists z. minimum o s2 z) by (chain o ch by let s2 = \x. ch x /\ exists y. ch y /\ not o x y /\ not o y x in not (exists y:'a. s2 y so subset s2 ch so exists u. minimum o s2 u so exists z. ch z /\ not o u z /\ o z u so s2 z) so (forall x y. ch x /\ ch y /\ not o x y /\ not o y x -> false by s2 x) `````` Martin Clochard committed Jun 21, 2016 267 268 269 270 271 272 273 274 275 276 `````` ) so match f ch with | None -> nx = ch | Some u -> nx = add ch u so (exists z. s2 z /\ z <> u so let s3 = inter s2 ch in subset s3 ch /\ s3 z so exists z. minimum o s3 z so minimum o s2 z ) || (y = u so minimum o s2 y) end `````` Martin Clochard committed Feb 22, 2016 277 `````` `````` Martin Clochard committed Jan 25, 2016 278 279 280 281 `````` lemma reach_only_chains : forall o f,ch1 ch2:'a -> bool. ub_builder o f /\ reflexive o /\ chain o ch1 /\ reach_ch o f ch1 ch2 -> chain o ch2 by forall o1 f1 b1 x. o1 = o /\ f1 = f /\ b1 = ch1 -> `````` Martin Clochard committed Feb 22, 2016 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 `````` ("induction" tr_reach (subchain o1) (extends_ch o1 f1) b1 x) -> chain o1 x lemma reach_only_wf_chains : forall o f,ch1 ch2:'a -> bool. ub_builder o f /\ reflexive o /\ wf_chain o ch1 /\ reach_ch o f ch1 ch2 -> wf_chain o ch2 by forall o1 f1 b1 x. o1 = o /\ f1 = f /\ b1 = ch1 -> ("induction" tr_reach (subchain o1) (extends_ch o1 f1) b1 x) -> wf_chain o1 x lemma reach_ch_interval : forall o:'a -> 'a -> bool,f ch1 chm ch2. ub_builder o f /\ reach_ch o f ch1 ch2 /\ order o /\ subchain o ch1 chm /\ subchain o chm ch2 -> not (not reach_ch o f ch1 chm so let sb = subchain o in let xt = extends_ch o f in (forall o1 f1 b1 ch0. o1 = sb /\ f1 = xt /\ b1 = ch1 -> ("induction" tr_reach o1 f1 b1 ch0) -> sb ch0 chm) by inflationary sb xt so (forall ch0. reach_ch o f ch1 ch0 /\ sb ch0 chm -> sb (xt ch0) chm by if sb (xt ch0) chm then true else `````` Martin Clochard committed Jun 21, 2016 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 `````` match f ch0 with | None -> false | Some f0 -> xt ch0 = add ch0 f0 so reach_ch o f ch1 (xt ch0) so (if sb (xt ch0) ch2 then true else false by separator sb xt ch0 ch2 so sb ch2 ch0 so order sb so sb ch2 ch0) so (if not chm f0 then true else false by subset (xt ch0) chm so forall a b. xt ch0 a /\ chm b /\ not xt ch0 b -> o a b) so sext ch0 chm by forall x. chm x -> if ch0 x then true else false by ch2 x so not xt ch0 x so xt ch0 f0 so ch2 f0 so o f0 x so o x f0 end) /\ (forall chh y. (forall x. chh x -> sb x chm) /\ supremum sb chh y -> sb y chm by upper_bound sb chh chm)) `````` Martin Clochard committed Jan 25, 2016 322 `````` `````` Martin Clochard committed Feb 08, 2016 323 `````` clone ChainExtension with `````` Martin Clochard committed Jan 25, 2016 324 `````` goal extends_inflationary, `````` Martin Clochard committed Feb 22, 2016 325 326 327 328 329 `````` goal extends_preserve_chains, goal extends_preserve_wf_chains, goal reach_only_chains, goal reach_only_wf_chains, goal reach_ch_interval `````` Martin Clochard committed Jan 25, 2016 330 331 `````` end``````