-- Restrict operation graphs to closed subcarriers.
-- 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.Restriction
import Ring.Core
import Set.Function

predicate ClosedBinary (S op : Set) := ∀ x ∈ S, ∀ y ∈ S, op(x, y) ∈ S
predicate ClosedUnary (S op : Set) := ∀ x ∈ S, op(x) ∈ S

theorem ClosedBinary.mem (S op x y : Set)
  requires closed : ClosedBinary(S, op)
  requires hx : x ∈ S
  requires hy : y ∈ S
  shows op(x, y) ∈ S
proof
  exact closed with x, hx, y, hy

theorem ClosedUnary.mem (S op x : Set)
  requires closed : ClosedUnary(S, op)
  requires hx : x ∈ S
  shows op(x) ∈ S
proof
  exact closed with x, hx

theorem restrictBinary.function (A S op : Set)
  requires function : IsMagma(A, op)
  requires subset : S ⊆ A
  requires closed : ClosedBinary(S, op)
  shows restrict(op, S × S) : S × S → S
proof
  have bounded := product.monotone with subset, subset
  have values : ∀ p ∈ S × S, op(p) ∈ S
    intros p hp
    obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp
    have output := ClosedBinary.mem with hx, hy
    unfold call2 at output
    rwa shape
  exact restrict.function at op, A × A, A, S × S, S with *

theorem restrictBinary.value (A S op x y : Set)
  requires function : IsMagma(A, op)
  requires subset : S ⊆ A
  requires closed : ClosedBinary(S, op)
  requires hx : x ∈ S
  requires hy : y ∈ S
  shows (restrict(op, S × S))(x, y) = op(x, y)
proof
  have bounded := product.monotone with subset, subset
  have values : ∀ p ∈ S × S, op(p) ∈ S
    intros p hp
    obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with hp
    have output := ClosedBinary.mem with hu, hv
    unfold call2 at output
    rwa shape
  have pair := product.pair at x, y, S, S with *
  unfold call2
  exact restrict.apply at op, A × A, A, S × S, S, (x, y) with *

-- Agreement of operation graphs does not require closure of the smaller carrier.
theorem restrictBinary.value_on_subset (A S op x y : Set)
  requires function : IsMagma(A, op)
  requires subset : S ⊆ A
  requires hx : x ∈ S
  requires hy : y ∈ S
  shows (restrict(op, S × S))(x, y) = op(x, y)
proof
  have bounded := product.monotone with subset, subset
  unfold IsMagma at function
  have values : ∀ p ∈ S × S, op(p) ∈ A
    intros p hp
    have member : p ∈ A × A by simp [Subset]
    exact FunctionBetween.apply_closed with function, member
  have pair := product.pair at x, y, S, S with *
  unfold call2
  exact restrict.apply with *

theorem restrictUnary.function (A S op : Set)
  requires function : op : A → A
  requires subset : S ⊆ A
  requires closed : ClosedUnary(S, op)
  shows restrict(op, S) : S → S
proof
  have values : ∀ x ∈ S, op(x) ∈ S
    intros x hx
    exact ClosedUnary.mem with *
  exact restrict.function with *

theorem restrictUnary.value (A S op x : Set)
  requires function : op : A → A
  requires subset : S ⊆ A
  requires closed : ClosedUnary(S, op)
  requires hx : x ∈ S
  shows (restrict(op, S))(x) = op(x)
proof
  have values : ∀ y ∈ S, op(y) ∈ S
    intros y hy
    exact ClosedUnary.mem with hy
  exact restrict.apply with *

theorem restrictBinary.associative (A S op : Set)
  requires function : IsMagma(A, op)
  requires subset : S ⊆ A
  requires closed : ClosedBinary(S, op)
  requires law : Associative(A, op)
  shows Associative(S, restrict(op, S × S))
proof
  intros x hx y hy z hz
  have included := subset
  have xIn := included with x, hx
  have yIn := included with y, hy
  have zIn := included with z, hz
  have closed0 := ClosedBinary.mem at S, op, x, y with *
  have value0 := restrictBinary.value at A, S, op, x, y with *
  have closed1 := ClosedBinary.mem at S, op, op(x, y), z with *
  have value1 := restrictBinary.value at A, S, op, op(x, y), z with *
  have closed2 := ClosedBinary.mem at S, op, y, z with *
  have value2 := restrictBinary.value at A, S, op, y, z with *
  have closed3 := ClosedBinary.mem at S, op, x, op(y, z) with *
  have value3 := restrictBinary.value at A, S, op, x, op(y, z) with *
  have original := law with x, xIn, y, yIn, z, zIn
  cc

theorem restrictBinary.commutative (A S op : Set)
  requires function : IsMagma(A, op)
  requires subset : S ⊆ A
  requires closed : ClosedBinary(S, op)
  requires law : Commutative(A, op)
  shows Commutative(S, restrict(op, S × S))
proof
  intros x hx y hy
  have included := subset
  have xIn := included with x, hx
  have yIn := included with y, hy
  have closed0 := ClosedBinary.mem with hx, hy
  have value0 := restrictBinary.value with hx, hy
  have closed1 := ClosedBinary.mem with hy, hx
  have value1 := restrictBinary.value with hy, hx
  have original := law with x, xIn, y, yIn
  cc

theorem restrictBinary.identity (A S op unit : Set)
  requires function : IsMagma(A, op)
  requires subset : S ⊆ A
  requires closed : ClosedBinary(S, op)
  requires law : Identity(A, op, unit)
  requires member : unit ∈ S
  shows Identity(S, restrict(op, S × S), unit)
proof
  unfold Identity
  refine ⟨member, ?_⟩
  intros x hx
  have included := subset
  have xIn := included with x, hx
  have original := law.right with x, xIn
  have left := restrictBinary.value at A, S, op, unit, x with *
  have right := restrictBinary.value at A, S, op, x, unit with *
  constructor
  . cc
  . cc

theorem restrictUnary.inverse (A S add zero neg : Set)
  requires addition : IsMagma(A, add)
  requires negation : neg : A → A
  requires subset : S ⊆ A
  requires addClosed : ClosedBinary(S, add)
  requires negClosed : ClosedUnary(S, neg)
  requires law : Inverse(A, add, zero, neg)
  shows Inverse(S, restrict(add, S × S), zero, restrict(neg, S))
proof
  have function := restrictUnary.function with *
  unfold Inverse
  refine ⟨function, ?_⟩
  intros x hx
  have included := subset
  have xIn := included with x, hx
  have closed0 := ClosedUnary.mem with *
  have value0 := restrictUnary.value with hx
  have closed1 := ClosedBinary.mem at S, add, neg(x), x with *
  have value1 := restrictBinary.value at A, S, add, neg(x), x with *
  have closed2 := ClosedBinary.mem at S, add, x, neg(x) with *
  have value2 := restrictBinary.value at A, S, add, x, neg(x) with *
  have original := law.right with x, xIn
  constructor
  . cc
  . cc

theorem restrictBinary.distributive (A S add mul : Set)
  requires addition : IsMagma(A, add)
  requires multiplication : IsMagma(A, mul)
  requires subset : S ⊆ A
  requires addClosed : ClosedBinary(S, add)
  requires mulClosed : ClosedBinary(S, mul)
  requires law : Distributive(A, add, mul)
  shows Distributive(S, restrict(add, S × S), restrict(mul, S × S))
proof
  intros x hx y hy z hz
  have included := subset
  have xIn := included with x, hx
  have yIn := included with y, hy
  have zIn := included with z, hz
  have closed0 := ClosedBinary.mem at S, add, y, z with *
  have value0 := restrictBinary.value at A, S, add, y, z with *
  have closed1 := ClosedBinary.mem at S, mul, x, call2(add, y, z) with *
  have value1 := restrictBinary.value at A, S, mul, x, call2(add, y, z) with *
  have closed2 := ClosedBinary.mem at S, mul, x, y with *
  have value2 := restrictBinary.value at A, S, mul, x, y with *
  have closed3 := ClosedBinary.mem at S, mul, x, z with *
  have value3 := restrictBinary.value at A, S, mul, x, z with *
  have closed4 := ClosedBinary.mem at S, add, call2(mul, x, y), call2(mul, x, z) with *
  have value4 := restrictBinary.value at A, S, add, call2(mul, x, y), call2(mul, x, z) with *
  have closed5 := ClosedBinary.mem at S, add, x, y with *
  have value5 := restrictBinary.value at A, S, add, x, y with *
  have closed6 := ClosedBinary.mem at S, mul, call2(add, x, y), z with *
  have value6 := restrictBinary.value at A, S, mul, call2(add, x, y), z with *
  have closed7 := ClosedBinary.mem at S, mul, y, z with *
  have value7 := restrictBinary.value at A, S, mul, y, z with *
  have closed8 := ClosedBinary.mem at S, add, call2(mul, x, z), call2(mul, y, z) with *
  have value8 := restrictBinary.value at A, S, add, call2(mul, x, z), call2(mul, y, z) with *
  have original := law with x, xIn, y, yIn, z, zIn
  constructor
  . cc
  . cc