Forced to use @

Stream: new members

[Pontus Sundqvist]

I'm probably missing something really simple here, but is there a way to avoid using @ in this situation? Shouldn't Lean see that a can be used?

def property_1 (i : ℕ) : Prop := true
def property_2 (i : ℕ) [property_1 i] : Prop := true

-- This does not work
theorem test1 (i : ℕ)
(a : property_1 i)
(b : property_2 i)
: i = i := sorry

-- But this works... is there anyway to avoid having to use `@`?
theorem test2 (i : ℕ)
(a : property_1 i)
(b : @property_2 i a)
: i = i := sorry

[Yakov Pechersky]

Have you read #tpil about explicit, implicit, and typeclass arguments?

[Pontus Sundqvist]

No... I probably should do that.

[Yakov Pechersky]

Making the first def a class makes your test1 work.

class property_1 (i : ℕ) : Prop := true
def property_2 (i : ℕ) [property_1 i] : Prop := true

-- This now works
theorem test1 (i : ℕ)
(a : property_1 i)
(b : property_2 i)
: i = i := sorry

[Yakov Pechersky]

But what's the larger problem? #xy

[Pontus Sundqvist]

I encountered the problem several times, but an example was in the following code:

import data.fintype.basic
import data.matrix.basic

universes u

variables {a b p q : Type u}
[fintype a] [fintype b] [fintype p] [fintype q]
[linear_order a] [linear_order b] [linear_order p] [linear_order q]

def conserves_order
(f : a -> b)
: Prop := ∀ a1 a2, (a1 < a2) ↔ (f a1 < f a2)

def submatrix
(m : matrix a b ℕ)
(f : p -> a) (g : q -> b) [conserves_order f] [conserves_order g] [function.injective f] [function.injective g]
: matrix p q ℕ
:= λ i j, m (f i) (g j)

theorem submatrix_is_minor
(m : matrix a b ℕ)
(f : p -> a) (g : q -> b) [conserves_order f] [conserves_order g] [function.injective f] [function.injective g]
(i : p) (j : q)
: (submatrix m f g) i j = (m.minor f g) i j
-- Lean: failed to synthesize type class instance [at submatrix] for [function.injective/conserves_order f/g]
:= sorry

I feel like using the same restrictions on f (and g) in the definition and the theorem should make it obvious that they satisfy the requirements.

[Pontus Sundqvist]

I should read up on classes, I haven't used them yet.

[Eric Wieser]

If you're going to put things in square brackets, they need to be tagged with @[class]

[Eric Wieser]

I think what you probably want to do is replace (f : p -> a) [conserves_order f] [function.injective f] with (f : p ↪o a), docs#order_embedding