defining a dependent function out of `fin 2`

Stream: general

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Simon Hudon]

What about using an if _ then _ else _?

[Scott Morrison]

How would that work?

[Scott Morrison]

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

[Simon Hudon]

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

[Simon Hudon]

If you find it again, please show me.

[Scott Morrison]

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]

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]

Ah ok, I misunderstood your problem

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Simon Hudon]

One thing you can do is:

def S : Π n : fin 2, T n
| ⟨0,_⟩ := X
| ⟨1,_⟩ := Y
| ⟨succ (succ n),h⟩ := false.elim $ by { admit, }

[Scott Morrison]

Excellent! That works, now the question becomes --- is my distant memory that there's an even better solution, correct? :-)

[Simon Hudon]

My brain times out looking for one

[Scott Morrison]

And what is the canonical way to fill in that admit, these days?

[Scott Morrison]

I'd hoped that linarith was up to proving discharging n+2 < 2 implies false, but apparently not.

[Simon Hudon]

There's a linarith tactic coming down the pipes. Maybe it can handle nat now? We'd have to check

[Simon Hudon]

Oh, that's too bad

[Scott Morrison]

There was a recent addition saying it could do nat.

[Scott Morrison]

Oh, maybe I haven't pulled that one yet...

[Simon Hudon]

It feels like the kind of proposition that you should be able to prove in two steps. All I can think of takes more

[Simon Hudon]

| ⟨succ (succ n),h⟩ := false.elim $ by { apply not_lt_of_ge _ h, repeat { apply succ_le_succ <|> apply zero_le } }

[Scott Morrison]

(deleted)

[Simon Hudon]

Ah! This is even shorter:

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

[Mario Carneiro]

that should be false by matching

[Scott Morrison]

hmm, that doesn't work for me?

[Scott Morrison]

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
| ⟨ nat.succ (nat.succ n), H ⟩ := false.elim $ by cases H with H H; cases H with H H; cases H

[Mario Carneiro]

You can also use fin.succ_rec_on to get the right induction principle

[Scott Morrison]

ah, and the new linarith really does it!

[Kenny Lau]

how about

@[elab_as_eliminator]
def fin2.rec_on {C : fin 2 → Sort*} : ∀ (n : fin 2), C 0 → C 1 → C n
| ⟨0, _⟩ C0 _ := C0
| ⟨1, _⟩ _ C1 := C1
| ⟨n+2, H⟩ _ _ := false.elim $ not_le_of_gt H $ nat.le_add_left _ _

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

(and actually gives you all the cases)