Use proof in custom tactic

Stream: lean4

[Marcus Rossel]

I'm trying to write a tactic that obtains a proof of some statement and then uses that proof to apply a lemma.
As an example:

theorem some_lemma {n : Nat} (h : n = 5) : n ≠ 10 := sorry

open Lean Elab.Tactic in
elab (name := solveNEq10) "solveNEq10" : tactic => do
  ...
  let h : n = 5 := sorry
  evalTactic (← `(tactic|exact some_lemma $h)) -- ?

The solveNEq10 should solve a a goal of the form n ≠ 10. It's able to obtain a proof of n = 5 and is supposed to use the some_lemma with that fact. I can't figure out how to actually use h here though.
So far I've only used evalTactic which works using Syntax. Is that appropriate here, or are there other mechanisms I should be using?

[Mario Carneiro]

How does the let h : n = 5 := sorry part work? It is mixing meta levels: I would expect something more like

elab (name := solveNEq10) "solveNEq10" : tactic => do
  ...
  evalTactic (← `(tactic| (
    let h : n = 5 := sorry
    exact some_lemma h)))

[Marcus Rossel]

Mario Carneiro said:

How does the let h : n = 5 := sorry part work? It is mixing meta levels: I would expect something more like

elab (name := solveNEq10) "solveNEq10" : tactic => do
  ...
  evalTactic (← `(tactic| (
    let h : n = 5 := sorry
    exact some_lemma h)))

I guess I'll have to explain my real world project a bit more for this. Like in lean4-maze I'm defining a game that is played by proving that a level (an instance of Game) is completable (using a sequence of moves):

structure Game where ...

inductive Move | up | down | left | right

-- Performing a move can fail!
def Game.move : Game → Move → Option Game := ...

inductive Game.completable : Game → Prop
  | completed {g} : <completion conditions> → completable g
  | move {g₁ g₂ : Game} {m} : (g₁.move m = some g₂) → completable g₂ → completable g₁

let level1 : Game := ...

theorem level1_completable : level1.completable := by
  move Move.up -- This move tactic is what I'm trying to define.
  move Move.left
  ...

I'm now trying to define the move tactic, such that it:

1. Gets the Game instance (let's call it g) for which we're trying to prove g.completable.
2. Performs the move (let's call it m) that was passed to the tactic: let g? := g.move m.
3. If the move was invalid (g? = Option.none), fails.
4. If the move was successful (g? = some g'), use this fact (this is the h from before) to apply Game.completable.move.

The remaining goal would then require us to prove the remaining condition for Game.completable.move, which is to show that g' is also completable.

I don't see how to do this in "pure syntax", since I wouldn't know how to get hold of g and hence let g? := g.move m.

[Sebastian Ullrich]

What's wrong with doing apply Game.completable.move (m := Move.up) rfl inside the quotation? It should succeed iff move Move.up evaluates to some _. If you want a nicer error message on failure, you can additionally evaluate move outside of the quotation as you apparently planned to do, but these two move invocations are otherwise independent. Because of proof irrelevance, it is not directly possible to reflect a proof back into syntax, i.e. we cannot implement Quote p for p : Prop.

[Marcus Rossel]

Sebastian Ullrich said:

What's wrong with doing apply Game.completable.move (m := Move.up) rfl inside the quotation? It should succeed iff move Move.up evaluates to some _. If you want a nicer error message on failure, you can additionally evaluate move outside of the quotation as you apparently planned to do, but these two move invocations are otherwise independent. Because of proof irrelevance, it is not directly possible to reflect a proof back into syntax, i.e. we cannot implement Quote p for p : Prop.

If I do:

open Lean Elab.Tactic in
elab (name := move) "move " m:term : tactic => do
  evalTactic (← `(tactic| apply Game.completable.move (m := $m) rfl))

def level1 : Game := ...

theorem level1_completable : level1.completable := by
  move Move.up

I get :

application type mismatch
  Game.completable.move rfl
argument
  rfl
has type
  Game.move ?m.2730 Move.up = Game.move ?m.2730 Move.up : Prop
but is expected to have type
  Game.move ?m.2730 Move.up = Option.some ?m.2731 : Prop

(Side Note: In my real project I'm not using Option but a Result type as the return type from Game.move.)

[Marcus Rossel]

And in order to prove Game.move ?m.2730 Move.up = Option.some ?m.2731 I would need Lean to execute/reduce the call to Game.move completely, because then it would see that the result is some _.
But I don't know how to express that.

[Marcus Rossel]

I've thought about simping with all the definitions involved in Game.move, but that got out of hand quickly.
The decide tactic also doesn't work because expected type must not contain free or meta variables.

[Sebastian Ullrich]

My bad, you'll want something like refine Game.completable.move (m := $m) rfl ?_ instead of apply so that the Game term gets inferred from the goal

[Marcus Rossel]

Hm, so in this MWE your approach works perfectly:

structure Game where
  x : Nat
  y : Nat

inductive Move | up | down | left | right

def Game.move (g : Game) : Move → Option Game
  | Move.up =>    some ⟨g.x, g.y + 1⟩
  | Move.right => some ⟨g.x + 1, g.y⟩
  | Move.down =>  if g.y == 0 then none else some ⟨g.x, g.y - 1⟩
  | Move.left =>  if g.x == 0 then none else some ⟨g.x - 1, g.y⟩

inductive Game.completable : Game → Prop
  | completed {g} : g.x > 5 → completable g
  | move {g₁ g₂ : Game} {m} : (g₁.move m = some g₂) → completable g₂ → completable g₁

def level1 : Game := ⟨0, 0⟩

open Lean Elab.Tactic Game.Move in
elab (name := move) "move " m:term : tactic => do
  evalTactic (← `(tactic| refine Game.completable.move (m := $m) rfl ?_))

theorem level1_completable : level1.completable := by
  move Move.right
  move Move.right
  move Move.right
  move Move.right
  move Move.right
  move Move.right
  simp [Game.completable.completed]

[Marcus Rossel]

In my real world project I still get:

application type mismatch
  Game.completable.move rfl
argument
  rfl
has type
  Game.move level1 Move.up = Game.move level1 Move.up : Prop
but is expected to have type
  Game.move level1 Move.up = Game.Move.Result.success ?m.2747 : Prop

[Sebastian Ullrich]

Hard to say without knowing more about move. Are you positive that term does in fact evaluate to success _? :)

[Marcus Rossel]

Unfortunately Game.move is too big to reduce sensibly. But I can do:

#eval (level1.move Move.up).get!

And get a success _.

Does the fact that Game.move is partial mess things up?

[Sebastian Ullrich]

Yes! You cannot prove anything about partial.

[Marcus Rossel]

Thanks for your patience :D