Distinguish dependet and nondependent `forallE`

Stream: lean4

[Horațiu Cheval]

How can I differentiate between a dependent and a nondependent Pi type when working with Exprs? I know about isArrow but it didn't achieve what I wanted it to. The context is that I'm trying to write in Lean a first-order logic construction defined by recursion on formulas. Since in FOL implication and universal quantification are entirely distinct constructors, they can be treated differently in such definitions.
Concretely, the $\operatorname{neg}$ function should map FOL formulas to FOL formulas according to the following recursive rules:

$$\operatorname{neg} (p \to q) := (\operatorname{neg} p) \to (\operatorname{neg} q) \\ \operatorname{neg} (\forall x \ p) := \forall x (\neg (\operatorname{neg} p))$$

so the body of a universal quantification should receive a negation, while neither the premise nor the conclusion of an implication should.

I tried using isArrow, which doesn't work, failing to distinguish as intended between implication and universal quantification, in expressions of the form ∀ x, p x → q x, as in the example at the end:

import Lean
open Lean Elab Term Meta
set_option autoImplicit false

def negate (e : Expr) : Expr := mkApp (mkConst `Not) e

partial def neg (e : TermElabM Expr) : TermElabM $ Expr := do
  let e ← whnf (← e)
  match e with
  | .forallE n p q m =>
    if Expr.isArrow (.forallE n p q m) then
      let pN := neg (pure p)
      let qN := neg (pure q)
      mkArrow (← pN) (← qN)
    else
      let qN ← neg (pure q)
      return .forallE n p (negate qN) m
  | e => return e

def negPretty (e : TermElabM Syntax) : TermElabM Format := do
  let e ← elabTermAndSynthesize (← e) none
  let e ← neg (pure e)
  ppExpr e

#eval negPretty `(∀ x : Nat, x = x → x = x)
-- Output: ∀ (x : Nat), ¬(x = x → ¬x = x)
-- `isArrow` identifies the open expression `x = x → x = x` as not being an arrow
-- Desired output: ∀ (x : Nat), ¬(x = x → x = x)

[Horațiu Cheval]

The remark above isArrowin the source code, that it assumes the expressions has no loose bound variables makes think that it is not appropriate for this job, but what can I use to make this distinction?

[Jannis Limperg]

You can use Expr.hasLooseBVar to check whether the forall-bound variable occurs in the body. This is exactly what distinguishes an implication from a forall. However, you may want to use one of the telescope functions (forallTelescope etc.) instead of dealing with open expressions.

[Horațiu Cheval]

Ok, thanks, so I replaced the isArrow check with !(Expr.hasLooseBVar q 0) and it seems to be working. I will leave the forallTelescope variant for later as it is a little over my head for now.

[Jannis Limperg]

Sounds good! We have a bit about these telescopes in the MetaM chapter of the metaprogramming book, if that helps (and I'm currently working on a PR to expand this section). They're fairly central, so I'm afraid you'll have to deal with them at some point. ;)