# Zulip Chat Archive

## Stream: new members

### Topic: How to destructure `fin` using pattern matching?

#### Marko Grdinić (Oct 18 2019 at 12:51):

-- 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 `fin`

s 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ć (Oct 18 2019 at 12:53):

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

#### Anne Baanen (Oct 18 2019 at 12:54):

There is `do`

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

#### Anne Baanen (Oct 18 2019 at 13:01):

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ć (Oct 18 2019 at 13:19):

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 (Oct 18 2019 at 13:22):

I guess the trouble is that `fin`

is not an inductive type... but maybe there are ways to deal with that.

#### Rob Lewis (Oct 18 2019 at 13:24):

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 (Oct 18 2019 at 13:25):

(Careful with duplicating the variable name `n'`

, by the way!)

#### Rob Lewis (Oct 18 2019 at 13:26):

In general, you should use `have`

for propositions and `let`

for data.

#### Marko Grdinić (Oct 18 2019 at 13:36):

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 (Oct 18 2019 at 13:46):

It's strict, and `let`

is nonrecursive.

#### Marko Grdinić (Oct 18 2019 at 14:42):

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.

Last updated: Dec 20 2023 at 11:08 UTC