(* Definition and lemmas about the transfinite sequence generated by an inflationary function on a chain-complete order. *) module IterateCommon use import order.Chain (* Transfinite reachability of an inflationary function in chain-complete orders. *) 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 module Iterates "W:non_conservative_extension:N" (* => IterateProof *) 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. 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) (* Transfinite chain stop at the first encountered fixpoint. *) 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 (* the set of reachable states from a given one is a well-founded chain for the base order relation. *) axiom tr_reach_wf : forall o f,x:'a. order o /\ inflationary o f -> wf_chain o (tr_reach o f x) && chain o (tr_reach o f x) end module IterateProof use import ho_set.Set use import order.WfChain use import order.LimUniq 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 = sup o (tr_reach o f u) lemma fixpoint_max_proof : forall o f,u:'a. 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 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 -> maximum o (tr_reach o f x) y 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 predicate all_acc (o:'a -> 'a -> bool) (f:'a -> 'a) (x:'a) (y:'a) = forall z. tr_reach o f x z /\ o z y -> acc_on (lower o) (tr_reach o f x) z lemma tr_reach_wf : forall o f,x:'a. order o /\ inflationary o f -> 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) clone Iterates with 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 use import option.Option use import Iterates use import ho_set.Set use import ho_rel.Rel use import order.Chain type ub_builder 'a = set 'a -> option 'a 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 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) = tr_reach (subchain o) (extends_ch o f) x y end (* Special shape of iterates: chain extension. This module contain the machinery to build chain iterates. *) module ChainExtension "W:non_conservative_extension:N" (* => ChainExtensionProof *) use import ho_rel.Rel use import order.SubChain use export ChainExtensionCommon axiom extends_inflationary : forall o:erel 'a,f. ub_builder o f -> inflationary (subchain o) (extends_ch o f) axiom extends_preserve_chains : forall o:erel 'a,f ch. ub_builder o f /\ chain o ch /\ reflexive o -> chain o (extends_ch o f ch) axiom extends_preserve_wf_chains : forall o:erel 'a,f ch. ub_builder o f /\ wf_chain o ch /\ reflexive o -> wf_chain o (extends_ch o f ch) axiom reach_only_chains : forall o:erel 'a,f ch1 ch2. ub_builder o f /\ chain o ch1 /\ reach_ch o f ch1 ch2 /\ reflexive o -> chain o ch2 axiom reach_only_wf_chains : forall o:erel 'a,f ch1 ch2. ub_builder o f /\ wf_chain o ch1 /\ reach_ch o f ch1 ch2 /\ reflexive o -> wf_chain o ch2 axiom reach_ch_interval : forall o:erel 'a,f ch1 chm ch2. 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 end module ChainExtensionProof use import option.Option use import ho_set.SubsetOrder use import ho_rel.Rel use import order.SubChain use import order.WfChain use import choice.Choice use import Iterates use import ChainExtensionCommon 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. ub_builder o f /\ chain o ch /\ reflexive o -> chain o (extends_ch o f ch) lemma extends_preserve_wf_chains : forall o:erel 'a,f ch. 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) ) 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 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 -> ("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 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)) clone ChainExtension with goal extends_inflationary, goal extends_preserve_chains, goal extends_preserve_wf_chains, goal reach_only_chains, goal reach_only_wf_chains, goal reach_ch_interval end