-- Functions on three points: the function on 3 with three given values in
-- a set, as a graph, with its values read off.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Set.Function.Triples
import Function
import Tuple

-- The function on 3 with the values a, b, c in S.
def tripleMap (S a b c : Set) : Set :=
  { p ∈ 3 × S | (fst(p) = 0 ∧ snd(p) = a) ∨
    (fst(p) = 1 ∧ snd(p) = b) ∨ (fst(p) = 2 ∧ snd(p) = c) }

theorem tripleMap.function (S a b c : Set)
  requires first : a ∈ S
  requires second : b ∈ S
  requires third : c ∈ S
  shows tripleMap(S, a, b, c) : 3 → S
proof
  constructor
  . intros p member
    exact member.left
  constructor
  . intros x y relatedY z relatedZ
    obtain ⟨inY, shapeY⟩ := relatedY
    obtain ⟨_, shapeZ⟩ := relatedZ
    obtain ⟨_, i, hi, _, _, pairY⟩ := product.membership.forward with inY
    obtain ⟨xi, rfl⟩ := orderedPair.injective with pairY
    rw xi at shapeY, shapeZ
    have cases := membership.three.forward with hi
    have apart01 : 0 ≠ 1 by simp
    have apart02 : 0 ≠ 2 by simp
    have apart12 : 1 ≠ 2 by simp
    have apart10 : 1 ≠ 0 by simp
    have apart20 : 2 ≠ 0 by simp
    have apart21 : 2 ≠ 1 by simp
    rcases cases with rfl | rfl | rfl
    . simp [fst.pair, snd.pair, apart01, apart02] at shapeY, shapeZ
      cc
    . simp [fst.pair, snd.pair, apart10, apart12] at shapeY, shapeZ
      cc
    . simp [fst.pair, snd.pair, apart20, apart21] at shapeY, shapeZ
      cc
  . intros x input
    have cases := membership.three.forward with input
    rcases cases with rfl | rfl | rfl
    . refine ⟨a, first, _⟩
      apply tripleMap.membership.backward
      refine ⟨(product.pair with input, first), _⟩
      simp [fst.pair, snd.pair]
    . refine ⟨b, second, _⟩
      apply tripleMap.membership.backward
      refine ⟨(product.pair with input, second), _⟩
      simp [fst.pair, snd.pair]
    . refine ⟨c, third, _⟩
      apply tripleMap.membership.backward
      refine ⟨(product.pair with input, third), _⟩
      simp [fst.pair, snd.pair]

theorem tripleMap.value (S a b c : Set)
  requires first : a ∈ S
  requires second : b ∈ S
  requires third : c ∈ S
  shows tripleMap(S, a, b, c)(0) = a ∧ tripleMap(S, a, b, c)(1) = b ∧
    tripleMap(S, a, b, c)(2) = c
proof
  have function := tripleMap.function with first, second, third
  have zero : 0 ∈ 3 by simp [membership.three]
  have one : 1 ∈ 3 by simp [membership.three]
  have two : 2 ∈ 3 by simp [membership.three]
  have atZero : relates(tripleMap(S, a, b, c), 0, a)
    apply tripleMap.membership.backward
    refine ⟨(product.pair with zero, first), _⟩
    simp [fst.pair, snd.pair]
  have atOne : relates(tripleMap(S, a, b, c), 1, b)
    apply tripleMap.membership.backward
    refine ⟨(product.pair with one, second), _⟩
    simp [fst.pair, snd.pair]
  have atTwo : relates(tripleMap(S, a, b, c), 2, c)
    apply tripleMap.membership.backward
    refine ⟨(product.pair with two, third), _⟩
    simp [fst.pair, snd.pair]
  exact ⟨(FunctionBetween.apply_value with function, zero, atZero),
    (FunctionBetween.apply_value with function, one, atOne),
    (FunctionBetween.apply_value with function, two, atTwo)⟩