Grace/Cumulus/Set/Tuple.g17

Open in Workbench Download source

Imports

Core · Relation

Declarations

• fstCandidates def
• sndCandidates def
• fst def
• snd def
• orderedPair.first_in_union theorem derivation
• orderedPair.second_in_union theorem derivation
• fstCandidates.pair theorem derivation
• sndCandidates.pair theorem derivation
• fst.pair theorem derivation
• snd.pair theorem derivation

Source

1-- The coordinates of an ordered pair, read back from the pair2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Set.Tuple8import Core9import Relation1011-- A structure bundled as a nested pair is read back through fst and snd:12-- fst((x, y)) = x and snd((x, y)) = y.13def fstCandidates (p : Set) : Set := { x ∈ ⋃ p | ∃ y, p = (x, y) }14def sndCandidates (p : Set) : Set := { y ∈ ⋃ p | ∃ x, p = (x, y) }15def fst (p : Set) : Set := ⋃ fstCandidates(p)16def snd (p : Set) : Set := ⋃ sndCandidates(p)1718theorem orderedPair.first_in_union (x y : Set)19  shows x ∈ ⋃ (x, y)20proof21  have inSingleton : x ∈ {x} := singleton.self at x22  have singletonIn : {x} ∈ (x, y) by simp [orderedPair, singleton, pair.membership]23  exact union.contains with singletonIn, inSingleton2425theorem orderedPair.second_in_union (x y : Set)26  shows y ∈ ⋃ (x, y)27proof28  have inPair : y ∈ {x, y} := pair.right at x, y29  have pairIn : {x, y} ∈ (x, y) by simp [orderedPair, singleton, pair.membership]30  exact union.contains with pairIn, inPair3132theorem fstCandidates.pair (x y : Set)33  shows fstCandidates((x, y)) = {x}34proof35  ext z36  constructor37  . intro member38    obtain ⟨bounded, w, shape⟩ := fstCandidates.membership.forward with member39    have same : x = z := orderedPair.first with shape40    rw ← same41    exact singleton.self at x42  . intro member43    have same : z = x := singleton.membership.forward with member44    have inUnion : x ∈ ⋃ (x, y) := orderedPair.first_in_union at x, y45    rw same46    apply fstCandidates.membership.backward47    refine ⟨inUnion, y, rfl⟩4849theorem sndCandidates.pair (x y : Set)50  shows sndCandidates((x, y)) = {y}51proof52  ext z53  constructor54  . intro member55    obtain ⟨bounded, w, shape⟩ := sndCandidates.membership.forward with member56    obtain ⟨sameFirst, same⟩ := orderedPair.injective with shape57    rw ← same58    exact singleton.self at y59  . intro member60    have same : z = y := singleton.membership.forward with member61    have inUnion : y ∈ ⋃ (x, y) := orderedPair.second_in_union at x, y62    rw same63    apply sndCandidates.membership.backward64    refine ⟨inUnion, x, rfl⟩6566theorem fst.pair (x y : Set)67  shows fst((x, y)) = x68proof69  simp [fst, fstCandidates.pair, union.singleton]7071theorem snd.pair (x y : Set)72  shows snd((x, y)) = y73proof74  simp [snd, sndCandidates.pair, union.singleton]75