# Zulip Chat Archive

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

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

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