Reference · Signed rationals

rainbow.math.rational.signed.structural-equality

Signed rationalssrc/rainbow/math/rational/signed/structural_equality.clj2 definitions, 8 theorems

Decidable STRUCTURAL equality for nonnegative and signed rationals. `signed/decide-equivalent` decides the QUOTIENT: 1/2 and 2/4 embed as different pairs that it correctly calls equivalent. Some checks need the opposite instrument: structural equality, under which two values are equal exactly when they carry the SAME pair. A signed value is a pair of nonnegative rationals, each a pair of unary naturals, so the decision is four `nat/decide-equality` calls under two `boolean/and`, and the proofs are assembled from parts that all exist: and-elimination, the nat decision's soundness and reflexivity, `product/eta` for reconstruction, and two-step congruence for the pair constructors. Both directions are proved at both layers -- a true verdict IS structural equality and structural equality FORCES a true verdict -- so a decision built on top of it is honest in both outcomes. Native and axiom-free.

Depends onmath.logic.boolean-andmath.linear.matrix.row-length-decider

nnrat/decide-structural-equal :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

signed/decide-structural-equal :
  (x₁ x₂ : ℚ)
  → data/Bool

nnrat/reconstruct :
  (value : ℚ≥0)
  → nnrat/make (nnrat/numerator value) (nnrat/denominator-predecessor value) = value

signed/reconstruct :
  (value : ℚ)
  → signed/make (signed/positive value) (signed/negative value) = value

nnrat/decide-structural-equal-true-sound :
  (left right : ℚ≥0)
  (h₁ : nnrat/decide-structural-equal left right = data/true)
  → left = right

nnrat/decide-structural-equal-reflexive-true :
  (value : ℚ≥0)
  → nnrat/decide-structural-equal value value = data/true

nnrat/decide-structural-equal-true-complete :
  (left right : ℚ≥0)
  (h₁ : left = right)
  → nnrat/decide-structural-equal left right = data/true

signed/decide-structural-equal-true-sound :
  (left right : ℚ)
  (h₁ : signed/decide-structural-equal left right = data/true)
  → left = right

signed/decide-structural-equal-reflexive-true :
  (value : ℚ)
  → signed/decide-structural-equal value value = data/true

signed/decide-structural-equal-true-complete :
  (left right : ℚ)
  (h₁ : left = right)
  → signed/decide-structural-equal left right = data/true