Hints for foundations for lemmas on Rat

Stream: lean4

[Arien Malec]

I'm a bit over my skis working on basic lemmas for Rat. In Lean 3 mathlib, https://github.com/leanprover-community/mathlib/blob/master/src/data/rat/defs.lean most of the really basic lemmas are defined in terms of num_denom_cases_on', e.g.:

protected theorem add_zero : a + 0 = a :=
num_denom_cases_on' a $ λ n d h,
by rw [← zero_mk d]; simp [h, -zero_mk]

and num_denom_cases_on' is defined in terms of num_denom, which relies on some definitional and implementation behavior that's different in Lean 4 (e.g., there's no pnat) and in terms of operators I don't understand (e.g. what's '/.'?)

In general rat and Rat are heavily pre-optimized, and add is inherently pretty complicated.

Some hints on the best Lean 4 equivalent for num_denom_cases_on' for the Lean 4 version of Rat would be greatly welcome.

[Kevin Buzzard]

docs4#Rat does this work?

[Kevin Buzzard]

So it looks like all the data has been defined (addition, subtraction etc) but none of the proofs?

[Kevin Buzzard]

Why not just sorry the proofs and make the ring instance?

[Arien Malec]

That would advance my project for sure but create a poor PR. If I had pointers to the hard bits I’d be happy to do the grunt work for a PR.

[Scott Morrison]

I think we have transitioned to the point in mathlib4 where PRs should either be

1. ports of entire files from mathlib3, faithfully preserving all their content and organisation
2. ad-hoc ports of material only if it is supporting tactic implementation.

[Scott Morrison]

So the ideal way to work on data/rat/defs.lean is first to run

cd src
leanproject import-graph --to data.rat.defs --exclude-tactics --port-status --reduce data.rat.defs.pdf

inside the mathlib repository.

[Scott Morrison]

This produces data.rat.defs.pdf

[Arien Malec]

What’s confusing is that this has moved to Std4 & the implementation details are just different enough that it’s not a mechanical port….

[Scott Morrison]

Oh dear, I hadn't realised Rat was in Std already!

[Scott Morrison]

Maybe the right choice is actually to backport this definition to mathlib3, so we can resume the "mechanical port".

[Arien Malec]

Arien Malec said:

in terms of operators I don't understand (e.g. what's '/.'?)

Realized that this is localized "infix (name := rat.mk) /. :70 := rat.mk" in rat so I can just use Rat.mk.

[Arien Malec]

I'm sorta making progress here, but I'm confused.

Given that /. means rat.mk and rat.mk is sorta 'mkRat' in Lean 4 Std4 (sorta because mathlib rat is defined in terms of int and pnat, where as Rat is Int and Nat & rat.mk is int -> int -> rat whereas mkRat is Int -> Nat -> Rat, I decided to try to rewrite

@[simp] theorem num_denom : ∀ {a : ℚ}, a.num /. a.denom = a
| ⟨n, d, h, (c:_=1)⟩ := show mk_nat n d = _,
  by simp [mk_nat, ne_of_gt h, mk_pnat, c]

as

@[simp] theorem num_den : ∀ {a : Rat}, mkRat a.num a.den = a
| ⟨n, d, h, (c:_=1)⟩ => show mkRat n d = _ by
  simp [mkRat, Nat.ne_of_gt h, mkRat, c]

but the net_of_gt simplification isn't working, and it's confusing to me why it should work in mathlib

It's spelled

lemma ne_of_gt {a b : α} (h : b < a) : a ≠ b :=
λ he, absurd h (he ▸ lt_irrefl a)

in mathlib

and

theorem ne_of_gt {a b : Nat} (h : b < a) : a ≠ b := (ne_of_lt h).symm

theorem ne_of_lt {a b : Nat} (h : a < b) : a ≠ b :=
  fun he => absurd (he ▸ h) (Nat.lt_irrefl a)

In Lean 4

Since the type of h is … OH(!) the types in mathlib and Lean 4 differ.

In mathlib the corresponding type is 0 < denom and in Lean 4 it's den ≠ 0 so back to the mines.

[Arien Malec]

So

@[simp] theorem num_den : ∀ {a : Rat}, mkRat a.num a.den = a
| ⟨n, d, h, (c:_=1)⟩ => show mkRat n d = _ by
  simp [mkRat,h,normalize, maybeNormalize,c]

closes the goal

Progress.

[Arien Malec]

I also now think I understand what that simp step is doing -- it's leading Lean down the path of understanding that mkRat is already pre-normalized by hypothesis.

[Kevin Buzzard]

docs#rat

[Kevin Buzzard]

You've made the assertion more than once that in loan 3 rat is defined using pnat but I don't think it's true.

[Mario Carneiro]

rat itself doesn't use pnat, but rat.mk uses rat.mk_pnat

[Kevin Buzzard]

Right -- the builtin constructor for rat is not rat.mk, it's rat.mk'

[Mario Carneiro]

ah yeah, maybe we should do that too, so we can use Rat.mk for the smart constructor

[Mario Carneiro]

The current lean 4 file is based not on the original data.rat.basic but on lean 4's Lean.Rat, which has slightly more efficient operations. We should try to make it align with mathlib better where it's reasonable to do so

[Mario Carneiro]

We also have another tool for replacements, @[csimp] lemmas, which allow us to use a naive and simple-to-reason-about definition as the official definition and sequester the messy and efficient definition to an auxiliary. I don't usually bother though unless we care about the defeqs

[Arien Malec]

Kevin Buzzard said:

You've made the assertion more than once that in loan 3 rat is defined using pnat but I don't think it's true.

Sorry, you are correct - as @Mario Carneiro notes, the path to construction goes through pnat but the rat itself is in terms of nat plus the assertion pos : 0 < denom

[Arien Malec]

Should the Lean 4 equivalent of /. for Rat be an HDiv?

[Arien Malec]

And…, how does one spell @[elab_as_eliminator] in Lean 4?

[David Renshaw]

@[elabAsElim]

[Jannis Limperg]

@[elab_as_elim] for recent nightlies -- the naming convention for attributes has reverted to snake_case.

[Arien Malec]

The update in this adventure is that things are going mostly well:

theorem ext_iff {p q : Rat} : p = q ↔ p.num = q.num ∧ p.den = q.den := by
  cases p; cases q; simp

@[ext] theorem ext {p q : Rat} (hn : p.num = q.num) (hd : p.den = q.den) : p = q := Rat.ext_iff.mpr ⟨hn, hd⟩

@[simp] theorem num_den : ∀ {a : Rat}, mkRat a.num a.den = a
| ⟨n, d, h, (c:_=1)⟩ => show mkRat n d = _ by
  simp [mkRat,h,normalize, maybeNormalize,c]

theorem num_den' : (⟨n, d, h, c⟩ : Rat) = mkRat n d := num_den.symm

/-- Define a (dependent) function or prove `∀ r : Rat, p r` by dealing with rational
numbers of the form `mkRat n d` with `d ≠ 0` and coprime `n`, `d`. -/
@[elab_as_elim] def num_denom_cases_on {C : Rat → Sort u} :
 ∀ (a : Rat) (H : ∀ n d, d ≠ 0 → (n.natAbs).coprime d → C (mkRat n  d)), C a
 | ⟨n, d, h, c⟩, H => by rw [num_den']; exact H n d h c

 /-- Define a (dependent) function or prove `∀ r : Rat, p r` by dealing with rational
numbers of the form `n /. d` with `d ≠ 0`. -/
@[elab_as_elim] def num_denom_cases_on' {C : Rat → Sort u}
   (a : Rat) (H : ∀ (n: Int) (d: Nat), d ≠ 0 → C (mkRat n d)) : C a :=
num_denom_cases_on a <| fun n d h _ => H n d h

But things that should be easy like the analogue of

@[simp] theorem zero_mk (n) : 0 /. n = 0 :=
by cases n; simp [mk]

end up being terrifying.

[Arien Malec]

I'm close, I think.

After

@[simp] theorem mk_zero: (mkRat 0 n) = 0 := by
  cases n with
  | zero => simp [mkRat]
  | succ n => simp [mkRat, normalize, maybeNormalize, Int.natAbs, Nat.gcd_zero_left, Int.zero_div]

I'm down to:

case succ
n: Nat
⊢ (if h : n = 0 then mk 0 (Nat.succ n) else mk 0 (Nat.succ n / Nat.succ n)) = 0

which, since I already handled the zero case in the first cases branch, and since Nat.succ n is always > 0, should resolve down to mk 0 1=0 which should close by rfl but I'm stuck in how to tell Lean that.

[Kevin Buzzard]

Assuming there's not yet a splitIfs tactic in lean 4, you want to do cases on n=0 and use if_pos and if_neg or whatever they're called in lean 4

[Damiano Testa]

There might be split_ifs

[Scott Morrison]

Yes, split_ifs landed in mathlib4#508.

[Sebastian Ullrich]

Is split_ifs mostly intended for porting and otherwise should be covered by core split (which also handles match) in most cases? It would be great if such overlaps would be discussed in the doc strings.

[Scott Morrison]

It is briefly mentioned in the doc-string at https://github.com/leanprover-community/mathlib4/pull/508/files#diff-42751ffdb8743d3ea4b619276a2600ccc8dd8476d972087dfcddb3bbfe52dc58R77.

Perhaps it would be worthwhile to go through the test file, and annotate the use cases for which the core split suffices.

[Arien Malec]

Now I see that I should have taken care of this case earlier.

That branch descends from
Nat.gcd (Int.natAbs 0) (Nat.succ n)=1 so it suffices to prove ∀ n, Nat.gcd (Int.natAbs 0) (Nat.succ n) ≠ 1

[Arien Malec]

Oh, but that's not true.

[Arien Malec]

It is, however, only true in the exact case where the theorem is true.

[Mario Carneiro]

You generally don't want to unfold multiple definitions in a single theorem, so this should be broken into multiple theorems. I came up with this:

import Std.Data.Rat

namespace Rat

attribute [simp] Int.ofNat_zero Int.ofNat_one

@[simp] theorem maybeNormalize_eq {num den g} (den_nz reduced) :
    maybeNormalize num den g den_nz reduced =
    { num := num / g, den := den / g, den_nz, reduced } := by
  unfold maybeNormalize <;> split
  · subst g; simp
  · rfl

@[simp] theorem normalize_zero (nz) : normalize 0 d nz = 0 := by
  simp [normalize, Int.zero_div, Int.natAbs_zero, Nat.div_self (Nat.pos_of_ne_zero nz)]; rfl

@[simp] theorem mk_zero : mkRat 0 n = 0 := by unfold mkRat; split <;> simp

[Arien Malec]

I love this!

[Arien Malec]

So update:

1) I hope my adventures here are useful -- aspirationally, I'd like to post a PR, but this may be beyond my capabilities at current levels of learning; less aspirationally, I'm hopeful that my struggles here in the differences between Lean 4 Std4 and mathlib are helpful for the eventual refactor and reconciliation -- if this is all distracting, I'm happy to self-mute
2) I realize now most of the heavy lifting in the core lemmas in mathlib is done in theorems like add_def that prove the behavior and invariants of the core operations and those go through lift_binop_eqwhich has a particularly hairy signature...
3) The signature of rat is in terms of int/nat with appropriate constraints on nonzero denominator, but the constructor goes mk_pnat and most of the /. heavy lifting is through rat.mk that is int -> int -> rat, and addressing that variation to Lean 4 makes signature modification for lift_binop_eq particularly hairy (that theorem assumes everything is int)

I think the pathway here is to recreate the mathlib equivalent for an Int -> Int -> Rat constructor, & try to port lift_binop_eq but happy to take any feedback....

[Arien Malec]

(FWIW, I think that core Std4.Rat should have the helper APIs and invariant lemmata on the core operations, and with that in place, proving the various algebraic lemmata in, say Std4.Rat.Basic would be pretty trivial.)