infix constructors

Stream: new members

[Patrick Thomas]

Is it possible to use an inductive type constructor as prefix in some places and infix in others, using something like backticks to make it infix, as in Haskell?

[Kevin Buzzard]

It's notation which is infix, not the constructor itself. With notation you can put it in brackets, for example:

#eval 3 * 4 -- 12
#eval (*) 3 4 -- 12

[Patrick Thomas]

I'm sorry, I'm not sure if I completely follow. For example, I have

@[derive decidable_eq] inductive formula : Type
| bottom : formula
| top : formula
| atom : string → formula
| not : formula → formula
| and : formula → formula → formula
| or : formula → formula → formula
| imp : formula → formula → formula
| iff : formula → formula → formula

Then in some places I would like to use and, or, imp and iff as infix, but not everywhere.

[Patrick Thomas]

The default being prefix.

[Reid Barton]

You could define some notation like notation x ` AND ` y := formula.and x y (add precedence to taste) and so on

[Patrick Thomas]

Then I would need to use AND for infix and formula.and for prefix?

[Kyle Miller]

There have been some experiments in having pseudo-Haskell infix notation here, but the closest Lean has to an infix form of an application is dot notation, like x.and y.

Here's an example of a Haskell-like notation:

notation a ` $[`:1023 f `] ` := f a

inductive foo
| baz : ℕ → ℕ → foo

def a := 2 $[foo.baz] 3
-- parses as `foo.baz 2 3`

def f (a b : ℕ) := a + b

def b := 2 $[f] 3 + 1
-- parses as `f 2 3 + 1`

(I'm not recommending this, but it's interesting it sort of can be done in a general way. It doesn't pretty print, which is a downside.)

[Patrick Thomas]

Thank you.

[Kyle Miller]

Example of dot notation: formula.bottom.and (formula.top.imp formula.bottom)

It even pretty prints that way by default. You can turn this off with the pp_nodot attribute on individual constructors:

attribute [pp_nodot] formula.and

[Patrick Thomas]

Cool. Thank you.

[Kayla Thomas]

By any chance was support for Haskell like backtick infix notation added in Lean 4?

[Adam Topaz]

In lean4 you can define infix notation even without backticks. Any particular reason you want backticks?

[Kayla Thomas]

No, it doesn't need to be backticks. Is that new in Lean 4?

[Eric Wieser]

My understanding is that backtick notation lets you infix _any_ function without defining any new notation; is that what you mean? So a `f` b = f a b for arbitrary f?

[Kayla Thomas]

Yes, that is what I meant.

[Eric Wieser]

What I believe Adam is describing is that for a particular f you can declare a specialized notation

[Kayla Thomas]

I see. That was doable in Lean 3 as well?

[Eric Wieser]

Yes, but it's more powerful in Lean 4

[Kayla Thomas]

Ok. Thank you.

[Eric Wieser]

I would imagine it is not too difficult to define a custom notation that implements a `f` b = f a b, but I don't think it's likely that Lean will come with it by default

[Kayla Thomas]

This is probably an odd question, but is there a way to define just the symbol, and just the symbol and fixity, without giving a precedence and not have Lean default to a precedence but instead force the use of parentheses? For example, a way to make this work:

inductive Formula : Type
  | pred_const_ : PredName → List VarName → Formula
  | pred_var_ : PredName → List VarName → Formula
  | eq_ : VarName → VarName → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | and_ : Formula → Formula → Formula
  | or_ : Formula → Formula → Formula
  | iff_ : Formula → Formula → Formula
  | forall_ : VarName → Formula → Formula
  | exists_ : VarName → Formula → Formula
  | def_ : DefName → List VarName → Formula
  deriving Inhabited, DecidableEq

infix " .= " => eq_
" .T " => true_
" .F " => false_
prefix " .¬ " => not_
infix " .→ " => imp_
infix " .∧ " => and_
infix " .∨ " => or_
infix " .↔ " => iff_
prefix " .∀ " => forall_
prefix " .∃ " => exists_

and give an error if parentheses are not used around each except .T and .F.

[Kayla Thomas]

Barring that, do you know where the notation for the mathlib builtin equivalent of these constructors is defined?

[Kayla Thomas]

Also, is there a way to make notation context sensitive, in order to not need the dot in front of each to avoid clashes with the builtin versions?

[Kayla Thomas]

Maybe the dot actually means something in Lean here?

[Yury G. Kudryashov]

Note that Lean interprets .mk a as TargetType.mk a

[Yury G. Kudryashov]

This can interfere with your notation (not sure how exactly)

[Kayla Thomas]

Yeah, I think the problem might actually be something else. I changed it to a following underscore, and it still doesn't seem to work right.
I have

infix:50 " =_ " => eq_
notation " T_ " => true_
notation " F_ " => false_
prefix:40 " ¬_ " => not_
infix:25 " →_ " => imp_
infix:20 " ∧_ " => and_
infix:20 " ∨_ " => or_
infix:20 " ↔_ " => iff_
notation:30 " ∀_ " x phi => forall_ x phi
notation:30 " E_ " x phi => exists_ x phi

There is something wrong I am doing with the forall and exists it seems.

[Kayla Thomas]

If I do

inductive IsPropAxiom : Formula → Prop
  -- ⊢ ⊤
  | prop_true_ :
    IsPropAxiom true_

  -- ⊢ phi → (psi → phi)
  | prop_1_
    (phi psi : Formula) :
    IsPropAxiom (phi.imp_ (psi.imp_ phi))

  -- ⊢ (phi → (psi → chi)) → ((phi → psi) → (phi → chi))
  | prop_2_
    (phi psi chi : Formula) :
    IsPropAxiom ((phi.imp_ (psi.imp_ chi)).imp_ ((phi.imp_ psi).imp_ (phi.imp_ chi)))

  -- ⊢ (¬ phi → ¬ psi) → (psi → phi)
  | prop_3_
  (phi psi : Formula) :
  IsPropAxiom (((not_ phi).imp_ (not_ psi)).imp_ (psi.imp_ phi))

  | def_false_ :
  IsPropAxiom (F_ ↔_ (¬_ T_))

  | def_and_
  (phi psi : Formula) :
  IsPropAxiom ( ((phi ∧_ psi) ↔_ ¬_ (phi →_ ¬_ psi)) )

  | def_or_
  (phi psi : Formula) :
  IsPropAxiom ( ((phi ∨_ psi) ↔_ (¬_ phi →_ psi)) )

  | def_iff_
  (phi psi : Formula) :
  IsPropAxiom ( ¬_ (((phi ↔_ psi) →_ ¬_ ((phi →_ psi) →_ ¬_ (psi →_ phi))) →_ ¬_ (¬_ ((phi →_ psi) →_ ¬_ (psi →_ phi)) →_ (phi ↔_ psi))) )

  | def_exists_
  (x : VarName)
  (phi : Formula) :
  IsPropAxiom ((∃_ x phi) ↔_ ¬_ (∀_ x (¬_ phi)))

There is a red underscore under the phi in ∃_ x phi at the bottom and a message saying expected ','.

[Kayla Thomas]

If I change it to exists_ x phi then the message moves to the phi in the (∀_ x (¬_ phi))). If I change that to (forall_ x (¬_ phi))) then the message goes away.

[Kayla Thomas]

Full example

import Std.Tactic.Lint.Frontend
import Mathlib.Util.CompileInductive


namespace FOL


/--
  The type of variable names.
-/
inductive VarName : Type
  | mk : String → VarName
  deriving Inhabited, DecidableEq

/--
  The string representation of variable names.
-/
def VarName.toString : VarName → String
  | VarName.mk x => x

instance : ToString VarName :=
  { toString := fun x => x.toString }

instance : Repr VarName :=
  { reprPrec := fun x _ => x.toString.toFormat }


/--
  The type of predicate names.
-/
inductive PredName : Type
  | mk : String → PredName
  deriving Inhabited, DecidableEq

/--
  The string representation of predicate names.
-/
def PredName.toString : PredName → String
  | PredName.mk X => X

instance : ToString PredName :=
  { toString := fun X => X.toString }

instance : Repr PredName :=
  { reprPrec := fun X _ => X.toString.toFormat }


/--
  The type of definition names.
-/
inductive DefName : Type
  | mk : String → DefName
  deriving Inhabited, DecidableEq

/--
  The string representation of definition names.
-/
def DefName.toString : DefName → String
  | DefName.mk X => X

instance : ToString DefName :=
  { toString := fun X => X.toString }

instance : Repr DefName :=
  { reprPrec := fun X _ => X.toString.toFormat }


/--
  The type of formulas.
-/
inductive Formula : Type
  | pred_const_ : PredName → List VarName → Formula
  | pred_var_ : PredName → List VarName → Formula
  | eq_ : VarName → VarName → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | and_ : Formula → Formula → Formula
  | or_ : Formula → Formula → Formula
  | iff_ : Formula → Formula → Formula
  | forall_ : VarName → Formula → Formula
  | exists_ : VarName → Formula → Formula
  | def_ : DefName → List VarName → Formula
  deriving Inhabited, DecidableEq

compile_inductive% Formula

open Formula


infix:50 " =_ " => eq_
notation " T_ " => true_
notation " F_ " => false_
prefix:40 " ¬_ " => not_
infix:25 " →_ " => imp_
infix:20 " ∧_ " => and_
infix:20 " ∨_ " => or_
infix:20 " ↔_ " => iff_
notation:30 " ∀_ " x phi => forall_ x phi
notation:30 " E_ " x phi => exists_ x phi

inductive IsPropAxiom : Formula → Prop
  | def_exists_
  (x : VarName)
  (phi : Formula) :
  IsPropAxiom ((∃_ x phi) ↔_ ¬_ (∀_ x (¬_ phi)))

[Kayla Thomas]

expected ','

[Kayla Thomas]

@Mario Carneiro fixed it:

notation:30 " ∀_ " x:max phi => forall_ x phi
notation:30 " ∃_ " x:max phi => exists_ x phi

inductive IsPropAxiom : Formula → Prop
  | def_exists_
  (x : VarName)
  (phi : Formula) :
  IsPropAxiom ((∃_ x phi) ↔_ ¬_ (∀_ x (¬_ phi)))

The ∃_ in the notation was misspelled as E_ and I needed to add the :max.