Lean typing questions

Stream: new members

[Ching-Tsun Chou]

Lean's typing behavior is driving me crazy. Consider the following code:

variable (α : Type*) [inst : Fintype α] [DecidableEq α]

def Perm := α ≃ Fin (Fintype.card α)

def hasSetPrefix (s : Finset α) (p : Perm α) : Prop := ∀ a ∈ s, p.toFun a ≤ s.card

variable (s : Finset α) (p : Perm α) in
#check (hasSetPrefix (α := α) s p)

theorem num_perms_set_prefix (s : Finset α) :
    Fintype.card { p : Perm α // hasSetPrefix (α := α) s p } = s.card.factorial * (Fintype.card α - s.card).factorial := by
  sorry

Question 1: Why is the (α := α) necessary in the #check? I found that if I drop it, Lean gets confused about the type of p.

Question 2: Lean "failed to synthesize Fintype { p // hasSetPrefix α s p }" on the subtype construction in the last theorem. Why? What is going on?

[Aaron Liu]

Question 1: Why is the (α := α) necessary in the #check? I found that if I drop it, Lean gets confused about the type of p.

Since you wrote (α : Type*) at the top, Lean is expecting hasSetPrefix α s p, so when you write hasSetPrefix s p, Lean tries to convert s to a type, and then gets confused when p is not a Finset.

[Ching-Tsun Chou]

That's a good point. The (α := α) can be replaced by α.

[Ching-Tsun Chou]

I used the explicit (α : Type*) because of the issues discussed in #new members > How to prove some simple combinatoric identities

[Ching-Tsun Chou]

So my question 1 is solved. Question 2 remains.

[Aaron Liu]

Question 2: Lean "failed to synthesize Fintype { p // hasSetPrefix α s p }" on the subtype construction in the last theorem. Why? What is going on?

Fintype means "I can list out all the elements of this type without duplication and without missing any (and I can prove my listing has these properties)". "Failed to synthesize" means Lean's typeclass system was not able to automatically find a way to have a Fintype for your type.
The problem is, when making a list of all the { p : Perm α // hasSetPrefix (α := α) s p }, Lean has no way of knowing if a certain Perm α should go in the list or not.
One way to fix this is by using open Classical to tell Lean to use the axiom of choice to figure out if a permuatation should be included.
Another way to solve this is by writing a docs#Decidable instance for your hasSetPrefix function, that gives an algorithm for deciding (I recommend this way).
Another way is to not use Fintype.card, but instead something like docs#Nat.card which doesn't need a Fintype instance but cannot be evaluated either.

[Aaron Liu]

Here's an example Decidable instance for hasSetPrefix.

instance : Decidable (hasSetPrefix α s p) := decidable_of_iff' _ (iff_of_eq <| hasSetPrefix.eq_def ..)

[Aaron Liu]

Alternatively, you can say abbrev hasSetPrefix instead of def hasSetPrefix and the typeclass system will unfold your definition and derive the decidability for the underlying forall statement.

[Ching-Tsun Chou]

Thanks for the explanations! How is abbrev different from def?

[Kevin Buzzard]

It's more reducible (more parts of the system will unfold it)

[Ching-Tsun Chou]

abbrev is not mentioned in any of the documents listed in the "Books" section here:

https://leanprover-community.github.io/learn.html

It is described in "Functional programming in Lean", but I thought I was just doing theorem proving.

[Aaron Liu]

The elaborator has a concept called transparency. Every definition has a transparency associated with it, and the definition will only be unfolded if it is transparent enough.
The four definition transparencies are:

@[reducible] def
@[instance] def
def and
@[irreducible] def

The four transparency modes are:

reducible : unfold reducible defs
instances : unfold reducible and instance defs
default : unfold everything except irreducible defs
all : unfold everything

abbrev is short for @[reducible] def, so typeclass inference will unfold it.
Metaprogramming in Lean has a section on transparency here.

[Ching-Tsun Chou]

Thanks for the explanation!