function on fin by cases

Stream: new members

[Bjørn Kjos-Hanssen]

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]

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]

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

[Eric Wieser]

by linarith also works for the final case, usually

[Eric Wieser]

Since the hypotheses at that point are a contradiction

[Eric Wieser]

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

[Bjørn Kjos-Hanssen]

@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]

I meant replace the 1 with by linarith

[Eric Wieser]

Not the whole line

[Eric Wieser]

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]

Why not just

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

?

[Bjørn Kjos-Hanssen]

@Yakov Pechersky okay, in this specific case yes

[Bjørn Kjos-Hanssen]

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

[Alex J. Best]

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]

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]

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

[Alex J. Best]

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

[Alex J. Best]

Maybe dec_trivial counts as a tactic :smile:

[Bjørn Kjos-Hanssen]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

and what would the rest be?

[Bjørn Kjos-Hanssen]

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]

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

[Bjørn Kjos-Hanssen]

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

[Yakov Pechersky]

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]

I'm not sure what you mean by descriptive name

[Bjørn Kjos-Hanssen]

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

[Yakov Pechersky]

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