Zulip Chat Archive

Stream: new members

Topic: Inferring has_zero given nonzero fin n


view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 00:09):

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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jun 18 2020 at 00:13):

an instance of has_zero is just a zero

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jun 18 2020 at 00:14):

suggest can tell you the first line of the proof

view this post on Zulip Jalex Stark (Jun 18 2020 at 00:14):

so can {! !}

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 00:19):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 00:20):

That's true about the z : fin n

view this post on Zulip 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).

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 00:29):

Which would require a nonempty (fin n)

view this post on Zulip Reid Barton (Jun 18 2020 at 00:29):

Just do the same thing but without saying has_zero.

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 00:29):

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

view this post on Zulip Reid Barton (Jun 18 2020 at 00:29):

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

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 00:30):

Oh.

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 00:31):

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

view this post on Zulip 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

view this post on Zulip 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