opaque "synthesize placeholder" error

Stream: new members

[Jalex Stark]

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]

specifically I get

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

at the end of my mwe

[Jalex Stark]

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

[Johan Commelin]

Shouldn't alpha be explicit in the structure def

[Johan Commelin]

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

[Johan Commelin]

So you want C : chain_decomposition \alpha

[Jalex Stark]

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

[Jalex Stark]

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]

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

[Yury G. Kudryashov]

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

[Jalex Stark]

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]

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

[Jalex Stark]

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

[Yury G. Kudryashov]

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]

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

[Jalex Stark]

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

[Jalex Stark]

/me goes off to read tpil section 2.6

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

Try Section 6.2

[Jalex Stark]

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]

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

[Jalex Stark]

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

[Kevin Buzzard]

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]

I rarely read any book cover to cover

[Yury G. Kudryashov]

@Kenny Lau Including fiction?

[Kenny Lau]

yeah

[Jalex Stark]

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]

Out of interest what are you trying to prove here?

[Jalex Stark]

dilworth's theorem on maximal antichains and minimal chain decompositions