Elimination of product of fintypes in proof

Stream: new members

[Yakov Pechersky]

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]

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]

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]

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]

Does it help to write @fin_zero_elim explicitly?

[Yakov Pechersky]

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]

That's using @fin_zero_elim

[Reid Barton]

You will have to write some other stuff too.

[Yakov Pechersky]

Right, sorry

[Reid Barton]

I think eta expanding is likely better.

[Reid Barton]

Something like λ p x, fin_zero_elim p.1 x

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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]

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