Zulip Chat Archive

Stream: general

Topic: clearing all hypothesis


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.

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.

Kevin Buzzard (Apr 20 2019 at 22:26):

I am getting sick of

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

holes

Kevin Buzzard (Apr 20 2019 at 22:30):

ha ha I've got an algorithm

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.

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

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!

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.

Kevin Buzzard (Apr 20 2019 at 22:36):

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

Kevin Buzzard (Apr 20 2019 at 22:36):

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

Simon Hudon (Apr 20 2019 at 22:36):

As far as you know, no it doesn't

Kevin Buzzard (Apr 20 2019 at 22:37):

unknown identifier 'parse'

Kevin Buzzard (Apr 20 2019 at 22:37):

I'm not very good at meta

Kevin Buzzard (Apr 20 2019 at 22:37):

you have to spoonfeed me :-/

Simon Hudon (Apr 20 2019 at 22:37):

Give me a moment, I'll PR it

Simon Hudon (Apr 20 2019 at 22:43):

Just update mathlib to HEAD

Simon Hudon (Apr 20 2019 at 22:43):

Revision 9daa1a579fd86c537229c34a00a18a23fdad4db8

Kevin Buzzard (Apr 20 2019 at 22:52):

And now I have to compile mathlib manually, right?

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.

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.

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

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.

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.

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

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.

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

Simon Hudon (Apr 21 2019 at 00:37):

Are you suggesting we put it into core?

Mario Carneiro (Apr 21 2019 at 00:42):

that or make a clear'

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

Mario Carneiro (Apr 21 2019 at 00:43):

they should all be backward compatible afaik

Simon Hudon (Apr 21 2019 at 00:43):

I agree with the latest statement.

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?

Mario Carneiro (Apr 21 2019 at 00:47):

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

Mario Carneiro (Apr 21 2019 at 00:48):

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

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

Simon Hudon (Apr 21 2019 at 00:52):

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

Simon Hudon (Apr 21 2019 at 00:52):

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

Mario Carneiro (Apr 21 2019 at 00:54):

btw this notation exactly matches the coq tactic iirc

Mario Carneiro (Apr 21 2019 at 00:54):

what about clear * - h1 h2?

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

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.

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

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: Dec 20 2023 at 11:08 UTC