-- Core field theory
-- 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.Algebra.Field.Core
import Defs
import Ring.Core

-- Division is multiplication by the inverse.  Packaging that familiar
-- operation as a function graph lets notation select it through the same
-- instance machinery as addition and multiplication.
def fieldDiv (A mul inv : Set) : Set :=
  { p ∈ ((A × A) × A) |
    ∃ x ∈ A, ∃ y ∈ A,
      p = ((x, y) ↦ call2(mul, x, inv(y))) }

theorem fieldDiv.relates (A mul inv x y : Set)
  requires mulFunction : mul : A × A → A
  requires invFunction : inv : A → A
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  shows relates(fieldDiv(A, mul, inv), (x, y),
    call2(mul, x, inv(y)))
proof
  have inverseInA : inv(y) ∈ A
    exact FunctionBetween.apply_closed with invFunction, yInA
  have inputInProduct := product.pair with xInA, inverseInA
  have quotientInA : call2(mul, x, inv(y)) ∈ A
    unfold call2
    exact FunctionBetween.apply_closed with mulFunction, inputInProduct
  unfold relates
  apply fieldDiv.membership.backward
  constructor
  . apply product.pair at (x, y), call2(mul, x, inv(y)), A × A, A
    . exact product.pair with xInA, yInA
    . exact quotientInA
  . refine ⟨x, xInA, y, yInA, rfl⟩

theorem fieldDiv.factors (A mul inv input output : Set)
  requires mapped : relates(fieldDiv(A, mul, inv), input, output)
  shows ∃ x ∈ A, ∃ y ∈ A,
    input = (x, y) ∧ output = call2(mul, x, inv(y))
proof
  unfold relates at mapped
  simp [fieldDiv.membership] at mapped
  rcases mapped with ⟨bounded, x, xInA, y, yInA, shape⟩
  obtain ⟨inputShape, outputShape⟩ := orderedPair.injective with shape
  refine ⟨x, xInA, y, yInA, inputShape, outputShape⟩

theorem fieldDiv.total (A mul inv : Set)
  requires mulFunction : mul : A × A → A
  requires invFunction : inv : A → A
  shows TotalBetween(fieldDiv(A, mul, inv), A × A, A)
proof
  intros input inputInProduct
  obtain ⟨bounded, x, xInA, y, yInA, inputShape⟩ := product.membership.forward with inputInProduct
  have inverseInA : inv(y) ∈ A
    exact FunctionBetween.apply_closed with invFunction, yInA
  have mulInput := product.pair with xInA, inverseInA
  have quotientInA : call2(mul, x, inv(y)) ∈ A
    unfold call2
    exact FunctionBetween.apply_closed with mulFunction, mulInput
  witness call2(mul, x, inv(y))
  constructor
  . exact quotientInA
  . rw inputShape
    exact fieldDiv.relates with mulFunction, invFunction, xInA, yInA

theorem fieldDiv.functional (A mul inv : Set)
  shows Functional(fieldDiv(A, mul, inv))
proof
  intros input first inputFirst second inputSecond
  obtain ⟨x, xInA, y, yInA, firstInput, firstOutput⟩ := fieldDiv.factors with inputFirst
  obtain ⟨u, uInA, v, vInA, secondInput, secondOutput⟩ := fieldDiv.factors with inputSecond
  rw firstInput at secondInput
  obtain ⟨sameLeft, sameRight⟩ := orderedPair.injective with secondInput
  rw [firstOutput, secondOutput, sameLeft, sameRight]
  rfl

theorem fieldDiv.function (A mul inv : Set)
  requires mulFunction : mul : A × A → A
  requires invFunction : inv : A → A
  shows fieldDiv(A, mul, inv) : A × A → A
proof
  constructor
    intros p hp
    simp [fieldDiv.membership] at hp
    rcases hp with ⟨bounded, witnesses⟩
    exact bounded
  . have functional := fieldDiv.functional at A, mul, inv
    refine ⟨functional, _⟩
    exact fieldDiv.total with mulFunction, invFunction

theorem DivisionSemiring.semiring (A add zero mul one inv : Set)
  requires h : DivisionSemiring(A, add, zero, mul, one, inv)
  shows IsSemiring(A, add, zero, mul, one)
proof
  simp [DivisionSemiring]

theorem Semifield.comm_semiring (A add zero mul one inv : Set)
  requires h : Semifield(A, add, zero, mul, one, inv)
  shows CommSemiring(A, add, zero, mul, one)
proof
  simp [Semifield]

theorem DivisionRing.ring (A add zero neg mul one inv : Set)
  requires h : DivisionRing(A, add, zero, neg, mul, one, inv)
  shows IsRing(A, add, zero, neg, mul, one)
proof
  simp [DivisionRing]

theorem DivisionRing.nontrivial (A add zero neg mul one inv : Set)
  requires h : DivisionRing(A, add, zero, neg, mul, one, inv)
  shows Nontrivial(A, zero, one)
proof
  simp [DivisionRing]

theorem DivisionRing.inverse (A add zero neg mul one inv : Set)
  requires h : DivisionRing(A, add, zero, neg, mul, one, inv)
  shows MultiplicativeInverse(A, mul, zero, one, inv)
proof
  simp [DivisionRing]

theorem IsFieldWithInverse.comm_ring (A add zero neg mul one inv : Set)
  requires h : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)
  shows IsCommRing(A, add, zero, neg, mul, one)
proof
  simp [IsFieldWithInverse]

theorem IsFieldWithInverse.nontrivial (A add zero neg mul one inv : Set)
  requires h : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)
  shows Nontrivial(A, zero, one)
proof
  simp [IsFieldWithInverse]

theorem IsFieldWithInverse.inverse (A add zero neg mul one inv : Set)
  requires h : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)
  shows MultiplicativeInverse(A, mul, zero, one, inv)
proof
  simp [IsFieldWithInverse]

theorem IsFieldWithInverse.one_in_carrier (A add zero neg mul one inv : Set)
  requires field : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)
  shows one ∈ A
proof
  have commRing := IsFieldWithInverse.comm_ring with field
  have ring := IsCommRing.ring with commRing
  have monoid := IsRing.multiplicative with ring
  exact IsMonoid.unit_in_carrier with monoid

theorem IsFieldWithInverse.inverse_closed (A add zero neg mul one inv x : Set)
  requires field : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)
  requires xInA : x ∈ A
  shows inv(x) ∈ A
proof
  obtain ⟨function, laws⟩ := IsFieldWithInverse.inverse with field
  exact FunctionBetween.apply_closed with function, xInA

theorem IsFieldWithInverse.inverse_left (A add zero neg mul one inv x : Set)
  requires field : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)
  requires xInA : x ∈ A
  requires nonzero : x ≠ zero
  shows call2(mul, inv(x), x) = one
proof
  obtain ⟨function, laws⟩ := IsFieldWithInverse.inverse with field
  obtain ⟨left, right⟩ := laws with x, xInA, nonzero
  exact left

theorem IsFieldWithInverse.inverse_right (A add zero neg mul one inv x : Set)
  requires field : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)
  requires xInA : x ∈ A
  requires nonzero : x ≠ zero
  shows call2(mul, x, inv(x)) = one
proof
  obtain ⟨function, laws⟩ := IsFieldWithInverse.inverse with field
  obtain ⟨left, right⟩ := laws with x, xInA, nonzero
  exact right

theorem IsFieldWithInverse.division_ring (A add zero neg mul one inv : Set)
  requires h : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)
  shows DivisionRing(A, add, zero, neg, mul, one, inv)
proof
  rcases h with ⟨commRing, division⟩
  rcases commRing with ⟨ring, commutative⟩
  refine ⟨ring, division⟩

theorem IsFieldWithInverse.integral_domain (A add zero neg mul one inv : Set)
  requires h : IsFieldWithInverse(A, add, zero, neg, mul, one, inv)
  requires noZero : NoZeroDivisors(A, mul, zero)
  shows IsIntegralDomain(A, add, zero, neg, mul, one)
proof
  rcases h with ⟨commRing, nontrivial, inverse⟩
  refine ⟨commRing, nontrivial, noZero⟩