Zulip Chat Archive

Stream: general

Topic: clearing all hypothesis


view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:23):

I want to focus on one of five subgoals. I do this using an inelegant combination of swaps and sorrys. Once I am there, at the heart of the matter, I realise that my context is gigantic; I don't think I'll be using add_left_neg any more, for example.
Is there a command which just clears as much of the context as it is possible to do? I have come to an interesting sub-question and I want to see better what's going on.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:24):

/--
`clear h₁ ... hₙ` tries to clear each hypothesis `hᵢ` from the local context.
-/
meta def clear : parse ident*  tactic unit :=
tactic.clear_lst

Can I use this tactic somehow? I don't speak meta.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:26):

I am getting sick of

clear tactic failed, hypothesis 'zero_add' depends on 'add_assoc'

holes

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:30):

ha ha I've got an algorithm

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:31):

  clear right_distrib left_distrib add_comm add_zero add_assoc add,

found by switching view to the weird ctrl-shift-alt-enter "info view" which I never use, and then just clearing the first thing it complained about as well. This is getting through it nicely.

view this post on Zulip Simon Hudon (Apr 20 2019 at 22:32):

Feel free to use: https://github.com/avigad/qpf/blob/97befa73d34ed26137dbb991941d5ce1b1a3e794/src/for_mathlib.lean#L614-L618

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:35):

  show (zero_1 = zero),
  -- refl still fails
  clear add_left_neg, -- only 20 more to go
  clear zero_add,
  clear right_distrib left_distrib add_comm add_zero add_assoc add,
  clear neg,
  clear mul_one one_mul mul_assoc mul,
  clear one,
  clear add_zero_1 add_left_neg_1 zero_add_1 add_assoc_1 add_1,
  /-
  clear tactic failed, hypothesis 'add_left_neg_1' depends on 'add_zero_1'

  dammit my algo failed!
  -/
end

Dammit my algo just failed!

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:35):

meta def clear_except (xs : parse ident *) : tactic unit :=
do let ns := name_set.of_list xs,
   local_context >>= mmap' (λ h : expr,
     when (¬ ns.contains h.local_pp_name) $
try $ tactic.clear h)  list.reverse

Simon's tactic.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:36):

I don't understand a word of it, but let's give it a go

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:36):

It doesn't delete all my files, does it?

view this post on Zulip Simon Hudon (Apr 20 2019 at 22:36):

As far as you know, no it doesn't

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:37):

unknown identifier 'parse'

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:37):

I'm not very good at meta

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:37):

you have to spoonfeed me :-/

view this post on Zulip Simon Hudon (Apr 20 2019 at 22:37):

Give me a moment, I'll PR it

view this post on Zulip Simon Hudon (Apr 20 2019 at 22:43):

Just update mathlib to HEAD

view this post on Zulip Simon Hudon (Apr 20 2019 at 22:43):

Revision 9daa1a579fd86c537229c34a00a18a23fdad4db8

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:52):

And now I have to compile mathlib manually, right?

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:52):

You have given me an assembly manual for your new tool, and now I have to build it myself.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:53):

I've learnt a lot more about git recently. The perfectoid project has taught me a lot about teamwork.

view this post on Zulip Simon Hudon (Apr 20 2019 at 22:54):

:) yeah, unfortunately, being on the bleeding edge means you have to do more work yourself. You can also wait until it gets into the nightly build

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:55):

I don't mind compiling. I am only just beginning to realise that it's much better for you to make a PR than it is to start posting code here. it's easier for both you and me.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 22:56):

you get a preliminary version up and running at your end, throw out a new branch and I can get it, compile, and test it. It's all just dawning on me really, how all this stuff works.

view this post on Zulip Simon Hudon (Apr 20 2019 at 23:02):

I find it really interesting how important it is to learning to write very large proofs to learn to just use the tools effectively

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 23:03):

We're 11000 lines in and are running into technical issues with the typeclass system; debugging these instances is, for me, the best way of understanding them; it's better than just asking. I am finally learning to find my own way around Lean.

view this post on Zulip Mario Carneiro (Apr 21 2019 at 00:36):

I like the idea of clear_except, but it would be nice if it can be written clear - h1 h2

view this post on Zulip Simon Hudon (Apr 21 2019 at 00:37):

Are you suggesting we put it into core?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 00:42):

that or make a clear'

view this post on Zulip Mario Carneiro (Apr 21 2019 at 00:42):

Actually maybe that's a thing we can do on the community fork now... update all the core tactics to match the primed versions

view this post on Zulip Mario Carneiro (Apr 21 2019 at 00:43):

they should all be backward compatible afaik

view this post on Zulip Simon Hudon (Apr 21 2019 at 00:43):

I agree with the latest statement.

view this post on Zulip Simon Hudon (Apr 21 2019 at 00:43):

The thing with the clear - h idea is: does clear h - h' mean anything? Should it mean something?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 00:47):

the thing after clear is a list of names so it's not a problem

view this post on Zulip Mario Carneiro (Apr 21 2019 at 00:48):

I was thinking only clear h1 h2 or clear - h1 h2

view this post on Zulip Mario Carneiro (Apr 21 2019 at 00:49):

clear h - h' doesn't really mean anything not expressible with one of the other two options

view this post on Zulip Simon Hudon (Apr 21 2019 at 00:52):

And if you want to clear everything, you write clear - which I don't like

view this post on Zulip Simon Hudon (Apr 21 2019 at 00:52):

Maybe we could have a tactic called clear_all and add options clear_all - h0 h1

view this post on Zulip Mario Carneiro (Apr 21 2019 at 00:54):

btw this notation exactly matches the coq tactic iirc

view this post on Zulip Mario Carneiro (Apr 21 2019 at 00:54):

what about clear * - h1 h2?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 00:56):

also there is another predicate I can imagine saying which isn't expressible: clear everything except for x and the hypotheses that depend on x

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 02:35):

Oh, clear_except works really well for me! Thank you Simon -- you are a master tool maker when it comes to things like this.

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 02:37):

A tactic state with over 30 hypotheses became

A : Huber_pair,
v : (Spa A),
zero zero_1 : ring_completion (valuation_field (out (v.val)))
 zero_1 = zero

view this post on Zulip Simon Hudon (Apr 21 2019 at 02:37):

I cheated: I've been using it for over a year so I had some time to improve it


Last updated: May 11 2021 at 22:14 UTC