RFC: make && and || right-associative

Stream: lean4

[Kenny Lau]

Currently && and || are left-associative, which does not align with ∧ and ∨. Moreover, Bool.and and Bool.or are actually short-circuiting on the left, so they should be right-associative, because currently (b₁ && b₂) && b₃ would never short-circuit on b₁ but b₁ && (b₂ && b₃) would.

[Kenny Lau]

or rather, the former takes 2 steps to short-circuit on b₁, and the latter takes only one step

[Kenny Lau]

I wrote some code to test the time to kernel-reduce false && false && ... && false (repeated 2000 times), with left-associative vs. right-associative:

[Kenny Lau]

import Lean

open Lean

syntax choice := &"left" <|> &"right"

elab "test" c:choice : term => do
  have falseE := mkConst ``false
  let mut e₁ : Expr := falseE
  let mut e₂ : Expr := falseE
  for _ in List.replicate 2000 0 do
    e₁ := mkApp2 (mkConst ``Bool.and) e₁ falseE
    e₂ := mkApp2 (mkConst ``Bool.and) falseE e₂
  match c with
  | `(choice| left) => return e₁
  | _ => return e₂

set_option maxRecDepth 99999

#time -- 62ms
#reduce test left

#time -- 7ms
#reduce test right

[Eric Wieser]

I suspect this is copying the associativity of these operators in C/C++ and in python