removing an unused typeclass

Stream: metaprogramming / tactics

[Chris Henson]

Suppose that I have something like:

class Synth (X : Type) where
  prop : Prop

theorem lemma_with_extra_typeclasses (X : Type) [inst : Synth X] : inst.prop := by
  sorry

where I know that once I have used Synth.prop that the instance is irrelevant to the actual proof. Is there a way that I can simp inst.prop, remove the typeclass instance, and keep the body of the proof?

[Aaron Liu]

Is this what you want?

class Synth (X : Type) where
  prop : Prop

theorem lemma_with_extra_typeclasses (X : Type) [inst : Synth X] : inst.prop := by
  have : inst = {prop := inst.prop} := rfl
  generalize inst.prop = prop at this
  subst this
  sorry

[Chris Henson]

Yes, but I would like this to happen as a metaprogram that removes [inst : Synth X] so that it does not appear in the type signature of the theorem.

[Aaron Liu]

Then you can't do it with just theorem. How to you expect to interface this action?

[Chris Henson]

I may have been unclear, let me try again. If I want to insert typeclass instances, I can do something like:

import Std
import Lean.Elab.Command

class Synth (X : Type) where
  prop : Prop

-- in a real use case this would depend on $sig, but in a way where I know we
-- should be able to remove Synth instances and still have a valid proof
syntax (name := synth_theorem)
  (priority := default + 1) declModifiers group("synth_theorem " declId ppIndent(declSig) declVal) : command
macro_rules
  | `(synth_theorem $name : $sig := $proof) => `(theorem $name (X : Type) [inst : Synth X] : inst.prop := $proof)
  | `(synth_theorem $name $args : $sig := $proof) => `(theorem $name $args (X : Type) [inst : Synth X] : inst.prop := $proof)

synth_theorem lemma_with_extra_typeclasses : False := by
  sorry

-- lemma_with_extra_typeclasses : ∀ (X : Type) [inst : Synth X], Synth.prop X
#check lemma_with_extra_typeclasses

At the end I have ∀ (X : Type) [inst : Synth X], Synth.prop X, and I know that the only thing that the typeclass instance is doing is providing some proposition, and that the proof would be valid with or without it. So I would like to have a metaprogram that gives us a new theorem that uses the same proof, but removes [inst : Synth X].

[Jovan Gerbscheid]

I don't understand how you expect inst.prop to be a well defined term after we remove the [inst : Synth X] binder.

[Chris Henson]

Jovan Gerbscheid said:

I don't understand how you expect inst.prop to be a well defined term after we remove the [inst : Synth X] binder.

This is my initial assumption, that once you simplify inst.prop it is not otherwise dependent on the instance. (I would expect the metaprogram to simply fail if this were somehow violated). As an extreme example, suppose there were a polymorphic instance of Synth where prop is now always 1 = 1. Should it not make sense that after simplifying inst.prop to this, we should be able to remove the inst from the type signature and be left with a valid proof?

[Jovan Gerbscheid]

Ah that makes sense. You want the program to simplify the type (and maybe even the proof) and if some variable doesn't appear anymore, remove it from the theorem.

[Chris Henson]

Yes, exactly. I want, as a metaprogram, to simplify inst.prop and remove the instance from the theorem. I am fine assuming the only place it appears is this type of the theorem, so I am fine transferring the proof as is.

[Jovan Gerbscheid]

There are two parts to this: what simplification function do you use, and adding the modified declaration to the environment.

I wouldn't be surprised if there already exists some function that unfolds type class projections.

[Jovan Gerbscheid]

This one: docs#Mathlib.Tactic.unfoldProjs

[Chris Henson]

Nice! I was able to use that along with docs#Lean.Meta.unfoldDefinition to simplify the type at least.

[Jovan Gerbscheid]

What did you need unfoldDefinition for? Didn't you only want to unfold the type class projections? Or did unfoldProjs not unfold the instance in your example?

[Chris Henson]

Yes, in my example the projections are sufficient. In my actual use case it takes the proof signature as an argument, so I needed to unfold once.

[Chris Henson]

Is there a section of the docs similarly helpful for modifying the declaration?

[Jovan Gerbscheid]

Well I don't there is an easy way to modify a declaration directly. You can make a new declaration with docs#Lean.addDecl (or docs#Lean.addAndCompile)

[Chris Henson]

Been trying this for a bit. Does this look headed in the right direction?

import Lean.Elab.Command
open Lean

class Synth (X : Type) where
  prop : Prop

-- want to remove `[inst : Synth X]` from this
theorem simp_with_extra_typeclasses (X : Type) [inst : Synth X] :  1 = 1 := by rfl

def filterSynth (name : Name) : CoreM Unit := do
  let env ← getEnv
  match Lean.Environment.find? env name with
  -- is this the right constrcutor where I could filter out `[inst : Synth X]`?
  -- just changing the name to test for now
  | some (Lean.ConstantInfo.thmInfo val) =>
      let new_decl := Lean.Declaration.thmDecl {val with name := val.name.appendAfter "_filt"}
      addAndCompile new_decl
  | _ => return

-- eval the function and see it successfully registers the new declaration
#eval filterSynth `simp_with_extra_typeclasses
#check simp_with_extra_typeclasses_filt

I think I understand accessing a declaration by its name, but I am unsure how to take that old declaration and filter out the instances I want to remove.

[Chris Henson]

Okay, I finally figured it out! Thanks for all the help. By pattern matching on the Exprs of Lean.TheoremVal.type and Lean.TheoremVal.value, I was able to remove the unused instances.