Lean.Expr.proj

Stream: lean4

[Arthur Paulino]

In the metaprogramming book, @Edward Ayers described this constructor as:

proj is for projection. Suppose you have a structure such as p : α × β,
rather than storing the projection π₁ p as app π₁ p, it is expressed as
proj Prod 0 p. This is for efficiency reasons

Is this documented somewhere? Where can I learn more about it? Thanks in advance!

[Mario Carneiro]

well, you are talking about the very book that would be the documentation, so not really

[Mario Carneiro]

is there something in particular you want to know about it?

[Mario Carneiro]

They are called "primitive projections" and they correspond to the fields of a structure

[Arthur Paulino]

Hm, is there anything we lose (but efficiency) if we face them as regular applications? Like some expressiveness power

[Mario Carneiro]

no, it's just for efficiency

[Mario Carneiro]

they are not supposed to be an extension to the logic, they just abbreviate applications of the recursor

[Mario Carneiro]

nat and string literals are the same way

[Arthur Paulino]

Alright, thanks!

[Arthur Paulino]

How can I make it print proj?

import Lean

open Lean Elab Command Term in
elab "#inspect" t:term : command => do
  liftTermElabM `inspect do
    let t ← elabTerm t none
    synthesizeSyntheticMVarsNoPostponing
    dbg_trace t.ctorName

structure Foo where
  aa : Nat
  bb : String

#inspect (Foo.mk 1 "hi").1  -- app
#inspect (Foo.mk 1 "hi").aa -- app
#inspect (1, 2).1           -- app
#inspect (1, 2).fst         -- app

[Mario Carneiro]

Not easily. proj is generally not supposed to show up in normal terms. But you can look at the implementation of the projections to find occurrences of proj:

import Lean

elab "#inspect" t:ident : command => do
  if let some ci := (← Lean.getEnv).find? t.getId then
    dbg_trace repr ci.value!

structure Foo where
  aa : Nat
  bb : String

#inspect Foo.aa
-- Lean.Expr.lam
--   `self
--   (Lean.Expr.const `Foo [] (Expr.mkData 1485976967 (bi := Lean.BinderInfo.default)))
--   (Lean.Expr.proj
--     `Foo
--     0
--     (Lean.Expr.bvar 0 (Expr.mkData 4279369707 (looseBVarRange := 1) (bi := Lean.BinderInfo.default)))
--     (Expr.mkData 1237988559 (looseBVarRange := 1) (approxDepth := 1) (bi := Lean.BinderInfo.default)))
--   (Expr.mkData 3385561612 (approxDepth := 2) (bi := Lean.BinderInfo.default))

[Jakob von Raumer]

Is there any way to reduce an Expr in a way that minimizes the constructors used? I.e. reducing away not only lets but also projs and literals?

[Sebastian Ullrich]

No built-in way I think, since Lean of course wants to preserve these

[Mario Carneiro]

Note that lean does know that a projection can unfold:

example : Foo.aa = @Foo.rec (λ _ => Nat) (λ x y => x) := rfl

[Mario Carneiro]

(on second thought, this might be eta for structures kicking in instead)

[Jakob von Raumer]

Sebastian Ullrich said:

No built-in way I think, since Lean of course wants to preserve these

For all kinds of transformations it is a bit weird to work on those doublets though, since making the transformation consistent already determines them uniquely

[Sebastian Ullrich]

Mario Carneiro said:

(on second thought, this might be eta for structures kicking in instead)

It's actually older than that, see isDefEqProj. And isDefEqNat/isDefEqStringLit for literals.