## Stream: new members

### Topic: function on fin by cases

#### Bjørn Kjos-Hanssen (Dec 15 2020 at 22:04):

def τ : (fin 2) → (fin 2) → (fin 2)
| 0 0 := 1
| 0 1 := 0
| 1 0 := 1
| 1 1 := 1


This doesn't work... the following cases are missing: τ ⟨(succ _).succ, _⟩ ⟨_, _⟩.

What's a better way to define a finite function? (The other way I know would be using nested ite...)

#### Alex J. Best (Dec 15 2020 at 22:10):

You can just add a final case which would never be matched

def τ : (fin 2) → (fin 2) → (fin 2)
| ⟨0,_⟩ ⟨0,_⟩ := 1
| ⟨0,_⟩ ⟨1,_⟩ := 0
| ⟨1,_⟩ ⟨0,_⟩ := 1
| ⟨1,_⟩ ⟨1,_⟩ := 1
| _ _ := 1


#### Bjørn Kjos-Hanssen (Dec 15 2020 at 22:12):

Thanks! Why do we need the⟨0,_⟩ as opposed to just 0?

#### Eric Wieser (Dec 15 2020 at 22:12):

by linarith also works for the final case, usually

#### Eric Wieser (Dec 15 2020 at 22:12):

Since the hypotheses at that point are a contradiction

#### Eric Wieser (Dec 15 2020 at 22:13):

@Bjørn Kjos-Hanssen, the _ matches the proof that 0 < 2

#### Bjørn Kjos-Hanssen (Dec 15 2020 at 22:17):

@Eric Wieser thanks ---

def τ : (fin 2) → (fin 2) → (fin 2)
| ⟨0,_⟩ ⟨0,_⟩ := 1
| ⟨0,_⟩ ⟨1,_⟩ := 0
| ⟨1,_⟩ ⟨0,_⟩ := 1
| ⟨1,_⟩ ⟨1,_⟩ := 1
by linarith


doesn't seem to work in this case

#### Eric Wieser (Dec 15 2020 at 22:18):

I meant replace the 1 with by linarith

#### Eric Wieser (Dec 15 2020 at 22:18):

Not the whole line

#### Eric Wieser (Dec 15 2020 at 22:18):

But using that instead of 1 only really matters for the case when you don't have any default value available, which this isn't

#### Yakov Pechersky (Dec 15 2020 at 22:19):

Why not just

def τ : (fin 2) → (fin 2) → (fin 2)
| ⟨0,_⟩ ⟨1,_⟩ := 0
| _ _ := 1


?

#### Bjørn Kjos-Hanssen (Dec 15 2020 at 22:20):

@Yakov Pechersky okay, in this specific case yes

#### Bjørn Kjos-Hanssen (Dec 15 2020 at 22:21):

okay I'll look into how to import linarith ...

#### Alex J. Best (Dec 15 2020 at 22:22):

I think to use linarith to not give a value for the impossible cases you need two matches

def τ : (fin 2) → (fin 2) → (fin 2)
| ⟨0,_⟩ ⟨0,_⟩ := 1
| ⟨0,_⟩ ⟨1,_⟩ := 0
| ⟨1,_⟩ ⟨0,_⟩ := 1
| ⟨1,_⟩ ⟨1,_⟩ := 1
| ⟨h + 2, _⟩ _ := by linarith
| _ ⟨g + 2, _⟩ := by linarith


#### Yakov Pechersky (Dec 15 2020 at 22:30):

Or, to avoid linarith and see what's going on:

def τ : (fin 2) → (fin 2) → (fin 2)
| ⟨0, _⟩ ⟨0, _⟩ := 1
| ⟨0, _⟩ ⟨1, _⟩ := 1
| ⟨1, _⟩ ⟨0, _⟩ := 1
| ⟨1, _⟩ ⟨1, _⟩ := 1
| ⟨n + 2, hn⟩ ⟨_, _⟩ := false.elim (not_lt_of_le n.zero_le (add_lt_iff_neg_right.mp hn))
| ⟨_, _⟩ ⟨m + 2, hm⟩ := false.elim (not_lt_of_le m.zero_le (add_lt_iff_neg_right.mp hm))


#### Yakov Pechersky (Dec 15 2020 at 22:31):

There might be a cleaner term-mode proof, but that's how I thought about it

#### Alex J. Best (Dec 15 2020 at 22:37):

absurd hn dec_trivial works as a term mode replacement of by linarith

#### Alex J. Best (Dec 15 2020 at 22:39):

Maybe dec_trivial counts as a tactic :smile:

#### Bjørn Kjos-Hanssen (Dec 15 2020 at 22:51):

Thanks all for the at least four different solutions! Maybe this is a different topic but is there a way to do something like

def τ : (fin 2) → (fin 2) → (fin 2)
let q_ε := 0 in
| ⟨ q_ε,_⟩ ⟨0,_⟩ := 1
-- omitting the rest


?

#### Yakov Pechersky (Dec 15 2020 at 22:54):

What will you be doing with this tau definition? let ... in ...  might not have the best structure for proving things about it.

#### Yakov Pechersky (Dec 15 2020 at 22:54):

Do you want to have this sort of structure to easily make the variants where you change the q_eps?

#### Yakov Pechersky (Dec 15 2020 at 22:55):

and what would the rest be?

#### Bjørn Kjos-Hanssen (Dec 15 2020 at 22:58):

I want to do something with say fin 6 instead of fin 2, and then have each element of fin 6 have a descriptive name... or maybe replace fin 6 by a set or type defined in a different way, like {apple, banana, orange, grape, plum, berry}

#### Bjørn Kjos-Hanssen (Dec 15 2020 at 22:59):

Using the numbers 0 through 5 does not give enough intuition in my intended use case

#### Bjørn Kjos-Hanssen (Dec 15 2020 at 23:00):

Yes, I also noticed that let..in is cumbersome for proofs.

#### Yakov Pechersky (Dec 15 2020 at 23:02):

import tactic.derive_fintype

@[derive [fintype, decidable_eq]]
inductive bjorntype
| apple
| banana
| orange
| grape
| plum
| berry

open bjorntype

def τ : bjorntype → bjorntype → ℕ
| berry plum := 0
| _ _ := 1

#reduce τ berry plum
#reduce τ berry berry


#### Yakov Pechersky (Dec 15 2020 at 23:03):

I'm not sure what you mean by descriptive name

#### Bjørn Kjos-Hanssen (Dec 15 2020 at 23:04):

This looks great... yes by descriptive name I mean just something like this, apple

#### Yakov Pechersky (Dec 15 2020 at 23:08):

And you then have that your custom inductive type is isomorphic to fin 6 via docs#fintype.equiv_fin

Last updated: May 15 2021 at 23:13 UTC