Inferring has_zero given nonzero fin n

Stream: new members

[Yakov Pechersky]

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]

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

[Jalex Stark]

import tactic

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

[Jalex Stark]

an instance of has_zero is just a zero

[Jalex Stark]

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

[Jalex Stark]

suggest can tell you the first line of the proof

[Jalex Stark]

so can {! !}

[Reid Barton]

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]

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

[Reid Barton]

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

[Yakov Pechersky]

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]

That's true about the z : fin n

[Yakov Pechersky]

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]

Which would require a nonempty (fin n)

[Reid Barton]

Just do the same thing but without saying has_zero.

[Yakov Pechersky]

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

[Reid Barton]

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

[Yakov Pechersky]

Oh.

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

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