Converting Expr projection to recursor application

Stream: Is there code for X?

[Easyoakland]

The doc comment for Lean.Expr.proj says

When exporting Lean developments to other systems, proj can be replaced with typeName.rec applications.

Does this code already exist somewhere? I know how it will work conceptually, but wonder if it already exists.

[Robin Arnez]

That statement is a half-lie since projections are (usually) the primitive for structures, see e.g.:

example : @Prod.rec = fun {_ _ _} mk t => mk t.1 t.2 := rfl

but

import Lean

open Lean Meta

def projToRec (e : Expr) : MetaM (Option Expr) := do
  let .proj nm idx struct := e | return none
  let ind ← getConstInfoInduct nm
  let [ctorName] := ind.ctors | throwError "invalid projection"
  let ctor ← getConstVal ctorName
  let rec ← getConstInfoRec (nm ++ `rec)
  let casesOn := mkCasesOnName nm
  let type ← inferType struct
  let type ← withTransparency .all (whnf type)
  let propRecursor := rec.levelParams.length == ind.levelParams.length
  type.withApp fun fn paramsAndIndices => do
    unless fn.isConstOf nm do
      throwError "invalid projection {e}"
    let params := paramsAndIndices.extract 0 ind.numParams
    let indices := paramsAndIndices.extract ind.numParams
    let ctorType ← instantiateForall ctor.type params
    let indType ← instantiateForall ind.type params
    forallTelescope indType fun indexVars _ => do
    withLocalDeclD `x (mkAppN (mkAppN fn params) indexVars) fun structVar => do
      let indexVars := indexVars.push structVar
      let rec mkCtorNth (type : Expr) (i n : Nat) : Expr :=
        match type with
        | .forallE nm t b bi => .lam nm t (mkCtorNth b i (n + 1)) bi
        | _ => .bvar (n - i - 1)
      let rec mkCasesOnApp (motive : Expr) (i : Nat) (indicesAndStruct : Array Expr) : MetaM Expr := do
        let levels ← if propRecursor then pure fn.constLevels! else pure ((← getLevel motive) :: fn.constLevels!)
        let expr := mkAppN (.const casesOn levels) params
        let expr := .app expr (← mkLambdaFVars indexVars motive)
        let expr := mkAppN expr indicesAndStruct
        return .app expr (mkCtorNth ctorType i 0)
      let rec traverseCtor (type : Expr) (i : Nat) : MetaM Expr := do
        let .forallE nm t b bi := type | throwError "invalid projection {e}, out of range"
        if i < idx then
          traverseCtor (b.instantiate1 (← mkCasesOnApp t i indexVars)) (i + 1)
        else
          mkCasesOnApp t i (indices.push struct)
      termination_by idx - i
      some <$> traverseCtor ctorType 0

should produce something definitionally equivalent to a projection.

[Aaron Liu]

I ran into an edge case where it doesn't work

open Qq

def pp (α : Q(Prop)) (P : Q($α → Prop)) (h : Q(Exists $P)) : Q($α) := q(($h).1)

#check by_elab do
  let some u ← projToRec (pp q(7 < 3) q(fun h => [][20] = 4) q(sorry)) | failure
  pure u

[Robin Arnez]

You're right; I think it should work now (I edited the original message)

[Aaron Liu]

My edge case generator generated another edge case where it doesn't work

open Qq

def pp (α : Q(Prop)) (β : Q(Prop)) (h : Q($α ×' $β)) : Q($α) := q(($h).1)

#check by_elab do
  let some u ← projToRec (pp q(1 + 1 = 2) q(False ∨ ¬False) q(⟨rfl, .inr not_false⟩)) | failure
  pure u

[Aaron Liu]

oh never mind this one is just the elaborator screwing with me

open Qq

def pp (α : Q(Prop)) (β : Q(Prop)) (h : Q($α ×' $β)) : Q($α) := Expr.proj `PProd 0 h

#check by_elab do
  let some u ← projToRec (pp q(1 + 1 = 2) q(False ∨ ¬False) q(⟨rfl, .inr not_false⟩)) | failure
  pure u

[Aaron Liu]

ok this one is an actual counterexample

open Qq

set_option bootstrap.inductiveCheckResultingUniverse false in
set_option genSizeOf false in
set_option genInjectivity false in
inductive PProd' : Sort u → Sort v → Sort (max u v) where
  | mk {α : Sort u} {β : Sort v} (a : α) (b : β) : PProd' α β

def pp (α : Q(Type)) (β : Q(Prop)) (h : Q(PProd' $α $β)) : Q($α) := q(($h).1)

#check by_elab do
  let some u ← projToRec (pp q(False ⊕' ¬False) q(1 + 1 = 2) q(⟨.inr not_false, rfl⟩)) | failure
  pure u

[Robin Arnez]

Yeah, this one's impossible to convert to recursor though: lean4#7637

[Easyoakland]

Thanks!

@Aaron Liu what is this edge case generator you speak of?

[Aaron Liu]

Easyoakland said:

Aaron Liu what is this edge case generator you speak of?

I generate edge cases with my brain