tidy

Stream: general

[Patrick Massot]

tidy has been merged! :tada: :tada: :tada:

[Kevin Buzzard]

Mathlib is looking in really good shape at the minute. Many unmerged things are either WIPs or very new.

[Reid Barton]

@Scott Morrison does mathlib's tidy not contain "backwards reasoning"? Or am I just not seeing it?

[Patrick Massot]

At least the version merged in Orsay didn't

[Reid Barton]

I see. That throws a minor :wrench: in my continuity plans, but nothing too serious

[Patrick Massot]

Actually I'm curious to know why we got that nerfed tidy

[Keeley Hoek]

@Reid Barton not Scott but that's currently still chilling out in https://github.com/semorrison/lean-tidy/tree/master/src/tidy

[Reid Barton]

Thanks Keeley!
Patrick, I wonder too. It looks like backwards_reasoning is fairly simple.

[Reid Barton]

In particular I'm not sure whether I should try to PR backwards_reasoning into mathlib, or roll my own version to use in continuity

[Scott Morrison]

No, it's not there yet. It wasn't necessary for the early parts of the
category theory library, so I took it out just to reduce the initial PR
footprint.

[Scott Morrison]

I agree it would be good to get in soon. It was written before ext was available, and the appearance of ext took away a lot of the need for the "more aggressive" backwards_reasoning.

[Scott Morrison]

I think it would be worth rewriting backwards_reasoning one more time, looking to see what we can share with ext.

[Scott Morrison]

I'm trying to catch up on non-Lean life this week, so if someone wants to go ahead with a PR, please do, otherwise I'll do it "soon".

[Scott Morrison]

@Reid Barton, @Patrick Massot (et al.)
I've found there a two types of lemmas one frequently wants to apply backwards reasoning with. The "strong" variety are just lemmas that you always want to apply whenever they match. There's also a "weak" variety where you want to make sure that any hypotheses of the lemma can be immediately discharged from hypotheses.

[Scott Morrison]

In my first implementation of backwards_reasoning, I introduced two attributes @[back] and @[back'] for labelling the strong and weak cases.

[Scott Morrison]

This is terrible naming!

[Scott Morrison]

But I'm unsure what the right way to handle this is. Any suggestions welcome, and I'll get on with a backwards_reasoning PR.

[Scott Morrison]

(I've decided my limits PR may be painful without having backwards_reasoning available.)

[Simon Hudon]

How about @[backward] and @[strong_back]? Also, do you have an example of the kind of proof it does?

[Simon Hudon]

You could also go with @[backward strong] and @[backward weak] with weak being the default?

[Scott Morrison]

I'll (eventually) prepare some examples; at the moment everything I have is invisible, because tidy is just doing it in secret. :-) I think actually strong should be the default --- for lemmas that are "safe" to always apply, whereas weak is the more dangerous "you can apply this, but you have to be careful you can actually immediately solve all new goals" setting.

[Mario Carneiro]

How about @[back!] and @[back]?

[Mario Carneiro]

or @[back] and @[back?]

[Reid Barton]

I would just comment that the "safe"/"unsafe" terminology can be confusing--if you mark something as "safe" when it's safe to apply and "unsafe" otherwise then it's "more safe" (i.e., more likely to be correct/sound) to mark something as "unsafe" than as "safe".

[Reid Barton]

For example the Haskell FFI uses safe/unsafe in the opposite sense from your terminology: unsafe is used to mark a function which is called "unsafely" (without any special setup/teardown), which means it had better be a function which is "safe" to call from any context (e.g., sin). safe means that the RTS will prepare a safe context from which to call the function, so it's safe to import most functions as safe. I'm used to this naming convention but I know some people find it confusing.

[Reid Barton]

Back on topic, I'm not sure I have a good intuition for which lemmas should fall into either of these two categories.

[Sebastien Gouezel]

Is there a way to tell tidy that is should never unfold something, possibly with some attribute? Whenever there are real numbers involved, it unfolds them to Cauchy sequences. For instance,

lemma foo {x : ℝ} : 0 ≤ x :=
begin
  tidy,
  sorry
end

gives a goal of the form

x_val : ℕ → ℚ,
x_property : is_cau_seq abs x_val
⊢ 0 ≤ quot.mk setoid.r ⟨x_val, x_property⟩

[Kevin Buzzard]

unfolding real numbers should be tagged untidy

[Scott Morrison]

Ugh, that is bad. :-) I'll admit I've never touched a real number in Lean!

[Scott Morrison]

The problem is just that auto_cases applies first, and it, somewhat ridiculously, runs induction x immediately.

[Scott Morrison]

There are certainly cases where this _is_ helpful behaviour, on the other hand.

[Scott Morrison]

I wonder if there is a useful line to draw.

[Scott Morrison]

One dumb solution is to just remove induction on quotients from auto_cases entirely, and have users of tidy explicitly add back in a tactic that does this (e.g. the very blunt case_bash tactic I have somewhere, which just tries cases on everything!)

[Scott Morrison]

I suspect that the occasions where it makes sense to use induction on a quotient, the quotient relation is "very near at hand". But I'm having trouble thinking how to quantify/measure that.

[Sebastien Gouezel]

Is the induction on quotients often helpful? I mean, if you remove it from auto_cases, does it break something in your category library? If not, I guess it is safe to remove it. Otherwise, one would need a mechanism to fine tune it, maybe with some attributes..

[Scott Morrison]

It breaks exactly one thing, and clearly that doesn't justify the hassle caused elsewhere. I'll PR a one line change to auto_cases soon*.

[Scott Morrison]

Ok, I've PR'd this one-line change: https://github.com/leanprover/mathlib/pull/451

[Sebastien Gouezel]

Thanks!

[Scott Morrison]

Huh, it turns out someone else was using tidy in a way that relied on induction on quotients: https://travis-ci.org/leanprover/mathlib/jobs/448843966

[Scott Morrison]

I can just rewrite that proof.

[Scott Morrison]

An alternative would be to have auto_cases perform induction on "things that are explicitly quotients"

[Scott Morrison]

For one, this would include things that actually match quot _ or quotient _.

[Scott Morrison]

But for this use case I'd also want to to fire on quotient_module.quotient.

[Scott Morrison]

And it seems the only way to handle that would be to make decisions based on the _name_ itself.

[Kevin Buzzard]

Yes there's a huge difference between real numbers as quotient and quotient modules as quotients! I guess another fix would be to rewrite the real numbers as Dedekind cuts ;-)

[Floris van Doorn]

Or make real irreducible (after the file data.real.basic) and not unfold irreducible definitions?

[Scott Morrison]

Hmm, it seems making real irreducible doesn't work; lots of things fail.

[Scott Morrison]

e.g. rw div_mul_div at this producing:

/home/travis/build/leanprover/mathlib/data/real/irrational.lean:19:2: error: rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_3 / ?m_4 * (?m_5 / ?m_6)
state:
sqrt_two_irrational : irrational (sqrt 2)
n : ℤ
d : ℕ
h : d > 0
c : nat.coprime (int.nat_abs n) d
e : sqrt 2 = ↑n / ↑d
d0 : 0 < ↑d
this : ↑n / ↑d * (↑n / ↑d) = 2

[Scott Morrison]

I don't really understand how reducibility caused a problem there.

[Chris Hughes]

The issue is that this expression no longer type checks after real is made irreducible

example : @cau_seq.completion.has_mul ℚ _ ℚ _ abs _ =  (show has_mul ℝ, by apply_instance) :=

real.mul_self_sqrt uses cau_seq.completion.has_mul, so you end up with two has_mul's that are no longer reduced to the same thing.

[Chris Hughes]

Making cau_seq.completion irreducible instead might be a better idea.

[Scott Morrison]

Thanks! I will investigate that.

[Scott Morrison]

Hmm, making attribute [irreducible] cau_seq.completion.Cauchy (is that what you had in mind, @Chris Hughes?) seems to cause troubles later:

/Users/scott/projects/lean/mathlib/analysis/real.lean:185:29: error: type mismatch at application

Perhaps this is a dead-end.

[Chris Hughes]

I tried making real irreducible immediately after exists_sup and that seemed to work. Two proofs in analysis broke, but they were easy to fix.

[Scott Morrison]

Would you be interested in pursuing that to a PR? (Both because I think you'll do a better job at it that I would, and also I need to go to sleep? :-)

[Scott Morrison]

@Chris Hughes , it looks like something cropped up later:

/home/travis/build/leanprover/mathlib/analysis/bounded_linear_maps.lean:100:9: error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  normed_ring.to_ring ℝ
inferred
  domain.to_ring ℝ

[Chris Hughes]

I haven't managed to work out what's going on there.

[Chris Hughes]

Done some investigation. There's some weird behaviour going on.

example : (normed_ring.to_ring ℝ).zero = real.ring.zero := rfl --works
example : (normed_ring.to_ring ℝ).one = real.ring.one := rfl --works
example : (normed_ring.to_ring ℝ).mul = real.ring.mul := rfl --works
example : (normed_ring.to_ring ℝ).add = real.ring.add := rfl --works

example : (normed_ring.to_ring ℝ).add_comm = real.ring.add_comm := rfl --doesn't work
example : (normed_ring.to_ring ℝ).mul_assoc = real.ring.mul_assoc := rfl --doesn't work

Not quite sure why all the data is equal by rfl but none of the proofs. @Mario Carneiro, what's happening?

[Mario Carneiro]

I don't have the setup to test that myself right now, but if they are proofs then it should be an easy rfl, as long as the statement itself typechecks

[Chris Hughes]

They are proofs and the statement type checks and it isn't an easy rfl.

[Chris Hughes]

proof_irrel _ _ works though

[Chris Hughes]

The context is that I made real irreducible in case you hadn't caught up with the discussion

[Mario Carneiro]

is normed_ring.to_ring ℝ = real.ring doesn't work, I assume?

[Chris Hughes]

That doesn't work.

[Mario Carneiro]

How is the instance normed_ring ℝ defined? Is normed_ring an old style structure?

[Chris Hughes]

For reals it's derived from norm_field \R, which is a new style structure, as is normed_ring

[Mario Carneiro]

In that case, the normed_ring instance should literally include real.ring as the appropriate component in its definition

[Chris Hughes]

But that's doesn't really work, since it's defined from a general instance normed_field.to_normed_ring

[Mario Carneiro]

aha:

@[instance]
protected def normed_field.to_normed_ring : Π {α : Type u_1} [i : normed_field α], normed_ring α :=
λ {α : Type u_1} [i : normed_field α],
  {to_has_norm := normed_field.to_has_norm α i,
   to_ring := {add := discrete_field.add (normed_field.to_discrete_field α),
               add_assoc := _,
               zero := discrete_field.zero α (normed_field.to_discrete_field α),
               zero_add := _,
               add_zero := _,
               neg := discrete_field.neg (normed_field.to_discrete_field α),
               add_left_neg := _,
               add_comm := _,
               mul := discrete_field.mul (normed_field.to_discrete_field α),
               mul_assoc := _,
               one := discrete_field.one α (normed_field.to_discrete_field α),
               one_mul := _,
               mul_one := _,
               left_distrib := _,
               right_distrib := _},
   to_metric_space := normed_field.to_metric_space α i,
   dist_eq := _,
   norm_mul := _}

Apparently ..i unfolds the ring component unnecessarily

[Mario Carneiro]

adding to_ring := by apply_instance there simplifies the generated term

[Mario Carneiro]

does that fix the issue?

[Chris Hughes]

Yes. Thanks. I'm not sure if it's worth making reals irreducible if it generates this sort of problem however.

[Chris Hughes]

As in, I was hoping for a solution which only changed data.real.basic

[Mario Carneiro]

well, I think this is a bug in structure literals, but indeed even eta expanding real.ring should be defeq because it's a structure. Did you mark real.ring irreducible?

[Chris Hughes]

No, just real

[Mario Carneiro]

Oh, but then I think I can see how the problem arises... real.comm_ring expands to cau_seq.completion.comm_ring, which contains real internals in its type

[Mario Carneiro]

you should try changing the definition to real.comm_ring := {.. cau_seq.completion.comm_ring}

[Mario Carneiro]

local attribute [reducible] real

in real.lean is a real doozy. By marking it irreducible but locally reducible, you get terms that typecheck locally, which stop typechecking later

[Kevin Buzzard]

so you just put local attribute [irredible] real just afterwards, right?

[Mario Carneiro]

well, that's the same thing

[Kevin Buzzard]

I mean you can switch it on when you need it

[Mario Carneiro]

I think one principle we need is that any definition which would not typecheck in the current environment (because of irreducible markings) should itself be irreducible

[Reid Barton]

I was about to say: I haven't been following closely but I feel like we need a more principled approach to all this.

[Mario Carneiro]

In this case, real.comm_ring := cau_seq.completion.comm_ring does not typecheck once the definition of real is hidden

[Reid Barton]

I'm hopeful that the right irreducibility annotations will make the real numbers generally more pleasant to work with, but I would guess that tweaking annotations one by one is not the best way to get there. This feels related to enforcing abstraction boundaries, something Lean seems to have no capabilities for.

[Chris Hughes]

I tried this change instance : comm_ring ℝ := { ..cau_seq.completion.comm_ring }, but it has the same problem. I guess the proofs still don't type check.

[Mario Carneiro]

what about

@[irreducible] def real.comm_ring' : comm_ring ℝ := cau_seq.completion.comm_ring
instance : comm_ring ℝ := {.. real.comm_ring' }

[Chris Hughes]

Breaks a lot of proofs in real.basic

[Chris Hughes]

It seems like making things irreducible after proving things about them isn't really practical.

[Mario Carneiro]

you may have to do the same trickery with local reducible, global irreducible

[Chris Hughes]

That seems like a really bad idea, because then things that typechecked when I wrote them no longer typecheck

[Mario Carneiro]

that's why we're making the things that depend on irreducible things irreducible

[Chris Hughes]

Making real.comm_ring irreducible at the same time that real is made irreducible actually works. I can't do the same thing with discrete_field however, otherwise discrete_field.to_comm_ring or whatever, won't be equal to real.comm_ring

[Chris Hughes]

This fails now example : field.to_comm_ring ℝ = real.comm_ring := rfl

[Mario Carneiro]

you just have to make sure the right things end up opaque

[Mario Carneiro]

I think if you build another discrete_linear_ordered_field ℝ over top of real.comm_ring' and discrete_linear_ordered_field ℝ , and make the latter two opaque, you should be able to prove the unfolding

[Mario Carneiro]

Without abbreviating things, the longhand way to do this is to define terms zero : R, one : R, zero_add : zero + x = x etc, make them all opaque, and then build typeclasses on top of them

[Mario Carneiro]

Typeclass unfolding should never be opaque, this causes problems

[Chris Hughes]

That seems to fix everything.

[Chris Hughes]

It does seem like a slightly fragile solution, and that it might cause problems later on.

[Mario Carneiro]

In metamath we actually took a really hard line on making real opaque, which is weird since we don't do that anywhere else

[Mario Carneiro]

we construct the reals, forget the construction and axiomatize

[Mario Carneiro]

It's actually a nice and principled way to do it, because you can pick an appropriate axiomatization of the reals that you know to be complete (no pun intended)

[Mario Carneiro]

You don't need all the discrete field axioms, of course some of them are redundant

[Chris Hughes]

Now a whole load of rfl proofs have broken in complex.basic.

[Mario Carneiro]

that's not good

[Mario Carneiro]

they should be "above" the construction

[Chris Hughes]

They shouldn't be proved with rfl? It is nice that some things about reals are definitional.

[Mario Carneiro]

oh, shoot - I just remembered that some things are definitional like 0 + 0 = 0

[Kenny Lau]

oh man

[Mario Carneiro]

that's out the window if you axiomatize

[Mario Carneiro]

lol this is probably that bunch of simp proofs that kenny made rfl

[Chris Hughes]

I'm pretty sure it is that. I think the reason they weren't rfl in the first place, is because complex.basic was written with old reals.

[Mario Carneiro]

but I think that it is actually a bad idea to use rfl

[Mario Carneiro]

this is why I say defeq breaks abstractions

[Mario Carneiro]

it's bad practice to rely on definitional details

[Johan Commelin]

I like those claims. They are reassuring. I was getting used to thinking that I should care a lot about defeq. But now you make me think that I should stick to my mathematical habits (-;

[Chris Hughes]

I managed to fix everything. The problems were things like ((1 : nat) : real) = (1 : real) no longer being definitional.

[Scott Morrison]

Just reporting that @Chris Hughes's recent fixes to reducibility have solved @Sebastien Gouezel's original complaint:

Is there a way to tell tidy that is should never unfold something, possibly with some attribute? Whenever there are real numbers involved, it unfolds them to Cauchy sequences. For instance,

lemma foo {x : ℝ} : 0 ≤ x :=
begin
  tidy,
  sorry
end

gives a goal of the form

x_val : ℕ → ℚ,
x_property : is_cau_seq abs x_val
⊢ 0 ≤ quot.mk setoid.r ⟨x_val, x_property⟩

[Sam Lichtenstein]

Is there some reason tidy doesn't have tauto in its default list of things to try?

[Johan Commelin]

Probably speed

[Sam Lichtenstein]

usually tauto is pretty fast for me, whereas tidy seems to die with deterministic timeout rather than failing when tauto could have closed the goal.

[Johan Commelin]

You can locally mark it with the tidy attribute, to include it in the list.

[Johan Commelin]

But I guess it gets tagged onto the end of the list...

[Sam Lichtenstein]

I mean in this case the solution for me is just to use tauto instead of tidy :)

[Reid Barton]

What's an example that tauto solves where tidy gets stuck?

[Sam Lichtenstein]

let me #mwe-ify it

[Reid Barton]

If tauto works then using it is better, but I would have thought tidy tries most things that tauto does, so I'm a bit surprised. It could be that tidy goes down the wrong path using simp and can't recover, or something.

[Sam Lichtenstein]

aha my example was a non-example. I had a stray edit to one of the imports which I think lean was trying to recompile (even though I had not saved the imported file?!)

[Sam Lichtenstein]

i think that caused the timeout

[Sam Lichtenstein]

oh nvm
it's still timing out with tidy

[Sam Lichtenstein]

import linear_algebra.direct_sum_module
       linear_algebra.tensor_product
       linear_algebra.basis
       linear_algebra.finsupp_vector_space
       data.finsupp
       tactic

noncomputable theory
open_locale classical
universes u v w
variables (R : Type u) [comm_ring R]
variables (ι : Type*)

namespace module

def free := ι →₀ R
instance : has_coe_to_fun (free R ι) := finsupp.has_coe_to_fun

end module

notation R ` ^⊕ `:40 ι:66  := module.free R ι

namespace free

instance : add_comm_group (R^⊕ι)  := finsupp.add_comm_group
instance : module R (R^⊕ι) := {..@finsupp.module ι R R _ _ _}

lemma equiv_of_bijection {μ : Type*} (h : ι ≃ μ) : R^⊕ι ≃ₗ[R] R^⊕μ :=
{ to_fun := finsupp.map_domain h.to_fun,
  add := λ x y, finsupp.map_domain_add,
  smul := finsupp.map_domain_smul,
  inv_fun := λ x, finsupp.comap_domain h.to_fun x (by tidy),
  left_inv := sorry,
  right_inv := λ x, finsupp.map_domain_comap_domain h.to_fun x (by tidy)
              (by {have := equiv.surjective h, tidy})
              -- (by {have := equiv.surjective h, tauto})
              }
#check equiv_of_bijection right_inv

end free

[Reid Barton]

what's the state when tidy gives up?

[Sam Lichtenstein]

1 goal
R : Type u,
_inst_1 : comm_ring R,
ι : Type u_1,
μ : Type u_2,
h : ι ≃ μ,
x : R ^⊕ μ,
this : function.surjective ⇑h
⊢ ↑(x.support) ⊆ set.range h.to_fun

[Sam Lichtenstein]

of course I was also a bit surprised I had to help with have := equiv.surjective h

[Yury G. Kudryashov]

What happens if you squeeze_simp?

[Yury G. Kudryashov]

I think that some simp lemma is missing

[Sam Lichtenstein]

How do I see what simp tried when it fails to simplify? The only trick I know is set_option trace.simplify.rewrite true but that doesn't yield an information trace when simp fails AFAICT.

[Bryan Gin-ge Chen]

set_option trace.simplify true. It's mentioned near the top of this page on simp.

[Sam Lichtenstein]

Yeah, so I think tracing simp is not so useful for diagnosing tidy's timeout here -- it just shows a gazillion rewrites that simp tried but that don't work. This isn't surprising since to close the goal you do need to use the surjectivity of h here, which isn't just a term rewrite.