isDefEq proofIrrelevance

Stream: metaprogramming / tactics

[Chase Norman]

I'm having trouble with the following isDefEq query between two terms that are identical, except for a subterm replaced with a metavariable:

import Lean
open Lean Meta Expr Elab Tactic Core

axiom p : Unit → ∃ x : Unit, True
noncomputable def concrete := fun x => (p x).choose

-- set_option trace.Meta.isDefEq true
#eval (do
  let value := (← getConstInfo ``concrete).value!
  let e1 := value.bindingBody!.instantiate1 (.const ``Unit.unit [])
  let e2 := value.bindingBody!.instantiate1 (← mkFreshExprMVar (Expr.const ``Unit []))
  withConfig (fun c => { c with proofIrrelevance := false }) do
    let _ ← isDefEq e1 e2
    dbg_trace (← instantiateMVars e2)
)

Looking at the trace, the metavariable is never assigned, probably due to proof irrelevance. However, I've specifically set proofIrrelevance to false in the Config. Is there a way that I can get a more syntactic match in this case?

[Justin Asher]

Isn't this due to choose being opaque?

[Robin Arnez]

Maybe it's applying subsingleton elimination?

[Kyle Miller]

It looks like isDefEqArgsFirstPass in ExprDefEq implicitly encodes proof irrelevance. When proof arguments are being compared, then the arguments are completely skipped if neither is of the form fun x_1 ... x_n => ?m y_1 ... y_m, where n and m can be 0. Here, p () =?= p ?_ is being skipped.

It's probably worth creating an issue.

[Chase Norman]

Thanks @Kyle Miller for the really helpful analysis. I have created an issue here: https://github.com/leanprover/lean4/issues/9612.

:+1:'s on the issue are appreciated, as well as ideas for how to work around the issue. I'd like to release a feature for Canonical that depends on a guarantee that a successful isDefEq query between a term with metavariables and a term without metavariables always assigns all of the metavariables, even if they are in proof arguments.

[Chase Norman]

Here's my workaround:

def isDefEqForce (u v : Expr) : MetaM Bool := do
  match u, v with
  | app f a, app f' a' => isDefEqForce f f' <&&> isDefEqForce a a'
  | _, _ => isDefEqGuarded u v