-- Sublattices and the restricted order
-- 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.Lattice.Sublattice
import LatticeHom
import Set.WellOrder

predicate IsSublattice (A r B : Set) :=
  IsLattice(A, r) ∧ (B ⊆ A) ∧
  (∀ x ∈ B, ∀ y ∈ B, join(A, r, x, y) ∈ B ∧ meet(A, r, x, y) ∈ B)

theorem IsSublattice.lattice (A r B : Set)
  requires h : IsSublattice(A, r, B)
  shows IsLattice(A, r)
proof
  simp [IsSublattice]

theorem IsSublattice.subset (A r B : Set)
  requires h : IsSublattice(A, r, B)
  shows B ⊆ A
proof
  simp [IsSublattice]

theorem IsSublattice.join_closed (A r B x y : Set)
  requires h : IsSublattice(A, r, B)
  requires hx : x ∈ B
  requires hy : y ∈ B
  shows join(A, r, x, y) ∈ B
proof
  rcases h with ⟨lattice, bounded, closed⟩
  have both := closed with x, hx, y, hy
  exact both.left

theorem IsSublattice.meet_closed (A r B x y : Set)
  requires h : IsSublattice(A, r, B)
  requires hx : x ∈ B
  requires hy : y ∈ B
  shows meet(A, r, x, y) ∈ B
proof
  rcases h with ⟨lattice, bounded, closed⟩
  have both := closed with x, hx, y, hy
  exact both.right

theorem IsSublattice.whole (A r : Set)
  requires lattice : IsLattice(A, r)
  shows IsSublattice(A, r, A)
proof
  refine ⟨lattice, Subset.reflexive at A, ?_⟩
  intros x hx y hy
  refine ⟨(join.member with lattice, hx, hy), (meet.member with lattice, hx,
      hy)⟩

theorem IsSublattice.intersection (A r B C : Set)
  requires hB : IsSublattice(A, r, B)
  requires hC : IsSublattice(A, r, C)
  shows IsSublattice(A, r, B ∩ C)
proof
  have lattice := IsSublattice.lattice with hB
  have bounded := Subset.transitive with (intersection.subset_left at B, C),
      (IsSublattice.subset with hB)
  refine ⟨lattice, bounded, ?_⟩
  intros x hx y hy
  have xBoth := intersection.membership.forward with hx
  have yBoth := intersection.membership.forward with hy
  constructor
  . apply intersection.membership.backward
    constructor
    . exact IsSublattice.join_closed with hB, xBoth.left, yBoth.left
    . exact IsSublattice.join_closed with hC, xBoth.right, yBoth.right
  . apply intersection.membership.backward
    constructor
    . exact IsSublattice.meet_closed with hB, xBoth.left, yBoth.left
    . exact IsSublattice.meet_closed with hC, xBoth.right, yBoth.right

-- The restriction of a partial order to a subset

theorem restrictOrder.partial (A r B : Set)
  requires order : IsPartialOrder(A, r)
  requires hB : B ⊆ A
  shows IsPartialOrder(B, restrictOrder(r, B))
proof
  have reflexive := IsPartialOrder.reflexive with order
  have transitive := IsPartialOrder.transitive with order
  have antisymmetric := IsPartialOrder.antisymmetric with order
  constructor
  . constructor
    . exact restrictOrder.relation at r, B
    . constructor
      . intros x hx
        apply restrictOrder.relates.backward
        refine ⟨(reflexive with x, (hB with x, hx)), hx, hx⟩
      . intros x hx y hy z hz xy yz
        have first := restrictOrder.relates.forward with xy
        have second := restrictOrder.relates.forward with yz
        apply restrictOrder.relates.backward
        refine ⟨(transitive with x, (hB with x, hx), y, (hB with y, hy), z,
            (hB with z, hz), first.left, second.left), hx, hz⟩
  . intros x hx y hy xy yx
    have first := restrictOrder.relates.forward with xy
    have second := restrictOrder.relates.forward with yx
    exact antisymmetric with x, (hB with x, hx), y, (hB with y, hy),
        first.left, second.left

theorem IsSublattice.supremum (A r B x y : Set)
  requires h : IsSublattice(A, r, B)
  requires hx : x ∈ B
  requires hy : y ∈ B
  shows Supremum(B, restrictOrder(r, B), {x, y}, join(A, r, x, y))
proof
  have lattice := IsSublattice.lattice with h
  have bounded := IsSublattice.subset with h
  have xA := bounded with x, hx
  have yA := bounded with y, hy
  have joinB := IsSublattice.join_closed with h, hx, hy
  have left : relates(restrictOrder(r, B), x, join(A, r, x, y))
    apply restrictOrder.relates.backward
    refine ⟨(join.upper_left with lattice, xA, yA), hx, joinB⟩
  have right : relates(restrictOrder(r, B), y, join(A, r, x, y))
    apply restrictOrder.relates.backward
    refine ⟨(join.upper_right with lattice, xA, yA), hy, joinB⟩
  apply Supremum.of_pair with hx, hy, joinB, left, right
  intros b hb xb yb
  have xbR := restrictOrder.relates.forward with xb
  have ybR := restrictOrder.relates.forward with yb
  apply restrictOrder.relates.backward
  refine ⟨(join.least with lattice, xA, yA, (bounded with b, hb), xbR.left,
      ybR.left), joinB, hb⟩

theorem IsSublattice.infimum (A r B x y : Set)
  requires h : IsSublattice(A, r, B)
  requires hx : x ∈ B
  requires hy : y ∈ B
  shows Infimum(B, restrictOrder(r, B), {x, y}, meet(A, r, x, y))
proof
  have lattice := IsSublattice.lattice with h
  have bounded := IsSublattice.subset with h
  have xA := bounded with x, hx
  have yA := bounded with y, hy
  have meetB := IsSublattice.meet_closed with h, hx, hy
  have left : relates(restrictOrder(r, B), meet(A, r, x, y), x)
    apply restrictOrder.relates.backward
    refine ⟨(meet.lower_left with lattice, xA, yA), meetB, hx⟩
  have right : relates(restrictOrder(r, B), meet(A, r, x, y), y)
    apply restrictOrder.relates.backward
    refine ⟨(meet.lower_right with lattice, xA, yA), meetB, hy⟩
  apply Infimum.of_pair with hx, hy, meetB, left, right
  intros b hb bx byBound
  have bxR := restrictOrder.relates.forward with bx
  have byR := restrictOrder.relates.forward with byBound
  apply restrictOrder.relates.backward
  refine ⟨(meet.greatest with lattice, xA, yA, (bounded with b, hb), bxR.left,
      byR.left), hb, meetB⟩

theorem IsSublattice.restricted (A r B : Set)
  requires h : IsSublattice(A, r, B)
  shows IsLattice(B, restrictOrder(r, B))
proof
  have lattice := IsSublattice.lattice with h
  have order := restrictOrder.partial with (IsLattice.order with lattice),
      (IsSublattice.subset with h)
  apply IsLattice.of_pairs with order
  . intros x hx y hy
    refine ⟨join(A, r, x, y), (IsSublattice.supremum with h, hx, hy)⟩
  . intros x hx y hy
    refine ⟨meet(A, r, x, y), (IsSublattice.infimum with h, hx, hy)⟩

theorem IsSublattice.join (A r B x y : Set)
  requires h : IsSublattice(A, r, B)
  requires hx : x ∈ B
  requires hy : y ∈ B
  shows join(B, restrictOrder(r, B), x, y) = join(A, r, x, y)
proof
  have restricted := IsSublattice.restricted with h
  symm
  exact join.of_supremum with restricted, hx, hy, (IsSublattice.supremum with h,
      hx, hy)

theorem IsSublattice.meet (A r B x y : Set)
  requires h : IsSublattice(A, r, B)
  requires hx : x ∈ B
  requires hy : y ∈ B
  shows meet(B, restrictOrder(r, B), x, y) = meet(A, r, x, y)
proof
  have restricted := IsSublattice.restricted with h
  symm
  exact meet.of_infimum with restricted, hx, hy, (IsSublattice.infimum with h,
      hx, hy)

-- The image of a lattice homomorphism is a sublattice of its target.

theorem IsLatticeHom.image_sublattice (f A r B s : Set)
  requires h : IsLatticeHom(f, A, r, B, s)
  shows IsSublattice(B, s, functionImage(f, A, B))
proof
  have source := IsLatticeHom.source with h
  have target := IsLatticeHom.target with h
  refine ⟨target, (functionImage.subset at f, A, B), ?_⟩
  intros u hu v hv
  obtain ⟨uB, x, hx, rfl⟩ := functionImage.membership.forward with hu
  obtain ⟨vB, y, hy, rfl⟩ := functionImage.membership.forward with hv
  have joinA := join.member with source, hx, hy
  have meetA := meet.member with source, hx, hy
  have joinValue := IsLatticeHom.join with h, hx, hy
  have meetValue := IsLatticeHom.meet with h, hx, hy
  constructor
  . rw ← joinValue
    exact functionImage.membership.backward with
        ⟨(IsLatticeHom.apply_member with h, joinA), join(A, r, x, y), joinA, rfl⟩
  . rw ← meetValue
    exact functionImage.membership.backward with
        ⟨(IsLatticeHom.apply_member with h, meetA), meet(A, r, x, y), meetA, rfl⟩