## Stream: new members

### Topic: Elimination of product of fintypes in proof

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


#### 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.

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


#### 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?

#### Johan Commelin (Jun 22 2020 at 14:38):

Does it help to write @fin_zero_elim explicitly?

#### 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 ?


#### Yakov Pechersky (Jun 22 2020 at 14:39):

That's using @fin_zero_elim

#### Reid Barton (Jun 22 2020 at 14:42):

You will have to write some other stuff too.

Right, sorry

#### Reid Barton (Jun 22 2020 at 14:50):

I think eta expanding is likely better.

#### Reid Barton (Jun 22 2020 at 14:50):

Something like λ p x, fin_zero_elim p.1 x

#### 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''


#### Reid Barton (Jun 22 2020 at 15:02):

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

#### 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.

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