Int.eq

-- Observational equality of Int, and its logical equivalence with the
-- built-in ≡ ∈ Int. Int is a quotient (ℕ × ℕ) / IntR, so its OWN
-- defining relation is already the natural "observational" candidate —
-- but lifting IntR to Int × Int directly (via a double quot-elim
-- landing in Ω) needs its well-definedness proved as an Ω-code
-- equality, i.e. propositional extensionality between two DIFFERENT
-- IntR-applications, and this elaborator's propext check only
-- discharges the evident (𝟙-/reflexive-≡-shaped) cases automatically —
-- it does not search for the mutual-implication witnesses even when
-- they're sitting in context (see the Core/prop.nova-only bonus attempt
-- in the sibling Natural/eq.nova). So EqI instead compares CANONICAL
-- representatives (Int/normalize.nova's intNormalize), squashing an
-- ordinary EQUATION rather than an Ω-code — equations are
-- proof-irrelevant (every ≡-proof is ⋆ on the nose), so THIS
-- well-definedness is free.
-- IntR is Int's own quotient relation (Int.nova); a proof of it
-- gives equal classes directly (el-quot-eq, automatic given a term of
-- IntR p q in context — no extra machinery needed).

import Natural (+, zeroPlusId, sucPlus)
import Int (Int, IntR, intZero, intOne, toInt)
import Int.normalize (normPair, normSound, intNormalize)
import Core.equality (sym, trans, cong, pairext)
import Core.prop (↔, iffIntro, ∧, ¬, ⊥, andIntro, andFst, andSnd, impIntro, impApply)
import Natural.eq (EqN, eqNRefl, eqNSound, eqNComplete, predEq)

classEqOfRel : {p q : ℕ × ℕ} → IntR p q → class p ≡ class q ∈ Int
  using (Int.Int.unfold, Int.IntR.unfold)
classEqOfRel = λp q h. ⋆

-- normPair's own representative is IntR-related to its input (that's
-- normSound), so its class is the same Int
classNormPairEq : {p : ℕ × ℕ} → class (normPair (p .π₁) (p .π₂)) ≡ class p ∈ Int
  using (Int.Int.unfold, Int.IntR.eq, Int.normalize.normClass, Int.normalize.normPair.eq, normSound)
classNormPairEq = λp. classEqOfRel (normSound (p .π₁) (p .π₂))

-- normalization doesn't change the value: intNormalize z is z. The
-- quot-elim's well-definedness goal here is an EQUATION (not an Ω
-- code), so it's discharged for free by proof irrelevance regardless
-- of how the representative varies.
intNormalizeId : (z : Int) → intNormalize z ≡ z
  using (classNormPairEq,
    Int.Int.unfold,
    Int.normalize.intNormalize.eq,
    Int.normalize.normClass,
    Int.normalize.normPair.eq)
intNormalizeId = λz. quot-elim (p. classNormPairEq) z

EqI : Int → Int → Ω
EqI = λz1 z2. intNormalize z1 ≡ intNormalize z2

eqIRefl : (z : Int) → EqI z z using (Int.eq.EqI.unfold, intNormalizeId)
eqIRefl = λz. ⋆

-- soundness: z1 and z2 both equal their own normalizations, which
-- coincide whenever EqI holds
eqISound : {z1 z2 : Int} → EqI z1 z2 → z1 ≡ z2
  using (Int.eq.EqI.eq,
    Int.eq.EqI.unfold,
    intNormalizeId,
    Int.Int.eq,
    Int.Int.unfold,
    Int.normalize.intNormalize.eq)
eqISound =
  λz1 z2 h. trans
    _
    _
    _
    sym _ _ (intNormalizeId z1)
    trans (intNormalize z1) _ _ h (intNormalizeId z2)

-- completeness: z1 ≡ z2 reflects, so intNormalize z1 and intNormalize
-- z2 are the same term — the evident-≡-shape squashee bare ⋆ handles
eqIComplete : {z1 z2 : Int} → (z1 ≡ z2) → EqI z1 z2
  using (Int.eq.EqI.unfold, intNormalizeId, Int.Int.unfold)
eqIComplete = λz1 z2 h. ⋆

-- the logical equivalence, packaged with Core/prop.nova's ↔ against the
-- squashed built-in equality
eqISoundP : {z1 z2 : Int} → EqI z1 z2 → z1 ≡ z2 using (intNormalizeId)
eqISoundP = λz1 z2 h. eqISound h

-- ∥p∥ ≐ p (code-squash-idem): h already proves the equation
eqICompleteP : {z1 z2 : Int} → (z1 ≡ z2) → EqI z1 z2 using (Int.eq.EqI.unfold, intNormalizeId)
eqICompleteP = λz1 z2 h. eqIComplete h

eqIIff : {z1 z2 : Int} → EqI z1 z2 ↔ (z1 ≡ z2)
  using (intNormalizeId, Core.prop.↔.unfold, Core.prop.∧.unfold)
eqIIff = λz1 z2. iffIntro eqISoundP eqICompleteP

-- ===== observational equality, the computing one =====
--
-- EqI above compares canonical representatives with the BUILT-IN
-- equality, so it never reduces to ⊤/⊥ and yields no disequalities.
-- The relation below does: it extracts the canonical representative as
-- a PAIR OF NATS and compares componentwise with Natural/eq.nova's EqN.
--
-- Extracting the representative is the whole difficulty. It is a
-- quot-elim landing in ℕ × ℕ, so its well-definedness is
--   normPair a b ≡ normPair c d  whenever  a + d ≡ b + c,
-- a NAT-level equation — no propositional extensionality anywhere,
-- which is what blocked the direct Ω-valued comparison (see the note
-- at the top of this file).
--
-- SINCE: Core/prop.nova's propExt (supplied witnesses, e-star-propext)
-- and Int/effective.nova have both landed, so the Ω-valued route is no
-- longer blocked, and a bare DISEQUALITY no longer needs any of this —
-- effectivity reads IntR straight off a class equation
-- (Int/nonZero.nova's intNeqOfNotRel). What survives the change is the
-- part effectivity cannot give: intCanon is a FUNCTION into data, and
-- that is what lets Int/nonZero.nova DECIDE zero-ness and hand back a
-- witness. Propositional effectivity is not a decision procedure.
-- normPair n Z ≡ (n , Z)
normPairZR : {n : ℕ} → normPair n Z ≡ (n, Z) using (Int.normalize.normPair.eq)
normPairZR = λn. ℕ-elim ⋆ (k ih. ⋆) n

-- normPair c (b + c) ≡ (Z , b): the successors cancel pairwise
normPairLeftZ : (b c : ℕ) → normPair c (b + c) ≡ (Z, b)
  using (Int.normalize.normPair.eq, Natural.+.eq, Natural.plusZeroId)
normPairLeftZ = λb c. ℕ-elim ⋆ (k ih. ⋆) c

-- normPair (n + d) d ≡ (n , Z)
normPairRightZ : (n d : ℕ) → normPair (n + d) d ≡ (n, Z)
  using (Int.normalize.normPair.eq, Natural.+.eq, normPairZR)
normPairRightZ = λn d. ℕ-elim normPairZR (k ih. ⋆) d

normPairWD : (a b c d : ℕ) (h : a + d ≡ b + c) → normPair a b ≡ normPair c d
  using (Int.eq.normPairZR,
    Int.normalize.normPair.eq,
    normPairLeftZ,
    normPairRightZ,
    sucPlus,
    zeroPlusId)
normPairWD =
  λa. ℕ-elim
    λb c d h. trans
      _
      _
      _
      ⋆
      trans
        _
        _
        _
        sym _ _ (normPairLeftZ b c)
        cong (λu. ℕ × ℕ) (λx. normPair c x) (sym _ _ (trans _ _ _ (sym _ _ (zeroPlusId d)) h))
    a' ih. λb. ℕ-elim
      λc d h. trans
        _
        _
        _
        ⋆
        trans
          _
          _
          _
          sym _ _ (normPairRightZ (S a') d)
          cong (λu. ℕ × ℕ) (λx. normPair x d) (trans _ _ _ h (zeroPlusId c))
      b' ihb. λc d h. ih
        b'
        c
        d
        predEq (trans _ _ _ (sym _ _ (sucPlus a' d)) (trans _ _ _ h (sucPlus b' c)))
      b
    a

-- the canonical representative of an integer
intCanon : Int → ℕ × ℕ using (Int.Int.unfold, normPairWD)
intCanon = λz. quot-elim (p. normPair (p .π₁) (p .π₂)) z

intCanonToInt : (z : Int) → toInt (intCanon z) ≡ z
  using (classNormPairEq,
    Int.eq.intCanon.eq,
    Int.Int.eq,
    Int.Int.unfold,
    Int.toInt.unfold,
    Int.toInt.eq,
    Int.normalize.normClass,
    Int.normalize.normPair.eq)
intCanonToInt = λz. quot-elim (p. classNormPairEq) z

intCanonClass : (z : Int) → class (intCanon z) ≡ z
  using (classNormPairEq,
    Int.eq.intCanon.eq,
    Int.Int.eq,
    Int.Int.unfold,
    Int.normalize.normClass,
    Int.normalize.normPair.eq)
intCanonClass = λz. quot-elim (p. classNormPairEq) z

intCanonOne : intCanon intOne ≡ (S Z, Z)
  using (Int.eq.intCanon.eq, Int.intOne.eq, Int.normalize.normPair.eq)
intCanonOne = ⋆

intCanonZero : intCanon intZero ≡ (Z, Z)
  using (Int.eq.intCanon.eq, Int.intZero.eq, Int.normalize.normPair.eq)
intCanonZero = ⋆

-- ===== EqZ: equality that computes =====
EqZ : Int → Int → Ω
EqZ = λz1 z2. EqN (intCanon z1 .π₁) (intCanon z2 .π₁) ∧ EqN (intCanon z1 .π₂) (intCanon z2 .π₂)

eqZRefl : (z : Int) → EqZ z z
  using (Int.eq.EqZ.eq,
    Int.eq.EqZ.unfold,
    Int.eq.intCanon.eq,
    Natural.eq.EqN.eq,
    Int.Int.unfold,
    Core.prop.∧.unfold)
eqZRefl = λz. andIntro (eqNRefl (intCanon z .π₁)) (eqNRefl (intCanon z .π₂))

eqZSound : {z1 z2 : Int} → EqZ z1 z2 → z1 ≡ z2 using (Int.eq.EqZ.eq)
eqZSound =
  λz1 z2 h. trans
    _
    _
    _
    sym _ _ (intCanonToInt z1)
    trans
      _
      _
      _
      cong _ toInt (pairext (eqNSound (andFst h)) (eqNSound (andSnd h)))
      intCanonToInt z2

eqZComplete : {z1 z2 : Int} → (z1 ≡ z2) → EqZ z1 z2
  using (Int.eq.EqZ.eq,
    Int.eq.EqZ.unfold,
    Int.eq.intCanon.eq,
    Natural.eq.EqN.eq,
    Int.Int.unfold,
    Core.prop.∧.unfold)
eqZComplete =
  λz1 z2 h. andIntro
    eqNComplete (cong (λu. ℕ) (λz. intCanon z .π₁) h)
    eqNComplete (cong (λu. ℕ) (λz. intCanon z .π₂) h)

eqZSoundP : {z1 z2 : Int} → EqZ z1 z2 → z1 ≡ z2
eqZSoundP = λz1 z2 h. eqZSound h

eqZCompleteP : {z1 z2 : Int} → (z1 ≡ z2) → EqZ z1 z2 using (Int.eq.EqZ.unfold, Core.prop.∧.unfold)
eqZCompleteP = λz1 z2 h. eqZComplete h

eqZIff : (z1 z2 : Int) → EqZ z1 z2 ↔ (z1 ≡ z2) using (Core.prop.↔.unfold, Core.prop.∧.unfold)
eqZIff = λz1 z2. iffIntro eqZSoundP eqZCompleteP

-- ===== NeqZ: disequality that computes =====
NeqZ : Int → Int → Ω
NeqZ = λz1 z2. ¬ (EqZ z1 z2)

neqZSound : {z1 z2 : Int} → NeqZ z1 z2 → ¬ (z1 ≡ z2)
  using (Int.eq.EqZ.eq,
    Int.eq.NeqZ.eq,
    Int.eq.NeqZ.unfold,
    Int.eq.intCanon.eq,
    Natural.eq.EqN.eq,
    Int.Int.eq,
    Int.Int.unfold,
    Natural.+.eq,
    Core.prop.¬.eq,
    Core.prop.¬.unfold,
    Core.prop.∧.eq,
    Core.prop.⊃.eq,
    Core.prop.⊃.unfold,
    Core.prop.⊥.eq)
neqZSound = λz1 z2 h. impIntro {z1 ≡ z2} {∥𝟘∥} (λe. impApply h (eqZCompleteP e))

neqZComplete : {z1 z2 : Int} → ¬ (z1 ≡ z2) → NeqZ z1 z2
  using (Int.eq.EqZ.eq,
    Int.eq.EqZ.unfold,
    Int.eq.NeqZ.eq,
    Int.eq.NeqZ.unfold,
    Int.eq.intCanon.eq,
    Natural.eq.EqN.eq,
    Int.Int.eq,
    Int.Int.unfold,
    Int.normalize.normPair.eq,
    Core.prop.¬.eq,
    Core.prop.¬.unfold,
    Core.prop.∧.eq,
    Core.prop.∧.unfold,
    Core.prop.⊃.eq,
    Core.prop.⊃.unfold,
    Core.prop.⊤.eq,
    Core.prop.⊥.eq)
neqZComplete = λz1 z2 h. impIntro {EqZ z1 z2} {∥𝟘∥} (λe. impApply h (eqZSoundP e))

neqZIff : (z1 z2 : Int) → NeqZ z1 z2 ↔ ¬ (z1 ≡ z2) using (Core.prop.↔.unfold, Core.prop.∧.unfold)
neqZIff = λz1 z2. iffIntro neqZSound neqZComplete

-- ===== the payoff: an actual disequality =====
--
-- EqZ intOne intZero REDUCES: the canonical representatives are
-- (S Z, Z) and (Z, Z), so it is EqN (S Z) Z ∧ EqN Z Z, i.e. ⊥ ∧ ⊤.
-- Its first projection is already the absurdity.
eqZOneZero : NeqZ intOne intZero
  using (Int.eq.EqZ.eq,
    Int.eq.EqZ.unfold,
    Int.eq.NeqZ.eq,
    Int.eq.NeqZ.unfold,
    Int.eq.intCanon.eq,
    Natural.eq.EqN.eq,
    Int.intOne.eq,
    Int.intZero.eq,
    Int.normalize.normPair.eq,
    Core.prop.¬.eq,
    Core.prop.¬.unfold,
    Core.prop.∧.eq,
    Core.prop.∧.unfold,
    Core.prop.⊃.eq,
    Core.prop.⊃.unfold,
    Core.prop.⊥.eq)
eqZOneZero =
  impIntro
    {EqZ intOne intZero}
    {⊥}
    λh. andFst {⊥} {EqN (intCanon intOne .π₂) (intCanon intZero .π₂)} h

intOneNotZero : ¬ (intOne ≡ intZero) using (Core.prop.¬.unfold, Core.prop.⊃.unfold)
intOneNotZero = neqZSound eqZOneZero

-- and a positive computation: 2 = 2 even spelled differently
eqZTwo : EqZ (class (2, Z)) (class (3, S Z))
  using (Int.eq.EqZ.eq,
    Int.eq.EqZ.unfold,
    Int.eq.intCanon.eq,
    Natural.eq.EqN.eq,
    Int.Int.unfold,
    Int.normalize.normPair.eq,
    Core.prop.∧.eq,
    Core.prop.∧.unfold,
    Core.prop.⊤.eq,
    Core.prop.⊥.eq)
eqZTwo = andIntro {∥𝟙∥} {∥𝟙∥} ⋆ ⋆