Data.Real.CauSeq

Stream: mathlib4

[Moritz Doll]

I have a problem with rw being stupid:
https://github.com/leanprover-community/mathlib4/blob/mcdoll/data_real_causeq/Mathlib/Data/Real/CauSeq.lean#L435
https://github.com/leanprover-community/mathlib4/blob/mcdoll/data_real_causeq/Mathlib/Data/Real/CauSeq.lean#L467
The first one is very weird: it should be a trivial application of mul_apply, but even when giving mul_apply all arguments it cannot find (a * b) n.

[Kevin Buzzard]

Are there errors earlier in the file for you?

[Moritz Doll]

yes, but they are very unrelated.

[Moritz Doll]

replacing all broken proofs by sorry's does not help

[Kevin Buzzard]

I replaced all broken proofs with sorry up to instance ring : Ring (CauSeq β abv) := by and for me this has an error (unknown tactic for refine_struct) and because this is the definition of the ring structure this might be the problem with the CommRing structure. Are you 100% sure that the problem is not the earlier errors? Can you post a version with no errors other than the ones you're interested in? I'm on your branch.

[Moritz Doll]

pushed

[Moritz Doll]

(have to go and make dinner, feel free to push fixes)

[Eric Wieser]

I have a mathlib3 PR that removes the use of refine_struct there, if that's useful

[Eric Wieser]

#17796

[Patrick Massot]

@Moritz Doll please tell us whether Eric's mathlib3 PR would make your mathlib4 life easier. If yes then we can merge the mathlib3 PR today and then we'll have to run mathport again.

[Moritz Doll]

the diff does not say that it removes anything in CauSeq

[Kevin Buzzard]

Are you honestly sure that the problem with a multiplication not being defeq to another multiplication is not related to the fact that you have sorried the ring structure?

[Kevin Buzzard]

I don't understand these things well enough so I might be worrying about nothing.

[Moritz Doll]

if the PR gets merged, ping me and I merge in the new mathport version into my mathlib4-PR

[Kevin Buzzard]

The issue is that one multiplication uses CauSeq.instMulCauSeq and the other does not.

[Eric Wieser]

the diff does not say that it removes anything in CauSeq

Fixed

[Moritz Doll]

that is great - is it possible to remove the ring refine_struct as well?

[Kevin Buzzard]

The other uses src✝ which uses CauSeq.ring which uses sorry

[Patrick Massot]

Sorrying data in structures is a very well-known way of creating a lot of hard to debug mess down the road.

[Patrick Massot]

So Kevin's explanation seems very likely.

[Kevin Buzzard]

One multiplication uses

instance : Mul (CauSeq β abv) :=
  ⟨fun f g =>
    ⟨f * g, fun _ ε0 =>
      let ⟨_, _, hF⟩ := f.bounded' 0
      let ⟨_, _, hG⟩ := g.bounded' 0
      let ⟨_, δ0, Hδ⟩ := rat_mul_continuous_lemma abv ε0
      let ⟨i, H⟩ := exists_forall_ge_and (f.cauchy₃ δ0) (g.cauchy₃ δ0)
      ⟨i, fun j ij =>
        let ⟨H₁, H₂⟩ := H _ le_rfl
        Hδ (hF j) (hG i) (H₁ _ ij) (H₂ _ ij)⟩⟩⟩

and the other uses

instance ring : Ring (CauSeq β abv) := by sorry

and this is why the rewrite fails right now.

[Moritz Doll]

Kevin Buzzard said:

The issue is that one multiplication uses CauSeq.instMulCauSeq and the other does not.

you are right.

[Eric Wieser]

Moritz Doll said:

that is great - is it possible to remove the ring refine_struct as well?

Done. Is Algebra.Ring.Pi ported yet? docs4#Pi.instRing?

[Eric Wieser]

Seems not; my suggestion would be to port Algebra.Ring.Pi first, and then by the time you're done my PR could be through

[Patrick Massot]

No it isn't ported yet.

[Patrick Massot]

Eric, can I assume the data/real folder compile on your branch?

[Eric Wieser]

Not as of the last two commits, because I only just authored them

[Patrick Massot]

I mean: does it compile on your computer?

[Eric Wieser]

I can try for you now?

[Patrick Massot]

I'm not talking about compiling the whole mathlib, only those two files.

[Eric Wieser]

Oh, so not the whole data/real folder, just data/real/basic?

[Eric Wieser]

data/real/basic.lean and its dependencies compile on that branch

[Eric Wieser]

Note that we seem to be missing Algebra.Group.Pi as well as Algebra.Ring.Pi

[Patrick Massot]

Ok, it is very unlikely that build will fail later so I told bors to merge.

[Eric Wieser]

Thanks!

[Patrick Massot]

Now you can port those two Pi files while waiting for the merge :wink:

[Eric Wieser]

I'm going to pretend/assume that was aimed at @Moritz Doll!

[Patrick Massot]

Moritz is having dinner now.

[Eric Wieser]

Group.Pi landed in mathlib4#1088

[Eric Wieser]

And GroupAction.Pi landed in mathlib4#1115; so I think it really is just one file

[Moritz Doll]

I can port Algebra.Ring.Pi tomorrow if nobody does it before me.
As for the errors, did something change about extending structures from Lean 3 to Lean 4? If a type has a Mul and an Add instance, then a sorried out Ring instance should not skrew up proofs without any good error messages.
Probably I just never encountered this in Lean 3.

[Kevin Buzzard]

There has definitely been a change in how instance synthesis works in Lean 4 v Lean 3, because if you set pp.all to true then in Lean 4 you get monster monster terms which we never had in Lean 3 -- stuff like LinearOrder.toPartialOrder.toPreorder.toLE.

[Kevin Buzzard]

The first a * b is

@HMul.hMul.{?u.91695, ?u.91695, ?u.91695}
      (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
      (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
      (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
      (@instHMul.{?u.91695} (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
        (@NonUnitalNonAssocSemiring.toMul.{?u.91695}
          (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
          (@NonUnitalSemiring.toNonUnitalNonAssocSemiring.{?u.91695}
            (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
            (@Semiring.toNonUnitalSemiring.{?u.91695}
              (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
              (@Ring.toSemiring.{?u.91695}
                (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
                (@Ring.mk.{?u.91695} (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
                  (@Ring.toSemiring.{?u.91695}
                    (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv) src✝)
                  (@Ring.toNeg.{?u.91695}
                    (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv) src✝)
                  (@Ring.toSub.{?u.91695}
                    (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv) src✝)
                  (@Ring.sub_eq_add_neg.{?u.91695}
                    (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv) src✝)
                  (@Ring.zsmul.{?u.91695}
                    (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv) src✝)
                  (@Ring.zsmul_zero'.{?u.91695}
                    (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv) src✝)
                  (@Ring.zsmul_succ'.{?u.91695}
                    (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv) src✝)
                  (@Ring.zsmul_neg'.{?u.91695}
                    (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv) src✝)
                  (@Ring.add_left_neg.{?u.91695}
                    (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv) src✝)
                  (@Ring.toIntCast.{?u.91695}
                    (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv) src✝)
                  (@Ring.intCast_ofNat.{?u.91695}
                    (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv) src✝)
                  (@Ring.intCast_negSucc.{?u.91695}
                    (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv) src✝)))))))
      a b

and the second is

@HMul.hMul.{?u.91695, ?u.91695, ?u.91695}
      (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
      (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
      (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
      (@instHMul.{?u.91695} (@CauSeq.{?u.91476, ?u.91695} α inst✝³ β (@CommRing.toRing.{?u.91695} β inst✝) abv)
        (@CauSeq.instMulCauSeq.{?u.91476, ?u.91695} α β inst✝³ (@CommRing.toRing.{?u.91695} β inst✝) abv i))
      a b

[Kevin Buzzard]

The first one traces Mul back up to the sorried Ring instance even though the Mul is already there. The second one catches the Mul you already defined -- this is @CauSeq.instMulCauSeq.

[Sky Wilshaw]

I was looking at porting Algebra.Ring.Pi yesterday, I think it required (a mathlib4 version of) tactic.pi_instances, which I don't think has been ported.

[Kevin Buzzard]

tactic#pi_instances

[Eric Wieser]

Eric Wieser said:

I have a mathlib3 PR that removes the use of refine_struct there, if that's useful

I have a similar PR that removes the use for real.comm_ring at #8146, although I expect that might have build issues

[Moritz Doll]

I encountered a new and weird problem, namely that I have lots of casts that seem to be not defeq and there are no simp-lemmas for them. I have no time to work on that until the 25th, so if anyone that knows how casts in the algebraic hierachy work, please have a look at this mess:
https://github.com/leanprover-community/mathlib4/pull/1124/files#diff-18f1434dcab7d38fad2c5144ab5f653c1eef55b9d1d49d20951e556af4ad0317R432
(I've added a few definitions and lemmas that probably should not exist, but otherwise I had no idea what was going on)

[Moritz Doll]

the natCast in AddGroupWithOne was previously fun n => const n

[Eric Wieser]

Can we get the mathlib 4 CI to show errors inline like mathlib 3 does?

[Eric Wieser]

theorem natCast_eq' {n m : ℕ} :
    @Nat.cast (ℕ → β) NonAssocRing.toNatCast n m = (n : β) := by
  simp
  sorry

looks like docs4#Pi.NonAssocRing was ported incorrectly

[Eric Wieser]

theorem natCast_eq' {n m : ℕ} :
    @Nat.cast (ℕ → β) NonAssocRing.toNatCast n m = (n : β) := by
  simp
  sorry

looks like docs4#Pi.NonAssocRing was ported incorrectly

[Eric Wieser]

Oh. The docs are not up to date :(

[Eric Wieser]

(bad wifi. Sorry for double post)

[Eric Wieser]

mathlib4#1185 should fix this

[Patrick Massot]

Do you understand why mathlib3 didn't hit this issue?

[Eric Wieser]

Yes, because we broke the file in the port. It was not broken in mathlib3

[Eric Wieser]

(The reason is that in mathlib3 we implemented things with a tactic that doesn't exist in mathlib4)

[Eric Wieser]

I suppose the safe way to handle this is to backport the removal of the tactic first (to make sure everything works), then do a regular port

[Patrick Massot]

I guess the most efficient way is to merge your fix but then think about backporting the removal of pi_instance in files that are sufficient far away from the rising tide.

[Eric Wieser]

This should be unblocked again

[Moritz Doll]

I've merged master (and your fix is definitively in there), but it did not fix the issue

[Moritz Doll]

it seems there are other instances where we have defeq problems

[Eric Wieser]

docs#Pi.addMonoidWithOne is to blame, it also wasn't ported correctly

[Eric Wieser]

Default arguments are dangerous because if we forget to port them, we get the wrong thing instead of an error

[Eric Wieser]

mathlib4#1197

[Moritz Doll]

thanks so much.

[Moritz Doll]

That does fix the errors

[Reid Barton]

Dumb question: why is this in a different place than in mathlib 3?

[Reid Barton]

Ad-hoc thingy?

[Reid Barton]

https://github.com/leanprover-community/mathlib/blob/master/src/data/nat/cast/basic.lean#L255

[Reid Barton]

mathlib4#1088

[Reid Barton]

So there is still https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Nat/Cast/Basic.lean#L284 as well; is this good/bad?

[Eric Wieser]

Reid Barton said:

Dumb question: why is this in a different place than in mathlib 3?

Floris van Doorn suggested this in a previous thread

[Eric Wieser]

Reid Barton said:

So there is still https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Nat/Cast/Basic.lean#L284 as well; is this good/bad?

I guess bad, let me rewrite to use that but it's not imported yet for me to use

[Eric Wieser]

"messy" is probably more accurate than "bad"

[Reid Barton]

Can we get a porting note about how this instance was moved? Moving instances is always tricky, because of their implicit nature

[Moritz Doll]

there seems to be one error left which probably also comes from a diamond: sub_add_sub_cancel times out on l592 in
https://github.com/leanprover-community/mathlib4/pull/1124/files#diff-18f1434dcab7d38fad2c5144ab5f653c1eef55b9d1d49d20951e556af4ad0317R592
My guess was that the Sub instance is somehow bad and I replaced it by the analogue of the Add instance, but that did not help, so I am suspecting that the Pi-stuff is to blame again.

[Eric Wieser]

You're probably right

[Eric Wieser]

docs4#Pi.addGroup

[Eric Wieser]

Looks ok to me

[Eric Wieser]

You can use the infoview to debug the diamond and tactics like dsimp [Pi.addGroup] etc

[Eric Wieser]

It's apparent we need a linter to check that we don't define WeakInstance Foo and StrongInstance Foo in a way that causes a diamond

[Eric Wieser]

Or we remove all the default-valued fields so that this doesn't happen in the first place

[Moritz Doll]

I've used set_option pp.all true and that is a huge mess, but without that I cannot see anything useful in the infoview. I haven't considered dsimp

[Eric Wieser]

You can use the widgets in the infoview instead of pp.all

[Eric Wieser]

You want to find where the instances come from (by clicking on -) and unfold them until you see a default coming from somewhere

[Eric Wieser]

I had a quick look and nothing jumped out as obvious

[Eric Wieser]

The usual approach of using convert _ using 1 times out

[Eric Wieser]

I pushed a commit that gets it to as simple as possible a case where exact sub fails

[Eric Wieser]

Ah, fixed!

[Eric Wieser]

I think this is just a Lean4 unification problem

[Eric Wieser]

For whatever reason, rw [some_lemma] failed but exact some_lemma.symm worked

[Eric Wieser]

It's pretty scary that this fails in such a confusing way

[Moritz Doll]

that sounds like a bug to me. The rw should clearly not fail if all the instances are fine.

[Eric Wieser]

My hunch is that we actually need to define the Pi instances more like

instance Pi.group'{I : Type u}{f : I → Type v} [∀ i, Group <| f i] : Group (∀ i : I, f i) :=
  { Pi.divInvMonoid with
    mul := Mul.mul
    div := Div.div
    inv := Inv.inv
    one := One.one
    zpow := fun z x i => x i ^ z
    --pi_instance
    mul_left_inv := by intros; ext; exact mul_left_inv _
    }

that is, copy over all the data fields manually in ways such that the inner operators unify differently

[Eric Wieser]

We effectively do this in Mathlib3, and the port dropped this; I've run into problems in Lean3 in the past where this helped

[Eric Wieser]

branch4#eric-wieser/test-pi-instances is hitting timeouts when I try to do the above, which suggests to me this might indeed be the fix

[Eric Wieser]

In particular,

instance commRing [∀ i, CommRing <| f i] : CommRing (∀ i : I, f i) :=
  { Pi.ring, Pi.commSemiring with
    zero := Zero.zero
    mul := Mul.mul
    one := One.one
    sub := Sub.sub
    add := Add.add }

times out

[Eric Wieser]

Which looks a bit like @Kevin Buzzard's frame/coframe problem

[Kevin Buzzard]

Eric Wieser said:

My hunch is that we actually need to define the Pi instances more like

instance Pi.group'{I : Type u}{f : I → Type v} [∀ i, Group <| f i] : Group (∀ i : I, f i) :=
  { Pi.divInvMonoid with
    mul := Mul.mul
    div := Div.div
    inv := Inv.inv
    one := One.one
    zpow := fun z x i => x i ^ z
    --pi_instance
    mul_left_inv := by intros; ext; exact mul_left_inv _
    }

that is, copy over all the data fields manually in ways such that the inner operators unify differently

Does this suggestion "go against new structures"? I would be interested in hearing the views of the people who properly understand why the switch to new structures is important. @Floris van Doorn ?

[Kevin Buzzard]

Note that also that Pi was not the only very slow instance in that complete lattice file. Here I give three examples of super-speedup hacks, and only one involves Pi.

[Kevin Buzzard]

I'm finding these things difficult to minimise because as I slim down the questions the timeouts get shorter. I replace a bunch of proofs with sorrys and a five second declaration goes down to two seconds. The actual time taken in the mathlib file is horrible. One could easily switch to my slick constructions in the link above and leave a porting note but my guess is that this is going to keep happening and I've seen situations where the data needed to feed to mk is not to hand; we're lucky in the linked examples.

By the way I don't know how to switch the profiler on, but I would love to report something of the form "elaboration of this declaration took n heart beats on lean version blah, which was about 5 seconds on my new fast machine".

[Eric Wieser]

I don't think this goes against new style structures necessarily. The conflict is between "a pi type has multiplication because it is a monoid because every fibre is a monoid" and "a pi type has multiplication because every fibre has multiplication because every fibre is a monoid". These are defeq, but tricky to unify and this only gets worse the more typeclass paths there are (eg for Ring)

[Kevin Buzzard]

Another thing which would be nice would be a machine which de-mathlibiffied my examples because the code in the issue I opened https://github.com/leanprover/lean4/issues/1986 took ages for me to write -- for example notation is getting complex and notation3 is in mathlib and I don't really understand the code so stripping it out was hard for me. Also there is this crazy bug I run into in VS Code where jump to definition will sometimes jump to a file which is not imported, which is really confusing. Feels a bit like the issue where if you change a file you import and write to disc, Lean4 doesn't auto-reload. Also difficult to minimise -- stuff is just broken and you kill all Lean process and restart VS Code and it usually fixes itself.

[Chris Hughes]

This PR is now ready for review

[Eric Wieser]

Let's make sure to update the porting comments before merging