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