Zulip Chat Archive

Stream: new members

Topic: opaque "synthesize placeholder" error


view this post on Zulip Jalex Stark (May 21 2020 at 04:25):

Below I make a definition chain_decomposition. Lean doesn't complain when i declare it, and also doesn't complain when I #checkit, but does complain when I try to use it in any sense.

import tactic
import data.finset
import data.setoid


universe u
open finset

variables {α : Type u}[partial_order α] [fintype α]

def is_chain (x : set α) : Prop :=  a b  x, a  b  b  a

structure chain_decomposition :=
(val : setoid α )
(chains : set (set α))
(chains_spec : chains = setoid.classes val)
(chain_spec :  x  chains, is_chain x)

example (C : chain_decomposition) : Prop

view this post on Zulip Jalex Stark (May 21 2020 at 04:26):

specifically I get

don't know how to synthesize placeholder
context:
 Type ?

at the end of my mwe

view this post on Zulip Jalex Stark (May 21 2020 at 04:27):

I think this is either universe polymorphism stuff or variables stuff, but maybe I'm making a much more basic error

view this post on Zulip Johan Commelin (May 21 2020 at 04:29):

Shouldn't alpha be explicit in the structure def

view this post on Zulip Johan Commelin (May 21 2020 at 04:30):

In your example, C is a chain decomposition, but of what?

view this post on Zulip Johan Commelin (May 21 2020 at 04:30):

So you want C : chain_decomposition \alpha

view this post on Zulip Jalex Stark (May 21 2020 at 04:30):

Does that mean I don't get to exploit variables to make my other definitions shorter?

view this post on Zulip Jalex Stark (May 21 2020 at 04:31):

This works, following Johan's suggestion:

import tactic
import data.finset
import data.setoid
universe u
open finset

def is_chain {α : Type u}[partial_order α] [fintype α] (x : set α) : Prop :=  a b  x, a  b  b  a

def is_antichain {α : Type u}[partial_order α] [fintype α] (x : set α) : Prop :=  a b  x, ¬ (a  b  b  a)

structure chain_decomposition (α : Type u) :=
(val : setoid α )
(chains : set (set α))
(chains_spec : chains = setoid.classes val)
(chain_spec :  x  chains, is_chain x)

example {α : Type u} (C : chain_decomposition α) : Prop

view this post on Zulip Jalex Stark (May 21 2020 at 04:32):

hmm okay, i think it's clear to me that I was asking for magic

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 04:34):

variables just declare types, they don't magically add arguments to all definitions&lemmas.

view this post on Zulip Jalex Stark (May 21 2020 at 04:35):

The magic i want is to say at the beginning of my file "whenever I say α, I mean a term of Type u with instance of partial_order and fintype"

view this post on Zulip Jalex Stark (May 21 2020 at 04:36):

but really i should tell every function what typeclass instances it needs

view this post on Zulip Jalex Stark (May 21 2020 at 04:36):

and if I have a huge list of typeclasses I should make a typeclass that includes all of them

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 04:36):

You can declare variables {α : Type u} [partial_order α] [fintype α], then declare chain_decomposition (α : Type u) (this will be another α, so add typeclasses if needed), then use α again.

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 04:37):

Or you can use variable (α) before chain_decomposition and variable {α} after it.

view this post on Zulip Jalex Stark (May 21 2020 at 04:37):

So variable (α) does add an argument to every definition?

view this post on Zulip Jalex Stark (May 21 2020 at 04:38):

/me goes off to read tpil section 2.6

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 04:41):

Yes and no.

  1. If a definition/theorem uses α, then variable (α) [partial_order α] will automatically add (α) [partial_order α] to arguments.
  2. This doesn't work if a definition/theorem uses α only inside a tactic block (by, begin...end).

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 04:43):

Try Section 6.2

view this post on Zulip Jalex Stark (May 21 2020 at 04:44):

I think i am a fan of this switching between variable (α) and variable {α} business, it feels pretty close to the magic I wanted

view this post on Zulip Jalex Stark (May 21 2020 at 04:46):

maybe I am now at a point where if i read tpil cover to cover I will remember most of it

view this post on Zulip Jalex Stark (May 21 2020 at 04:46):

section 6.2 says the things I want, thanks for the pointer :)

view this post on Zulip Kevin Buzzard (May 21 2020 at 07:13):

I read tpil cover to cover three times and got more out of it each time (typeclasses only made sense to me the third time)

view this post on Zulip Kenny Lau (May 21 2020 at 07:13):

I rarely read any book cover to cover

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 07:13):

@Kenny Lau Including fiction?

view this post on Zulip Kenny Lau (May 21 2020 at 07:14):

yeah

view this post on Zulip Jalex Stark (May 21 2020 at 07:43):

I think the only math texts i have read cover-to-cover are abridged lecture notes for a course or papers written by me

view this post on Zulip Bhavik Mehta (May 21 2020 at 22:16):

Out of interest what are you trying to prove here?

view this post on Zulip Jalex Stark (May 21 2020 at 22:17):

dilworth's theorem on maximal antichains and minimal chain decompositions


Last updated: May 10 2021 at 00:31 UTC