A clear tactic that doesn't care about dependency order

Stream: new members

[Jannis Limperg]

I wrote a small wrapper around clear that can clear multiple hypotheses which depend on each other and don't need to be specified in dependency order. So the following succeeds where clear fails:

variables (α : Type) (β : α → Type) (γ : ∀ a, β a → Type)

lemma test (a) (b : β a) (c : γ a b) : unit :=
  begin
    smart_clear a b c,
    exact (),
  end

Does this already exist somewhere? (I did it mostly to learn about Lean metaprogramming, so didn't look for it much.)

(Also hi, first time posting here.)

[Kevin Buzzard]

Did you PR it? I occasionally get irritated by this :-)

[Patrick Massot]

Yes, please PR that. I guess this should be clear', following the standard convention to name fixes to the core library tactics.

[Mario Carneiro]

Why not just have clearing a also clear b and c? I kind of thought this was how clear already worked

[Patrick Massot]

This is definitely not how clear works.

[Patrick Massot]

But this is certainly how I would like it to work.

[Johan Commelin]

@Jannis Limperg Wow! That's a really nice first post! I'm looking forward to your next posts (-; Welcome!
And yes, please contribute this to mathlib.

[Reid Barton]

This is how revert works

[Jannis Limperg]

Thank you for the warm welcome. I'll polish the code a bit more and submit a PR.

Wrt whether we should be able to write just clear a in my example: I'd consider this too much magic, but if you all want it, I can implement that as well. Coq's clear dependent works like this. (Coq's clear works like my smart_clear.)

[Reid Barton]

maybe clear! a, for the equivalent of clear dependent?

[Jannis Limperg]

PR: https://github.com/leanprover-community/mathlib/pull/1899 (without clear! for now).

[Johan Commelin]

@Jannis Limperg awesome. Thanks! I made a minor comment on style.

[Johan Commelin]

E.g., you indent too much. For the test I suggest:

example {α : Type} {β : α → Type} (a : α) (b : β a) : true :=
begin
  clear' a b,
  -- clear would fail since `b` depends on `a`
  trivial
end

[Jannis Limperg]

@Johan Commelin Thanks, I've fixed the indentation.

I also have an implementation of clear! now (thanks to Simon Hudon). However, clear! doesn't seem to be a legal name. Is there any way to enable this notation?

[Rob Lewis]

clear should be a single tactic that parses an optional !. There are various tactics you can look at to see how to do this, e.g. set.

[Jannis Limperg]

Oh okay, makes sense. Thanks!

[Johan Commelin]

@Jannis Limperg I've never actually written a tactic myself, but I was wondering: can you use things like guard_hyp in your tests, to guarantee that the context looks the way you want?

[Jannis Limperg]

Looks like it. I wasn't aware of this family of tactics, but I should be able to use them to make the tests more meaningful. Will do. (Also, I just discovered some format macros that I can probably use.)

[Reid Barton]

Yeah clear! won't exactly work, because clear is a tactic defined in the core library

[Rob Lewis]

Oh, right. This should be a drop-in replacement for clear, right? Maybe it should be a PR to 3.5c replacing the old one?

[Rob Lewis]

I'll have time next week to look into migrating mathlib officially to 3.5c.

[Kevin Buzzard]

clear'!?

[Rob Lewis]

clear'?!

[Jannis Limperg]

@Johan Commelin I've made the tests more accurate, per your suggestion. Thanks again!

Wrt the name: I think I'll just keep clear_dependent. clear'! is too ugly, and nondescript to boot.

Wrt improving the builtin clear instead: This would certainly be preferable. However, I'm not sure that my current implementation is robust enough to go into the stdlib. It's a bit of a hack (using revert under the hood) and I don't have the necessary experience with Lean tactics to judge what might go wrong. (For example, many tactics seem to have logic related to goal tags which I don't understand.) Ideally, the C++ for clear would be changed to use the revert logic, but I don't dare to go near that.

[Mario Carneiro]

I think clear'! is better, because the tick represents a todo to fix the builtin tactic for the next version of lean

[Mario Carneiro]

I don't see a problem with using revert. The goal tags thing is so that you can use the case tactic. It isn't very important that tactics preserve this unless you want to do processing between induction and case