data.nat.fib mathlib4#1644

Stream: mathlib4

[Shreyas Srinivas]

I am starting the port of data.nat.fib After running the start_port script, I try pushing and git asks me to authenticate myself with my username and password. I have not seen this before. I created the necessary authentication token but I was denied access. I tried to push to the branch Data.Nat.Fib.

[Shreyas Srinivas]

What is the correct fix here?

[Anne Baanen]

What is the output of git remote -v? You might want to switch from HTTPS (https://github.com/leanprover-community/mathlib.git) to SSH (git@github.com:leanprover-community/mathlib.git) or vice versa.

[Shreyas Srinivas]

origin  git@github.com:Shreyas4991/mathlib4.git (fetch)
origin  git@github.com:Shreyas4991/mathlib4.git (push)
upstream    https://github.com/leanprover-community/mathlib4 (fetch)
upstream    https://github.com/leanprover-community/mathlib4 (push)

[Anne Baanen]

Then you probably want to do git remote set-url upstream git@github.com:leanprover-community/mathlib4.git.

[Shreyas Srinivas]

Thanks. Now I get a different error : error: src refspec Data.Nat.Fib does not match any

[Shreyas Srinivas]

The branch exists and I also tried a pull

[Shreyas Srinivas]

https://github.com/leanprover-community/mathlib4/tree/Data.Nat.Fib

[Anne Baanen]

That's weird. What is the output of git status?

[Shreyas Srinivas]

On branch port/Data.Nat.Fib nothing to commit, working tree clean

[Anne Baanen]

Just to be sure, you're running the command git push upstream or git push upstream port/Data.Nat.Fib?

[Shreyas Srinivas]

git push upstream Data.Nat.Fib

[Shreyas Srinivas]

Since that was the name of the remote branch that I created

[Shreyas Srinivas]

I tried port/Data.Nat.Fib and it worked

[Shreyas Srinivas]

But I haven't faced a requirement that the local and remote branches should have the same name before, even here in mathlib

[Anne Baanen]

I see! The local branch name is indeed port/Data.Nat.Fib. So to push to a remote branch named Data.Nat.Fib (without the port/ in front) you have to write git push upstream port/Data.Nat.Fib:Data.Nat.Fib. Or if you want to be totally sure Git does the right thing, git push -u upstream +port/Data.Nat.Fib:Data.Nat.Fib

[Shreyas Srinivas]

Ah okay. So git was complaining that I was trying to push a local branch that did not exist. Thanks a lot :)

[Anne Baanen]

Shreyas Srinivas said:

But I haven't faced a requirement that the local and remote branches should have the same name before, even here in mathlib

By default, the first git push on a branch will assume local and remote branch names are the same, with the colon you can specify the difference. Once things are pushed I believe it should remember the remote name so you don't have to specify it anymore.

[Shreyas Srinivas]

I am stuck at a goal that looks like this : ↑(fib n) * ↑(fib (1 + n) * 2) + ↑(fib (1 + n)) ^ 2 = ↑(fib n) * ↑(fib (1 + n)) * 2 + ↑(fib (1 + n)) ^ 2
The only hiccup is to rewrite using a rule that would say↑(fib (1 + n) * 2) = ↑(fib (1 + n)) * 2

[Shreyas Srinivas]

But I can't find any coercion theorems which say that coercing Nats to Ints does not change their product.

[Shreyas Srinivas]

ring won't resolve this (the variants ring! and the lean4 suggested ring_nf and ring_nf! did not resolve this either). Maybe that is reasonable. But it seems intuitively clear that coercing Nat to Int does not change their product.

[Shreyas Srinivas]

The PR in question: mathlib4#1644
See theorem fib_bit1_succ on line 188 in the latest commit on this branch

[David Renshaw]

what about norm_cast or zify?

[Shreyas Srinivas]

zify seems to be the cause. I got rid of most issues zify introduced by coercing subtractions.

[Heather Macbeth]

@Shreyas Srinivas There are a lot of bugs in zify; you can basically expect it not to work until they are fixed.

[Heather Macbeth]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/zify.20bugs.3F

[Heather Macbeth]

(It would be great if someone wanted to work on them .... :smile: )

[Shreyas Srinivas]

applying zify again followed by simp produced the following goal : ↑(fib n) * (↑(fib (1 + n)) * ↑2) = ↑(fib n) * ↑(fib (1 + n)) * 2

[Heather Macbeth]

You might like to check whether zify works for the same goal in mathlib3.

[Shreyas Srinivas]

Yeah it worked there.

[Heather Macbeth]

Can you narrow that down to a self-contained test case and add it to the thread on zify bugs?

[Shreyas Srinivas]

But in this case, all I am missing is something that can rewrite ↑2 to 2

[Heather Macbeth]

Ah, that sounds like the same as the second zify bug listed on Rob's post.

[Shreyas Srinivas]

update : I got around it

[Heather Macbeth]

Please add a porting note with a reference to the thread on zify bugs.

[Heather Macbeth]

Or, better, the corresponding issue: mathlib4#1576

[Shreyas Srinivas]

okay I will link it there. Basically I applied a sequence of simp operations more zify and , an rw with mul_assoc

[Shreyas Srinivas]

and it got sorted

[Heather Macbeth]

A fix like that is definitely the right move for now, but since we used to have automation for this kind of proof, we want to record it so that we don't lose it permanently.

[Shreyas Srinivas]

My best guess (based on my example) is that either zify only looks at the first one or two levels of the expression tree or it does not try enough coe + arithmetic theorems. It seems that in lean 3, it can ensure that where possible, the up arrow is attached to the innermost possible expression (past all the arithmetic operations). I don't know if this is because of the changes in behaviour of coercions that I have read about often, between lean 3 and 4, or just a bug somewhere.

[Shreyas Srinivas]

without my applying the theoremInt.coe_nat_sub, zify was not even pushing past the top level arithmetic.

[Heather Macbeth]

If you have time, can you please make a self-contained test case for your example? It would be nice to know whether there are any new bugs appearing in your example or whether this is a repeat of the previously-reported ones.

[Heather Macbeth]

This work is just as important as porting!

[Shreyas Srinivas]

I have a guess : lean3 zify looks for all norm_cast lemmas ( guess based on the line in the tactic def(z2, p2) ← norm_cast.derive_push_cast extra_lems z1,).

lean4 zify doesn't seem to include norm_cast lemmas for some reason.

[Shreyas Srinivas]

A large number of lemmas in Data.Int.Cast... seem to be tagged with norm_cast.

[Shreyas Srinivas]

all the coe_... lemmas in Data.Int.Basic also seem to be tagged with norm_cast including the ones I used

[Shreyas Srinivas]

I can't be 100% sure these lemmas are not being summoned indirectly somewhere else, but seeing as I had to apply them explicitly in lean4 while they were taken care of by lean3's zify, it seems like a reasonable guess.

[Shreyas Srinivas]

Here's a simplified example to debug zify:

import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.Zify
import Mathlib
import Mathlib.Data.Int.Cast.Basic
import Mathlib.Data.Int.Cast.Lemmas
variable (p : x ≤ 2*y)

-- works in lean 3
theorem attempt_1 : x * (2 * y - x) + (y ^ 2 + x ^ 2) = y * (2 * x + y) := by
  zify
  ring

theorem attempt_2: x * (2 * y - x) + (y ^ 2 + x ^ 2) = y * (2 * x + y) := by
  zify
  rw[Int.coe_nat_sub]
  ring

theorem attempt_3: x * (2 * y - x) + (y ^ 2 + x ^ 2) = y * (2 * x + y) := by
  zify
  rw[Int.coe_nat_sub]
  ring_nf!
  zify
  simp
  rw [Int.mul_assoc]
  simp
  apply p

[Shreyas Srinivas]

About the PR mathlib4#1644 :

1. There are 3 syntax errors in tactic code. I am not confident about debugging these parts.
2. There are 3 other errors : one error each with attributes @[mono], @[pp_nodot] and @[norm_num].
   2 a) @[mono] and @[pp_nodot] don't seem to be valid names (perhaps there are imports for these).
   2 b) @[norm_num] on some unsafe def which requires extra terms, probably the function that is being implemented.

[Heather Macbeth]

@[mono] is an attribute for a tactic mono that isn't implemented yet. Comment it and add a porting note.

The declaration tagged with @[norm_num] is a tactic. You can comment this whole section out (leave a porting note); eventually someone who knows how to write tactics will come along and port it.

[Shreyas Srinivas]

Oh okay. I will wrap this up in the morning. It is too late for me today. Thanks a lot for helping me out :)

[Heather Macbeth]

@Shreyas Srinivas I'm confused about the example that you say works in Lean 3. Here is my translation, which doesn't work (and wouldn't be expected to work, because of nat-subtraction issues). Did you perhaps over-simplify your example?

import tactic

theorem attempt_1 (x y : ℕ) :
  x * (2 * y - x) + (y ^ 2 + x ^ 2) = y * (2 * x + y) :=
begin
  zify,
  ring -- a goal remains
end

[Shreyas Srinivas]

I think apply p would cover it

[Shreyas Srinivas]

I did simplify it a bit

[Shreyas Srinivas]

I will check tomorrow

[Heather Macbeth]

The idea is to produce something which displays the bug in Lean 4, but whose exact translation to Lean 3 works fine. Sorry if I wasn't clear.

[Shreyas Srinivas]

import tactic

variable (p : x \leq 2*y)
theorem attempt_1 (x y : ℕ) :
  x * (2 * y - x) + (y ^ 2 + x ^ 2) = y * (2 * x + y) :=
begin
  zify,
  ring,
  apply p
end

[Shreyas Srinivas]

Edit: I didn't put that last line in because there are two goals after zify. Solving the equation is the first one and this is where the issue lies. The other goal is exactly p

[Heather Macbeth]

(deleted erroneous statement)

[Heather Macbeth]

I think this one is not actually a bug; rather, this is a mathlib3 feature of zify which hasn't been implemented yet. In mathlib4 zify as currently implemented, it seems you need to specify any hypotheses used to simplify a nat-subtraction, like zify [p]. This works in Lean 4:

import Mathlib.Tactic.Zify
import Mathlib.Tactic.Ring

variable (p : x ≤ 2*y)

theorem attempt_1 : x * (2 * y - x) + (y ^ 2 + x ^ 2) = y * (2 * x + y) := by
  zify [p]
  ring

[Heather Macbeth]

In the mathlib3 version it will find relevant hypotheses without you specifying them.

import tactic.zify
import tactic.ring

variables {x y : ℕ} (p : x ≤ 2*y)
include p

theorem attempt_1 : x * (2 * y - x) + (y ^ 2 + x ^ 2) = y * (2 * x + y) :=
begin
  zify,
  ring
end

[Heather Macbeth]

It might be worth opening a separate issue for this; it looks like the missing feature hasn't been noted before.

[Shreyas Srinivas]

The PR is on #queue4