Grace/Cumulus/Relation/Algebra.g17

Open in Workbench Download source

Imports

Set.Function.Image

Declarations

• domain.contains theorem derivation
• domain.membership_iff theorem derivation
• range.membership_iff theorem derivation
• domain.subset theorem derivation
• range.subset theorem derivation
• domain.monotone theorem derivation
• range.monotone theorem derivation
• domain.empty theorem derivation
• domain.union2 theorem derivation
• range.union2 theorem derivation
• RelationBetween.domain_range theorem derivation
• FunctionBetween.domain theorem derivation
• FunctionBetween.range theorem derivation
• restrict.subset theorem derivation
• restrict.relation theorem derivation
• restrict.whole theorem derivation
• restrict.empty theorem derivation
• restrict.intersection theorem derivation
• restrict.monotone theorem derivation
• restrict.union2 theorem derivation
• restrict.domain theorem derivation
• converse.converse theorem derivation
• converse.monotone theorem derivation
• converse.domain theorem derivation
• converse.range theorem derivation
• compose.associative theorem derivation
• compose.restrict theorem derivation

Source

1-- The algebra of relations: domains and ranges, restrictions, converses,2-- and composition3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Relation.Algebra9import Set.Function.Image1011-- Domains and ranges1213theorem domain.contains (x y r : Set)14  requires h : relates(r, x, y)15  shows x ∈ domain(r)16proof17  have member : (x, y) ∈ r := h18  apply domain.membership.backward19  constructor20  . unfold coordinateBound21    apply set.union.backward22    witness {x, y}23    constructor24    . apply set.union.backward25      witness (x, y)26      constructor27      . exact member28      . simp [orderedPair, pair.membership]29    . simp [pair.membership]30  . witness y31    exact member3233theorem domain.membership_iff (x r : Set)34  shows x ∈ domain(r) ↔ ∃ y, relates(r, x, y)35proof36  constructor37  . intro h38    simp [domain.membership] at h39    obtain ⟨y, hy⟩ := h.right40    witness y41    exact hy42  . intro h43    obtain ⟨y, hy⟩ := h44    exact domain.contains with hy4546theorem range.membership_iff (y r : Set)47  shows y ∈ range(r) ↔ ∃ x, relates(r, x, y)48proof49  constructor50  . intro h51    simp [range.membership] at h52    obtain ⟨x, hx⟩ := h.right53    witness x54    exact hx55  . intro h56    obtain ⟨x, hx⟩ := h57    exact range.contains at x, y, r with hx5859theorem domain.subset (r A B : Set)60  requires relation : RelationBetween(r, A, B)61  shows domain(r) ⊆ A62proof63  intros x hx64  obtain ⟨y, hy⟩ := domain.membership_iff.forward with hx65  have bounds := RelationBetween.bounds with relation, hy66  exact bounds.left6768theorem range.subset (r A B : Set)69  requires relation : RelationBetween(r, A, B)70  shows range(r) ⊆ B71proof72  intros y hy73  obtain ⟨x, hx⟩ := range.membership_iff.forward with hy74  have bounds := RelationBetween.bounds with relation, hx75  exact bounds.right7677theorem domain.monotone (r s : Set)78  requires h : r ⊆ s79  shows domain(r) ⊆ domain(s)80proof81  intros x hx82  obtain ⟨y, hy⟩ := domain.membership_iff.forward with hx83  have inS : (x, y) ∈ s := h with (x, y), hy84  exact domain.contains at x, y, s with inS8586theorem range.monotone (r s : Set)87  requires h : r ⊆ s88  shows range(r) ⊆ range(s)89proof90  intros y hy91  obtain ⟨x, hx⟩ := range.membership_iff.forward with hy92  have inS : (x, y) ∈ s := h with (x, y), hx93  exact range.contains with inS9495theorem domain.empty96  shows domain(∅) = ∅97proof98  apply Subset.empty_iff.forward99  intros x hx100  obtain ⟨y, hy⟩ := domain.membership_iff.forward with hx101  have member : (x, y) ∈ ∅ := hy102  exfalso103  exact set.empty with member104105theorem domain.union2 (r s : Set)106  shows domain(r ∪ s) = domain(r) ∪ domain(s)107proof108  ext x109  constructor110  . intro hx111    obtain ⟨y, hy⟩ := domain.membership_iff.forward with hx112    have member : (x, y) ∈ r ∪ s := hy113    simp [union2.membership] at member114    simp [union2.membership]115    cases member with hr | hs116    . left117      exact domain.contains at x, y, r with hr118    . right119      exact domain.contains at x, y, s with hs120  . intro hx121    simp [union2.membership] at hx122    have leftSubset := union2.subset_left at r, s123    have rightSubset := union2.subset_right at r, s124    cases hx with hr | hs125    . exact domain.monotone with leftSubset, x, hr126    . exact domain.monotone with rightSubset, x, hs127128theorem range.union2 (r s : Set)129  shows range(r ∪ s) = range(r) ∪ range(s)130proof131  ext y132  constructor133  . intro hy134    obtain ⟨x, hx⟩ := range.membership_iff.forward with hy135    have member : (x, y) ∈ r ∪ s := hx136    simp [union2.membership] at member137    simp [union2.membership]138    cases member with hr | hs139    . left140      exact range.contains with hr141    . right142      exact range.contains with hs143  . intro hy144    simp [union2.membership] at hy145    have leftSubset := union2.subset_left at r, s146    have rightSubset := union2.subset_right at r, s147    cases hy with hr | hs148    . exact range.monotone with leftSubset, y, hr149    . exact range.monotone with rightSubset, y, hs150151theorem RelationBetween.domain_range (r A B : Set)152  requires relation : RelationBetween(r, A, B)153  shows r ⊆ domain(r) × range(r)154proof155  have included : r ⊆ A × B := relation156  intros p hp157  have shape : p ∈ A × B := included with p, hp158  simp [product.membership] at shape159  obtain ⟨bound, x, hx, y, hy, equation⟩ := shape160  rw equation at hp161  rw equation162  have inDomain := domain.contains at x, y, r with hp163  have inRange := range.contains with hp164  exact product.pair with inDomain, inRange165166theorem FunctionBetween.domain (f A B : Set)167  requires function : f : A → B168  shows domain(f) = A169proof170  apply Subset.antisymmetric171  . exact domain.subset with function.left172  . intros x hx173    have related := FunctionBetween.relates_apply with function, hx174    exact domain.contains with related175176theorem FunctionBetween.range (f A B : Set)177  requires function : f : A → B178  shows range(f) = functionImage(f, A, B)179proof180  ext y181  constructor182  . intro hy183    obtain ⟨x, hx⟩ := range.membership_iff.forward with hy184    have bounds := RelationBetween.bounds with function.left, hx185    have value := FunctionBetween.apply_value with function, bounds.left, hx186    simp [functionImage.membership]187    constructor188    . exact bounds.right189    . witness x190      constructor191      . exact bounds.left192      . symm193        exact value194  . intro hy195    simp [functionImage.membership] at hy196    obtain ⟨inB, x, hx, shape⟩ := hy197    have related := FunctionBetween.relates_apply with function, hx198    rw shape199    exact range.contains at x, f(x), f with related200201-- Restrictions202203theorem restrict.subset (r A : Set)204  shows restrict(r, A) ⊆ r205proof206  intros p hp207  simp [restrict.membership] at hp208  exact hp.left209210theorem restrict.relation (r A B S : Set)211  requires relation : RelationBetween(r, A, B)212  shows RelationBetween(restrict(r, S), S ∩ A, B)213proof214  intros p hp215  simp [restrict.membership] at hp216  obtain ⟨hr, x, hx, y, equation⟩ := hp217  rw equation at hr218  rw equation219  have bounds := RelationBetween.bounds at r, A, B, x, y with relation, hr220  apply product.pair221  . simp [intersection.membership]222  . exact bounds.right223224theorem restrict.whole (r A B : Set)225  requires relation : RelationBetween(r, A, B)226  shows restrict(r, A) = r227proof228  have included : r ⊆ A × B := relation229  apply Subset.antisymmetric230  . exact restrict.subset at r, A231  . intros p hp232    have shape : p ∈ A × B := included with p, hp233    simp [product.membership] at shape234    obtain ⟨bound, x, hx, y, hy, equation⟩ := shape235    simp [restrict.membership]236    constructor237    . exact hp238    . witness x239      constructor240      . exact hx241      . witness y242        exact equation243244theorem restrict.empty (r : Set)245  shows restrict(r, ∅) = ∅246proof247  apply Subset.empty_iff.forward248  intros p hp249  simp [restrict.membership] at hp250251theorem restrict.intersection (r S T : Set)252  shows restrict(restrict(r, S), T) = restrict(r, S ∩ T)253proof254  ext p255  constructor256  . intro hp257    simp [restrict.membership] at hp258    obtain ⟨inner, x, hxT, y, equation⟩ := hp259    simp [restrict.membership] at inner260    obtain ⟨hr, z, hzS, w, equationZ⟩ := inner261    rw equation at equationZ262    have coordinates := orderedPair.injective with equationZ263    simp [restrict.membership]264    constructor265    . exact hr266    . witness x267      constructor268      . simp [intersection.membership]269      . witness y270        exact equation271  . intro hp272    simp [restrict.membership] at hp273    obtain ⟨hr, x, hx, y, equation⟩ := hp274    simp [intersection.membership] at hx275    simp [restrict.membership]276    constructor277    . constructor278      . exact hr279      . exact ⟨x, hx.left, y, equation⟩280    . exact ⟨x, hx.right, y, equation⟩281282theorem restrict.monotone (r S T : Set)283  requires h : S ⊆ T284  shows restrict(r, S) ⊆ restrict(r, T)285proof286  intros p hp287  simp [restrict.membership] at hp288  obtain ⟨hr, x, hx, y, equation⟩ := hp289  simp [restrict.membership]290  constructor291  . exact hr292  . exact ⟨x, (h with x, hx), y, equation⟩293294theorem restrict.union2 (r S T : Set)295  shows restrict(r, S ∪ T) = restrict(r, S) ∪ restrict(r, T)296proof297  ext p298  constructor299  . intro hp300    simp [restrict.membership] at hp301    obtain ⟨hr, x, hx, y, equation⟩ := hp302    simp [union2.membership] at hx303    simp [union2.membership]304    cases hx with hS | hT305    . left306      simp [restrict.membership]307      exact ⟨hr, x, hS, y, equation⟩308    . right309      simp [restrict.membership]310      exact ⟨hr, x, hT, y, equation⟩311  . intro hp312    simp [union2.membership] at hp313    have leftSubset := union2.subset_left at S, T314    have rightSubset := union2.subset_right at S, T315    cases hp with hS | hT316    . exact restrict.monotone at r, S, S ∪ T with leftSubset, p, hS317    . exact restrict.monotone at r, T, S ∪ T with rightSubset, p, hT318319theorem restrict.domain (r S : Set)320  shows domain(restrict(r, S)) = domain(r) ∩ S321proof322  ext x323  constructor324  . intro hx325    obtain ⟨y, hy⟩ := domain.membership_iff.forward with hx326    have related := restrict.relates.forward with hy327    simp [intersection.membership]328    constructor329    . exact domain.contains with related.right330    . exact related.left331  . intro hx332    simp [intersection.membership] at hx333    obtain ⟨y, hy⟩ := domain.membership_iff.forward with hx.left334    have related := restrict.relates.backward at r, S, x, y with ⟨hx.right, hy⟩335    exact domain.contains with related336337-- Converses338339theorem converse.converse (r A B : Set)340  requires relation : RelationBetween(r, A, B)341  shows converse(converse(r, A, B), B, A) = r342proof343  ext p344  constructor345  . intro hp346    simp [converse.membership] at hp347    obtain ⟨bound, y, hy, x, hx, equation, related⟩ := hp348    have member : (y, x) ∈ converse(r, A, B) := related349    simp [converse.membership] at member350    obtain ⟨boundInner, x2, hx2, y2, hy2, equationInner, relatedInner⟩ := member351    have coordinates := orderedPair.injective with equationInner352    rw equation353    rwa [← coordinates.left, ← coordinates.right] at relatedInner354  . intro hp355    have included : r ⊆ A × B := relation356    have shape : p ∈ A × B := included with p, hp357    simp [product.membership] at shape358    obtain ⟨bound, x, hx, y, hy, equation⟩ := shape359    rw equation at hp360    rw equation361    have once := converse.relates at r, A, B, x, y with hx, hy, hp362    exact converse.relates with hy, hx, once363364theorem converse.monotone (r s A B : Set)365  requires h : r ⊆ s366  shows converse(r, A, B) ⊆ converse(s, A, B)367proof368  intros p hp369  simp [converse.membership] at hp370  obtain ⟨bound, x, hx, y, hy, equation, related⟩ := hp371  rw equation372  have inS : (x, y) ∈ s := h with (x, y), related373  exact converse.relates at s, A, B, x, y with hx, hy, inS374375theorem converse.domain (r A B : Set)376  requires relation : RelationBetween(r, A, B)377  shows domain(converse(r, A, B)) = range(r)378proof379  ext y380  constructor381  . intro hy382    obtain ⟨x, hx⟩ := domain.membership_iff.forward with hy383    have member : (y, x) ∈ converse(r, A, B) := hx384    simp [converse.membership] at member385    obtain ⟨bound, x2, hx2, y2, hy2, equation, related⟩ := member386    have coordinates := orderedPair.injective with equation387    rw [coordinates.left]388    exact range.contains at x2, y2, r with related389  . intro hy390    obtain ⟨x, hx⟩ := range.membership_iff.forward with hy391    have bounds := RelationBetween.bounds with relation, hx392    have flipped := converse.relates with bounds.left, bounds.right, hx393    exact domain.contains with flipped394395theorem converse.range (r A B : Set)396  requires relation : RelationBetween(r, A, B)397  shows range(converse(r, A, B)) = domain(r)398proof399  ext x400  constructor401  . intro hx402    obtain ⟨y, hy⟩ := range.membership_iff.forward with hx403    have member : (y, x) ∈ converse(r, A, B) := hy404    simp [converse.membership] at member405    obtain ⟨bound, x2, hx2, y2, hy2, equation, related⟩ := member406    have coordinates := orderedPair.injective with equation407    rw [coordinates.right]408    exact domain.contains with related409  . intro hx410    obtain ⟨y, hy⟩ := domain.membership_iff.forward with hx411    have bounds := RelationBetween.bounds with relation, hy412    have flipped := converse.relates with bounds.left, bounds.right, hy413    exact range.contains at y, x, converse(r, A, B) with flipped414415-- Composition416417theorem compose.associative (h g f A B C D : Set)418  requires fFunction : f : A → B419  requires gFunction : g : B → C420  requires hFunction : h : C → D421  shows compose(h, compose(g, f, A, B, C), A, C, D) = compose(compose(h, g, B, C, D), f, A, B, D)422proof423  have inner := compose.function with fFunction, gFunction424  have outer := compose.function with gFunction, hFunction425  apply FunctionBetween.ext with (compose.function with inner, hFunction), (compose.function with fFunction, outer)426  intros x hx427  have valueB := FunctionBetween.apply_closed with fFunction, hx428  have leftStep := compose.apply with inner, hFunction, hx429  have innerStep := compose.apply with fFunction, gFunction, hx430  have rightStep := compose.apply with fFunction, outer, hx431  have outerStep := compose.apply with gFunction, hFunction, valueB432  rw [leftStep, innerStep, rightStep, outerStep]433  rfl434435theorem compose.restrict (g f A B C S : Set)436  requires fFunction : f : A → B437  requires gFunction : g : B → C438  requires hS : S ⊆ A439  shows restrict(compose(g, f, A, B, C), S) = compose(g, restrict(f, S), S, B, C)440proof441  have composed := compose.function with fFunction, gFunction442  have closed : ∀ x ∈ S, f(x) ∈ B443    intros x hx444    exact FunctionBetween.apply_closed with fFunction, (hS with x, hx)445  have restricted := restrict.function with fFunction, hS, closed446  have closedComposed : ∀ x ∈ S, compose(g, f, A, B, C)(x) ∈ C447    intros x hx448    exact FunctionBetween.apply_closed with composed, (hS with x, hx)449  have restrictedComposed := restrict.function with composed, hS, closedComposed450  have composedRestricted := compose.function with restricted, gFunction451  apply FunctionBetween.ext with restrictedComposed, composedRestricted452  intros x hx453  have hxA : x ∈ A := hS with x, hx454  have leftStep := restrict.apply with composed, hS, closedComposed, hx455  have innerStep := compose.apply with fFunction, gFunction, hxA456  have rightStep := compose.apply with restricted, gFunction, hx457  have restrictedStep := restrict.apply with fFunction, hS, closed, hx458  rw [leftStep, innerStep, rightStep, restrictedStep]459  rfl460