Zulip Chat Archive

Stream: new members

Topic: function on fin by cases


view this post on Zulip 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...)

view this post on Zulip 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

view this post on Zulip Bjørn Kjos-Hanssen (Dec 15 2020 at 22:12):

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

view this post on Zulip Eric Wieser (Dec 15 2020 at 22:12):

by linarith also works for the final case, usually

view this post on Zulip Eric Wieser (Dec 15 2020 at 22:12):

Since the hypotheses at that point are a contradiction

view this post on Zulip Eric Wieser (Dec 15 2020 at 22:13):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 15 2020 at 22:18):

I meant replace the 1 with by linarith

view this post on Zulip Eric Wieser (Dec 15 2020 at 22:18):

Not the whole line

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Dec 15 2020 at 22:19):

Why not just

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

?

view this post on Zulip Bjørn Kjos-Hanssen (Dec 15 2020 at 22:20):

@Yakov Pechersky okay, in this specific case yes

view this post on Zulip Bjørn Kjos-Hanssen (Dec 15 2020 at 22:21):

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

view this post on Zulip 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

view this post on Zulip 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))

view this post on Zulip Yakov Pechersky (Dec 15 2020 at 22:31):

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

view this post on Zulip Alex J. Best (Dec 15 2020 at 22:37):

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

view this post on Zulip Alex J. Best (Dec 15 2020 at 22:39):

Maybe dec_trivial counts as a tactic :smile:

view this post on Zulip 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

?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Dec 15 2020 at 22:55):

and what would the rest be?

view this post on Zulip 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}

view this post on Zulip 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

view this post on Zulip Bjørn Kjos-Hanssen (Dec 15 2020 at 23:00):

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Dec 15 2020 at 23:03):

I'm not sure what you mean by descriptive name

view this post on Zulip Bjørn Kjos-Hanssen (Dec 15 2020 at 23:04):

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

view this post on Zulip 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