## 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 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ć (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