Zulip Chat Archive

Stream: new members

Topic: Elimination of product of fintypes in proof


view this post on Zulip Yakov Pechersky (Jun 22 2020 at 05:12):

I'm testing out notation for n-dim "matrices" by reworking data.matrix.notation. I had a wrong defn for vec_cons before. Now that I've fixed it, I'm trying to prove the amended lemmas, but I don't know the right tactic invocation to reduce the indexing. mwe with sorry'd lemma below:

import data.matrix.notation

universe u
variables {α : Type u}

open_locale matrix

variables {ι : Type} [fintype ι]

def vec_empty : (fin 0 × ι)  α :=
λ n, i, fin_zero_elim n

def vec_cons {n : } (h : ι  α) (t : (fin n × ι)  α) : (fin n.succ × ι)  α :=
λ ⟨⟨ni, hni, mi, (nat.cases_on ni
  (λ _, h mi) (λ k hk, t (k, nat.lt_of_succ_lt_succ hk, mi))) hni

notation `![` l:(foldr `, ` (h t, vec_cons h t) vec_empty `]`) := l

def vec_head {n : } (v : (fin n.succ × ι)  α) : ι -> α :=
λ i, v ⟨⟨0, nat.succ_pos', i

def vec_tail {n : } (v : (fin n.succ × ι)  α) : (fin n × ι)  α :=
λ ⟨⟨k, hn, i, v ⟨⟨k.succ, nat.succ_lt_succ hn, i

lemma empty_eq (v : (fin 0 × ι)  α) : v = ![] :=
by { ext i, fin_cases i }

variables {m : }

@[simp] lemma cons_val_zero (x : ι  α) (u : (fin m × ι)  α) : (λ i, vec_cons x u 0, i) = x :=
begin
  ext i,
  sorry
end

view this post on Zulip Yakov Pechersky (Jun 22 2020 at 05:18):

Doing cases m doesn't seem productive since the defn of vec_cons just relies on passing 0 to access the h mi case, which is just the element we just vec_cons'd in.

view this post on Zulip Johan Commelin (Jun 22 2020 at 05:45):

not helpful for your sorry, I guess, but starting definitions with

λ n, i,

is unfortunately not a good idea, because a pair p is not defeq to ⟨p.1,p.2⟩. (Of course they are provably equal.)
Hence it's better to write

λ p, blabla p.1 foobar p.2

view this post on Zulip Yakov Pechersky (Jun 22 2020 at 14:36):

Your suggested syntax throws an error:

import data.matrix.notation

universe u
variables {α : Type u}

open_locale matrix

variables {ι : Type} [fintype ι]

def vec_empty : (fin 0 × ι)  α :=
-- λ ⟨n, i⟩, fin_zero_elim n
λ p, fin_zero_elim p.1
--type mismatch, term
--  λ (p : fin 0 × ι), fin_zero_elim p.fst
--has type
--  Π (p : fin 0 × ι), ?m_1[p] p.fst : Sort (imax 1 ?)
--but is expected to have type
--  fin 0 × ι → α : Type u

Is there some pi.instance I should be employing?

view this post on Zulip Johan Commelin (Jun 22 2020 at 14:38):

Does it help to write @fin_zero_elim explicitly?

view this post on Zulip Yakov Pechersky (Jun 22 2020 at 14:39):

type mismatch at application
  fin_zero_elim
term
  p.fst
has type
  fin 0 : Type
but is expected to have type
  fin 0  Sort ? : Type ?

view this post on Zulip Yakov Pechersky (Jun 22 2020 at 14:39):

That's using @fin_zero_elim

view this post on Zulip Reid Barton (Jun 22 2020 at 14:42):

You will have to write some other stuff too.

view this post on Zulip Yakov Pechersky (Jun 22 2020 at 14:42):

Right, sorry

view this post on Zulip Reid Barton (Jun 22 2020 at 14:50):

I think eta expanding is likely better.

view this post on Zulip Reid Barton (Jun 22 2020 at 14:50):

Something like λ p x, fin_zero_elim p.1 x

view this post on Zulip Yakov Pechersky (Jun 22 2020 at 14:55):

I don't understand what would be the term of fin 0 -> Sort u that would be required for the implicit argument of fin_zero_elim. I have the following working using composition, but earlier posts in the channel suggested staying away from composition.

import data.matrix.notation

universe u
variables {α : Type u}

open_locale matrix

variables {ι : Type} [fintype ι]

def vec_empty : fin 0 -> α :=
fin_zero_elim

def vec_empty' : (fin 0 × ι)  α :=
λ p, fin_zero_elim (prod.fst p)

def vec_empty'' : (fin 0 × ι)  α :=
fin_zero_elim  prod.fst
--type mismatch, term
--  λ (p : fin 0 × ι), fin_zero_elim p.fst
--has type
--  Π (p : fin 0 × ι), ?m_1[p] p.fst : Sort (imax 1 ?)
--but is expected to have type
--  fin 0 × ι → α : Type u

#print vec_empty
#check @vec_empty''

view this post on Zulip Reid Barton (Jun 22 2020 at 15:02):

It's the motive for the elimination, namely \lam _, α.

view this post on Zulip Yakov Pechersky (Jun 22 2020 at 15:05):

Thanks for the insight. I didn't think that I could just supply the type \a as the term, but that makes total sense, since it's asking for a term of type Sort. Still getting in the mindset of dependent type theory.

view this post on Zulip Yakov Pechersky (Jun 23 2020 at 00:04):

Thanks for the guidance on removing the inductive pair elimination in the defn. Now the proof is easy:

import data.matrix.notation

universe u
variables {α : Type u}

open_locale matrix

variables {ι : Type} [fintype ι]

def vec_empty : (fin 0 × ι)  α :=
λ p, @fin_zero_elim (λ _, α) p.1

def vec_cons {n : } (h : ι  α) (t : (fin n × ι)  α) : (fin n.succ × ι)  α :=
λ p, (nat.cases_on p.1.1
  (λ _, h p.2) (λ k hk, t (k, nat.lt_of_succ_lt_succ hk, p.2))) p.1.2

variables {m : }

@[simp] lemma cons_val_zero (x : ι  α) (u : (fin m × ι)  α) : (λ i, vec_cons x u 0, i) = x := rfl

Last updated: May 15 2021 at 00:39 UTC