How to destructure `fin` using pattern matching?

Stream: new members

[Marko Grdinić]

-- def nat.foldl.fin {α : Type} (n' : nat) : ∀ (n : fin n') (s : α) (f : fin n' → α → α), α
--     | 0 s f := s
--     | (n+1) s f := f n (nat.foldl.fin n s f)

def nat.foldl {α : Type} : ∀ (n : nat) (s : α) (f : nat → α → α), α
    | 0 s f := s
    | (n+1) s f := f n (nat.foldl n s f)

def array.map_foldl {α β : Type} {n : nat} (a : array n α) (f : α → β → α × β) (s : β) : array n α × β :=
    n.foldl (a, s) (fun (i : fin n) ⟨ a , s ⟩,
        let (el, s) := f (a.read i) s in
        (a.write i el, s)
        )

I am trying to make a little helper for array and it requires fins rather than nat in order to ensure bounds checking. But fin uses anonymous constructors and I am not sure how to destructure it in patterns nor how to construct it normally. How should I do this?

[Marko Grdinić]

As an aside, does Lean have any special syntax for monadic computations like Haskell or Idris for example?

[Anne Baanen]

There is do notation, described here: https://leanprover.github.io/programming_in_lean/#07_Monads.html

[Anne Baanen]

Pointy brackets ⟨_, _, _, ...⟩ work for con-/destructing any structure:

def nat.foldl.fin {α : Type} (n' : nat) : ∀ (n : fin n') (s : α) (f : fin n' → α → α), α
| ⟨0, _⟩ s f := s
| ⟨n+1, lt⟩ s f := let n' : fin n' := ⟨n, sorry⟩ in f n' (nat.foldl.fin n' s f)

[Marko Grdinić]

def nat.foldl.fin {α : Type} (n' : nat) : ∀ (n : fin n') (s : α) (f : fin n' → α → α), α
| ⟨0, _⟩ s f := s
| ⟨n+1, lt⟩ s f := let n' : fin n' := ⟨n, buffer.lt_aux_1 lt ⟩ in f n' (nat.foldl.fin n' s f)

I've filled in that sorry. Interesting that when I write it like...

def nat.foldl.fin {α : Type} (n' : nat) : ∀ (n : fin n') (s : α) (f : fin n' → α → α), α
| ⟨0, _⟩ s f := s
| ⟨n+1, lt⟩ s f := have n' : fin n', from ⟨n, buffer.lt_aux_1 lt ⟩, f n' (nat.foldl.fin n' s f)

It runs into issues with termination checking. Why is that?

[Johan Commelin]

I guess the trouble is that fin is not an inductive type... but maybe there are ways to deal with that.

[Rob Lewis]

No, the problem is that using have hides the definitional content of n'. If you do that, n' is just an arbitrary term of type fin n', and Lean can't confirm that it's structurally smaller than <n+1, lt>.

[Rob Lewis]

(Careful with duplicating the variable name n', by the way!)

[Rob Lewis]

In general, you should use have for propositions and let for data.

[Marko Grdinić]

I see.

(Careful with duplicating the variable name n', by the way!)

That reminds me, is Lean lazy like Haskell or strict like Idris? I remember running into unexpected issues when doing variable shadowing in Haskell.

[Reid Barton]

It's strict, and let is nonrecursive.

[Marko Grdinić]

def nat.foldl.fin_template {α : nat → Type} (n' : nat)
    : ∀ (n : fin n') (s : α 0) (f : ∀ (n : fin n'), (α n.val) → α (n.val+1)), α n.val
| ⟨0, _⟩ s f := s
| ⟨n+1, lt⟩ s f := let n' : fin n' := ⟨n, buffer.lt_aux_1 lt ⟩ in f n' (nat.foldl.fin_template n' s f)

def nat.foldl.fin {α : nat → Type}
    : ∀ (n : nat) (s : α 0) (f : ∀ (n : fin n), (α n.val) → α (n.val+1)), α n
| 0 s f := s
| (n+1) s f :=
    let n' : fin (n+1) := ⟨ n, lt_add_one n ⟩ in
    f n' (nat.foldl.fin_template (n+1) n' s f)

def array.map_foldl {α β χ : Type} {n : nat} (a : array n α) (f : α → β → χ × β) (s : β) : array n χ × β :=
    @nat.foldl.fin (fun n, array n χ × β) n (array.nil, s)
        (fun (i : fin n) ⟨ a' , s ⟩,
            let (el, s) := f (a.read i) s in
            (a'.push_back el, s)
            )

Here is how I did the functions. I realized after doing the first version that the types weren't general enough for my use case so I redesigned them. This is coming along nicely. I've studied dependently typed programming and theorem proving seriously for the last 6 months, but this is the first time I am doing a project out of my own volition without some book or tutorial to guide me. I am still acclimating to Lean, but it is definitely nice to not be completely lost at what is going on. There were many such situations in the first few months while I was working in Coq and to a lesser extent, Agda.