Zulip Chat Archive

Stream: new members

Topic: Forced to use @


view this post on Zulip Pontus Sundqvist (Feb 28 2021 at 16:44):

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

view this post on Zulip Yakov Pechersky (Feb 28 2021 at 16:48):

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

view this post on Zulip Pontus Sundqvist (Feb 28 2021 at 16:49):

No... I probably should do that.

view this post on Zulip Yakov Pechersky (Feb 28 2021 at 16:51):

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

view this post on Zulip Yakov Pechersky (Feb 28 2021 at 16:51):

But what's the larger problem? #xy

view this post on Zulip Pontus Sundqvist (Feb 28 2021 at 17:15):

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.

view this post on Zulip Pontus Sundqvist (Feb 28 2021 at 17:16):

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

view this post on Zulip Eric Wieser (Feb 28 2021 at 17:26):

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

view this post on Zulip Eric Wieser (Feb 28 2021 at 17:27):

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


Last updated: May 13 2021 at 23:16 UTC