Projections for Exists

Stream: lean4

[Adam Topaz]

I came across the following which I don't understand:

import Lean

open Lean

def foo (n m : Nat) (h : ∃ _ : m = n, True) : m = n := h.1

#eval show MetaM Unit from do
  let some c := (← getEnv).find? `foo | unreachable!
  let some val := c.value? | unreachable!
  Meta.lambdaLetTelescope val fun _fvars val => do
    match val with
    | .proj nm idx _struct =>
      println! nm -- Exists
      println! idx -- 0
      println! getStructureFields (← getEnv) nm -- PANIC
    | _ => unreachable!

What I really want to do is convert the projection to a function application, but I don't know how to do that in this case!

[Adam Topaz]

The thing is, in my mental model of how things work in MetaM world, if I have an expression of the form .proj nm idx struct then I should be able to call getStructureFields env nm, but clearly this is not the case.

[Adam Topaz]

As far as I can tell, in this case the projection h.1 actually cannot be converted to a function application without using Exists.choose. Note that using Exists.choose adds that as a used axiom, but foo as written above does not depend on any axioms.

[Edward van de Meent]

actually, because this is subsingleton elimination, there might be a way to do this without choice?

[Adam Topaz]

I don't really care about whether or not choice is used TBH. I really just want to convert this Expr.proj to an Expr.app.

[Edward van de Meent]

theorem foo (h : ∃ _ : P, True) : P := by
  have : Nonempty P := nonempty_of_exists h
  exact (nonempty_prop P).mp this

#print axioms foo

indeed it exists

[Adam Topaz]

I mean... there is also docs#Exists.fst but that's not the point. The point is that I want some MetaM program that is able to convert Expr.proj to Expr.app. I could write such a program which checks for special cases like Exists, but I hope that's not necessary.

[Mario Carneiro]

it's not always possible in general, unless someone made a definition with a compatible type and you happen to know what it is

[Mario Carneiro]

Exists.fst is not a special function, unlike structure projection functions

[Adam Topaz]

It seems that the docstring on docs#Lean.Expr.proj is slightly misleading then

[Mario Carneiro]

in what way is it misleading?

[Adam Topaz]

I interpret the word "redundant" as indicating that they can always be interpreted in terms of the other constructors.

[Mario Carneiro]

oh, that is true, but it's not always a direct application of an existing function

[Adam Topaz]

yeah, I understand.

[Mario Carneiro]

the formal expression equivalent to proj T e i is T.casesOn e (fun x1 ... xn => xi)

[Adam Topaz]

Oh yeah, good point.

[Adam Topaz]

@Mario Carneiro do you know off the top of your head where the code is for the elaboration of projections like h.1?

[Mario Carneiro]

inferProjType in Lean.Meta.InferType is one place

[Mario Carneiro]

next to src#Lean.Meta.throwTypeExcepted

[Adam Topaz]

Thanks! That's helpful

[Mario Carneiro]

I think there is also code for expanding .proj expressions but this is less common since lean really doesn't want to expand it

[Adam Topaz]

That would be very helpful indeed!

[Mario Carneiro]

lean4#2747 involved touching every single location that interacts with .proj, so it might be useful to you

[Mario Carneiro]

actually, maybe it doesn't exist after all. The code for generating the type of the projection has to do something pretty similar, but it looks like lean will not recognize the defeq of a projection to its definition in terms of casesOn