Zulip Chat Archive

Stream: general

Topic: indexed with fin n


view this post on Zulip Logan Murphy (Aug 14 2020 at 02:34):

I've been going over the documentation but I'm having some trouble writing simple concrete tuples using fin n as index type (trying to avoid using vectors). I feel like I should be able to write something like the following

def silly : fin 2  bool := λ i, match i with
| 0,_⟩ := ff
| 1,_⟩ := tt
end

Lean wants an additional case

(nat.succ _).succ, _⟩

If fin 2 is a type with two elements, each being a nat with evidence that this nat is less than two, what is the third case trying to account for?

view this post on Zulip Mario Carneiro (Aug 14 2020 at 02:37):

the third case can be proved impossible, but lean can't show it immediately

view this post on Zulip Mario Carneiro (Aug 14 2020 at 02:37):

You should use fin.cons to construct functions like this

view this post on Zulip Yakov Pechersky (Aug 14 2020 at 02:41):

You can also do tt for 0 and ff for the rest

view this post on Zulip Kenny Lau (Aug 14 2020 at 05:07):

import data.fin2
import data.matrix.notation

open fin2

def silly : fin2 2  bool
| fz      := ff
| (fs fz) := tt

def silly' : fin 2  bool :=
![ff, tt]

#eval silly fz      -- ff
#eval silly (fs fz) -- tt
#eval silly' 0      -- ff
#eval silly' 1      -- tt

Last updated: May 10 2021 at 18:22 UTC