// ----------------------------------------------------------------- // sets.txt: sets, relations, and graphs // Concrete Abstractions: Sets, Relations, and Graphs // (c) 2020, Wolfgang Schreiner, RISC, JKU Linz, Austria // ----------------------------------------------------------------- // ----------------------------------------------------------------- // sets // ----------------------------------------------------------------- val M:ℕ; type elem = ℕ[M]; type set = Set[elem]; theorem equalDef(a:set,b:set) ⇔ a = b ⇔ ∀x:elem. x ∈ a ⇔ x ∈ b; val empty: set = ∅[elem]; val universe: set = { x | x:elem }; theorem emptyset() ⇔ ∀x:elem. x ∉ empty; theorem universe() ⇔ ∀x:elem. x ∈ universe; theorem emptysetDef() ⇔ empty = choose e:set with ∀x:elem. x ∉ e; theorem universeDef() ⇔ universe = choose u:set with ∀x:elem. x ∈ u; theorem subsetDef(a:set,b:set) ⇔ a ⊆ b ⇔ ∀x∈a. x∈b; theorem minMaxSubset(a:set) ⇔ ∅[elem] ⊆ a ∧ a ⊆ universe; theorem equalSubset(a:set,b:set) ⇔ a = b ⇔ a ⊆ b ∧ b ⊆ a; theorem reflexiveSubset(a:set) ⇔ a ⊆ a; theorem antiSymmetricSubset(a:set,b:set) ⇔ a ⊆ b ∧ b ⊆ a ⇒ a = b; theorem transitiveSubset(a:set,b:set,c:set) ⇔ a ⊆ b ∧ b ⊆ c ⇒ a ⊆ c; theorem unionDef(a:set,b:set) ⇔ ∀x:elem. x ∈ a ∪ b ⇔ x ∈ a ∨ x ∈ b; theorem intersectDef(a:set,b:set) ⇔ ∀x:elem. x ∈ a ∩ b ⇔ x ∈ a ∧ x ∈ b; theorem withoutDef(a:set,b:set) ⇔ ∀x:elem. x ∈ a \ b ⇔ x ∈ a ∧ x ∉ b; theorem unionDef2(a:set,b:set) ⇔ a ∪ b = { x | x:elem with x ∈ a ∨ x ∈ b }; theorem intersectDef2(a:set,b:set) ⇔ a ∩ b = { x | x:elem with x ∈ a ∧ x ∈ b }; theorem withoutDef2(a:set,b:set) ⇔ a \ b = { x | x:elem with x ∈ a ∧ x ∉ b }; theorem idempotentUnion(a:set) ⇔ a ∪ a = a; theorem commutativeUnion(a:set,b:set) ⇔ a ∪ b = b ∪ a; theorem associativeUnion(a:set,b:set,c:set) ⇔ a ∪ (b ∪ c) = (a ∪ b) ∪ c; theorem neutralUnion(a:set) ⇔ a ∪ ∅[elem] = a; theorem distributiveUnion(a:set,b:set,c:set) ⇔ a ∪ (b ∩ c) = (a ∪ b) ∩ (a ∪ c); theorem idempotentIntersect(a:set) ⇔ a ∩ a = a; theorem commutativeIntersect(a:set,b:set) ⇔ a ∩ b = b ∩ a; theorem associativeIntersect(a:set,b:set,c:set) ⇔ a ∩ (b ∩ c) = (a ∩ b) ∩ c; theorem neutralIntersect(a:set) ⇔ a ∩ universe = a; theorem distributiveIntersect(a:set,b:set,c:set) ⇔ a ∩ (b ∪ c) = (a ∩ b) ∪ (a ∩ c); theorem withoutBasic(a:set) ⇔ a\a = ∅[elem] ∧ a\∅[elem] = a ∧ ∅[elem]\a = ∅[elem] ∧ a\universe = ∅[elem]; theorem withoutUnion(a:set,b:set,c:set) ⇔ a\(b ∪ c) = (a\b) ∩ (a\c); theorem withoutIntersect(a:set,b:set,c:set) ⇔ a\(b ∩ c) = (a\b) ∪ (a\c); fun complement(a:set):set = universe\a; theorem complementDef(a:set) ⇔ ∀x:elem. x ∈ complement(a) ⇔ x ∉ a; theorem complementInvolution(a:set) ⇔ complement(complement(a)) = a; theorem complementUnion(a:set) ⇔ a ∪ complement(a) = universe; theorem complementIntersect(a:set) ⇔ a ∩ complement(a) = ∅[elem]; theorem emptysetComplement() ⇔ complement(∅[elem]) = universe; theorem universeComplement() ⇔ complement(universe) = ∅[elem]; theorem subseteqComplement(a:set,b:set) ⇔ a ⊆ b ⇔ complement(b) ⊆ complement(a); theorem deMorganUnion(a:set,b:set) ⇔ complement(a ∪ b) = complement(a) ∩ complement(b); theorem deMorganIntersect(a:set,b:set) ⇔ complement(a ∩ b) = complement(a) ∪ complement(b); type set2 = Set[set]; theorem powersetDef(a:set) ⇔ ∀x:set. x ∈ Set(a) ⇔ x ⊆ a; theorem powersetBasic(a:set) ⇔ ∅[elem] ∈ Set(a) ∧ a ∈ Set(a); theorem bigUnionDef(A:set2) ⇔ ∀x:elem. x ∈ ⋃A ⇔ ∃a∈A. x ∈ a; theorem bigIntersectDef(A:set2) ⇔ ∀x:elem. x ∈ ⋂A ⇔ ∀a∈A. x ∈ a; theorem bigUnionEmpty() ⇔ ⋃ ∅[set] = empty; theorem bigIntersectEmpty() ⇔ ⋂ ∅[set] = universe; type size = ℕ[M+1]; type map = Map[size,elem]; pred bijection(m:map,n:size,a:set) ⇔ (∀i:size with i < n. m[i] ∈ a) ∧ (∀i1:size, i2:size with i1 < i2 ∧ i2 < n. m[i1] ≠ m[i2]) ∧ (∀x∈a. ∃i:size with i < n. m[i] = x); theorem sizeEquiv(a:set) ⇔ ∀n:size. n = |a| ⇔ ∃m:map. bijection(m,n,a); theorem sizeEmptyset() ⇔ |∅[elem]| = 0; theorem sizeUnionIntersect(a:set,b:set) ⇔ |a ∪ b| + |a ∩ b| = |a| + |b|; theorem sizePowerset(a:set) ⇔ |Set(a)| = 2^|a|; // ----------------------------------------------------------------- // relations // ----------------------------------------------------------------- type pair = Tuple[elem,elem]; type rel = Set[pair]; val identity:rel = { ⟨x,x⟩ | x:elem }; fun converse(r:rel):rel = { ⟨p.2,p.1⟩ | p ∈ r }; fun comp(r1:rel,r2:rel):rel = { ⟨p1.1,p2.2⟩ | p1 ∈ r1, p2 ∈ r2 with p1.2 = p2.1 }; theorem identityNeutral(r:rel) ⇔ comp(r,identity) = r ∧ comp(identity,r) = r; theorem compAssoc(r1:rel,r2:rel,r3:rel) ⇔ comp(r1,comp(r2,r3)) = comp(comp(r1,r2),r3); theorem converseTwice(r:rel) ⇔ converse(converse(r)) = r; theorem converseComp(r1:rel,r2:rel) ⇔ converse(comp(r1,r2)) = comp(converse(r2),converse(r1)); pred reflexive(r:rel) ⇔ ∀x:elem. ⟨x,x⟩ ∈ r; pred symmetric(r:rel) ⇔ ∀p∈r. ⟨p.2,p.1⟩ ∈ r; pred antisymmetric(r:rel) ⇔ ∀p∈r. ⟨p.2,p.1⟩ ∈ r ⇒ p.1 = p.2; pred transitive(r:rel) ⇔ ∀p1∈r,p2∈r with p1.2 = p2.1. ⟨p1.1,p2.2⟩ ∈ r; pred reflexiveTransitiveClosure(r:rel,c:rel) ⇔ r ⊆ c ∧ reflexive(c) ∧ transitive(c) ∧ ∀d:rel with r ⊆ d ∧ reflexive(d) ∧ transitive(d). c ⊆ d; type seq = Array[M+1,elem]; type int = ℤ[-1,M+1]; pred connected(p:pair,r:rel) ⇔ ∃s:seq with s[0] = p.1. ∃n:int with 1 ≤ n ∧ n ≤ M+1 ∧ s[n-1] = p.2. ∀k:int with 0 ≤ k ∧ k < n-1. ⟨s[k],s[k+1]⟩ ∈ r; val univrel:rel = { p | p:pair }; val M2 = |univrel|; proc reflexiveTransitiveClosure(r:rel):rel ensures reflexiveTransitiveClosure(r,result); { var c:rel ≔ r ∪ identity; var d:rel; do invariant r ⊆ c ∧ reflexive(c); invariant ∀p∈c. connected(p,r); invariant ∀p1∈c, p2∈r with (p1.2 = p2.1). ⟨p1.1,p2.2⟩ ∉ c ⇒ p1 ∉ d; decreases if c = d then 0 else M2+1-|c|; { d ≔ c; c ≔ c ∪ comp(c,r); } while c ≠ d; return c; } proc reflexiveTransitiveClosure2(r:rel):rel ensures reflexiveTransitiveClosure(r,result); { var c:rel ≔ r ∪ identity; var d:rel; do invariant r ⊆ c ∧ reflexive(c); invariant ∀p∈c. connected(p,r); invariant ∀p1∈c, p2∈c with (p1.2 = p2.1). ⟨p1.1,p2.2⟩ ∉ c ⇒ p1 ∉ d ∨ p2 ∉ d; decreases if c = d then 0 else M2+1-|c|; { d ≔ c; c ≔ comp(c,c); } while c ≠ d; return c; } pred connected(p:pair,r:rel,k:int) requires 0 ≤ k ∧ k ≤ M+1; ⇔ ∃s:seq with s[0] = p.1. ∃n:int with 1 ≤ n ∧ n ≤ M+1 ∧ s[n-1] = p.2. (∀i:int with 0 ≤ i ∧ i < n-1. ⟨s[i],s[i+1]⟩ ∈ r) ∧ (∀i:int with 1 ≤ i ∧ i < n-1. s[i] < k); proc warshall(r:rel):rel ensures reflexiveTransitiveClosure(r,result); { var c:rel = r ∪ identity; for var k:int ≔ 0; k ≤ M; k ≔ k+1 do invariant 0 ≤ k ∧ k ≤ M+1; invariant r ⊆ c ∧ reflexive(c); invariant ∀p:pair. p ∈ c ⇔ p ∈ r ∨ p.1 = p.2 ∨ connected(p,r,k); decreases M+1-k; { for var i:int ≔ 0; i ≤ M; i ≔ i+1 do invariant k = old_k ∧ 0 ≤ i ∧ i ≤ M+1; invariant r ⊆ c ∧ reflexive(c); invariant ∀p:pair. p ∈ c ⇔ p ∈ r ∨ p.1 = p.2 ∨ connected(p,r,k) ∨ (p.1 < i ∧ connected(p,r,k+1)); decreases M+1-i; { for var j:int ≔ 0; j ≤ M; j ≔ j+1 do invariant k = old_k ∧ i = old_i ∧ 0 ≤ j ∧ j ≤ M+1; invariant r ⊆ c ∧ reflexive(c); invariant ∀p:pair. p ∈ c ⇔ p ∈ r ∨ p.1 = p.2 ∨ connected(p,r,k) ∨ (p.1 < i ∧ connected(p,r,k+1)) ∨ (p.1 = i ∧ p.2 < j ∧ connected(p,r,k+1)); decreases M+1-j; { if ⟨i,k⟩ ∈ c ∧ ⟨k,j⟩ ∈ c then c ≔ c ∪ {⟨i,j⟩}; } } } return c; } // ----------------------------------------------------------------- // graphs // ----------------------------------------------------------------- val D:ℕ; type dist = ℕ[D]; type graph = Map[pair,dist]; pred connected(p:pair,g:graph,s:seq,n:int) ⇔ s[0] = p.1 ∧ 1 ≤ n ∧ n ≤ M+1 ∧ s[n-1] = p.2 ∧ ∀k:int with 0 ≤ k ∧ k < n-1. g[⟨s[k],s[k+1]⟩] ≠ D; pred connected(p:pair,g:graph,s:seq,n:int,k:int) requires 0 ≤ k ∧ k ≤ M+1; ⇔ connected(p,g,s,n) ∧ ∀i:int with 1 ≤ i ∧ i < n-1. s[i] < k; fun dist(g:graph,s:seq,n:int): dist requires 1 ≤ n ∧ n ≤ M+1; = let d = ∑k:int with 0 ≤ k ∧ k < n-1. g[⟨s[k],s[k+1]⟩] in if d ≤ D then d else D; fun distance(g:graph,p:pair):dist = if ∃s:seq,n:int. connected(p,g,s,n) then min s:seq,n:int with connected(p,g,s,n). dist(g,s,n) else D; proc floydWarshall(g:graph):graph requires ∀e:elem. g[⟨e,e⟩] = 0; requires ∀e1:elem, e2:elem with e1 ≠ e2. g[⟨e1,e2⟩] > 0; ensures ∀p:pair. result[p]=distance(g,p); { var d:graph = g; for var k:int ≔ 0; k ≤ M; k ≔ k+1 do invariant 0 ≤ k ∧ k ≤ M+1; invariant ∀p:pair with d[p] < D. ∃s:seq,n:int with connected(p,g,s,n,k). d[p] = dist(g,s,n); invariant ∀p:pair. ∀s:seq,n:int with connected(p,g,s,n,k). d[p] ≤ dist(g,s,n); decreases M+1-k; { for var i:int ≔ 0; i ≤ M; i ≔ i+1 do invariant k = old_k ∧ 0 ≤ i ∧ i ≤ M+1; invariant ∀p:pair with d[p] < D. ∃s:seq,n:int with if p.1 < i then connected(p,g,s,n,k+1) else connected(p,g,s,n,k). d[p] = dist(g,s,n); invariant ∀p:pair. ∀s:seq,n:int with if p.1 < i then connected(p,g,s,n,k+1) else connected(p,g,s,n,k). d[p] ≤ dist(g,s,n); decreases M+1-i; { for var j:int ≔ 0; j ≤ M; j ≔ j+1 do invariant k = old_k ∧ i = old_i ∧ 0 ≤ j ∧ j ≤ M+1; invariant ∀p:pair with d[p] < D. ∃s:seq,n:int with if p.1 < i ∨ (p.1 = i ∧ p.2 < j) then connected(p,g,s,n,k+1) else connected(p,g,s,n,k). d[p] = dist(g,s,n); invariant ∀p:pair. ∀s:seq,n:int with if p.1 < i ∨ (p.1 = i ∧ p.2 < j) then connected(p,g,s,n,k+1) else connected(p,g,s,n,k). d[p] ≤ dist(g,s,n); decreases M+1-j; { val d1 = d[⟨i,k⟩]; val d2 = d[⟨k,j⟩]; if d1+d2 < d[⟨i,j⟩] then d[⟨i,j⟩] ≔ d1+d2; } } } return d; } pred connected(p:pair,g:graph,s:seq,n:int,q:set) ⇔ connected(p,g,s,n) ∧ ∀i:int with 0 ≤ i ∧ i < n-1. s[i] ∉ q; fun distance(g:graph,p:pair,q:set):dist = if ∃s:seq,n:int. connected(p,g,s,n,q) then min s:seq,n:int with connected(p,g,s,n,q). dist(g,s,n) else D; proc dijkstra(g:graph,x:elem,y:elem):dist requires ∀e:elem. g[⟨e,e⟩] = 0; requires ∀e1:elem, e2:elem with e1 ≠ e2. g[⟨e1,e2⟩] > 0; ensures result = distance(g,⟨x,y⟩); { var q:set = universe; var d:Map[elem,dist] = Map[elem,dist](D); d[x] ≔ 0; while y ∈ q do invariant ∀e1:elem with e1 ∉ q, e2 ∈ q. distance(g,⟨x,e1⟩) ≤ distance(g,⟨x,e2⟩); invariant ∀e:elem with e ∉ q. d[e] = distance(g,⟨x,e⟩); invariant ∀e:elem with e ∈ q. d[e] = distance(g,⟨x,e⟩,q); decreases |q|; { choose m ∈ q with ∀e∈q. d[m] ≤ d[e]; q ≔ q\{m}; for z ∈ q with g[⟨m,z⟩] ≠ D do invariant q = old_q; invariant ∀e:elem with e ∉ q. d[e] = distance(g,⟨x,e⟩); invariant ∀e:elem with e ∈ q\forSet. d[e] = distance(g,⟨x,e⟩,q∪{m}); invariant ∀e:elem with e ∈ forSet. d[e] = distance(g,⟨x,e⟩,q); { val dz = d[m]+g[⟨m,z⟩]; if dz < d[z] then d[z] ≔ dz; } } return d[y]; } // ----------------------------------------------------------------- // end of file // -----------------------------------------------------------------