/-
Port of `Lattice/IterProd.agda`: the `k`-fold product `A × (A × ⋯ × B)`.

With propositional equality and typeclasses, the Agda `Everything` record
(which threaded the lattice operations and the conditional fixed-height proof
through one recursion, so that the operations built by separate recursions
would agree) is no longer needed: the `Lattice` instance is one recursive
definition, and the fixed-height structure is another recursion over it.

Correspondence:
  IterProd            ↦ Spa.IterProd
  build               ↦ Spa.IterProd.build
  isLattice/lattice   ↦ instance Spa.IterProd.instLattice
  fixedHeight,
  isFiniteHeightLattice,
  finiteHeightLattice ↦ Spa.IterProd.fixedHeight (+ instFiniteHeight instance)
  ⊥-built             ↦ Spa.IterProd.bot_fixedHeight
-/
import Spa.Lattice.Prod
import Spa.Lattice.Unit

namespace Spa

universe u

/-- Agda: `IterProd k = iterate k (A × ·) B`. (As in the Agda module, `A` and
`B` are constrained to the same universe to keep the recursion simple.) -/
def IterProd (A B : Type u) : ℕ → Type u
  | 0 => B
  | k + 1 => A × IterProd A B k

namespace IterProd

variable {A B : Type u}

instance instLattice [Lattice A] [Lattice B] :
    ∀ k, Lattice (IterProd A B k)
  | 0 => inferInstanceAs (Lattice B)
  | k + 1 => @Prod.instLattice A (IterProd A B k) _ (instLattice k)

instance instDecidableEq [DecidableEq A] [DecidableEq B] :
    ∀ k, DecidableEq (IterProd A B k)
  | 0 => inferInstanceAs (DecidableEq B)
  | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (instDecidableEq k)

/-- Agda: `build`. -/
def build (a : A) (b : B) : (k : ℕ) → IterProd A B k
  | 0 => b
  | k + 1 => (a, build a b k)

variable [Lattice A] [Lattice B]

def fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
    ∀ k, FiniteHeightLattice (IterProd A B k)
  | 0 => inferInstanceAs (FiniteHeightLattice B)
  | k + 1 => @Spa.prod A (IterProd A B k) _ (instLattice k) _ (fixedHeight k)

instance instFiniteHeight [FiniteHeightLattice A] [FiniteHeightLattice B] (k : ℕ) :
    FiniteHeightLattice (IterProd A B k) := fixedHeight k

theorem bot_fixedHeight [FiniteHeightLattice A] [FiniteHeightLattice B] :
    ∀ k, (fixedHeight (A := A) (B := B) k).bot = build (⊥ : A) (⊥ : B) k
  | 0 => rfl
  | k + 1 => by
    show ((⊥ : A), (fixedHeight (A := A) (B := B) k).bot)
        = ((⊥ : A), build (⊥ : A) (⊥ : B) k)
    rw [bot_fixedHeight k]

end IterProd

end Spa