Pattern matching lambda body in conv

Stream: lean4

[Tomas Skrivan]

It seems that pattern matching on lambda body in conv does not seem to be working in this case:

def test : (λ x : Nat => id (id x)) = λ x => x := by
  conv in (id _) =>      --- error: 'pattern' conv tactic failed, pattern was not found
    simp

Why is the pattern failing here?

[Mac]

@Tomas Skrivan I am not very familiar with conv mode so the term 'pattern matching' may mean something different there. But usually in Lean, you can only pattern match on constructors or functions with the @[matchPattern] attribute. id is neither so I would not expect the pattern to work.

[Tomas Skrivan]

It is described as pattern matching in the doc - https://leanprover.github.io/theorem_proving_in_lean4/conv.html

For example, if you do

def test : id (λ x : Nat => id (id x)) = λ x => x := by
  conv in (id _) =>   .  -- the goal here is: id fun x => id (id x)

It correctly matches the lhs .

[Tomas Skrivan]

Also pattern (f _) seems to have trouble matching f x y i.e. the pattern needs to have all applied arguments in it. I had similar issue with simp tactic before and that got fixed.

Example:

def test2 : (Function.comp id id) = λ x : Nat => x := by
  conv in (Function.comp _) =>      --- error: 'pattern' conv tactic failed, pattern was not found
    simp

pattern Function.comp _ _ works as expected

[Leonardo de Moura]

@Tomas Skrivan I pushed fixes for the issues above.

[Leonardo de Moura]

@Mac Yeah, "pattern matching" is a bit overloaded :sweat_smile: The "pattern" here is not referring to a match-expression pattern.

[Tomas Skrivan]

@Leonardo de Moura Thank you very much!

[Tomas Skrivan]

Works great! However, it does not work with let as I would expect:

def test : (λ x => x)
           =
           (λ x : Nat =>
             let foo := λ y => id (id y)
             foo x) := by
  conv =>
    pattern (id _)
    .

After pattern (id _) the goal is:

let foo := fun y => id (id y);
  foo x

I would expect it to be id (id y).

Also focusing on the definition of foo just by spelling out foo would be nice. Something like pattern (let foo := _)

---

A bit unrelated, enter and pattern zooms in on a subexpression. Is there a command to jump back? Maybe allowing conv block inside of another conv block?

Also, I would find useful to pattern on the inner most occurrence of the pattern.

[Sebastian Ullrich]

Tomas Skrivan said:

A bit unrelated, enter and pattern zooms in on a subexpression. Is there a command to jump back? Maybe allowing conv block inside of another conv block?

You can nest steps in { ... } to delimit their scope. But allowing conv => with the same meaning sounds sensible to me.

[Tomas Skrivan]

How am I supposed to use { ... }? I was using it in Lean 3, but in Lean 4 it never does what I would expect.

Example of unexpected behavior:

def twice : Nat → Nat := λ n => 2*n

def test : (λ x : Nat => id (twice (id x))) = twice := by
  conv in (id _) =>
    . --- Goal: id (twice (id x))
    { enter [1,1]; simp }
    .  -- Here I would expect the goal to be `id (twice x)`, but I'm getting `goals accomplished`

[Sebastian Ullrich]

Ah, then I was mistaken about their use

[Tomas Skrivan]

In order to focus on the inner most pattern I would expect that this would(almost) do it:

repeat {pattern (id _); enter [1]}

but it does not. The problem is probably that repeat tries to apply rfl tactic at the end, but I would expect it to do nothing at the end.

[Tomas Skrivan]

Ok, I do not understand curly braces, but the above repeat kind of works with normal braces(or even without them)

repeat pattern (id _); enter [1]

However, it creates bunch of goals, one for each repeat.

Similarly, repeat (ext x) creates goals f x, f x1 x, f x2 x1 x, ... until all arguments of f are exhausted. I want just one goal with fully applied f.

[Tomas Skrivan]

Interesting, repeat actually works as expected but it presents goals in an odd way. Placing cursor at the end of repeat rw [thrm] shows the goal after only one transformation of rw [thrm]. However, when you move further it will show the actual goal after many rewrites. Because of this reason, I have no used repeat for couple of weeks now as I though that it is not doing what I want.

Also, I think repeat in conv should not call tactic => rfl at the end but it should preform no operation. One way to do it is to call tactic' => skip, but I'm not sure if it is really "no operation" tactic.

An example of these behaviors:

namespace Lean.Parser.Tactic.Conv

  macro "no_op" : conv => `(tactic' => skip)

  syntax "repeat' " convSeq : conv
  macro_rules
    | `(conv| repeat' $seq) => `(conv| first | ($seq); repeat' $seq | no_op)

end Lean.Parser.Tactic.Conv

def repeat_ext : (λ x y z : Nat => x + y + z) = (λ x y z : Nat => 0) :=
by
  conv =>
    lhs
    repeat' (ext x)  -- Cursor here shows 4 goals
    no_op            -- Cursor here shows the one expected goal

  . -- Looks like that exiting `conv` invokes `rfl` automatically. So this line fails if the theorem is actually provable by `rfl`, as there will be no more goals.

  admit

Using repeat instead of repeat' will show goals accomplished when the cursor is on no_op.

When exiting the conv block, the tactic rfl(maybe simp?) is called. So if the right hand side is (λ x y z : Nat => x + y +z) the line with . fails as all goals have been solved. I understand that this is useful behavior when proving theorems, but I'm experimenting with tactic mode to write/rewrite programs and I need a fine control over when I want to finish the rewriting process.

[Tomas Skrivan]

Another thing, with the recent fix to pattern it looks like that if the pattern is not present the tactic does not fail but it does nothing. This might be undesirable when it is used in repeat as that relies on tactic failing. I have not yet run into problems with this though, just surprised that it actually terminates.

[Tomas Skrivan]

Concerning the issue from jumping back from enter and pattern. I propose adding enter*, pattern*, arg* that creates two goals, the first goal zooms in on a subexpression and the second one is the original expression with the modified subexpression.

[Mario Carneiro]

Rather than a modifier on all those tactics, that sounds like a sequencing primitive. Do ; and blocks not already work?

[Tomas Skrivan]

@Mario Carneiro I have tried different combinations of {}, blocks and ; but never got the result I expected.

[Mario Carneiro]

what about conv => as a conv tactic?

[Tomas Skrivan]

It is not there by default, I do not know how to define it. I have tried this:

syntax "conv => " convSeq : conv
macro_rules
  | `(conv | conv => $seq) => `(conv | $seq)

but it does not even compile and I doubt it would work.

[Mario Carneiro]

Oh, it's defined in mathport but I guess that one was skipped

[Mario Carneiro]

Here's a demonstration of the lean 3 equivalent tactic:

import tactic
theorem foo (y : ℕ) : (λ x, x + y = 0) = (λ x, false) :=
begin
  conv {
    -- | (λ (x : ℕ), x + y = 0) = λ (x : ℕ), false
    conv {
      -- | (λ (x : ℕ), x + y = 0) = λ (x : ℕ), false
      to_lhs,
      -- | λ (x : ℕ), x + y = 0
      funext,
      -- | x + y = 0
      rw [add_comm],
      -- | y + x = 0
    },
    -- | (λ (x : ℕ), y + x = 0) = λ (x : ℕ), false
  },
  -- ⊢ (λ (x : ℕ), y + x = 0) = λ (x : ℕ), false
end

[Tomas Skrivan]

And where is convConv defined? I grepped the repo and and the only occurrence of convConv is in that Syntax.lean file.

[Mario Carneiro]

@Leonardo de Moura could you add conv => as a conv tactic, like the above?

[Mario Carneiro]

It's not defined in mathport, only declared as syntax

[Leonardo de Moura]

Mario Carneiro said:

Leonardo de Moura could you add conv => as a conv tactic, like the above?

@Mario Carneiro I will do it later this week. I am currently in "slide deck" building mode :sweat_smile:

[Leonardo de Moura]

Tomas Skrivan said:

Works great! However, it does not work with let as I would expect:

def test : (λ x => x)
           =
           (λ x : Nat =>
             let foo := λ y => id (id y)
             foo x) := by
  conv =>
    pattern (id _)
    .

After pattern (id _) the goal is:

let foo := fun y => id (id y);
  foo x

I would expect it to be id (id y).

Also focusing on the definition of foo just by spelling out foo would be nice. Something like pattern (let foo := _)

---

A bit unrelated, enter and pattern zooms in on a subexpression. Is there a command to jump back? Maybe allowing conv block inside of another conv block?

Also, I would find useful to pattern on the inner most occurrence of the pattern.

I pushed a fix for this issue.

[Leonardo de Moura]

Leonardo de Moura said:

Mario Carneiro said:

Leonardo de Moura could you add conv => as a conv tactic, like the above?

Mario Carneiro I will do it later this week. I am currently in "slide deck" building mode :sweat_smile:

I added the conv => as a conv tactic.