Grace/Cumulus/Set/Function/Triples.g17

Open in Workbench Download source

Imports

Function · Tuple

Declarations

• tripleMap def
• tripleMap.function theorem derivation
• tripleMap.value theorem derivation

Source

1-- Functions on three points: the function on 3 with three given values in2-- a set, as a graph, with its values read off.3-- 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.Set.Function.Triples9import Function10import Tuple1112-- The function on 3 with the values a, b, c in S.13def tripleMap (S a b c : Set) : Set :=14  { p ∈ 3 × S | (fst(p) = 0 ∧ snd(p) = a) ∨15    (fst(p) = 1 ∧ snd(p) = b) ∨ (fst(p) = 2 ∧ snd(p) = c) }1617theorem tripleMap.function (S a b c : Set)18  requires first : a ∈ S19  requires second : b ∈ S20  requires third : c ∈ S21  shows tripleMap(S, a, b, c) : 3 → S22proof23  constructor24  . intros p member25    exact member.left26  constructor27  . intros x y relatedY z relatedZ28    obtain ⟨inY, shapeY⟩ := relatedY29    obtain ⟨_, shapeZ⟩ := relatedZ30    obtain ⟨_, i, hi, _, _, pairY⟩ := product.membership.forward with inY31    obtain ⟨xi, rfl⟩ := orderedPair.injective with pairY32    rw xi at shapeY, shapeZ33    have cases := membership.three.forward with hi34    have apart01 : 0 ≠ 1 by simp35    have apart02 : 0 ≠ 2 by simp36    have apart12 : 1 ≠ 2 by simp37    have apart10 : 1 ≠ 0 by simp38    have apart20 : 2 ≠ 0 by simp39    have apart21 : 2 ≠ 1 by simp40    rcases cases with rfl | rfl | rfl41    . simp [fst.pair, snd.pair, apart01, apart02] at shapeY, shapeZ42      cc43    . simp [fst.pair, snd.pair, apart10, apart12] at shapeY, shapeZ44      cc45    . simp [fst.pair, snd.pair, apart20, apart21] at shapeY, shapeZ46      cc47  . intros x input48    have cases := membership.three.forward with input49    rcases cases with rfl | rfl | rfl50    . refine ⟨a, first, _⟩51      apply tripleMap.membership.backward52      refine ⟨(product.pair with input, first), _⟩53      simp [fst.pair, snd.pair]54    . refine ⟨b, second, _⟩55      apply tripleMap.membership.backward56      refine ⟨(product.pair with input, second), _⟩57      simp [fst.pair, snd.pair]58    . refine ⟨c, third, _⟩59      apply tripleMap.membership.backward60      refine ⟨(product.pair with input, third), _⟩61      simp [fst.pair, snd.pair]6263theorem tripleMap.value (S a b c : Set)64  requires first : a ∈ S65  requires second : b ∈ S66  requires third : c ∈ S67  shows tripleMap(S, a, b, c)(0) = a ∧ tripleMap(S, a, b, c)(1) = b ∧68    tripleMap(S, a, b, c)(2) = c69proof70  have function := tripleMap.function with first, second, third71  have zero : 0 ∈ 3 by simp [membership.three]72  have one : 1 ∈ 3 by simp [membership.three]73  have two : 2 ∈ 3 by simp [membership.three]74  have atZero : relates(tripleMap(S, a, b, c), 0, a)75    apply tripleMap.membership.backward76    refine ⟨(product.pair with zero, first), _⟩77    simp [fst.pair, snd.pair]78  have atOne : relates(tripleMap(S, a, b, c), 1, b)79    apply tripleMap.membership.backward80    refine ⟨(product.pair with one, second), _⟩81    simp [fst.pair, snd.pair]82  have atTwo : relates(tripleMap(S, a, b, c), 2, c)83    apply tripleMap.membership.backward84    refine ⟨(product.pair with two, third), _⟩85    simp [fst.pair, snd.pair]86  exact ⟨(FunctionBetween.apply_value with function, zero, atZero),87    (FunctionBetween.apply_value with function, one, atOne),88    (FunctionBetween.apply_value with function, two, atTwo)⟩89