English
cmp_to_nat expresses that, for all m,n, the Ordering given by cmp m n corresponds to the nat-cast order, i.e., (m : ℕ) ? (n : ℕ) matches the comparison result.
Русский
cmp_to_nat выражает, что для всех m,n Ordering cmp m n соответствует порядку вывода в Nat, то есть сравнение по Nat совпадает с результатом сравнения.
LaTeX
$$$\\forall m,n, \\text{Ordering}(\\mathrm{cmp}(m,n)) \\text{ совпадает с порядком по }\\mathbb{N}$$$
Lean4
theorem cmp_to_nat : ∀ m n, (Ordering.casesOn (cmp m n) ((m : ℕ) < n) (m = n) ((n : ℕ) < m) : Prop)
| 1, 1 => rfl
| bit0 a, 1 =>
let h : (1 : ℕ) ≤ a := to_nat_pos a
Nat.add_le_add h h
| bit1 a, 1 => Nat.succ_lt_succ <| to_nat_pos <| bit0 a
| 1, bit0 b =>
let h : (1 : ℕ) ≤ b := to_nat_pos b
Nat.add_le_add h h
| 1, bit1 b => Nat.succ_lt_succ <| to_nat_pos <| bit0 b
| bit0 a, bit0 b => by
dsimp [cmp]
have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
· exact Nat.add_lt_add this this
· rw [this]
· exact Nat.add_lt_add this this
| bit0 a, bit1 b => by
dsimp [cmp]
have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
· exact Nat.le_succ_of_le (Nat.add_lt_add this this)
· rw [this]
apply Nat.lt_succ_self
· exact cmp_to_nat_lemma this
| bit1 a, bit0 b => by
dsimp [cmp]
have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
· exact cmp_to_nat_lemma this
· rw [this]
apply Nat.lt_succ_self
· exact Nat.le_succ_of_le (Nat.add_lt_add this this)
| bit1 a, bit1 b => by
dsimp [cmp]
have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
· exact Nat.succ_lt_succ (Nat.add_lt_add this this)
· rw [this]
· exact Nat.succ_lt_succ (Nat.add_lt_add this this)
