## Stream: general

### Topic: defining a dependent function out of fin 2

#### Scott Morrison (Sep 16 2018 at 04:35):

I'm stuck on something basic to do with fin n.

#### Scott Morrison (Sep 16 2018 at 04:35):

Suppose I have T : fin 2 → Type, and I happen to have X : T ⟨ 0, by tidy ⟩ and a Y : T ⟨ 1, by tidy ⟩.

#### Scott Morrison (Sep 16 2018 at 04:36):

How do I construct the dependent function Π n : fin 2, T n which sends 0 to X and 1 to Y?

#### Simon Hudon (Sep 16 2018 at 04:36):

What about using an if _ then _ else _?

#### Scott Morrison (Sep 16 2018 at 04:37):

How would that work?

#### Scott Morrison (Sep 16 2018 at 04:37):

I remember someone showing me a trick to do match on fin n, but I can't find it anywhere now. :-(

#### Simon Hudon (Sep 16 2018 at 04:37):

def T : fin 2  Type | x :=
if x = 0 then X else Y

#### Simon Hudon (Sep 16 2018 at 04:38):

If you find it again, please show me.

#### Scott Morrison (Sep 16 2018 at 04:40):

I don't see how your suggestion helps, @Simon Hudon:

import tactic.tidy

def T : fin 2 → Type := sorry
def X : T ⟨ 0, by tidy ⟩ := sorry
def Y : T ⟨ 1, by tidy ⟩ := sorry

def S : Π n : fin 2, T n
| x := if x = 0 then X else Y

#### Scott Morrison (Sep 16 2018 at 04:40):

errors with

type mismatch at application
ite (x = 0) X
term
X
has type
T ⟨0, X._proof_1⟩
but is expected to have type
T x

#### Simon Hudon (Sep 16 2018 at 04:41):

Ah ok, I misunderstood your problem

#### Scott Morrison (Sep 16 2018 at 04:47):

Here's a example of my problem:

import tactic.tidy

def T : fin 2 → Type := ([ℕ, ℤ].to_array).data
def X : T ⟨ 0, by tidy ⟩ := begin show ℕ, exact 1 end
def Y : T ⟨ 1, by tidy ⟩ := begin show ℤ, exact -1 end

def S : Π n : fin 2, T n
| ⟨ 0, _ ⟩ := X
| ⟨ 1, _ ⟩ := Y
| _ := sorry

#### Scott Morrison (Sep 16 2018 at 04:47):

The question is to define S, following the intention shown, but without a sorry.

#### Scott Morrison (Sep 16 2018 at 04:47):

(Side questions include better ways to write T in the first place.)

#### Simon Hudon (Sep 16 2018 at 04:47):

One thing you can do is:

def S : Π n : fin 2, T n
| 0,_⟩ := X
| 1,_⟩ := Y

(deleted)

#### Simon Hudon (Sep 16 2018 at 04:58):

Ah! This is even shorter:

by { repeat { have h := lt_of_succ_lt_succ h }, cases h }

#### Mario Carneiro (Sep 16 2018 at 05:01):

that should be false by matching

#### Scott Morrison (Sep 16 2018 at 05:01):

hmm, that doesn't work for me?

#### Scott Morrison (Sep 16 2018 at 05:01):

but Kenny just showed me:

import tactic.tidy
-- import tactic.linarith

def T : fin 2 → Type := ([ℕ, ℤ].to_array).data
def X : T ⟨ 0, by tidy ⟩ := begin show ℕ, exact 1 end
def Y : T ⟨ 1, by tidy ⟩ := begin show ℤ, exact -1 end

def S : Π n : fin 2, T n
| ⟨ 0, _ ⟩ := X
| ⟨ 1, _ ⟩ := Y

#### Scott Morrison (Sep 16 2018 at 05:04):

import tactic.tidy
import tactic.linarith

def T : fin 2 → Type := ([ℕ, ℤ].to_array).data
def X : T ⟨ 0, by tidy ⟩ := begin show ℕ, exact 1 end
def Y : T ⟨ 1, by tidy ⟩ := begin show ℤ, exact -1 end

def S : Π n : fin 2, T n
| ⟨ 0, _ ⟩ := X
| ⟨ 1, _ ⟩ := Y
| ⟨ n + 2, H ⟩ := by exfalso; linarith

#### Mario Carneiro (Sep 16 2018 at 05:13):

import data.fin data.list.basic

def T : fin 2 → Type := ([ℕ, ℤ].to_array).data
def X : T ⟨0, dec_trivial⟩ := (1 : ℕ)
def Y : T ⟨1, dec_trivial⟩ := (-1 : ℤ)

def S : Π n : fin 2, T n :=
fin.cases X (λ i, fin.cases Y (λ i, i.elim0) i)

#### Scott Morrison (Sep 16 2018 at 07:17):

Thanks, Mario. I think I might use the match version, even if it depends on linarith, for decipherability.

#### Scott Morrison (Sep 16 2018 at 07:18):

I think I'll also write a fin_cases tactic, that works with a fin n hypothesis with n a numeral.

#### Scott Morrison (Sep 16 2018 at 07:18):

(and actually gives you all the cases)

Last updated: May 08 2021 at 19:11 UTC