Tactic to add instances from hypotheses

Stream: general

[Violeta Hernández]

In combinatorial game theory, some games are "numeric", and these games have the property that any options (games one can arrive to after a move) are also numeric. The consequence is that we sometimes have to add a lot of instances at once and in a long proof this becomes quite annoying. I want some tactic that adds all of these instances automatically, e.g.

import Mathlib.Data.Set.Defs

axiom Game : Type
axiom Options : Game → Set Game

class Numeric (x : Game) : Prop

axiom numeric_of_mem_options {x y : Game} [Numeric x] (h : y ∈ Options x) : Numeric y

example {x y : Game} [Numeric x] (h : y ∈ Options x) : True := by
  have := numeric_of_mem_options h -- could a tactic `numeric` do this automatically for all applicable variables?
  sorry

[Violeta Hernández]

This presumably would just be a tactic that executes try have := numeric_of_mem_options h for all hypotheses h. It seems like it should be easy to make a quick and dirty implementation of this, but I don't know how.

[Aaron Liu]

This seems like something I could write

[Violeta Hernández]

I probably should have started by asking you

[František Silváši 🦉]

Very dirty (pretty much just does what you suggested with try have ...):

import Mathlib.Data.Set.Defs
import Lean

axiom Game : Type
axiom Options : Game → Set Game

class Numeric (x : Game) : Prop

axiom numeric_of_mem_options {x y : Game} [Numeric x] (h : y ∈ Options x) : Numeric y

open Lean Elab Tactic in
private def instances (constants : Array Name) (goal : MVarId) : MetaM (Option MVarId) := goal.withContext do
  let mut tacStr := ""
  for h in ←getLCtx do
    if h.isImplementationDetail then continue
    for c in constants do
      tacStr := tacStr.append s!"(try have := {c} {h.userName});"
  let .ok tac := Parser.runParserCategory (←getEnv) `tactic s!"({tacStr})" | return .none
  let ([goal], _) ← runTactic goal tac | return .none
  return goal

elab "instances" "[" cs:ident,+ "]" : tactic =>
  Lean.Elab.Tactic.liftMetaTactic1 (instances <| cs.getElems.map (·.getId))

example {x y : Game} [Numeric x] (h : y ∈ Options x) : True := by
  instances [numeric_of_mem_options]
  sorry

I made it parametric over the constants you want to try (in this case it's numeric_of_mem_options).

[Violeta Hernández]

Thank you very much!

[Violeta Hernández]

Just to make sure. You don't mind this if I go ahead and add this to the CGT repo? With credit, of course.

[František Silváši 🦉]

Not at all, go ahead :).

[Violeta Hernández]

Hm, I think I just came across a bug

import Mathlib.Data.Set.Defs
import Lean

axiom Game : Type
axiom Options : Game → Set Game

class Numeric (x : Game) : Prop

axiom numeric_of_mem_options {x y : Game} [Numeric x] (h : y ∈ Options x) : Numeric y

open Lean Elab Tactic in
private def instances (constants : Array Name) (goal : MVarId) : MetaM (Option MVarId) := goal.withContext do
  let mut tacStr := ""
  for h in ←getLCtx do
    if h.isImplementationDetail then continue
    for c in constants do
      tacStr := tacStr.append s!"(try have := {c} {h.userName});"
  let .ok tac := Parser.runParserCategory (←getEnv) `tactic s!"({tacStr})" | return .none
  let ([goal], _) ← runTactic goal tac | return .none
  return goal

elab "instances" "[" cs:ident,+ "]" : tactic =>
  Lean.Elab.Tactic.liftMetaTactic1 (instances <| cs.getElems.map (·.getId))

-- (kernel) declaration has metavariables '_example'
example {x y z : Game} [Numeric x] (h : y ∈ Options x) : Numeric z := by
  instances [numeric_of_mem_options]

[Violeta Hernández]

The tactic shouldn't really be closing the goal

[Violeta Hernández]

This generally seems to happen when the goal has the shape Numeric _

[František Silváši 🦉]

It doesn't close the goal for me :thinking:?
I copy-pasted the whole thing in. The state is:

x y z : Game
inst✝ : Numeric x
h : y ∈ Options x
this : Numeric y
⊢ Numeric z

On leanprover/lean4:v4.26.0-rc2.

[František Silváši 🦉]

What version should I try this on?

[Violeta Hernández]

I'm running this on Lean web

[František Silváši 🦉]

I can repro this on the web version, whatever that may be. I'll have a look.

[Violeta Hernández]

Oddly enough the web version also seems to be Lean 4.26.0-rc2...

[František Silváši 🦉]

The parser invocation fails on the web version; I am assuming this is because there's something odd with (←getEnv) in the web version, which queries the local environment.

[František Silváši 🦉]

And I assume the server doesn't want me querying the local environment. I'll rewrite this in a way that doesn't parse to obtain the syntax I want, give me a sec.

[Violeta Hernández]

It also fails in the repo, but only in some files and not in others...

[František Silváši 🦉]

I'll construct the syntax by hand to be Environment-independent :).

[František Silváši 🦉]

This works for me locally and on the webview (I tossed in an extra typeclass / constant) - the behaviour is _slightly_ changed because the names of the instances are inaccessible by default here.

import Mathlib.Data.Set.Defs
import Lean

axiom Game : Type
axiom Options : Game → Set Game

class Numeric (x : Game) : Prop

class Numeric' (x : Game) : Prop

axiom numeric_of_mem_options {x y : Game} [Numeric x] (h : y ∈ Options x) : Numeric y

axiom numeric_of_mem_options' {x y : Game} [Numeric x] (h : y ∈ Options x) : Numeric' y

open Lean Elab Tactic in
private def instances (constants : Array Name) (goal : MVarId) : MetaM (Option MVarId) := goal.withContext do
  let mut goal := goal
  for h in ←getLCtx do
    if h.isImplementationDetail then continue
    for c in constants do
      let ([goal'], _) ← runTactic goal (←`(tactic | try have := $(mkIdent c) $(mkIdent h.userName)))
        | logError "Applying {h.userName} to {c} must yield a single goal."; return .none
      goal := goal'
  return goal

elab "instances" "[" cs:ident,+ "]" : tactic =>
  Lean.Elab.Tactic.liftMetaTactic1 (instances <| cs.getElems.map (·.getId))

example {x y z : Game} [Numeric x] (h : y ∈ Options x) : Numeric z := by
  instances [numeric_of_mem_options, numeric_of_mem_options']

[Violeta Hernández]

Well, that somehow fixed things... Thanks!

[František Silváši 🦉]

Will not fail silently now in case something goes wrong again at the very least :sweat_smile:.

[Violeta Hernández]

CGT#253 :slight_smile:

[Aaron Liu]

I have a proposed implementation

[Violeta Hernández]

Aaron Liu said:

I have a proposed implementation

Different from the implementation we already have?

[Aaron Liu]

it's not the same

[Aaron Liu]

I would argue it's better since you don't need to involve the elaborator

[Jovan Gerbscheid]

I think my proposed class abbrev would subsume this.
Sorry, I read it too fast

[Jovan Gerbscheid]

(deleted)

[Aaron Liu]

here it is

import Lean.Meta.Tactic.Assert
import Lean.Elab.Tactic.Meta

open Lean Meta Elab Tactic

def instances (constants : Array Name) (goal : MVarId) : MetaM (Option MVarId) := goal.withContext do
  let mut goal := goal
  for h in ← getLCtx do
    if h.isImplementationDetail then continue
    ⟨_, goal⟩ ← goal.assertHypotheses =<< constants.filterMapM fun c => do
      let hc ← try mkAppM c #[h.toExpr] catch _ => return none
      return some {
        userName := ← mkFreshUserName `inst
        type := ← inferType hc
        value := hc
      }
  return goal

[Violeta Hernández]

What's the difference between this and the implementation(s) above?

[Aaron Liu]

doesn't use the elaborator

[Aaron Liu]

no runTactic

[Violeta Hernández]

put your impl in the PR

[Aaron Liu]

I hope it works (haven't tested it)

[Violeta Hernández]

It builds, so I guess it works