Pretty printing `let (a,b) := `

Stream: lean4

[Tomas Skrivan]

Is there a way to pretty print let (a,b) := ... ? It gets de-sugared into a match statement which are a bit hard to read when the expression gets a bit more complicated:

#check
  let (a, b) := (0,1)
  let (a, b) := (b, a + b)
  let (a, b) := (b, a + b)
  b

The output is:

match (0, 1) with
| (a, b) =>
  match (b, a + b) with
  | (a, b) =>
    match (b, a + b) with
    | (a, b) => b : ℕ

[Tomas Skrivan]

Here is my attempt, but it does not work

set_option pp.all true in
def bar :
  (let (a, b) := (0,1)
   let (a, b) := (b, a + b)
   b) = 1 :=
by
  rfl

@[app_unexpander bar.match_1] def unexpandMatch : Lean.PrettyPrinter.Unexpander
  | `($(_) $motive:term $xy:term fun ($a:ident $b:ident : $A:term) => $val:term) => `(let ($a,$b) := $xy; $val)
  | _  => throw ()

#check bar

[James Gallicchio]

Not only does it print ugly, it proves ugly too! I don't know how let binding hypotheses work, but it would be great if single case match expressions were treated specially so that e.g. let (a,b) := (0,1) would introduce (a,b) = (0,1) to the context

[Mario Carneiro]

that's not a thing though

[Mario Carneiro]

or rather, if you want an equality then that's not what let does

[Mario Carneiro]

The set tactic will introduce an equality hypothesis like this

[Mario Carneiro]

you can also use (r)cases for this

[James Gallicchio]

I don't want to de-rail Tomas's question too much, but here is an example where I would want better pretty-printing and better proofing:

import Std

def div_mod (n d : Nat) (hd : d > 0) : Nat × Nat :=
  if h:n < d then (0,n) else
  have : n - d < n := by
    apply Nat.sub_lt ?_ hd
    apply Nat.lt_of_lt_of_le hd
    apply Nat.ge_of_not_lt h
  let res := div_mod (n-d) d hd
  (res.1+1,res.2)
termination_by _ n _ _ => n

theorem Nat.div_mod_eq (n d : Nat) {hd}
  : div_mod n d hd = (q,r) → n = q * d + r
  := by
  intro h
  induction n using Nat.strongInductionOn generalizing q r
  case ind n ih =>
  unfold div_mod at h
  split at h
  next hn =>
    rcases h
    simp
  next hn =>
    have : n - d < n := by
      apply Nat.sub_lt ?_ hd
      apply Nat.lt_of_lt_of_le hd
      apply Nat.ge_of_not_lt hn
    generalize hres : div_mod (n-d) d hd = res at h
    have := ih (n-d) this hres
    simp at h
    rcases h with ⟨rfl,rfl⟩
    rw [Nat.succ_mul,
        Nat.add_comm _ d,
        Nat.add_assoc d,
        ←this,
        Nat.add_comm,
        Nat.sub_add_cancel]
    apply Nat.ge_of_not_lt hn

In particular, I'd want to write let (q,r) := div_mod (n-d) d hd in the function instead of having to assign the product to an intermediate value.

[James Gallicchio]

oh wait this is a bad example because the proof still works with that :joy:

[James Gallicchio]

you can still see the finagling I have to do with generalize

[Mario Carneiro]

an alternative to the generalize and the three lines after it is

    revert h
    rcases hres : div_mod (n-d) d hd with ⟨q, r⟩
    simp; rintro rfl rfl
    have := ih (n-d) this hres

[Mario Carneiro]

alternatively, you don't even need the cases in this example since

    cases h
    have := ih (n-d) this rfl

works

[James Gallicchio]

Yeah, I think the most readable way to do this is

    match hres : div_mod (n-d) d hd with
    | (q',r') =>
    rw [hres] at h
    cases h
    have := ih (n-d) this hres

but that is still quite a bit of finagling for something that (IMO) should just work

[Sebastian Ullrich]

You can also just use another split at h, it pretty much does what you asked for
James Gallicchio said:

let (a,b) := (0,1) would introduce (a,b) = (0,1) to the context

[Sebastian Ullrich]

That destructuring let requires some sort of case split in the proof unless it is computed away seems quite reasonable to me

[James Gallicchio]

ah, you're totally right. match in hypothesis ==> split.

that might be an argument against delaborating it to a destructuring let.

[James Gallicchio]

though... on the other hand, perhaps it should be specially delaborated, and there should be a new tactic to perform split at <hyp>; case _ <vars> _ =>, since I imagine that is often what you want to do.

[James Gallicchio]

(where the new var names are copied from the vars bound in the destructuring let)

[Sebastian Ullrich]

Well that would be unhygienic

[James Gallicchio]

fair enough. I guess if I had to explain it to a first-year I'd tell them that destructuring lets are just doing a match, and that's why split works on both matches and lets.....