# Zulip Chat Archive

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

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

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