## Stream: new members

### Topic: opaque "synthesize placeholder" error

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


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

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

#### Johan Commelin (May 21 2020 at 04:29):

Shouldn't alpha be explicit in the structure def

#### Johan Commelin (May 21 2020 at 04:30):

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

#### Johan Commelin (May 21 2020 at 04:30):

So you want C : chain_decomposition \alpha

#### Jalex Stark (May 21 2020 at 04:30):

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

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


#### Jalex Stark (May 21 2020 at 04:32):

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

#### Yury G. Kudryashov (May 21 2020 at 04:34):

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

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

#### Jalex Stark (May 21 2020 at 04:36):

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

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

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

#### Yury G. Kudryashov (May 21 2020 at 04:37):

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

#### Jalex Stark (May 21 2020 at 04:37):

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

#### Jalex Stark (May 21 2020 at 04:38):

/me goes off to read tpil section 2.6

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

Try Section 6.2

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

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

#### Jalex Stark (May 21 2020 at 04:46):

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

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

#### Kenny Lau (May 21 2020 at 07:13):

I rarely read any book cover to cover

#### Yury G. Kudryashov (May 21 2020 at 07:13):

@Kenny Lau Including fiction?

yeah

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

#### Bhavik Mehta (May 21 2020 at 22:16):

Out of interest what are you trying to prove here?

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