## Stream: new members

### Topic: an example

#### Alex Zhang (Jun 03 2021 at 04:06):

I am tring to prove the first direction in the following example

import data.set.function tactic
open set function
variables {α β : Type*} [inhabited α]
noncomputable theory
open_locale classical

def inverse (f : α → β) : β → α :=
λ y : β, if h : ∃ x, f x = y then classical.some h else default α

theorem inverse_spec {f : α → β} (y : β) (h : ∃ x, f x = y) :
f (inverse f y) = y :=
begin
rw inverse, dsimp, rw dif_pos h,
exact classical.some_spec h
end

variable  f : α → β

example : injective f ↔ left_inverse (inverse f) f  :=
begin
split,
{
intros inj_f x,
simp [inverse],
},
{
sorry
},
end


I currently have the goal classical.some _ = x. How can I give the underscore a name/identifier or do I need to prove this direction in another way without using simp at all?

#### Mario Carneiro (Jun 03 2021 at 04:10):

don't simp [inverse], never unfold inverse and instead use inverse_spec

#### Mario Carneiro (Jun 03 2021 at 04:12):

try apply inj_f

#### Alex Zhang (Jun 03 2021 at 04:17):

Thanks! I have solved it.

#### Alex Zhang (Jun 03 2021 at 04:19):

By the way, I am still curious about that once I have the goal classical.some _ = x, is it possible to give the underscore an identifier then or by modifying anything before?

#### Alex J. Best (Jun 03 2021 at 04:25):

The underscore is a proof, which is hidden by lean by default, you can turn on printing of these with set_option pp.proofs true to see what it is.

#### Eric Wieser (Jun 03 2021 at 07:35):

tactic#generalize_proofs

#### Alex Zhang (Jun 09 2021 at 14:34):

import data.matrix.basic
import algebra.field
import tactic.suggest

universes v w
variables {α : Type v} {β : Type w}
variables m n: ℕ+
variables {F : Type*} [field F]

def silly (M : matrix (fin m) (fin n) α) : matrix (fin (2*m)) (fin (2*n)) α
| x y := M 0 0


Why does this definition fail?
error: failed to synthesize type class instance

#### Kevin Buzzard (Jun 09 2021 at 14:35):

⊢ has_zero (fin ↑n)

#### Kevin Buzzard (Jun 09 2021 at 14:36):

This means that the type class system cannot figure out a proof that this type has a zero

#### Kevin Buzzard (Jun 09 2021 at 14:36):

instance foo (n : ℕ) : has_zero (fin (n+1)) := infer_instance -- works
instance bar (n : ℕ+) : has_zero (fin n) := infer_instance -- fails


#### Eric Wieser (Jun 09 2021 at 14:37):

Which is probably because I don't think fin (n : ℕ+) is used by mathlib anywhere

#### Eric Wieser (Jun 09 2021 at 14:37):

We normally use fin n.succ instead

#### Kevin Buzzard (Jun 09 2021 at 14:37):

You could add this instance manually, or if you want to keep things simple you could have n : nat and use n+1 everywhere

#### Kevin Buzzard (Jun 09 2021 at 14:38):

instance pnat.fin_has_zero (n : ℕ+) : has_zero (fin n) := ⟨⟨0, pnat.pos n⟩⟩

def silly (M : matrix (fin m) (fin n) α) : matrix (fin (2*m)) (fin (2*n)) α
| x y := M 0 0 -- works


#### Alex Zhang (Jun 09 2021 at 14:40):

Cool! I am trying to understand the syntax of the first line. If I get any further question, I will post here.

#### Kevin Buzzard (Jun 09 2021 at 14:41):

def add : ℕ → ℕ → ℕ
| x 0 := x
| x (n+1) := (add x n) + 1


#### Alex Zhang (Jun 10 2021 at 03:12):

import data.matrix.basic
import algebra.field
import tactic.suggest

universes v w
variables {α : Type v} {β : Type w}
variables {m n: ℕ+}
variables {a b: ℕ}
variables {F : Type*} [field F]

instance pnat.fin_has_zero (n : ℕ+) : has_zero (fin n) := ⟨⟨0, pnat.pos n⟩⟩

def silly (M : matrix (fin m) (fin n) α) : matrix (fin (2*m)) (fin (2*n)) α
| x y := M (m - 1) (y / 2)

def silly' (M : matrix (fin a.succ) (fin b.succ) α) : matrix (fin (2*a.succ)) (fin (2*b.succ)) α
| x y := M (a.succ - 1) (y / 2)


How can I fix the errors in the first definition besides changing the use of N+ to N?

#### Mario Carneiro (Jun 10 2021 at 03:52):

fin.elim

#### Anne Baanen (Jun 10 2021 at 07:56):

You can also import data.matrix.notation and write ![], if you want something more readable :)

#### Alex Zhang (Jun 10 2021 at 09:02):

Any solution to the mismatch errors? :sweat:

#### Anne Baanen (Jun 10 2021 at 09:10):

Sorry for missing the question! The missing ingredient is a way to write 1 as an element of fin (n : pnat).

#### Anne Baanen (Jun 10 2021 at 09:12):

The reason silly' works is that Lean inserts the coercion docs#nat.cast_coe, which maps 0 + 1 + 1 + ... + 1 : ℕ to any type with 0, 1 and +.

#### Anne Baanen (Jun 10 2021 at 09:14):

Something like this should make silly work as well:

instance pnat.fin_has_one : Π n : ℕ+, has_one  (fin n)
| ⟨0, h⟩ := absurd h (lt_irrefl 0)
| ⟨nat.succ n', h⟩ := (infer_instance : has_one (fin n'.succ))


#### Alex Zhang (Jun 27 2021 at 09:31):

def silly''
(p q m n: ℕ) (A : matrix (fin m) (fin n) α)
: matrix (fin (m * p)) (fin (n * q)) α :=
λ i j,
A (i / p) (j / q)


How can I fix the error here?

type mismatch at application
has_div.div j
term
j
has type
fin (n * q)
but is expected to have type
fin n


#### Eric Wieser (Jun 27 2021 at 09:51):

Instead of / you might want docs#fin_prod_fin_equiv

#### Eric Wieser (Jun 27 2021 at 09:52):

(fin_prod_fin_equiv.symm j).fst looks like what you want

#### Alex Zhang (Jun 27 2021 at 10:03):

I don't quite understand however :( Could you show the corrected code?

#### Eric Wieser (Jun 27 2021 at 10:13):

def silly'' {p q m n : ℕ} (A : matrix (fin m) (fin n) α) : matrix (fin (m * p)) (fin (n * q)) α :=
λ i j, A ((fin_prod_fin_equiv.symm i).fst) ((fin_prod_fin_equiv.symm j).fst)


#### Eric Wieser (Jun 27 2021 at 10:14):

The problem is that you can't divide a fin (m * p) by a nat: all lean knows how to do is promote the fin (m * p) to a nat, then divide that nat by a nat. But that doesn't work here, because lean wants you to provide a fin m

#### Eric Wieser (Jun 27 2021 at 10:17):

You can fix this with

def silly'' {p q m n : ℕ} (A : matrix (fin m) (fin n) α) : matrix (fin (m * p)) (fin (n * q)) α :=
λ i j, A ⟨i / p, sorry⟩ ⟨j / q, sorry⟩


My observation is that rather than filling out the sorry by hand, you can use fin_prod_fin_equiv which already give you the proof

#### Kevin Buzzard (Jun 27 2021 at 11:39):

A term of type fin n is not a natural number, it is a pair consisting of a natural number and a proof it's less than n. You can't divide a pair by a natural (or at least you can't until you explain to lean exactly what you mean by this).

#### Alex Zhang (Jun 28 2021 at 10:43):

instance mine [ring α] : has_scalar α α := sorry
How can I close the goal by using the mul as smul?

#### Kevin Buzzard (Jun 28 2021 at 10:51):

example mine [ring α] : has_scalar α α :=
infer_instance


works for me, which means that Lean is already assuming that rings have smuls and they're (no doubt) equal to muls

#### Kevin Buzzard (Jun 28 2021 at 10:52):

If the instance can already be found (in term mode by infer_instance and in tactic mode by apply_instance) then you don't need to start putting other instances in yourself (indeed, this is in general a bad idea)

#### Alex Zhang (Jun 28 2021 at 14:17):

Right, Kevin. This has already been defined. I got an error if using
instance silly [ring α] : has_scalar α α := ring.mul . I am not sure how to fix it if not using infer_instance.

#### Alex Zhang (Jun 28 2021 at 14:35):

Is it possible to know what infer_instance is using or to find the already defined instance?
I am not sure why ring.mul won't work.

#### Damiano Testa (Jun 28 2021 at 14:40):

If you use by apply_instance instead, then you can add by show_term{apply_instance} and you should see the proof that Lean finds.

#### Alex J. Best (Jun 28 2021 at 15:08):

docs#has_scalar is a structure (with only one field), so you can provide ring.mul as that field but you have to use the right syntax:

import algebra.ring.basic
import group_theory.group_action.defs

example {α : Type*} [ring α] : has_scalar α α := ⟨ring.mul⟩


#### Alex Zhang (Jun 28 2021 at 15:11):

Right! I misread the defn for has_scalar

#### Eric Wieser (Jun 28 2021 at 18:47):

In this case it's finding docs#has_mul.to_has_scalar

Last updated: Dec 20 2023 at 11:08 UTC