 ### examples/in_progress: 2wp_gen, cont'd

parent 58f09fef
 (* Basic arrow definitions *) module Fun use export HighOrd predicate ext (f g:'a -> 'b) = forall x. f x = g x predicate equalizer (a:'a -> bool) (f g:'a -> 'b) = forall x. a x -> f x = g x function compose (g:'b -> 'c) (f:'a -> 'b) : 'a -> 'c = \x. g (f x) function rcompose (f:'a -> 'b) (g:'b -> 'c) : 'a -> 'c = compose g f function id : 'a -> 'a = \x.x function const (x:'b) : 'a -> 'b = \_.x function fst (x:('a,'b)) : 'a = let (x,_) = x in x function snd (x:('a,'b)) : 'b = let (_,x) = x in x function flip (f:'a -> 'b -> 'c) : 'b -> 'a -> 'c = \x y. f y x function update (f:'a -> 'b) (x:'a) (y:'b) : 'a -> 'b = \z. if z = x then y else f z function ([<-]) (f:'a -> 'b) (x:'a) (y:'b) : 'a -> 'b = update f x y end (* Proof done via cloning+replacing axioms by goals *) (* Functional extensionality. *) module FunExt "W:non_conservative_extension:N" (* => FunProofs *) use export Fun axiom extensionality : forall f g:'a -> 'b. ext f g -> f = g let extensional (f g:'a -> 'b) : unit requires { ext f g } ensures { f = g } = () end (* Evident category properties of functions. *) module FunCategory "W:non_conservative_extension:N" (* => FunProofs *) use export Fun axiom assoc : forall f:'a -> 'b,g,h:'c -> 'd. compose (compose h g) f = compose h (compose g f) axiom neutral : forall f:'a -> 'b. compose f id = f = compose id f end (* Proofs of above Fun modules *) module FunProofs use import Fun predicate hack (f g h:'a -> 'b) = f = g = h lemma ext : forall f g:'a -> 'b. ext f g -> f = g by hack f (\x. (\y.y) (f x)) g lemma assoc : forall f:'a -> 'b,g,h:'c -> 'd. ext (compose (compose h g) f) (compose h (compose g f)) lemma neutral : forall f:'a -> 'b. ext (compose f id) f /\ ext (compose id f) f clone FunExt with goal extensionality clone FunCategory with goal assoc, goal neutral end (* Basic definition on sets-as-arrows *) module Set use import Fun type set 'a = 'a -> bool predicate subset (a b:set 'a) = forall x. a x -> b x predicate sext (a b:set 'a) = forall x. a x <-> b x lemma sext_is_ext : forall a b:set 'a. sext a b -> ext a b function neg (s:set 'a) : set 'a = \x. not (s x) function union (a b:set 'a) : set 'a = \x. a x \/ b x function inter (a b:set 'a) : set 'a = \x. a x /\ b x function diff (a b:set 'a) : set 'a = inter a (neg b) constant all : set 'a = \_. true constant none : set 'a = \_. false function sing (x:'a) : set 'a = (=) x function add (s:set 'a) (x:'a) : set 'a = \y. s y \/ x = y function remove (s:set 'a) (x:'a) : set 'a = \y. s y /\ y <> x end (* Basic definition on relations-as-arrows *) module Rel use import Fun type rel 'a 'b = 'a -> 'b -> bool type erel 'a = rel 'a 'a predicate rext (r1 r2:rel 'a 'b) = forall x y. r1 x y <-> r2 x y predicate reflexive (r:erel 'a) = forall x. r x x predicate symetric (r:erel 'a) = forall x y. r x y -> r y x predicate transitive (r:erel 'a) = forall x y z. r x y /\ r y z -> r x z predicate antisymetric (r:erel 'a) = forall x y. r x y /\ r y x -> x = y predicate total (r:erel 'a) = forall x y. r x y \/ r y x predicate preorder (r:erel 'a) = reflexive r /\ transitive r predicate order (r:erel 'a) = preorder r /\ antisymetric r predicate equivalence (r:erel 'a) = preorder r /\ symetric r inductive acc_on (erel 'a) ('a -> bool) 'a = | Acc : forall r s,x:'a. s x /\ (forall y. s y /\ r y x -> acc_on r s y) -> acc_on r s x predicate wf_on (r:erel 'a) (s:'a -> bool) = forall x. s x -> acc_on r s x constant id : rel 'a 'a = (=) function of_func (f:'a -> 'b) : rel 'a 'b = \x y. y = f x function compose (r1:rel 'a 'b) (r2:rel 'b 'c) : rel 'a 'c = \x z. exists y. r1 x y /\ r2 y z function reverse (r:rel 'a 'b) : rel 'b 'a = flip r end (* Relational extensionality. *) module RelExt "W:non_conservative_extension:N" (* => RelProofs *) use export Rel axiom extensionality : forall r1 r2:rel 'a 'b. rext r1 r2 -> r1 = r2 end (* Evident category properties of relations. *) module RelCategory "W:non_conservative_extension:N" (* => RelProofs *) use export Rel axiom assoc : forall r1:rel 'a 'b,r2,r3:rel 'c 'd. compose r1 (compose r2 r3) = compose (compose r1 r2) r3 axiom reverse_antimorphism : forall r1:rel 'a 'b,r2:rel 'b 'c. compose (reverse r2) (reverse r1) = reverse (compose r1 r2) axiom reverse_antimorphism_id : reverse id = (id:erel 'a) axiom reverse_involution : forall r:rel 'a 'b. reverse (reverse r) = r axiom neutral : forall r:rel 'a 'b. compose r id = r = compose id r end (* Relation product. *) module RelProduct use export Rel predicate rprod (r1:rel 'a 'b) (r2:rel 'c 'd) (x:('a,'c)) (y:('b,'d)) = let (xa,xc) = x in let (yb,yd) = y in r1 xa yb /\ r2 xc yd end (* Elements related to a set. *) module RelSet use import Set use export Rel predicate related (r:rel 'a 'b) (s:set 'a) (y:'b) = exists x. s x /\ r x y predicate i_related (r:rel 'a 'b) (s:set 'b) (x:'a) = exists y. s y /\ r x y end module RelProofs use import FunExt use import Rel lemma extensionality : forall r1 r2:rel 'a 'b. rext r1 r2 -> r1 = r2 by ext r1 r2 by forall x. ext (r1 x) (r2 x) predicate (==) (x y:rel 'a 'b) = rext x y meta rewrite_def predicate (==) meta rewrite_def predicate rext meta rewrite_def function compose lemma assoc : forall r1:rel 'a 'b,r2,r3:rel 'c 'd. compose r1 (compose r2 r3) == compose (compose r1 r2) r3 lemma reverse_antimorphism : forall r1:rel 'a 'b,r2:rel 'b 'c. compose (reverse r2) (reverse r1) == reverse (compose r1 r2) lemma reverse_antimorphism_id : reverse id == (id:erel 'a) lemma reverse_involution : forall r:rel 'a 'b. reverse (reverse r) == r lemma neutral : forall r:rel 'a 'b. compose r id == r == compose id r clone RelExt with goal extensionality clone RelCategory with goal assoc, goal reverse_antimorphism, goal reverse_antimorphism_id, goal reverse_involution, goal neutral end module SubsetOrder "W:non_conservative_extension:N" (* => SetProofs *) use export Set use import Rel axiom subset_order : order (subset:erel (set 'a)) end module SetProofs use import FunExt use import Set lemma anti_subset : forall s1 s2:set 'a. subset s1 s2 /\ subset s2 s1 -> sext s1 s2 clone SubsetOrder with goal subset_order end module Image use import Fun use import Set predicate image (f:'a -> 'b) (s:set 'a) (y:'b) = exists x. s x /\ f x = y predicate preimage (f:'a -> 'b) (s:set 'b) (x:'a) = s (f x) end

File added
 module Choice use import HighOrd use import fn.Fun use import option.Option constant default : 'a constant witness : 'a function choice ('a -> bool) : 'a axiom choice_def : forall p,x:'a. p x -> p (choice p) ... ...
 ... ... @@ -2,14 +2,14 @@ ... ...
No preview for this file type
 module Fun use export base.FunExt end module Category use export base.FunCategory end module Image use export base.Image end

File added
This diff is collapsed.
This diff is collapsed.
No preview for this file type
This diff is collapsed.
This diff is collapsed.
No preview for this file type
 module Rel use export base.RelExt end module Category use export base.RelCategory end module Prod use export base.RelProduct end module RelSet use export base.RelSet end \ No newline at end of file

File added
 module Set use export base.Set end module SubsetOrder use export base.SubsetOrder end \ No newline at end of file

File added
 (* Usual definition about (pre)orders. *) module Ordered module Order use export ho_rel.Rel use import HighOrd predicate lower (o:erel 'a) (x y:'a) = o x y /\ not o y x predicate reflexive (o:'a -> 'a -> bool) = forall x. o x x predicate antisymetric (o:'a -> 'a -> bool) = forall x y. o x y /\ o y x -> x = y predicate transitive (o:'a -> 'a -> bool) = forall x y z. o x y /\ o y z -> o x z predicate total (o:'a -> 'a -> bool) = forall x y. o x y \/ o y x predicate preorder (o:'a -> 'a -> bool) = reflexive o /\ transitive o predicate order (o:'a -> 'a -> bool) = reflexive o /\ antisymetric o /\ transitive o predicate lower (o:'a -> 'a -> bool) (x y:'a) = o x y /\ not o y x predicate upper_bound (o:'a -> 'a -> bool) (s:'a -> bool) (u:'a) = predicate upper_bound (o:erel 'a) (s:'a -> bool) (u:'a) = forall x. s x -> o x u predicate lower_bound (o:'a -> 'a -> bool) (s:'a -> bool) (l:'a) = predicate lower_bound (o:erel 'a) (s:'a -> bool) (l:'a) = forall x. s x -> o l x predicate maximum (o:'a -> 'a -> bool) (s:'a -> bool) (u:'a) = predicate maximum (o:erel 'a) (s:'a -> bool) (u:'a) = upper_bound o s u /\ s u lemma maximum_unique : forall o s,u1 u2:'a. antisymetric o /\ maximum o s u1 /\ maximum o s u2 -> u1 = u2 predicate minimum (o:'a -> 'a -> bool) (s:'a -> bool) (u:'a) = lower_bound o s u /\ s u predicate minimum (o:erel 'a) (s:'a -> bool) (l:'a) = lower_bound o s l /\ s l lemma minimum_unique : forall o s,l1 l2:'a. antisymetric o /\ minimum o s l1 /\ minimum o s l2 -> l1 = l2 predicate supremum (o:'a -> 'a -> bool) (s:'a -> bool) (x:'a) = predicate supremum (o:erel 'a) (s:'a -> bool) (x:'a) = minimum o (upper_bound o s) x lemma maximum_supremum : forall o s,x:'a. maximum o s x -> supremum o s x lemma maximum_supremum : forall o s,x:'a. maximum o s x -> supremum o s x predicate infimum (o:'a -> 'a -> bool) (s:'a -> bool) (x:'a) = predicate infimum (o:erel 'a) (s:'a -> bool) (x:'a) = maximum o (lower_bound o s) x lemma minimum_infimum : forall o s,x:'a. minimum o s x -> infimum o s x lemma minimum_infimum : forall o s,x:'a. minimum o s x -> infimum o s x predicate maximal (o:erel 'a) (s:'a -> bool) (x:'a) = forall y. s y /\ o x y -> o y x predicate maximal (o:'a -> 'a -> bool) (x:'a) = forall y. o x y -> o y x predicate minimal (o:erel 'a) (s:'a -> bool) (x:'a) = forall y. s y /\ o y x -> o x y predicate monotone (o1:erel 'a) (f:'a -> 'b) (o2:erel 'b) = forall x y. o1 x y -> o2 (f x) (f y) predicate minimal (o:'a -> 'a -> bool) (x:'a) = forall y. o y x -> o x y predicate monotone_on (s:'a -> bool) (o1:erel 'a) (f:'a -> 'b) (o2:erel 'b) = forall x y. s x /\ s y /\ o1 x y -> o2 (f x) (f y) predicate inflationary (o:erel 'a) (f:'a -> 'a) = forall x. o x (f x) end (* Monotonicity & inflationary functions. *) module Mono module LimUniq use import HighOrd use export Ordered use import choice.Choice predicate monotone (o1:'a -> 'a -> bool) (f:'a -> 'b) (o2:'b -> 'b -> bool) = forall x y. o1 x y -> o2 (f x) (f y) function min (o:erel 'a) (s:'a -> bool) : 'a = choice (minimum o s) function max (o:erel 'a) (s:'a -> bool) : 'a = choice (maximum o s) function inf (o:erel 'a) (s:'a -> bool) : 'a = max o (lower_bound o s) function sup (o:erel 'a) (s:'a -> bool) : 'a = min o (upper_bound o s) lemma maximum_uniq : forall o s,x:'a. order o /\ maximum o s x -> x = max o s by o x (max o s) so o (max o s) x lemma minimum_uniq : forall o s,x:'a. order o /\ minimum o s x -> x = min o s by o x (min o s) so o (min o s) x predicate inflationary (o:'a -> 'a -> bool) (f:'a -> 'a) = forall x. o x (f x) lemma infimum_uniq : forall o s,x:'a. order o /\ infimum o s x -> x = inf o s lemma supremum_uniq : forall o s,x:'a. order o /\ supremum o s x -> x = sup o s end (* Definition about chains in orders, e.g totally ordered subsets. *) module Chain use import HighOrd use import Order use import ho_set.Set use export Ordered (* chain for a relation = subset on which the relation is half-total. *) predicate chain (o:'a -> 'a -> bool) (s:'a -> bool) =