constructing expressions

Stream: metaprogramming / tactics

[Jon Eugster]

I am playing around with constructing Expr's manually.

What am I doing wrong with the following example, why are x and y not defeq?

import Lean
import Mathlib.Init.Function

open Lean Meta Function

def f : Prop → Prop := fun n => n

-- def Bijective (f : α → β) :=
--   Injective f ∧ Surjective f

def test : MetaM Unit := do
  let x : Expr := (.app (.const ``Bijective [1, 1]) (.const ``f []))
  let y : Expr := (mkAppN (.const ``And []) #[(.app (.const ``Injective [1, 1]) (.const ``f [])), (.app (.const ``Surjective [1, 1]) (.const ``f []))])
  dbg_trace x -- Function.Bijective.{1, 1} f
  dbg_trace y -- And (Function.Injective.{1, 1} f) (Function.Surjective.{1, 1} f)
  dbg_trace (← isDefEq x y) -- false

#eval test

[Anand Rao Tadipatri]

It might be that the expressions are not constructed correctly with all the implicit parameters filled in. It seems to work when using docs#Lean.Meta.mkAppM instead of the constructor docs#Lean.Expr.app.

[Damiano Testa]

I find that building Expr "by hand" is always very brittle. Try

  dbg_trace (← whnf x)
  dbg_trace (← whnf y)

to get some more insight on what the difference might be. :smile:

[Jon Eugster]

Thanks! mkAppM was indeed what I needed to figure out how things work. And the implicit arguments are indeed what I missed. This works now:

def test : MetaM Unit := do
  let x : Expr := (mkAppN (.const ``Bijective [1, 1]) #[(.sort 0), (.sort 0), (.const ``f [])])
  let y : Expr := (mkAppN (.const ``And []) #[(mkAppN (.const ``Injective [1, 1]) #[(.sort 0), (.sort 0), (.const ``f [])]), (mkAppN (.const ``Surjective [1, 1]) #[(.sort 0), (.sort 0), (.const ``f [])])])
  dbg_trace x
  dbg_trace y
  dbg_trace (← isDefEq x y)

[Jon Eugster]

Damiano Testa said:

Try

  dbg_trace (← whnf x)
  dbg_trace (← whnf y)

to get some more insight on what the difference might be. :smile:

Indeed, that showed

fun {β : Type} (f_1 : f -> β) => And (Function.Injective.{1, 1} f β f_1) (Function.Surjective.{1, 1} f β f_1)

vs.

And (Function.Injective.{1, 1} f) (Function.Surjective.{1, 1} f)

Damiano Testa said:

I find that building Expr "by hand" is always very brittle.

#xy-ing the problem I want to figure out if two Expr are definitional equivalent up to renaming of fvars and therefore wanted to understand Exprs better. I assume there is no existing function doing that already?

[Jannis Limperg]

An expression e with fvars h1 : T1, ..., hn : Tn is equivalent to a function λ (h1 : T1) ... (hn : Tn), e. If you perform this transformation for your two expressions and then check for defeq, the names of the functions' arguments don't matter, so you should get what you want.

[Kyle Miller]

An assumption for isDefEq is that the terms are type correct. You can use Meta.check to raise an error if they're not.

def test : MetaM Unit := do
  let x : Expr := (.app (.const ``Bijective [1, 1]) (.const ``f []))
  let y : Expr := (mkAppN (.const ``And []) #[(.app (.const ``Injective [1, 1]) (.const ``f [])), (.app (.const ``Surjective [1, 1]) (.const ``f []))])
  Meta.check x -- error
  Meta.check y
  dbg_trace x
  dbg_trace y
  dbg_trace (← isDefEq x y)

#eval test
/--
application type mismatch
  @Function.Bijective f
argument
  f
has type
  Prop → Prop : Type
but is expected to have type
  Type : Type 1
-/

[Kyle Miller]

There are some app builder meta functions to help fill in all the implicit arguments for you:

def test : MetaM Unit := do
  let fe : Expr := .const ``f []
  let x : Expr ← mkAppM ``Bijective #[fe]
  let y : Expr ← mkAppM ``And #[← mkAppM ``Injective #[fe], ← mkAppM ``Surjective #[fe]]
  Meta.check x
  Meta.check y
  dbg_trace x
  dbg_trace y
  dbg_trace (← isDefEq x y)

#eval test
/--
Function.Bijective.{1, 1} Prop Prop f
And (Function.Injective.{1, 1} Prop Prop f) (Function.Surjective.{1, 1} Prop Prop f)
true
-/

[Kyle Miller]

Could you #xy a bit further @Jon Eugster? What's the application where you have exprs with different fvars? Are they exprs in different local contexts? or the same context? Might there be metavariables too?