Zulip Chat Archive

Stream: general

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


view this post on Zulip Scott Morrison (Sep 16 2018 at 04:35):

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

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

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

view this post on Zulip Simon Hudon (Sep 16 2018 at 04:36):

What about using an if _ then _ else _?

view this post on Zulip Scott Morrison (Sep 16 2018 at 04:37):

How would that work?

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

view this post on Zulip Simon Hudon (Sep 16 2018 at 04:37):

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

view this post on Zulip Simon Hudon (Sep 16 2018 at 04:38):

If you find it again, please show me.

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

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

view this post on Zulip Simon Hudon (Sep 16 2018 at 04:41):

Ah ok, I misunderstood your problem

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

view this post on Zulip Scott Morrison (Sep 16 2018 at 04:47):

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

view this post on Zulip Scott Morrison (Sep 16 2018 at 04:47):

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

view this post on Zulip 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
| succ (succ n),h := false.elim $ by { admit, }

view this post on Zulip Scott Morrison (Sep 16 2018 at 04:49):

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

view this post on Zulip Simon Hudon (Sep 16 2018 at 04:50):

My brain times out looking for one

view this post on Zulip Scott Morrison (Sep 16 2018 at 04:50):

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

view this post on Zulip Scott Morrison (Sep 16 2018 at 04:51):

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

view this post on Zulip Simon Hudon (Sep 16 2018 at 04:51):

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

view this post on Zulip Simon Hudon (Sep 16 2018 at 04:51):

Oh, that's too bad

view this post on Zulip Scott Morrison (Sep 16 2018 at 04:52):

There was a recent addition saying it could do nat.

view this post on Zulip Scott Morrison (Sep 16 2018 at 04:52):

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

view this post on Zulip Simon Hudon (Sep 16 2018 at 04:53):

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

view this post on Zulip Simon Hudon (Sep 16 2018 at 04:54):

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

view this post on Zulip Scott Morrison (Sep 16 2018 at 04:56):

(deleted)

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

view this post on Zulip Mario Carneiro (Sep 16 2018 at 05:01):

that should be false by matching

view this post on Zulip Scott Morrison (Sep 16 2018 at 05:01):

hmm, that doesn't work for me?

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

view this post on Zulip Mario Carneiro (Sep 16 2018 at 05:03):

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

view this post on Zulip Scott Morrison (Sep 16 2018 at 05:03):

ah, and the new linarith really does it!

view this post on Zulip Kenny Lau (Sep 16 2018 at 05:03):

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 _ _

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

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

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

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

view this post on Zulip Scott Morrison (Sep 16 2018 at 07:18):

(and actually gives you all the cases)


Last updated: May 08 2021 at 19:11 UTC