Zulip Chat Archive

Stream: general

Topic: indexed with fin n


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?

Mario Carneiro (Aug 14 2020 at 02:37):

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

Mario Carneiro (Aug 14 2020 at 02:37):

You should use fin.cons to construct functions like this

Yakov Pechersky (Aug 14 2020 at 02:41):

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

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: Dec 20 2023 at 11:08 UTC