Data.Rat.Defs

Stream: mathlib4

[Patrick Massot]

@Ruben Van de Velde are you still working on that file?

[Patrick Massot]

I have a bit of time now.

[Ruben Van de Velde]

No, pushed the little bit that I accomplished

[Patrick Massot]

Ok, thanks

[Patrick Massot]

@Mario Carneiro could you have a look at a very strange simp behavior at https://github.com/leanprover-community/mathlib4/pull/998/commits/7d0e0318750daeb511776e8a968a2032955d8617? Line 135 has a simp doing nothing whereas when I extract the relevant goal in a lemma bar on line 117 it works normally

[Patrick Massot]

While you are in this file, it would also be nice to investigate why the elaborator needs more help in the definition of numDenCasesOn' than in Lean 3. Note that helping the elaborator is easy here, I'm only pointing out one possible improvement.

[Mario Carneiro]

Your bar lemma is wrong. The correct version is

lemma bar (b : ℕ) (hb : ¬b = 0) (a : ℤ)
  (h : ∀ (h : ¬b = 0), mkPNat a ⟨b, b.pos_of_ne_zero h⟩ = 0)  : False := by
  simp only [hb] at h
  sorry

and this indeed does not simplify

[Mario Carneiro]

Re: numDenCasesOn', it seems to work fine for me:

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

/-- Define a (dependent) function or prove `∀ r : ℚ, p r` by dealing with rational
numbers of the form `n /. d` with `d ≠ 0`. -/
@[elab_as_elim]
def numDenCasesOn'.{u} {C : ℚ → Sort u} (a : ℚ) (H : ∀ (n : ℤ) (d : ℕ), d ≠ 0 → C (n /. d)) :
    C a :=
  numDenCasesOn a fun n d h c => H n d h.ne'

[Patrick Massot]

I don't see any difference between your bar and mine

[Mario Carneiro]

h is a dependent function, because it mentions the local variable h

[Mario Carneiro]

you can see this in the pretty printer, it prints yours as a nondependent arrow and not mine

[Mario Carneiro]

as a result simp doesn't want to rewrite the ¬b = 0

[Mario Carneiro]

I think there was some kind of "canonize proofs" thing that lean 3 simp did that might explain the difference

[Patrick Massot]

Oh ok, I see the difference now.

[Mario Carneiro]

you could also try marking forall_prop_of_true as a simp lemma

[Patrick Massot]

Now at least consistency is restored, and we do have some simp regression compared to Lean 3.

[Mario Carneiro]

is forall_prop_of_true a simp lemma in lean 3? Is it used here?

[Patrick Massot]

The Lean 3 version has a simp only there.

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/master/src/data/rat/defs.lean#L106

[Mario Carneiro]

what does the rewrite trace look like?

[Patrick Massot]

The new definition of addition on $\mathbb{Q}$ will be a lot of work for porting this file

[Patrick Massot]

Rewrite trace in Lean 3?

[Mario Carneiro]

yes

[Mario Carneiro]

i.e. what did it do

[Patrick Massot]

Could you remind me the relevant option?

[Mario Carneiro]

eh, I do rewr + autocomplete

[Mario Carneiro]

something like simplify.rewrite

[Patrick Massot]

thanks

[Patrick Massot]

0. [simplify.rewrite] [[anonymous]]: b = 0 ==> false
0. [simplify.rewrite] [not_false_iff]: ¬false ==> true
0. [simplify.rewrite] [forall_true_left]: ∀ (h : true), mk_pnat a ⟨b, _⟩ = 0 ==> mk_pnat a ⟨b, _⟩ = 0

[Mario Carneiro]

with pp.proofs?

[Mario Carneiro]

because that's kind of magic

[Mario Carneiro]

I think it's using a custom congr to descend into both sides of a forall and getting some messy eq.rec term in that _

[Mario Carneiro]

Patrick Massot said:

The new definition of addition on $\mathbb{Q}$ will be a lot of work for porting this file

Note that the first theorem we will be proving is a + b = (a.num * b.den + b.num * a.den) /. (a.den * b.den) and all the other theorems follow from that, treating it as the definition

[Patrick Massot]

0. [simplify.rewrite] [[anonymous]]: b = 0 ==> false
0. [simplify.rewrite] [not_false_iff]: ¬false ==> true
0. [simplify.rewrite] [forall_true_left]: ∀ (h : true),
  mk_pnat a
      ⟨b,
       nat.pos_of_ne_zero
         (((not_congr (iff_false_intro (mt (congr_arg int.of_nat) b0))).trans not_false_iff).mpr h)⟩ =
    0 ==> mk_pnat a
    ⟨b,
     nat.pos_of_ne_zero
       (((not_congr (iff_false_intro (mt (congr_arg int.of_nat) b0))).trans not_false_iff).mpr true.intro)⟩ =
  0

[Mario Carneiro]

here's a lean 3 MWE:

@[congr] lemma forall_prop_congr' {p p' : Prop} {q q' : p → Prop}
  (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : (∀ h, q h) = ∀ h : p', q' (hp.2 h) :=
sorry

example (x : nat) (p : fin 5 → Prop) (h' : x < 5) : ∀ h : x < 5, p ⟨x, h⟩ :=
by { simp only [h'], sorry }

[Mario Carneiro]

simp does nothing unless you have that @[congr] lemma

[Mario Carneiro]

and would you look at that:

-- Porting note: `@[congr]` commented out for now.
-- @[congr]
theorem forall_prop_congr' {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
    (∀ h, q h) = ∀ h : p', q' (hp.2 h) :=
  propext (forall_prop_congr hq hp)

[Mario Carneiro]

so it looks like the root cause is that simp doesn't accept this congr lemma

[Jannis Limperg]

This is the same one as #mathlib4 > Difference in simp behaviour right?

[Kevin Buzzard]

this link works for me (and Jannis' doesn't)

[Kevin Buzzard]

https://github.com/leanprover/lean4/issues/1926

[Jannis Limperg]

Seems like you can't hash-link to topics containing backticks. :(

[Patrick Massot]

@Chris Hughes as you can see from this thread, I was also working on this file. It would have been nice to tell us you wanted to work on it too. All the work you pushed two hours ago was duplicated.

[Patrick Massot]

Mario Carneiro said:

Re: numDenCasesOn', it seems to work fine for me:

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

/-- Define a (dependent) function or prove `∀ r : ℚ, p r` by dealing with rational
numbers of the form `n /. d` with `d ≠ 0`. -/
@[elab_as_elim]
def numDenCasesOn'.{u} {C : ℚ → Sort u} (a : ℚ) (H : ∀ (n : ℤ) (d : ℕ), d ≠ 0 → C (n /. d)) :
    C a :=
  numDenCasesOn a fun n d h c => H n d h.ne'

I forgot to comment on this: the reason why I thought this didn't work is because mathport introduced parentheses that confused Lean. See for instance how Chris and I independently fixed things like these

[Kevin Buzzard]

@Patrick Massot this has happened to me too and I found it very frustrating. Right now what I am doing is only claiming files when I have time to do the initial run through the entire file fixing the trivial stuff (capitalization etc). Whenever I see a file half-done I am very scared to do more in case it happens to me again.

[Patrick Massot]

To be clear, I'm not blaming Chris for anything, only telling him to be more cautious when Scott explicitly tell people to work on a file. I'm delighted to see all the great work Chris is putting in the port. And there is plenty enough of work for all of us without duplication.

[Patrick Massot]

And now @Arien Malec is also pushing to that branch. I give up.

[Arien Malec]

Sorry, was responding to Scott's call for help. Happy to back off/revert.

[Patrick Massot]

Anyway, the file has a lot less errors now, and probably @Mario Carneiro should take over since the remaining stuff is really tied to the super un-mathematical new definitions.

[Patrick Massot]

Help is fine! But I think when there is explicit call for help then we should post here before editing the file.

[Patrick Massot]

And also post when we stop. Hence I post: I'm stopping now.

[Arien Malec]

Anyway from previous work here, I generally think the best approach is for @Mario Carneiro to provide the theorems for invariants in Std, at which the basic lemmas for Rat are trivial.

[Mario Carneiro]

I don't think I can work on it right at this moment, so my recommendation if it's holding up the port is to port all the theorems in terms of some interface theorems similar to the original mathlib definition and sorry the theorems asserting that the new definition matches this, and just commit the file with sorries

[Arien Malec]

Or for someone with the juice to prove things like add_def to get those invariants in place.

[Mario Carneiro]

Well even if someone does that I'm likely to significantly rewrite it on the way to Std so it's probably not worth it

[Mario Carneiro]

this whole file will be migrated to Std but it's easier to do that if it's mostly working already

[Mario Carneiro]

that is, I will wait until the feat: port Data.Rat.Defs PR is merged

[Mario Carneiro]

@Scott Morrison In response to:

      -- Apparently contrary to the documentation, `conv in a => rw [← Int.sign_mul_natAbs a]`
      -- rewrites all the `a`s, not just the first one.
      conv =>
        congr; congr; congr; rw [← Int.sign_mul_natAbs a]
      conv =>
        congr; congr; rfl; congr; rw [← Int.sign_mul_natAbs c]

you are missing the occs parameter:

      conv in (occs := 1) a => rw [← Int.sign_mul_natAbs a]
      conv in (occs := 1) c => rw [← Int.sign_mul_natAbs c]

Actually the default occs setting is (occs := 1) but there was a bug preventing it from matching the a's separately. Fixed in lean4#1956

[Mario Carneiro]

the code with congr can also be written more compactly using enter:

      conv => enter [1, 1, 1]; rw [← Int.sign_mul_natAbs a]
      conv => enter [1, 2, 1]; rw [← Int.sign_mul_natAbs c]

[Scott Morrison]

Thanks for minimizing and fixing this!

[Scott Morrison]

@Patrick Massot, sorry about the race conditions on this PR today. Perhaps I overemphasised its priority; hopefully you weren't too annoyed.

[Scott Morrison]

And just a heads up that I'm working on this file now. I'll push individual commits for every lemma that gets fixed. :-)

[Scott Morrison]

Okay, I'm stopping on Data.Rat.Defs. Still two sorries, and two broken proofs.

[Patrick Massot]

Please don't worry about me and continue the great work you're doing for all of us!

[Scott Morrison]

Gah, someone broke data.rat.defs?? What's going on? Yesterday there was just one error, which @Mario Carneiro was going to handle. Now there are lots. :-(

[Mario Carneiro]

I thought @Ruben Van de Velde was working on it

[Mario Carneiro]

I didn't do anything to data.rat.defs, but I added the theorems I said I was going to to Std

[Scott Morrison]

Ok. I will wait for Ruben.

[Scott Morrison]

Okay, I think I understand. Mario's new definition of /. basically borked Data.Rat.Defs in mathlib4, and Ruben has started over fixing things again.

[Scott Morrison]

It feels like we went a long way backwards there. :-(

[Mario Carneiro]

what's the issue? It should be the same as the old definition

[Scott Morrison]

Have a look at the branch data_rat_defs2.

[Scott Morrison]

This is where the file used to be, updated to latest Std4.

[Scott Morrison]

It used to be one missing proof, now almost everything fails.

[Mario Carneiro]

oops, I tried to look that up on mathlib4 and accidentally created a branch through the web interface instead

[Mario Carneiro]

the branch doesn't seem to exist

[Scott Morrison]

argh, sorry

[Scott Morrison]

Branch is there now.

[Scott Morrison]

Whereas back at https://github.com/leanprover-community/mathlib4/pull/998/commits/be6ad827179e8203d7ec2e34a2c1ac6a721bc9ec we just had one sorry.

[Mario Carneiro]

I think to a large extent this file should not be ported at all, just set up the statements and move on. It's basically waiting for the porting wave to pass over it so it can be migrated to std properly, and all the proofs will be written or rewritten at that point anyway

[Mario Carneiro]

it feels like while the migration is going on it's just going to be pain for the porting process

[Scott Morrison]

I don't really know what to do with that. :-(

[Mario Carneiro]

killing every last sorry is possibly counterproductive if the definitions might change

[Mario Carneiro]

what we need for migration to continue is to record all the statements we need

[Heather Macbeth]

@Mario Carneiro How long do you think the lemmas would have to remain in a sorry'd state? A week, a month? I don't really love the idea of leaving sorries in nominally-ported parts of mathlib.

[Mario Carneiro]

It's more an issue of not working on stuff that is currently under active development to avoid stepping on toes

[Scott Morrison]

I still don't understand what you're proposing we do with Data.Rat.Defs, Data.Rat.Basic, and Data.Rat.Order.

[Scott Morrison]

I had been assuming until this morning that you were going to fill in a proof of add_def in Data.Rat.Defs, and then we would have these three files ported before christmas.

[Mario Carneiro]

add_def is proved

[Scott Morrison]

But now Data.Rat.Defs is full of broken proofs again, and I'm not sure if you're proposing that we just sorry them all, or what.

[Mario Carneiro]

I need to take a closer look at the breakage you are talking about but I didn't make any major changes that should break everything

[Scott Morrison]

So you added

theorem Rat.add_def : ∀ (a b : ℚ), a + b = normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) :=

and

theorem Rat.add_def' : ∀ (a b : ℚ), a + b = mkRat (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) :=

in Std.

But mathlib4 wants:

theorem add_def'' {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) : a /. b + c /. d = (a * d + c * b) /. (b * d) := by

[Mario Carneiro]

ok so a lot of problems seem to be that mkNat and mkInt have not been aligned

[Scott Morrison]

You added a definition of /. that is different than what we had in data_rat_defs, so all the statements involving it have broken too.

[Mario Carneiro]

at least, these definitions still exist on data_rat_defs2

[Scott Morrison]

Yes, data_rat_defs2 does not include any attempt to update Mathlib.Data.Rat.Defs for your recent changes to Srtd

[Mario Carneiro]

oh, where am I supposed to be working then?

[Scott Morrison]

It was just to demonstrate that the mathlib4 branch went from one sorry to many errors.

[Scott Morrison]

The HEAD of data_rat_defs, I guess?

[Scott Morrison]

That appears to be Ruben's effort to update the branch to cope with the changes to Std

[Scott Morrison]

But I haven't looked at his changes beyond seeing that there are still lots of breakages.

[Ruben Van de Velde]

I'm sorry if I made life harder for you- I'm not currently looking at the branch, but I'd hoped that the new issues would be easier than the ones we had before

[Scott Morrison]

No problem, we'll get there. :-)

[Mario Carneiro]

all I'm seeing is that all the theorems are being replaced by half broken sorry proofs by one line reference-std proofs

[Scott Morrison]

Okay. Sorry to panic, I wasn't happy about seeing a sea of red.

[Scott Morrison]

To be clear, before we bumped, I'm pretty sure there were exactly two sorries.

[Scott Morrison]

(add_def and sub_def)

[Scott Morrison]

I had just started trying Data.Rat.Basic and Data.Rat.Order, and then was horrified to discover Data.Rat.Defs was full of errors. :-)

[Mario Carneiro]

it's sorry free now

[Ruben Van de Velde]

Thanks!

[Ruben Van de Velde]

Github was confused about the diff, showing a bunch of changes from the std4-update that landed already, so I merged with master

[Scott Morrison]

Amazing, thank you.

[Scott Morrison]

I added Data.Rat.Basic

[Scott Morrison]

I'm confused about casts in Data.Rat.Defs. @Mario Carneiro, would you be able to help here?

We currently have (in Data.Rat.Defs):

instance : IntCast ℚ :=
  ⟨ofInt⟩

@[simp]
theorem of_int_eq_cast (n : ℤ) : ofInt n = Int.cast n :=
  rfl

But it seems that the cast via ofInt is still being picked up as the default, and so several later theorems are written with explicit Int.cast so the LHS is in simp normal form.

What do we need to do here to have Int.cast be preferred?

[Mario Carneiro]

I punted on Int.cast before but we might need to move it to std just like Nat.cast

[Scott Morrison]

Okay, for now, I'm going to leave a note explaining that this problem, then merge as is.

[Mario Carneiro]

do you have an example with the issue?

[Mario Carneiro]

also I put a attribute [-simp] in data.rat.defs, this should be noted as a temporary workaround

[Mario Carneiro]

(the longer story is that mkRat is now preferred over divInt when the denominator is nonnegative, but this needs mkRat to have more API and simp lemmas to match mathlib's theorems about /.)

[Scott Morrison]

I'd like to change

theorem coe_int_eq_divInt (z : ℤ) : Int.cast z = z /. 1 := num_den'

to

theorem coe_int_eq_divInt (z : ℤ) : (z : ℚ) = z /. 1 := num_den'

but this messes up proofs later. Presumably they are fixable, I'm just not sure if I should do this now or not.

[Scott Morrison]

Oh, I seem to have sorted it out.

[Scott Morrison]

Data.Rat.Defs is hopefully all ready to go.

The two missing facts for Data.Rat.Order are:

theorem lt_iff_le_not_le {a b : ℚ} : a < b ↔ a ≤ b ∧ ¬b ≤ a  := ...
theorem le_iff_sub_num_nonneg (a b : ℚ) : a ≤ b ↔ 0 ≤ (b - a).num := ...

These probably belong in Std.

@Mario Carneiro, would you like to do this, or shall I have a go?

[Mario Carneiro]

do you have a proof relative to some le_def similar to the old definition?

[Mario Carneiro]

It looks like the definition trivially satisfies a < b <-> !(b <= a) so it probably comes down to transitivity and asymmetry of <

[Scott Morrison]

le_iff_sub_num_nonneg is essentially relating the new Std4 definition with the old mathlib3 definition. (But it's stated purely in std4 language).

[Scott Morrison]

So, no, I don't have a proof of le_iff_sub_num_nonneg to work from, since the lhs is the new Std4 definition which mathlib3 didn't talk about.

[Mario Carneiro]

aha, I see. (The lt definition is a bit lazy, it could have been just lt <-> not le like it is now)

[Mario Carneiro]

I'm done for the day, but I can work on it tomorrow