alternative to nesting of if..then..else

Stream: general

[Alexandre Rademaker]

def appendSuffixF : String → String → String
  | stem, suffix => stem ++ suffix.map (vh stem)
 where
  vh s :=
   if s.any (· ∈ "aou".toList) then back
   else if s.any (· ∈ [aUml, oUml, 'y']) then front else id

In the vh local definition above, I would like to avoid the if ... then ... else if ... then ... else .... The guards from Haskell would be perfect here. Any alternative?

Do we have any debug option to measure the time to evaluate a function? Like

#eval time EXP

[Edward van de Meent]

is it the syntax you dislike, or the resulting definition?

[Alexandre Rademaker]

The syntax, the function is working as expected.

[Edward van de Meent]

the reason i ask is because i don't know of an alternative definition, however i do know that lean has a nifty feature where you can define your own syntax

[Edward van de Meent]

you might be particularly interested in the book metaprogramming in lean 4

[Edward van de Meent]

(deleted)

[Alexandre Rademaker]

Yes, definitely, this book is on my list. Thanks.

[Kim Morrison]

if is pretty standard in Lean code, and probably preferable to using Haskell like "guard"s. We have tactic infrastructure (split in Lean, and split_ifs in Mathlib) that handles it well.

[Kyle Miller]

Lean has special support for else if in the whitespace-sensitive syntax for you to be able to write

def appendSuffixF : String → String → String
  | stem, suffix => stem ++ suffix.map (vh stem)
 where
  vh s :=
   if s.any (· ∈ "aou".toList) then
     back
   else if s.any (· ∈ [aUml, oUml, 'y']) then
     front
   else
     id

Sometimes you also see

def appendSuffixF : String → String → String
  | stem, suffix => stem ++ suffix.map (vh stem)
 where
  vh s :=
   if s.any (· ∈ "aou".toList) then back
   else if s.any (· ∈ [aUml, oUml, 'y']) then front
   else id

But you don't need the whole sub-if statement nested under the else

[Kyle Miller]

I'm not sure this is the only issue with it, but lean4#371 mentions a request for pattern guards.

[Kyle Miller]

(I was going to give some other variants, but I'm confused about this function since it doesn't type check...

Anyway, I think this looks better, but I can't check it:

def appendSuffixF (stem suffix : String) : String :=
  stem ++ suffix.map vh
where
  vh :=
    if stem.any (· ∈ ['a', 'o', 'u']) then back
    else if stem.any (· ∈ ['ä', 'ö', 'y']) then front
    else id

)

[Paul Chisholm]

I like Lean' s compact syntax but find chained if-then-else to be a bit awkward. I always liked Dijkstra's Guarded Command Language (GCL), it has a nice visual balance, which led to this definition:

syntax " if " (term " ⟹ " term " ‖ ")+ " ⟹ " term " fi " : term

macro_rules
  | `(if $c₁ ⟹ $e₁ ‖ ⟹ $e₂ fi) =>
    `(ite $c₁ $e₁ $e₂)
  | `(if $c₁ ⟹ $e₁ ‖ $[$cs₁ ⟹ $es₁ ‖]* ⟹ $e₂ fi) =>
    `(ite $c₁ $e₁ (if $[$cs₁ ⟹ $es₁ ‖]* ⟹ $e₂ fi))

def test (n : Nat) : String :=
    if n == 0 ⟹ "zero"
     ‖ n == 1 ⟹ "one"
     ‖ n == 2 ⟹ "two"
     ‖ n == 3 ⟹ "three"
     ‖        ⟹ "> 3"
    fi

#eval test 2
#eval test 4

def appendSuffixF (stem suffix : String) : String :=
  stem ++ suffix.map vh
where
  vh :=
    if stem.any (· ∈ ['a', 'o', 'u']) ⟹ id
     ‖ stem.any (· ∈ ['ä', 'ö', 'y']) ⟹ id
     ‖                                ⟹ id
    fi

Unlike GCL, the definition is deterministic, and requires a catchall.

Note: I replaced back and front in the definition of appendSuffixF to allow it to compile.

[James Sully]

Kyle Miller said:

I'm not sure this is the only issue with it, but lean4#371 mentions a request for pattern guards.

This seems to be for or-patterns, which aren't quite the same thing

[James Sully]

although they are mentioned in the issue discussion

[Edward van de Meent]

Paul Chisholm said:

which led to this definition:

is there a(n easy) way to amend this definition to also allow for dite?

[Kyle Miller]

@Paul Chisholm Interesting; a version of that that would fit right in as Lean syntax would be a Lisp-style cond using match syntax:

syntax condAlt := "| " ppIndent(term)? Lean.Parser.darrow colGe term
syntax "cond " many1(ppLine condAlt) : term

macro_rules
  | `(cond $[| $(cs)? => $as]* ) => show MacroM Term from do
    if as.isEmpty then Macro.throwUnsupported
    let t ← `(true)
    let cs := cs.map fun c => c.getD t
    unless cs.back == t do Macro.throwError "Last alternative must be unconditional"
    (cs.pop.zip as.pop).foldrM (init := as.back) fun (c, a) e =>
      `(if $c then $a else $e)

def test (n : Nat) : String :=
  cond
  | n == 0 => "zero"
  | n == 1 => "one"
  | n == 2 => "two"
  | n == 3 => "three"
  |        => "> 3"

[Kyle Miller]

@Edward van de Meent Yes:

import Lean

open Lean

syntax condAlt := "| " ppIndent(atomic(binderIdent " : ")? term)? Parser.darrow colGe term
syntax "cond " many1(ppLine condAlt) : term

macro_rules
  | `(cond $[| $[$[$bis:binderIdent :]? $cs:term]? => $as]* ) => show MacroM Term from do
    if as.isEmpty then Macro.throwUnsupported
    unless cs.back.isNone do Macro.throwError "Last alternative must be unconditional"
    let cs ← cs.mapM fun c => c.getDM `(true)
    unless bis.back.join.isNone do Macro.throwError "Last alternative must not have a proof binder"
    (bis.pop.zip (cs.pop.zip as.pop)).foldrM (init := as.back) fun (bi, c, a) e =>
      if let some bi := bi.join then
        `(if $bi : $c then $a else $e)
      else
        `(if $c then $a else $e)

def test (n : Nat) : String :=
  cond
  | n == 0 => "zero"
  | n == 1 => "one"
  | n == 2 => "two"
  | n == 3 => "three"
  |        => "> 3"

example (n : Nat) (a : Array Nat) : Nat :=
  cond
  | h : n < a.size => a[n]
  | => 0

[Kyle Miller]

Maybe _ could be allowed for the unconditional case.

[Edward van de Meent]

what are the imports?

[Kyle Miller]

@Edward van de Meent I just updated the last code block

[Paul Chisholm]

@Kyle Miller Nice alternative and, as you say, more consistent with existing Lean syntax.

[Alexandre Rademaker]

Thank you all, nice syntax extension. It will be cool to show the students how Lean language can be extended and a concrete example when this can make sense.

[Mac Malone]

Note that this syntax can reuse the if keyword instead of reserving a new one (since the syntaxes are non-overlapping):

import Lean.Parser

open Lean

syntax ifAlt := "| " ppIndent(atomic(binderIdent " : ")? term)? Parser.darrow colGe term
syntax "if " many1(ppLine ifAlt) : term

macro_rules
  | `(if $[| $[$[$bis:binderIdent :]? $cs:term]? => $as]* ) => show MacroM Term from do
    if as.isEmpty then Macro.throwUnsupported
    unless cs.back.isNone do Macro.throwError "Last alternative must be unconditional"
    let cs ← cs.mapM fun c => c.getDM `(true)
    unless bis.back.join.isNone do Macro.throwError "Last alternative must not have a proof binder"
    (bis.pop.zip (cs.pop.zip as.pop)).foldrM (init := as.back) fun (bi, c, a) e =>
      if let some bi := bi.join then
        `(if $bi : $c then $a else $e)
      else
        `(if $c then $a else $e)

def test (n : Nat) : String :=
  if
  | n == 0 => "zero"
  | n == 1 => "one"
  | n == 2 => "two"
  | n == 3 => "three"
  |        => "> 3"

example (n : Nat) (a : Array Nat) : Nat :=
  if
  | h : n < a.size => a[n]
  | => 0

[Yury G. Kudryashov]

Should we add this syntax to (a dependency of) Mathlib?