## 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.

#### 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 neg,
clear mul_one one_mul mul_assoc mul,
clear one,
/-

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

#### 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: May 11 2021 at 22:14 UTC