Menu

Rainbow docs menu

Reference · Foundations

rainbow.math.nonnegative-rational

Foundations src/rainbow/math/nonnegative_rational.clj13 definitions, 6 theorems

Nonnegative rationals as proof data: numerator plus denominator predecessor. The representation makes a zero denominator unrepresentable. Equality is deliberately cross-multiplication equivalence rather than product equality; no quotient rule or normalization axiom is added to the kernel.

nnrat/NonnegativeRational

DefinitionSource, line 80

nnrat/NonnegativeRational :
  → Type

nnrat/make

DefinitionSource, line 87

nnrat/make :
  (x₁ x₂ : ℕ)
  → ℚ≥0

ℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

nnrat/numerator

DefinitionSource, line 97

nnrat/numerator :
  (x₁ : ℚ≥0)
  → ℕ

ℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

nnrat/denominator-predecessor

DefinitionSource, line 109

nnrat/denominator-predecessor :
  (x₁ : ℚ≥0)
  → ℕ

ℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

nnrat/denominator

DefinitionSource, line 109

nnrat/denominator :
  (x₁ : ℚ≥0)
  → ℕ

ℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

nnrat/combine-denominator-predecessors

DefinitionSource, line 131

nnrat/combine-denominator-predecessors :
  (x₁ x₂ : ℕ)
  → ℕ

ℕ = data/Nat

nnrat/zero

DefinitionSource, line 143

nnrat/zero :
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

nnrat/one

DefinitionSource, line 150

nnrat/one :
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

nnrat/half

DefinitionSource, line 157

nnrat/half :
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

nnrat/quarter

DefinitionSource, line 164

nnrat/quarter :
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

nnrat/equivalent

DefinitionSource, line 171

nnrat/equivalent :
  (x₁ x₂ : ℚ≥0)
  → Prop

ℚ≥0 = nnrat/NonnegativeRational

nnrat/add

DefinitionSource, line 185

nnrat/add :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

nnrat/multiply

DefinitionSource, line 203

nnrat/multiply :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

nnrat/denominator-combine

TheoremHolds by unfolding a definitionNo axiomsSource, line 224

nnrat/denominator-combine :
  (left right : ℕ)
  → data/succ (nnrat/combine-denominator-predecessors left right) = nat/multiply (data/succ left) (data/succ right)

= = equality/Eqℕ = data/Nat

nnrat/equivalent-reflexive

TheoremHolds by unfolding a definitionNo axiomsSource, line 241

nnrat/equivalent-reflexive :
  (value : ℚ≥0)
  → value = value

= = nnrat/equivalent: equality of rational valuesℚ≥0 = nnrat/NonnegativeRational

nnrat/equivalent-symmetric

TheoremFor all inputsNo axiomsSource, line 255

nnrat/equivalent-symmetric :
  (left right : ℚ≥0)
  (same : left = right)
  → right = left

= = nnrat/equivalent: equality of rational valuesℚ≥0 = nnrat/NonnegativeRational

nnrat/equivalent-transitive

TheoremFor all inputsNo axiomsSource, line 276

nnrat/equivalent-transitive :
  (left middle right : ℚ≥0)
  (left-middle : left = middle)
  (middle-right : middle = right)
  → left = right

= = nnrat/equivalent: equality of rational valuesℚ≥0 = nnrat/NonnegativeRational

nnrat/add-respects-equivalence

TheoremFor all inputsNo axiomsSource, line 463

nnrat/add-respects-equivalence :
  (left left-equivalent right right-equivalent : ℚ≥0)
  (same-left : left = left-equivalent)
  (same-right : right = right-equivalent)
  → left + right = left-equivalent + right-equivalent

+ = nnrat/add= = nnrat/equivalent: equality of rational valuesℚ≥0 = nnrat/NonnegativeRational

nnrat/multiply-respects-equivalence

TheoremFor all inputsNo axiomsSource, line 369

nnrat/multiply-respects-equivalence :
  (left left-equivalent right right-equivalent : ℚ≥0)
  (same-left : left = left-equivalent)
  (same-right : right = right-equivalent)
  → left · right = left-equivalent · right-equivalent

= = nnrat/equivalent: equality of rational values· = nnrat/multiplyℚ≥0 = nnrat/NonnegativeRational