hidden benefit?

Stream: lean4

[Joseph O]

So, @Kyle Miller wrote this function some time ago:

def nth : {αs : List Type} → (t : Tuple αs) → (n : Nat) → (h : n < αs.length := by simp) → αs.get' n h
  | _, Tuple.unit, n, h => False.elim $ Nat.not_lt_zero _ h
  | _, Tuple.cons x xs, 0, h => x
  | _, Tuple.cons x xs, (n+1), h => xs.nth n (Nat.le_of_succ_le_succ h)

and i was wondering why he did not write it instead as

def nth {αs : List Type} : (t : Tuple αs) → (n : Nat) → (h : n < αs.length := by simp) → αs.get' n h
  | Tuple.unit, n, h => False.elim $ Nat.not_lt_zero _ h
  | Tuple.cons x xs, 0, h => x
  | Tuple.cons x xs, (n+1), h => xs.nth n (Nat.le_of_succ_le_succ h)

which is cleaner. Is there some hidden benefit I am unaware of?

[James Gallicchio]

Does the latter declaration typecheck? When Lean unifies within the cases of a match I think it only unifies the parameters that are within the match. I'm not sure whether we need to unify against αs here to get it to compile

[Joseph O]

James Gallicchio said:

Does the latter declaration typecheck? When Lean unifies within the cases of a match I think it only unifies the parameters that are within the match. I'm not sure whether we need to unify against αs here to get it to compile

The second one typechecks

[James Gallicchio]

Huh, cool :D I don't think there's any difference then

[Joseph O]

Ah ok. Is it some sort of style then, because I have seen other people writing functions in this style as well.

[Horatiu Cheval]

I guess the implicit matching is only against the parameters to the right of the colon (I only forget the precise changes from Lean 3 to Lean 4 here). But in Lean 4 it is also only a matter of style and syntactic sugar, while in 3 there was an actual distinction (you couldn't match on something to the left of the colon)

[Joseph O]

Ah I see.
That makes sense

[Sebastian Ullrich]

If I'm not mistaken, this is a recent change, it didn't use to work

[James Gallicchio]

Do matches now unify everything in context instead of just the match parameters?

[Sebastian Ullrich]

Yes https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2022-02-17

[Kyle Miller]

It's going to take a while to learn to write things in Lean 4 that in Lean 3 I was trained against expecting should work!

[Leonardo de Moura]

We have been improving the dependent pattern matching in Lean 4 since March of 2021. Many of the improvements appeared after @Daniel Fabian pointed out he had to use too many _s in his definitions. Example:

def balanceRR {h c} (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
match h, c, left, right with
| _, _, left, HR c => RR left y c
| _, _, left, HR c => RR left y c
| _, _, R a x b, HB c => LR (R a x b) y c
| _, _, B a x b, HB c => V (R (B a x b) y c)
| _, _, Leaf, HB c => V (R Leaf y c)

Now, we just have to write

def balanceRR (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
  match left, right with
  | left,    HR c => RR left y c
  | R a x b, HB c => LR (R a x b) y c
  | B a x b, HB c => V (R (B a x b) y c)
  | Leaf,    HB c => V (R Leaf y c)