-- Transport of well-orders along injections, without Choice.
-- 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

-- Copyright (c) 2026 Grant Passmore. Apache License 2.0.
module Grace.Cumulus.Set.OrderTransport
import Order

def transportedOrder (f A B r : Set) : Set :=
  {p ∈ B × B | ∃ x ∈ A, ∃ y ∈ A, relates(r, x, y) ∧ p = (f[x], f[y])}

theorem transportedOrder.decode (f A B r u v : Set)
  requires related : relates(transportedOrder(f, A, B, r), u, v)
  shows ∃ x ∈ A, ∃ y ∈ A, relates(r, x, y) ∧ u = f[x] ∧ v = f[y]
proof
  unfold relates at related
  obtain ⟨bounded, x, hx, y, hy, edge, shape⟩ := transportedOrder.membership.forward with related
  obtain ⟨left, right⟩ := orderedPair.injective with shape
  refine ⟨x, hx, y, hy, edge, left, right⟩

theorem transportedOrder.edge (f A B r x y : Set)
  requires function : f : A → B
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires related : relates(r, x, y)
  shows relates(transportedOrder(f, A, B, r), f[x], f[y])
proof
  have left := FunctionBetween.apply_closed at f, A, B, x with *
  have right := FunctionBetween.apply_closed at f, A, B, y with *
  have pair := product.pair with left, right
  unfold relates
  exact transportedOrder.membership.backward with ⟨pair, x, hx, y, hy, related, rfl⟩

theorem transportedOrder.reflect (f A B r x y : Set)
  requires injective : InjectiveBetween(f, A, B)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires related : relates(transportedOrder(f, A, B, r), f[x], f[y])
  shows relates(r, x, y)
proof
  obtain ⟨a, ha, b, hb, edge, left, right⟩ := transportedOrder.decode with related
  have sameA := Injective.apply_cancel with injective, hx, ha, left
  have sameB := Injective.apply_cancel with injective, hy, hb, right
  rw sameA
  rwa sameB

theorem transportedOrder.relation (f A B r : Set)
  requires function : f : A → B
  shows RelationBetween(transportedOrder(f, A, B, r), functionImage(f, A, B), functionImage(f, A, B))
proof
  intros p member
  obtain ⟨bounded, x, hx, y, hy, edge, shape⟩ := transportedOrder.membership.forward with member
  have left := functionImage.value with hx
  have right := functionImage.value with hy
  rw shape
  exact product.pair with left, right

theorem transportedOrder.strict_linear (f A B r : Set)
  requires injective : InjectiveBetween(f, A, B)
  requires order : StrictLinearOrder(A, r)
  shows StrictLinearOrder(functionImage(f, A, B), transportedOrder(f, A, B, r))
proof
  have function := Injective.function with injective
  have irreflexive := StrictLinearOrder.irreflexive with order
  have transitive := StrictLinearOrder.transitive with order
  have connected := StrictLinearOrder.connected with order
  constructor
    constructor
    . exact transportedOrder.relation at f, A, B, r with function
    . constructor
        intros u hu self
        obtain ⟨bound, x, hx, value⟩ := functionImage.membership.forward with hu
        rw value at self
        have original := transportedOrder.reflect at f, A, B, r, x, x with *
        exact irreflexive with x, hx, original
        intros u hu v hv w hw uv vw
        obtain ⟨bu, a, ha, uValue⟩ := functionImage.membership.forward with hu
        obtain ⟨bv, b, hb, vValue⟩ := functionImage.membership.forward with hv
        obtain ⟨bw, c, hc, wValue⟩ := functionImage.membership.forward with hw
        rw [uValue, vValue] at uv
        rw [vValue, wValue] at vw
        have ab := transportedOrder.reflect at f, A, B, r, a, b with *
        have bc := transportedOrder.reflect at f, A, B, r, b, c with *
        have ac := transitive with a, ha, b, hb, c, hc, ab, bc
        rw [uValue, wValue]
        exact transportedOrder.edge at f, A, B, r, a, c with *
    intros u hu v hv distinct
    obtain ⟨bu2, a2, ha2, uValue2⟩ := functionImage.membership.forward with hu
    obtain ⟨bv2, b2, hb2, vValue2⟩ := functionImage.membership.forward with hv
    have different : a2 ≠ b2 by simp
    have alternatives := connected with a2, ha2, b2, hb2, different
    rw [uValue2, vValue2]
    cases alternatives with ab2 | ba2
    . left
      exact transportedOrder.edge at f, A, B, r, a2, b2 with *
    . right
      exact transportedOrder.edge at f, A, B, r, b2, a2 with *

theorem transportedOrder.well_founded (f A B r : Set)
  requires injective : InjectiveBetween(f, A, B)
  requires founded : wellFoundedOn(r, A)
  shows wellFoundedOn(transportedOrder(f, A, B, r), functionImage(f, A, B))
proof
  intros S conditions
  rcases conditions with ⟨subsetS, nonemptyS⟩
  obtain ⟨u, hu⟩ := Nonempty.of_ne_empty with nonemptyS
  have inImage := subsetS with u, hu
  obtain ⟨bounded, x, hx, value⟩ := functionImage.membership.forward with inImage
  rw value at hu
  have preimageNonempty : Nonempty(functionPreimage(f, A, S)) := ⟨x, (functionPreimage.membership.backward with ⟨hx, hu⟩)⟩
  have preimageNe := Nonempty.ne_empty with preimageNonempty
  have preimageSubset : subset(functionPreimage(f, A, S), A) by simp [functionPreimage, subset]
  obtain ⟨m, hm, minimal⟩ := founded with functionPreimage(f, A, S), ⟨preimageSubset, preimageNe⟩
  obtain ⟨mInA, imageInS⟩ := functionPreimage.membership.forward with hm
  refine ⟨f[m], imageInS, ?_⟩
  intros v hv edge
  have vInImage := subsetS with v, hv
  obtain ⟨vBound, y, hy, vValue⟩ := functionImage.membership.forward with vInImage
  rw vValue at hv
  rw vValue at edge
  have yPreimage : y ∈ functionPreimage(f, A, S) := functionPreimage.membership.backward with ⟨hy, hv⟩
  have original := transportedOrder.reflect with *
  exact minimal with y, yPreimage, original

theorem transportedOrder.well_order (f A B r : Set)
  requires injective : InjectiveBetween(f, A, B)
  requires order : WellOrder(A, r)
  shows WellOrder(functionImage(f, A, B), transportedOrder(f, A, B, r))
proof
  have strict := WellOrder.strict_linear with order
  have founded := WellOrder.well_founded with order
  constructor
  . exact transportedOrder.strict_linear with *
  . exact transportedOrder.well_founded with *