transfinite.mlw 11.8 KB
Newer Older
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

9 10
  (* Transfinite reachability of an inflationary function
     in chain-complete orders. *)
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

23
module Iterates "W:non_conservative_extension:N" (* => IterateProof *)
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.
40
    order o /\ inflationary o f /\ q_chain_complete o ->
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)

44
  (* Transfinite chain stop at the first encountered fixpoint. *)
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

58
  (* the set of reachable states from a given one is a well-founded chain
59 60
     for the base order relation. *)
  axiom tr_reach_wf : forall o f,x:'a.
61 62
    order o /\ inflationary o f ->
      wf_chain o (tr_reach o f x) && chain o (tr_reach o f x)
63 64 65 66 67

end

module IterateProof

68 69 70
  use import ho_set.Set
  use import order.WfChain
  use import order.LimUniq
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 =
109
    sup o (tr_reach o f u)
110 111

  lemma fixpoint_max_proof : forall o f,u:'a.
112
    order o /\ q_chain_complete o /\ inflationary o f ->
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
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))
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
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
125 126

  predicate all_acc (o:'a -> 'a -> bool) (f:'a -> 'a) (x:'a) (y:'a) =
127 128
    forall z. tr_reach o f x z /\ o z y ->
      acc_on (lower o) (tr_reach o f x) z
129

130
  lemma tr_reach_wf : forall o f,x:'a.
131
    order o /\ inflationary o f ->
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)
160

161
  clone Iterates with
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

174
  use import option.Option
175
  use import Iterates
176
  use import ho_set.Set
177
  use import ho_rel.Rel
178 179
  use import order.Chain

180
  type ub_builder 'a = set 'a -> option 'a
181

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
187

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) =
195 196 197 198 199 200
    tr_reach (subchain o) (extends_ch o f) x y

end


(* Special shape of iterates: chain extension.
201
   This module contain the machinery to build chain iterates. *)
202
module ChainExtension "W:non_conservative_extension:N"
203
                      (* => ChainExtensionProof *)
204

205
  use import ho_rel.Rel
206
  use import order.SubChain
207 208
  use export ChainExtensionCommon

209
  axiom extends_inflationary : forall o:erel 'a,f.
210 211
    ub_builder o f -> inflationary (subchain o) (extends_ch o f)

212
  axiom extends_preserve_chains : forall o:erel 'a,f ch.
213
    ub_builder o f /\ chain o ch /\ reflexive o ->
214 215
    chain o (extends_ch o f ch)

216
  axiom extends_preserve_wf_chains : forall o:erel 'a,f ch.
217 218
    ub_builder o f /\ wf_chain o ch /\ reflexive o ->
    wf_chain o (extends_ch o f ch)
219

220
  axiom reach_only_chains : forall o:erel 'a,f ch1 ch2.
221 222 223
    ub_builder o f /\ chain o ch1 /\ reach_ch o f ch1 ch2 /\
    reflexive o -> chain o ch2

224
  axiom reach_only_wf_chains : forall o:erel 'a,f ch1 ch2.
225 226 227
    ub_builder o f /\ wf_chain o ch1 /\ reach_ch o f ch1 ch2 /\
    reflexive o -> wf_chain o ch2

228
  axiom reach_ch_interval : forall o:erel 'a,f ch1 chm ch2.
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

233 234 235 236
end

module ChainExtensionProof

237
  use import option.Option
238
  use import ho_set.SubsetOrder
239
  use import ho_rel.Rel
240 241
  use import order.SubChain
  use import order.WfChain
242 243 244 245
  use import choice.Choice
  use import Iterates
  use import ChainExtensionCommon

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.
251 252 253
    ub_builder o f /\ chain o ch /\ reflexive o ->
    chain o (extends_ch o f ch)

254
  lemma extends_preserve_wf_chains : forall o:erel 'a,f ch.
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)
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
277

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 ->
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
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))
322

323
  clone ChainExtension with
324
    goal extends_inflationary,
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
330 331

end