an example

Stream: new members

[Alex Zhang]

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]

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

[Mario Carneiro]

try apply inj_f

[Alex Zhang]

Thanks! I have solved it.

[Alex Zhang]

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]

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]

tactic#generalize_proofs

[Alex Zhang]

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]

⊢ has_zero (fin ↑n)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Eric Wieser]

We normally use fin n.succ instead

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Alex Zhang]

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]

fin.elim

[Anne Baanen]

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

[Alex Zhang]

Any solution to the mismatch errors? :sweat:

[Anne Baanen]

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

[Anne Baanen]

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]

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]

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]

Instead of / you might want docs#fin_prod_fin_equiv

[Eric Wieser]

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

[Alex Zhang]

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

[Eric Wieser]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

Right! I misread the defn for has_scalar

[Eric Wieser]

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