# Zulip Chat Archive

## 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):

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