Stream: general

Topic: tidy

Patrick Massot (Aug 28 2018 at 18:56):

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

Kevin Buzzard (Aug 28 2018 at 19:00):

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

Reid Barton (Sep 18 2018 at 15:40):

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

Patrick Massot (Sep 18 2018 at 15:44):

At least the version merged in Orsay didn't

Reid Barton (Sep 18 2018 at 15:58):

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

Patrick Massot (Sep 18 2018 at 15:58):

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

Keeley Hoek (Sep 18 2018 at 16:05):

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

Reid Barton (Sep 18 2018 at 16:12):

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

Reid Barton (Sep 18 2018 at 16:29):

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 (Sep 18 2018 at 20:25):

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 (Sep 19 2018 at 01:09):

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 (Sep 19 2018 at 01:09):

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

Scott Morrison (Sep 19 2018 at 01:10):

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 (Sep 20 2018 at 10:48):

@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 (Sep 20 2018 at 10:48):

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

Scott Morrison (Sep 20 2018 at 10:48):

This is terrible naming!

Scott Morrison (Sep 20 2018 at 10:49):

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 (Sep 20 2018 at 10:50):

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

Simon Hudon (Sep 20 2018 at 12:20):

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

Simon Hudon (Sep 20 2018 at 12:21):

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

Scott Morrison (Sep 20 2018 at 12:26):

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 (Sep 20 2018 at 13:00):

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

Mario Carneiro (Sep 20 2018 at 13:01):

or @[back] and @[back?]

Reid Barton (Sep 20 2018 at 13:17):

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 (Sep 20 2018 at 13:22):

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 (Sep 20 2018 at 13:28):

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 (Oct 30 2018 at 13:11):

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 (Oct 30 2018 at 13:22):

unfolding real numbers should be tagged untidy

Scott Morrison (Oct 30 2018 at 20:39):

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

Scott Morrison (Oct 30 2018 at 20:40):

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

Scott Morrison (Oct 30 2018 at 20:41):

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

Scott Morrison (Oct 30 2018 at 20:41):

I wonder if there is a useful line to draw.

Scott Morrison (Oct 30 2018 at 20:43):

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 (Oct 30 2018 at 20:44):

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 (Oct 31 2018 at 07:14):

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 (Oct 31 2018 at 10:08):

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 (Oct 31 2018 at 13:12):

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

Thanks!

Scott Morrison (Oct 31 2018 at 22:29):

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 (Oct 31 2018 at 22:29):

I can just rewrite that proof.

Scott Morrison (Oct 31 2018 at 22:30):

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

Scott Morrison (Oct 31 2018 at 22:30):

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

Scott Morrison (Oct 31 2018 at 22:30):

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

Scott Morrison (Oct 31 2018 at 22:31):

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

Kevin Buzzard (Oct 31 2018 at 22:42):

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 (Oct 31 2018 at 22:48):

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

Scott Morrison (Nov 01 2018 at 10:45):

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

Scott Morrison (Nov 01 2018 at 10:46):

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 (Nov 01 2018 at 10:48):

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

Chris Hughes (Nov 01 2018 at 11:13):

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 (Nov 01 2018 at 11:16):

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

Scott Morrison (Nov 01 2018 at 11:37):

Thanks! I will investigate that.

Scott Morrison (Nov 01 2018 at 12:25):

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


Chris Hughes (Nov 01 2018 at 12:27):

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 (Nov 01 2018 at 12:28):

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 (Nov 01 2018 at 21:29):

@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 (Nov 01 2018 at 21:46):

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

Chris Hughes (Nov 02 2018 at 23:14):

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 ℝ).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 (Nov 02 2018 at 23:16):

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 (Nov 02 2018 at 23:18):

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

Chris Hughes (Nov 02 2018 at 23:18):

proof_irrel _ _ works though

Chris Hughes (Nov 02 2018 at 23:19):

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

Mario Carneiro (Nov 02 2018 at 23:20):

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

Chris Hughes (Nov 02 2018 at 23:20):

That doesn't work.

Mario Carneiro (Nov 02 2018 at 23:21):

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

Chris Hughes (Nov 02 2018 at 23:25):

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

Mario Carneiro (Nov 02 2018 at 23:28):

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

Chris Hughes (Nov 02 2018 at 23:31):

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

Mario Carneiro (Nov 02 2018 at 23:33):

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,
zero := discrete_field.zero α (normed_field.to_discrete_field α),
neg := discrete_field.neg (normed_field.to_discrete_field α),
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 (Nov 02 2018 at 23:35):

adding to_ring := by apply_instance there simplifies the generated term

Mario Carneiro (Nov 02 2018 at 23:35):

does that fix the issue?

Chris Hughes (Nov 02 2018 at 23:44):

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

Chris Hughes (Nov 02 2018 at 23:44):

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

Mario Carneiro (Nov 02 2018 at 23:53):

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 (Nov 02 2018 at 23:53):

No, just real

Mario Carneiro (Nov 02 2018 at 23:56):

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 (Nov 02 2018 at 23:57):

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

Mario Carneiro (Nov 02 2018 at 23:59):

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 (Nov 03 2018 at 00:00):

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

Mario Carneiro (Nov 03 2018 at 00:00):

well, that's the same thing

Kevin Buzzard (Nov 03 2018 at 00:00):

I mean you can switch it on when you need it

Mario Carneiro (Nov 03 2018 at 00:01):

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 (Nov 03 2018 at 00:01):

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 (Nov 03 2018 at 00:01):

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

Reid Barton (Nov 03 2018 at 00:11):

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 (Nov 03 2018 at 11:17):

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 (Nov 03 2018 at 11:21):

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


Chris Hughes (Nov 03 2018 at 11:23):

Breaks a lot of proofs in real.basic

Chris Hughes (Nov 03 2018 at 11:26):

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

Mario Carneiro (Nov 03 2018 at 11:35):

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

Chris Hughes (Nov 03 2018 at 11:40):

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

Mario Carneiro (Nov 03 2018 at 11:43):

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

Chris Hughes (Nov 03 2018 at 11:52):

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 (Nov 03 2018 at 11:55):

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

Mario Carneiro (Nov 03 2018 at 11:57):

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

Mario Carneiro (Nov 03 2018 at 11:58):

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 (Nov 03 2018 at 11:59):

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 (Nov 03 2018 at 12:00):

Typeclass unfolding should never be opaque, this causes problems

Chris Hughes (Nov 03 2018 at 12:13):

That seems to fix everything.

Chris Hughes (Nov 03 2018 at 12:15):

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

Mario Carneiro (Nov 03 2018 at 12:23):

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 (Nov 03 2018 at 12:24):

we construct the reals, forget the construction and axiomatize

Mario Carneiro (Nov 03 2018 at 12:25):

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 (Nov 03 2018 at 12:25):

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

Chris Hughes (Nov 03 2018 at 12:27):

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

that's not good

Mario Carneiro (Nov 03 2018 at 12:27):

they should be "above" the construction

Chris Hughes (Nov 03 2018 at 12:28):

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

Mario Carneiro (Nov 03 2018 at 12:28):

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

oh man

Mario Carneiro (Nov 03 2018 at 12:28):

that's out the window if you axiomatize

Mario Carneiro (Nov 03 2018 at 12:29):

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

Chris Hughes (Nov 03 2018 at 12:30):

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 (Nov 03 2018 at 12:30):

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

Mario Carneiro (Nov 03 2018 at 12:30):

this is why I say defeq breaks abstractions

Mario Carneiro (Nov 03 2018 at 12:31):

it's bad practice to rely on definitional details

Johan Commelin (Nov 03 2018 at 12:32):

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 (Nov 03 2018 at 13:44):

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

Scott Morrison (Nov 06 2018 at 04:32):

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 (Jun 05 2020 at 14:26):

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

Probably speed

Sam Lichtenstein (Jun 05 2020 at 14:27):

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 (Jun 05 2020 at 14:31):

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

Johan Commelin (Jun 05 2020 at 14:31):

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

Sam Lichtenstein (Jun 05 2020 at 14:37):

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

Reid Barton (Jun 05 2020 at 14:38):

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

Sam Lichtenstein (Jun 05 2020 at 14:40):

let me #mwe-ify it

Reid Barton (Jun 05 2020 at 14:43):

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 (Jun 05 2020 at 14:44):

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 (Jun 05 2020 at 14:45):

i think that caused the timeout

Sam Lichtenstein (Jun 05 2020 at 14:45):

oh nvm
it's still timing out with tidy

Sam Lichtenstein (Jun 05 2020 at 14:45):

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 : module R (R^⊕ι) := {..@finsupp.module ι R R _ _ _}

lemma equiv_of_bijection {μ : Type*} (h : ι ≃ μ) : R^⊕ι ≃ₗ[R] R^⊕μ :=
{ to_fun := finsupp.map_domain h.to_fun,
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 (Jun 05 2020 at 14:46):

what's the state when tidy gives up?

Sam Lichtenstein (Jun 05 2020 at 14:47):

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 (Jun 05 2020 at 14:49):

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

Yury G. Kudryashov (Jun 05 2020 at 17:52):

What happens if you squeeze_simp?

Yury G. Kudryashov (Jun 05 2020 at 17:53):

I think that some simp lemma is missing

Sam Lichtenstein (Jun 06 2020 at 22:59):

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 (Jun 06 2020 at 23:02):

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

Sam Lichtenstein (Jun 06 2020 at 23:10):

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.

Last updated: May 12 2021 at 23:13 UTC