## Stream: new members

### Topic: Inferring has_zero given nonzero fin n

#### Yakov Pechersky (Jun 18 2020 at 00:09):

How can I convert a (n : \N) (h : 0 \neq n) to gain a has_zero (fin n)? fuller problem is here:

import data.real.basic
import data.matrix.basic
import linear_algebra.matrix

variables {n : ℕ} {R : Type*} [field R]

lemma inv_mat_nonzero (A : matrix (fin n) (fin n) R) (npos : 0 ≠ n)
(h : ∃ B, A * B = 1) : A ≠ 0 :=
begin
haveI : has_zero (fin n) := sorry,
intros H,
choose B hB using h,
rw [H, zero_mul] at hB,
replace hB := congr_fun (congr_fun hB 0) 0,
norm_num at hB,
exact hB
end


#### Yakov Pechersky (Jun 18 2020 at 00:09):

I guess I can try proving that A = 0 -> n = 0

#### Jalex Stark (Jun 18 2020 at 00:13):

import tactic

example {n : ℕ} (hn : n ≠ 0) : has_zero (fin n) :=
begin
refine {zero := _},
refine ⟨0, _⟩,
omega,
end


#### Jalex Stark (Jun 18 2020 at 00:13):

an instance of has_zero is just a zero

#### Jalex Stark (Jun 18 2020 at 00:13):

an element of fin n is a nat plus a proof that it's less than n

#### Jalex Stark (Jun 18 2020 at 00:14):

suggest can tell you the first line of the proof

#### Jalex Stark (Jun 18 2020 at 00:14):

so can {! !}

#### Reid Barton (Jun 18 2020 at 00:18):

Yakov Pechersky said:

  choose B hB using h,


I guess this works, but more normal is cases h with B hB or an rcases or obtain variant.

#### Yakov Pechersky (Jun 18 2020 at 00:19):

That's awesome. Never really got the hang of suggest

#### Reid Barton (Jun 18 2020 at 00:19):

Also, you don't really need has_zero specifically, do you? Just any z : fin n will do

#### Yakov Pechersky (Jun 18 2020 at 00:20):

With those insights:

import data.real.basic
import data.matrix.basic
import linear_algebra.matrix

variables {n : ℕ} {R : Type*} [field R]

lemma inv_mat_nonzero (A : matrix (fin n) (fin n) R) (npos : 0 < n)
(h : ∃ B, A * B = 1) : A ≠ 0 :=
begin
haveI : has_zero (fin n) := by {refine ⟨_⟩, refine ⟨0, _⟩, exact npos },
obtain ⟨B, hB⟩ := h,
intros H,
rw [H, zero_mul] at hB,
replace hB := congr_fun (congr_fun hB 0) 0,
norm_num at hB,
exact hB
end


#### Yakov Pechersky (Jun 18 2020 at 00:20):

That's true about the z : fin n

#### Yakov Pechersky (Jun 18 2020 at 00:25):

How does one just pluck an arbitrary fin n, would that be using arbitrary? Then I still have to show inhabited (fin n).

#### Yakov Pechersky (Jun 18 2020 at 00:29):

Which would require a nonempty (fin n)

#### Reid Barton (Jun 18 2020 at 00:29):

Just do the same thing but without saying has_zero.

#### Yakov Pechersky (Jun 18 2020 at 00:29):

  haveI : inhabited (fin n) := by {refine ⟨_⟩, refine ⟨0, _⟩, exact npos}


#### Reid Barton (Jun 18 2020 at 00:29):

have z : fin n := \<0, npos\>, etc.

Oh.

#### Yakov Pechersky (Jun 18 2020 at 00:31):

That's really cool. That's helping me understand better how fin n is defined.

#### Yakov Pechersky (Jun 18 2020 at 00:31):

import data.real.basic
import data.matrix.basic
import linear_algebra.matrix

variables {n : ℕ} {R : Type*} [field R]

lemma inv_mat_nonzero (A : matrix (fin n) (fin n) R) (npos : 0 < n)
(h : ∃ B, A * B = 1) : A ≠ 0 :=
begin
obtain ⟨B, hB⟩ := h,
intros H,
rw [H, zero_mul] at hB,
have z : fin n := ⟨0, npos⟩,
replace hB := congr_fun (congr_fun hB z) z,
norm_num at hB,
exact hB
end


#### Yakov Pechersky (Jun 18 2020 at 01:00):

Reid Barton said:

Yakov Pechersky said:

  choose B hB using h,


I guess this works, but more normal is cases h with B hB or an rcases or obtain variant.

How do rcases or obtain work with \ex !, the unique exists? The inverse is unique, so I might prefer to use that syntax. The error I get with rcases or obtain is

induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop


Last updated: May 14 2021 at 00:42 UTC