low level tactics

Stream: Is there code for X?

[Paige Thomas]

Is there a tactic that does nothing but expand notation? If not, how could that be done?

[Ruben Van de Velde]

set_option pp.notation false?

[Edward van de Meent]

if by notation you mean abbrev (and possibly def), using a tactic like dsimp might be what you're looking for

[Paige Thomas]

I was thinking along the lines of the ++ in

example
  {α : Type}
  (l : List α) :
  [] ++ l = l :=

[Paige Thomas]

And the lowest level set of tactics (tactics that do the least amount of work) that would solve this.

[Paige Thomas]

To make the proof as explicit as possible.

[Ruben Van de Velde]

Do you mean specifically "what does the HAppend instance for this type do"?

[Kyle Miller]

rfl should prove that one

[Paige Thomas]

I wanted to avoid rfl, because I think it does things I want to make explicit.

[Paige Thomas]

Ruben Van de Velde said:

Do you mean specifically "what does the HAppend instance for this type do"?

maybe? I didn't even know about HAppend until I tried the suggested set_option pp.notation false.

[Edward van de Meent]

you can hover over the term in the infoview to see what the notation means

[Edward van de Meent]

at that point, you typically can do some kind of dsimp only [HAppend.hAppend] (or whatever is the head term here) to simplify/reduce

[Paige Thomas]

Does dsimp unfold the definition like delta and nothing more?

[Edward van de Meent]

i did not know about delta, i think that indeed is a better tactic for the occasion.

[Edward van de Meent]

dsimp can do more, but it still guarantees that the result is defeq to the input. (afaict delta does this too)

[Paige Thomas]

If I did this

example
  {α : Type}
  (l : List α) :
  List.append [] l = l :=
  by
    delta List.append

α : Type
l : List α
⊢ List.brecOn (motive := fun x => List α → List α) []
    (fun x f x_1 =>
      (match (motive := (x : List α) → List α → List.below (motive := fun x => List α → List α) x → List α) x, x_1 with
        | [], r => fun x => r
        | a :: l, r => fun x => a :: x.fst.fst r)
        f)
    l =
  l

Is there a tactic that would only apply the match and not close the goal?

[Paige Thomas]

So that I would end up with l = l, by definition of the match?

[Kyle Miller]

This fact is immediate from the definition of List.append though. You can apply the equation lemma that's auto-generated from the definition:

example
  {α : Type}
  (l : List α) :
  [] ++ l = l :=
  List.append.eq_1 l

[Kyle Miller]

If you are using mathlib, you could use unfold_projs to unfold ++ to the underlying function.

example
  {α : Type}
  (l : List α) :
  [] ++ l = l := by
  unfold_projs  -- unfold (reduce) the `HAppend.hAppend` instance.
  -- ⊢ [].append l = l
  unfold List.append -- use the equation lemma
  -- ⊢ l = l
  rfl

[Kyle Miller]

delta unfolds to the underlying term, and it doesn't use equation lemmas or "smart unfolding". Regarding your question, you could use reduce from mathlib to get l = l. You can also use dsimp only, but it will see that the result is l = l and automatically close the goal with rfl.

[Kyle Miller]

reduce will unfold definitions though, just like rfl, so if you're wanting to very carefully control reduction, you shouldn't use it:

example
  {α : Type}
  (l : List α) :
  [] ++ l = l := by
  reduce
  -- ⊢ l = l
  rfl

[Kyle Miller]

You can take a look at docs#Lean.Meta.DSimp.Config to see all the things you can configure dsimp to do. Configuration options go inside the {} in dsimp (config := {}) only.

[Paige Thomas]

Kyle Miller said:

If you are using mathlib, you could use unfold_projs to unfold ++ to the underlying function.

example
  {α : Type}
  (l : List α) :
  [] ++ l = l := by
  unfold_projs  -- unfold (reduce) the `HAppend.hAppend` instance.
  -- ⊢ [].append l = l
  unfold List.append -- use the equation lemma
  -- ⊢ l = l
  rfl

This is exactly what I was looking for.

[Paige Thomas]

Thank you!

[Paige Thomas]

What are "projections of class instances at the given location" in the doc for unfold_projs?

[Paige Thomas]

Is there a way to do this, but not have it close the goal, but instead end up with a :: as.append bs = a :: as.append bs? I'm guessing being inside the conv makes it close it?

lemma List.cons_append
  {α : Type}
  (a : α)
  (as bs : List α) :
  (a::as) ++ bs = a::(as ++ bs) := by
  unfold_projs
  conv => left; unfold List.append

[Kyle Miller]

Recall that [] ++ l is notation for @HAppend.hAppend (List α) (List α) (List α) inst [] l, where inst stands for the HAppend instance for List α. The hAppend function is a projection for the hAppend field of HAppend. That's to say, this is inst.hAppend [] l. The unfold_projs tactic expands inst and gets the hAppend field out. This reduces it to List.append [] l after two steps (there's also an Append instance).

[Kyle Miller]

Yeah, conv closes goals using with_reducible rfl

[Paige Thomas]

Is there a way to make it not do that, or an alternative similar tactic that won't?

[Kyle Miller]

No, I don't believe so. You'd have to make your own.

Can you instead use a sequence of change tactics? Trying to unfold things like this using tactics is fairly artificial for Lean, and you'll be fighting against many tactics to never do rfl or auto-solve other trivial goals.

[Kyle Miller]

I'm imagining something like

lemma List.cons_append'
    {α : Type}
    (a : α)
    (as bs : List α) :
    (a::as) ++ bs = a::(as ++ bs) := by
  change (a :: as).append bs = a :: as.append bs
  change a :: as.append bs = a :: as.append bs
  rfl

[Paige Thomas]

It would be great if there were more lower level/finer grained tactics.

[Paige Thomas]

Maybe starting with one for each application of the typing rules, and building up.

[Paige Thomas]

I think it might help make some things clearer, at least for me.

[Paige Thomas]

I don't know if maybe it would also help with translating between other proof systems?

[Kevin Buzzard]

I wouldn't need such tactics because I just want to get goals closed. But if they're useful for what you're doing then lean 4 makes them pretty easy to write

[Paige Thomas]

I started looking at how to do that.