Zulip Chat Archive

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

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

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?

Kenny Lau (May 21 2020 at 07:14):

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: Dec 20 2023 at 11:08 UTC