Zulip Chat Archive

Stream: lean4

Topic: Distinguish dependet and nondependent `forallE`


Horațiu Cheval (Jun 27 2022 at 10:29):

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 neg\operatorname{neg} function should map FOL formulas to FOL formulas according to the following recursive rules:

neg(pq):=(negp)(negq)neg(x p):=x(¬(negp))\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 (Jun 27 2022 at 10:31):

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 (Jun 27 2022 at 10:42):

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 (Jun 27 2022 at 11:37):

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 (Jun 27 2022 at 11:39):

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. ;)


Last updated: Dec 20 2023 at 11:08 UTC