Autogenerate "forall" and "exists" lemmas

Stream: mathlib4

[Yury G. Kudryashov]

It would be nice to have a tactic that autogenerates lemmas like docs#Sigma.forall and docs#Sigma.exists

[Yury G. Kudryashov]

If someone is ready to teach me how to write meta code, I can try to write this.

[Yury G. Kudryashov]

E.g., what should I read first?

[Patrick Massot]

If you want to learn in a systematic way then you need to read Functional programming in Lean and then the meta-programming book. The indirect way is to try to read meta-code and try to imitate it.

[Kyle Miller]

Here's a general plan for a way to generate these lemmas sketched out inside a tactic proof:

import Mathlib.Tactic.ProxyType
import Mathlib.Data.ULift

inductive Foo
  | A (n : Nat) (h : n < 5)
  | B (b : Bool)

theorem mk_Foo_forall_exists (p : Foo → Prop) : false := by
  -- The `proxy_equiv%` machinery also has a direct metaprogramming interface.
  -- In the simps I'm making use of the name of the global definition it generates.
  let eqv := proxy_equiv% Foo
  have forall_lemma := Equiv.forall_congr_left' (p := p) eqv.symm
  simp [Foo.proxyTypeEquiv] at forall_lemma
  dsimp at forall_lemma
  /-
  forall_lemma :
    (∀ (x : Foo), p x) ↔
      (∀ (a : ℕ) (x : a < 5), p (Foo.A a x)) ∧ p (Foo.B false) ∧ p (Foo.B true)
  -/
  have exists_lemma := Equiv.exists_congr_left (p := p) eqv.symm
  simp [Foo.proxyTypeEquiv] at exists_lemma
  dsimp at exists_lemma
  /-
  exists_lemma :
    (∃ a, p a) ↔
      (∃ a x, p (Foo.A a x)) ∨ p (Foo.B false) ∨ p (Foo.B true)
  -/

(Though it's probably better and more general to generate the lemmas more directly from the recursor.)

[Kyle Miller]

You could check out how reassoc and elementwise work as a partial model, though it's going to be different since these don't start with a theorem to transform

[Kyle Miller]

Here's a rough implementation to generate forall lemmas by analyzing the recursor. It works at least for the examples I've thrown at it.

code

import Std
import Mathlib.Tactic.SolveByElim

namespace Mathlib.Tactic

open Lean Meta Elab

/-- Make a conjunction of `And`. -/
def mkConj : List Expr → Expr
  | [] => mkConst ``True
  | [p] => p
  | p :: ps => mkApp2 (mkConst ``And) p (mkConj ps)

/-- For a given inductive type, create a "forall lemma." -/
def mkForallIffType (decl : Name) : MetaM Expr := do
  let recOn := mkRecOnName decl
  let recInfo ← mkRecursorInfo recOn
  -- Specialize the motive to Prop:
  let us : List Level ← recInfo.univLevelPos.mapM fun
    | .motive => pure .zero
    | .majorType .. => mkFreshLevelMVar
  let recFn := mkConst recOn us
  --logInfo m!"recOn = {recOn}\nrecInfo = {recInfo}\nrecOn : {← inferType recFn}"
  forallTelescopeReducing (← inferType recFn) fun args _ => do
    let motive := args[recInfo.motivePos]!
    --let major := args[recInfo.majorPos]!
    unless recInfo.paramsPos.all (·.isSome) do
      throwError "(internal error) kernel recursors should have all paramsPos"
    let params := recInfo.paramsPos.toArray.map (args[·.get!]!)
    let minors := Array.range args.size |>.filter recInfo.isMinor |>.map (args[·]!)
    unless args.size == 1 + 1 + minors.size + params.size + recInfo.indicesPos.length do
      throwError "(internal error) recursor has unexpected number of arguments"
    -- Rename the motive to P:
    let lctx' := (← getLCtx).setUserName motive.fvarId! `P
    withLCtx lctx' (← getLocalInstances) do
      --logInfo m!"params = {params}\nmotive = {motive}\nminors = {minors}"
      let lhs ← forallTelescopeReducing (← inferType motive) fun idxs _ => do
        mkForallFVars idxs (mkAppN motive idxs)
      --logInfo m!"lhs = {lhs}"
      let rhs := mkConj (← minors.mapM inferType).toList
      --logInfo m!"rhs = {rhs}"
      let iff := mkApp2 (mkConst ``Iff) lhs rhs
      mkForallFVars (params.push motive) iff

def mkForallIffPf (decl : Name) : TermElabM Expr := do
  let ty ← mkForallIffType decl
  --logInfo m!"ty = {ty}"
  check ty
  let pf ← mkFreshExprMVar ty
  let g := pf.mvarId!
  let (_, g) ← g.intros
  let [gmp, gmpr] ← g.apply <| mkConst ``Iff.intro
    | throwError "apply did not generate exactly two goals"
  let [] ← Term.withoutErrToSorry <| Tactic.run gmp do Tactic.evalTactic <| ← `(tactic|
      simp (config := {contextual := true}))
    | throwError "could not solve forward direction"
  let [] ← Term.withoutErrToSorry <| Tactic.run gmpr do Tactic.evalTactic <| ← `(tactic| (
      simp only [and_imp]
      intros
      rename_i m
      induction m <;> solve_by_elim))
    | throwError "could not solve backward direction"
  instantiateMVars <| ← mkExpectedTypeHint pf ty

syntax (name := mkQuantifierLemma) "mk_quantifier_iffs" : attr

initialize registerBuiltinAttribute {
  name := `mkQuantifierLemma
  descr := ""
  applicationTime := .afterCompilation
  add := fun src ref kind => match ref with
  | `(attr| mk_quantifier_iffs) => MetaM.run' do
    if (kind != AttributeKind.global) then
      throwError "`mk_quantifier_iffs` can only be used as a global attribute"
    let tgt := Name.str src "forall_iff"
    let tgt' := Name.str src "exists_iff" -- TODO
    addDeclarationRanges tgt
      { range := ← getDeclarationRange (← getRef)
        selectionRange := ← getDeclarationRange ref }
    addDeclarationRanges tgt'
      { range := ← getDeclarationRange (← getRef)
        selectionRange := ← getDeclarationRange ref }
    let (levels, pf) ← Term.TermElabM.run' do
      let pf ← mkForallIffPf src
      let pf ← Elab.Term.levelMVarToParam pf
      return (← Term.getLevelNames, pf)
    let pf ← instantiateMVars pf
    addAndCompile <| .thmDecl
      { levelParams := levels, type := (← inferType pf), name := tgt, value := pf }
  | _ => throwUnsupportedSyntax }

Here are some examples:

@[mk_quantifier_iffs]
inductive Foo (α : Type u)
  | A (n : Nat) (h : n < 5)
  | B (b : Bool)
  | C (x : α)

#check Foo.forall_iff
/-
Foo.forall_iff.{u_1} {α : Type u_1} {P : Foo α → Prop} :
  (∀ (t : Foo α), P t) ↔ (∀ (n : ℕ) (h : n < 5), P (Foo.A n h))
                            ∧ (∀ (b : Bool), P (Foo.B b)) ∧ ∀ (x : α), P (Foo.C x)
-/

@[mk_quantifier_iffs]
inductive Primaries
  | Red | Green | Blue

#check Primaries.forall_iff
/-
Primaries.forall_iff {P : Primaries → Prop} :
  (∀ (t : Primaries), P t) ↔ P Primaries.Red ∧ P Primaries.Green ∧ P Primaries.Blue
-/

attribute [mk_quantifier_iffs] Fin
#check Fin.forall_iff
/-
Fin.forall_iff {n : ℕ} {P : Fin n → Prop} :
  (∀ (t : Fin n), P t) ↔ ∀ (val : ℕ) (isLt : val < n), P { val := val, isLt := isLt }
-/

attribute [mk_quantifier_iffs] Eq
#check Eq.forall_iff
/-
Eq.forall_iff.{u_1} {α : Sort u_1} {a✝ : α} {P : (a : α) → a✝ = a → Prop} :
  (∀ (a : α) (t : a✝ = a), P a t) ↔ P a✝ (_ : a✝ = a✝)
-/

attribute [mk_quantifier_iffs] List
#check List.forall_iff
/-
List.forall_iff.{u_1} {α : Type u_1} {P : List α → Prop} :
  (∀ (t : List α), P t) ↔ P [] ∧ ∀ (head : α) (tail : List α), P tail → P (head :: tail)
-/

[Yury G. Kudryashov]

Thanks! Will you PR it? BTW, should we use .forall/.exists or .forall_iff/.exists_iff?

[Kyle Miller]

It doesn't have exists lemmas yet, and it would be nice to more accurately generate the proof of the forall lemma rather than hope solve_by_elim works (I found that it doesn't work for Acc). But, yeah, I can PR it once it's ready

[Kyle Miller]

For names of the generated lemmas, both options seem fine, except forall is still a reserved keyword, which is a little awkward

[Yury G. Kudryashov]

We have lots of *.forall lemmas. All of them need to be protected anyway.

[Yury G. Kudryashov]

(you don't want many forall_iff lemmas available after open either)