Understanding Expressions

Stream: lean4

[Filippo A. E. Nuccio]

I am trying to learn a bit how expressions are handled, and I do not understand what I got wrong: in the example below, I am trying to set up a tactic that detects if there are functions in the context:

import Lean.Elab

partial def ExtrApp : TacticM Unit :=
  withMainContext
  (do
    let lctx ← getLCtx
    let mut xs : (List String) := []
    for lh in lctx do
      if lh.type.isApp then xs := "yes" :: xs
      else xs := "no" :: xs
    do logInfo m!"{xs}"
    return)

elab "exists_app" : tactic => ExtrApp

example (X Y : Type) (f : X → Y) : true := by
  exists_app -- [no, no, no, no]

If I modify the first ExtrApp changing if lh.type.isApp then xs := "yes" :: xs to if lh.type.isForall then xs := "yes" :: xs (so, AFAIU, asking for "for all expressions") I get [yes, no, no, yes]. I do not understand either of the outputs :sad:

[Henrik Böving]

isApp is for detecting function applications not function types themselves

[Filippo A. E. Nuccio]

A term of the form f x for some f : X -> Y and some x : X?

[Henrik Böving]

yes

[Henrik Böving]

Have you read the constructors of Expr and their documentaiton?

[Filippo A. E. Nuccio]

Yes, I have read them. I wouldn't go as far as saying I understood them :smile:

[Henrik Böving]

With which one are you having trouble then?

[Filippo A. E. Nuccio]

Well, I think I understand them when I read them (apart bvar that is a bit obscure due to this de Brujn index), but then I fail my exercices. So I have probably not understood them properly.

[Filippo A. E. Nuccio]

Also, I fail to understand the difference from lambdaexpressions and forAll.

[Filippo A. E. Nuccio]

Both are terms of some Pi type, no?

[Henrik Böving]

No, lambda is fun x => ... and forall is (x : a) -> b x

[Henrik Böving]

in particular forall also covers the case where the output type does not depend on the input value so a -> b as well. So in general inferring the type of a lambda should always yield a forall

[Henrik Böving]

Filippo A. E. Nuccio said:

A term of the form f x for some f : X -> Y and some x : X?

Also this view is not quite right. Expr is just syntax, you can trivially construct type incorrect Expr. So app really just syntactically represents f x, whether f and x are of the right type is a whole other question.

[Filippo A. E. Nuccio]

Henrik Böving said:

No, lambda is fun x => ... and forall is (x : a) -> b x

Not sure I understand this; I see your point below that these are "pure syntax" and can be wrong (in the sense that they do not typecheck), but why do you say that these things are different type-theoretically?

[Patrick Massot]

They are very different: one can be the type of the other.

[Patrick Massot]

fun x : Nat ↦ x is a lambda, while Nat → Nat is a forall.

[Patrick Massot]

The second one is the type of the first one.

[Filippo A. E. Nuccio]

You mean that a forall is a Pi-Type?

[Patrick Massot]

yes

[Filippo A. E. Nuccio]

Oh sure, I was confused. :face_with_peeking_eye:

[Henrik Böving]

Filippo A. E. Nuccio said:

You mean that a forall is a Pi-Type?

forall is not only a pi-type, it is the pi type

[Filippo A. E. Nuccio]

Yes yes, thanks. I think I am recovering from my blurred state of mind.

[Filippo A. E. Nuccio]

So, going back to Expr, IsForAll recovers if something is a PiType and IsLambda recovers if it is a lambda-term (inside some PiType)?

[Patrick Massot]

Those functions are so simple that the answer cannot be simpler than the definitions.

[Patrick Massot]

/-- Return `true` if the given expression is a forall-expression aka (dependent) arrow. -/
def isForall : Expr → Bool
  | forallE .. => true
  | _          => false

/-- Return `true` if the given expression is a lambda abstraction aka anonymous function. -/
def isLambda : Expr → Bool
  | lam .. => true
  | _      => false

[Filippo A. E. Nuccio]

Patrick Massot said:

Those functions are so simple that the answer cannot be simpler than the definitions.

Well, this answer is so simple that it cannot be more informative than the question :smile:

[Patrick Massot]

The informative part was being copy-pasted.

[Patrick Massot]

I should have sent only one message, sorry.

[Patrick Massot]

This is really the analogue of

def Nat.isZero : Nat → Bool
| .zero => true
| .succ _ => false

#eval Nat.isZero 0
#eval Nat.isZero 5

[Filippo A. E. Nuccio]

No problem, I just meant to say that I read those definitions, still I was a bit struggling. Perhaps an example would do, it is often helpful. Do we agree that IsForall should return true if it encounters

(n : Nat) -> Fin n

while IsLambda should return true if it encounters

fun n : Nat => (n-1) : Fin n

?

[Johan Commelin]

Did you mean

(n : Nat) -> Fin n

in your first example? (arrow instead of comma)

[Filippo A. E. Nuccio]

I did (I am still fighting with the "new" notation for PiTypes: I would write Π(n : Nat) Fin n)

[Johan Commelin]

I think you can use the logical forall symbol, if you like it better

[Johan Commelin]

Anyway, if you meant the arrow instead of the comma, then the answer to your question is "yes"

[Filippo A. E. Nuccio]

Thanks! I realised that most of my trouble came from the inconscious (and wrong, of course) intuition that "Expressions" found in the context could not be types...

[Patrick Massot]

@Filippo A. E. Nuccio , you can play with

import Mathlib

open Lean Elab Command

elab "#descr" e:term : command => do
  let E ← liftTermElabM <| Term.elabTerm e none
  logInfo (repr E)

#descr (n : Nat) → Fin n
#descr fun n : Nat ↦ (Fin.last n)

[Filippo A. E. Nuccio]

Oh, that's nice! Thanks @Patrick Massot