Zulip Chat Archive

Stream: general

Topic: tidy


view this post on Zulip Patrick Massot (Aug 28 2018 at 18:56):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Sep 18 2018 at 15:44):

At least the version merged in Orsay didn't

view this post on Zulip Reid Barton (Sep 18 2018 at 15:58):

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

view this post on Zulip Patrick Massot (Sep 18 2018 at 15:58):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 18 2018 at 16:12):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 20 2018 at 10:48):

This is terrible naming!

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 20 2018 at 10:50):

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

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Sep 20 2018 at 12:21):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 20 2018 at 13:00):

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

view this post on Zulip Mario Carneiro (Sep 20 2018 at 13:01):

or @[back] and @[back?]

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 13:22):

unfolding real numbers should be tagged untidy

view this post on Zulip Scott Morrison (Oct 30 2018 at 20:39):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Oct 30 2018 at 20:41):

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

view this post on Zulip Scott Morrison (Oct 30 2018 at 20:41):

I wonder if there is a useful line to draw.

view this post on Zulip 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!)

view this post on Zulip 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.

view this post on Zulip 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..

view this post on Zulip 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*.

view this post on Zulip Scott Morrison (Oct 31 2018 at 13:12):

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

view this post on Zulip Sebastien Gouezel (Oct 31 2018 at 13:53):

Thanks!

view this post on Zulip 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

view this post on Zulip Scott Morrison (Oct 31 2018 at 22:29):

I can just rewrite that proof.

view this post on Zulip Scott Morrison (Oct 31 2018 at 22:30):

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

view this post on Zulip Scott Morrison (Oct 31 2018 at 22:30):

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

view this post on Zulip Scott Morrison (Oct 31 2018 at 22:30):

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

view this post on Zulip 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.

view this post on Zulip 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 ;-)

view this post on Zulip Floris van Doorn (Oct 31 2018 at 22:48):

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

view this post on Zulip Scott Morrison (Nov 01 2018 at 10:45):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Nov 01 2018 at 10:48):

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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Nov 01 2018 at 11:16):

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

view this post on Zulip Scott Morrison (Nov 01 2018 at 11:37):

Thanks! I will investigate that.

view this post on Zulip 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

Perhaps this is a dead-end.

view this post on Zulip 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.

view this post on Zulip 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? :-)

view this post on Zulip 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 ℝ

view this post on Zulip Chris Hughes (Nov 01 2018 at 21:46):

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

view this post on Zulip 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 ).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?

view this post on Zulip 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

view this post on Zulip Chris Hughes (Nov 02 2018 at 23:18):

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

view this post on Zulip Chris Hughes (Nov 02 2018 at 23:18):

proof_irrel _ _ works though

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 02 2018 at 23:20):

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

view this post on Zulip Chris Hughes (Nov 02 2018 at 23:20):

That doesn't work.

view this post on Zulip Mario Carneiro (Nov 02 2018 at 23:21):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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,
   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

view this post on Zulip Mario Carneiro (Nov 02 2018 at 23:35):

adding to_ring := by apply_instance there simplifies the generated term

view this post on Zulip Mario Carneiro (Nov 02 2018 at 23:35):

does that fix the issue?

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Nov 02 2018 at 23:44):

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

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Nov 02 2018 at 23:53):

No, just real

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 02 2018 at 23:57):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 03 2018 at 00:00):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 00:00):

well, that's the same thing

view this post on Zulip Kevin Buzzard (Nov 03 2018 at 00:00):

I mean you can switch it on when you need it

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 03 2018 at 11:21):

what about

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

view this post on Zulip Chris Hughes (Nov 03 2018 at 11:23):

Breaks a lot of proofs in real.basic

view this post on Zulip Chris Hughes (Nov 03 2018 at 11:26):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 11:35):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 11:43):

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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Nov 03 2018 at 11:55):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 11:57):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:00):

Typeclass unfolding should never be opaque, this causes problems

view this post on Zulip Chris Hughes (Nov 03 2018 at 12:13):

That seems to fix everything.

view this post on Zulip Chris Hughes (Nov 03 2018 at 12:15):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:24):

we construct the reals, forget the construction and axiomatize

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:25):

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

view this post on Zulip Chris Hughes (Nov 03 2018 at 12:27):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:27):

that's not good

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:27):

they should be "above" the construction

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:28):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 12:28):

oh man

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:28):

that's out the window if you axiomatize

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:29):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:30):

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

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:30):

this is why I say defeq breaks abstractions

view this post on Zulip Mario Carneiro (Nov 03 2018 at 12:31):

it's bad practice to rely on definitional details

view this post on Zulip 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 (-;

view this post on Zulip 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.

view this post on Zulip 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⟩

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 05 2020 at 14:26):

Probably speed

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 05 2020 at 14:31):

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

view this post on Zulip Johan Commelin (Jun 05 2020 at 14:31):

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

view this post on Zulip 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 :)

view this post on Zulip Reid Barton (Jun 05 2020 at 14:38):

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

view this post on Zulip Sam Lichtenstein (Jun 05 2020 at 14:40):

let me #mwe-ify it

view this post on Zulip 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.

view this post on Zulip 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?!)

view this post on Zulip Sam Lichtenstein (Jun 05 2020 at 14:45):

i think that caused the timeout

view this post on Zulip Sam Lichtenstein (Jun 05 2020 at 14:45):

oh nvm
it's still timing out with tidy

view this post on Zulip 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 : 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

view this post on Zulip Reid Barton (Jun 05 2020 at 14:46):

what's the state when tidy gives up?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Jun 05 2020 at 17:52):

What happens if you squeeze_simp?

view this post on Zulip Yury G. Kudryashov (Jun 05 2020 at 17:53):

I think that some simp lemma is missing

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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