clearing all hypothesis

Stream: general

[Kevin Buzzard]

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]

/--
`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]

I am getting sick of

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

holes

[Kevin Buzzard]

ha ha I've got an algorithm

[Kevin Buzzard]

  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]

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

[Kevin Buzzard]

  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]

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]

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

[Kevin Buzzard]

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

[Simon Hudon]

As far as you know, no it doesn't

[Kevin Buzzard]

unknown identifier 'parse'

[Kevin Buzzard]

I'm not very good at meta

[Kevin Buzzard]

you have to spoonfeed me :-/

[Simon Hudon]

Give me a moment, I'll PR it

[Simon Hudon]

Just update mathlib to HEAD

[Simon Hudon]

Revision 9daa1a579fd86c537229c34a00a18a23fdad4db8

[Kevin Buzzard]

And now I have to compile mathlib manually, right?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Simon Hudon]

:) 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]

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]

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]

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]

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]

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

[Simon Hudon]

Are you suggesting we put it into core?

[Mario Carneiro]

that or make a clear'

[Mario Carneiro]

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]

they should all be backward compatible afaik

[Simon Hudon]

I agree with the latest statement.

[Simon Hudon]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Mario Carneiro]

btw this notation exactly matches the coq tactic iirc

[Mario Carneiro]

what about clear * - h1 h2?

[Mario Carneiro]

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]

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]

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]

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