Real.group

-- (ℝ, +, −, 0) as a GROUP, in Algebra/group.nova's vocabulary, plus the
-- rearrangement lemmas every later ℝ argument needs. These mirror
-- Rat/order.nova's ℚ block one level up: the proofs are the same
-- chains, and they have to be redone because the corpus has no
-- group-generic algebra — the laws live behind Id, and instantiating
-- them costs more than reproving them.

import Real (Real, realOfQ, realZero, realOne)
import Real.neg (realNeg, realNegNeg)
import Real.add (+, realAddComm, realAddAssoc, realAddZeroL, realAddZeroR, realAddNegL, realAddNegR)
import Algebra.monoid (IsMonoid)
import Algebra.group (IsGroup)
import Core.equality (trans, sym, cong)
import Core.id (Id, eqToId, idToEq)

realAddGroup : IsGroup Real using (Algebra.group.IsGroup.unfold, Algebra.monoid.IsMonoid.unfold)
realAddGroup =
  (,)
    (,)
      (+)
      realZero
      λx y z. eqToId _ _ (realAddAssoc x y z)
      λx. eqToId _ _ (realAddZeroL x)
      λx. eqToId _ _ (realAddZeroR x)
    realNeg
    λx. eqToId _ _ (realAddNegL x)
    λx. eqToId _ _ (realAddNegR x)

-- ===== rearrangement =====
realLeftSwap : (b c d : Real) → b + (c + d) ≡ c + (b + d)
realLeftSwap =
  λb c d. b + (c + d)
    ≡⟨ sym _ _ (realAddAssoc b c d) ⟩ b + c + d
    ≡⟨ cong (λv. Real) (λv. v + d) (realAddComm b c) ⟩ c + b + d
    ≡⟨ realAddAssoc c b d ⟩ c + (b + d)

realPairSwap : (a b c d : Real) → a + b + (c + d) ≡ a + c + (b + d)
realPairSwap =
  λa b c d. a + b + (c + d)
    ≡⟨ realAddAssoc a b (c + d) ⟩ a + (b + (c + d))
    ≡⟨ cong (λv. Real) (λv. a + v) (realLeftSwap b c d) ⟩ a + (c + (b + d))
    ≡⟨ sym _ _ (realAddAssoc a c (b + d)) ⟩ a + c + (b + d)

-- ===== inverses =====
realNegPlusCancel : (u v : Real) → realNeg u + (u + v) ≡ v
realNegPlusCancel =
  λu v. realNeg u + (u + v)
    ≡⟨ sym _ _ (realAddAssoc (realNeg u) u v) ⟩ realNeg u + u + v
    ≡⟨ cong (λw. Real) (λw. w + v) (realAddNegL u) ⟩ realZero + v
    ≡⟨ realAddZeroL v ⟩ v

-- explicit trans, not a chain: a chain step here lands at a
-- type-undetermined position inside realAdd's quot-elim (B-1)
realNegUnique : (u v : Real) → (u + v ≡ realZero) → v ≡ realNeg u
realNegUnique =
  λu v h. trans
    _
    _
    _
    sym _ _ (realNegPlusCancel u v)
    trans _ _ _ (cong (λw. Real) (λw. realNeg u + w) h) (realAddZeroR (realNeg u))

realNegAdd : (a b : Real) → realNeg (a + b) ≡ realNeg a + realNeg b
realNegAdd =
  λa b. sym
    _
    _
    realNegUnique
      a + b
      realNeg a + realNeg b
      a + b + (realNeg a + realNeg b)
        ≡⟨ realPairSwap a b (realNeg a) (realNeg b) ⟩ a + realNeg a + (b + realNeg b)
        ≡⟨ cong (λw. Real) (λw. w + (b + realNeg b)) (realAddNegR a) ⟩ realZero + (b + realNeg b)
        ≡⟨ realAddZeroL (b + realNeg b) ⟩ b + realNeg b
        ≡⟨ realAddNegR b ⟩ realZero

-- ===== subtraction =====
infixl 6 -
- : Real → Real → Real using (Real.Real.unfold)
(-) = λu v. u + realNeg v

realSubSelf : {u : Real} → u - u ≡ realZero
  using (Real.Real.unfold, Real.add.+.eq, Real.group.-.eq, Real.neg.realNeg.eq)
realSubSelf = λu. realAddNegR u

realSubZero : (u : Real) → u - realZero ≡ u
  using (Real.Real.unfold, Real.realZero.eq, Real.add.+.eq, Real.group.-.eq, Real.neg.realNeg.eq)
realSubZero = λu. trans _ _ _ (cong (λw. Real) (λw. u + w) Real.neg.realNegZero) (realAddZeroR u)

-- (u − v) + (v − w) ≡ u − w : the three-term split
realSubVia : {u v w : Real} → u - v + (v - w) ≡ u - w
realSubVia =
  λu v w. u + realNeg v + (v + realNeg w)
    ≡⟨ realAddAssoc u (realNeg v) (v + realNeg w) ⟩ u + (realNeg v + (v + realNeg w))
    ≡⟨ cong (λz. Real) (λz. u + z) (realNegPlusCancel v (realNeg w)) ⟩ u + realNeg w

-- −(u − v) ≡ v − u
realNegSub : {u v : Real} → realNeg (u - v) ≡ v - u
realNegSub =
  λu v. realNeg (u + realNeg v)
    ≡⟨ realNegAdd u (realNeg v) ⟩ realNeg u + realNeg (realNeg v)
    ≡⟨ cong (λz. Real) (λz. realNeg u + z) (realNegNeg v) ⟩ realNeg u + v
    ≡⟨ realAddComm (realNeg u) v ⟩ v + realNeg u

-- (u − v) + v ≡ u, and hence a zero difference is an equality
realSubPlusCancel : (u v : Real) → u - v + v ≡ u
realSubPlusCancel =
  λu v. u + realNeg v + v
    ≡⟨ realAddAssoc u (realNeg v) v ⟩ u + (realNeg v + v)
    ≡⟨ cong (λw. Real) (λw. u + w) (realAddNegL v) ⟩ u + realZero
    ≡⟨ realAddZeroR u ⟩ u

realSubZeroInv : {u v : Real} → (u - v ≡ realZero) → u ≡ v
realSubZeroInv =
  λu v h. trans
    _
    _
    _
    sym _ _ (realSubPlusCancel u v)
    trans _ _ _ (cong (λw. Real) (λw. w + v) h) (realAddZeroL v)