Type

Stream: general

[Hoang Le Truong]

When I write

variable α : Type
variable x:α
def f: α → α → Prop:= λ x y, x=y

#check f (x:α )

I get messages: type mismatch at application f x term x has type α :Type but is expected to have Type Type: Type 1
What mean is it? please can you explain it.

[Simon Hudon]

Add set_option pp.universes true before your #check statement, that should be informative. Also, please encode your code snippets between ticks ( ` ) so that the font helps seeing what is code and what isn't

[Reid Barton]

f has two arguments, alpha and x. You gave x but not alpha

[Reid Barton]

So it thinks that (x : alpha) is the first argument to f, which is the Type

[Kenny Lau]

oh lol alpha is explicit

[Simon Hudon]

Good catch

[Kevin Buzzard]

variable α : Type
variable x:α
def f: α → α → Prop:= λ x y, x=y

#check f -- Π (α : Type), α → α → Prop

variable {β : Type}
variable y : β
def g : β → β → Prop := λ x y, x = y

#check g -- ?M_1 → ?M_1 → Prop

#check g (y : β) -- β → Prop

[Hoang Le Truong]

I add ( set_option pp.universes true) but it not run. I do not understand why we need it. In fact, I need ( f(x: alpha) to definition next object. example

( def g (e: α × α): ℕ := if f e.1 e.2 then 2 else 0 )

[Kevin Buzzard]

If you use { } then beta is implicit

[Kevin Buzzard]

You used nothing, which is the same as ( ), for alpha, so it's explicit

[Kevin Buzzard]

so then you have to give it.

[Kevin Buzzard]

#check f α x -- α → Prop

[Simon Hudon]

And my suspicion that universes were the root of the trouble did not pan out so you can discard my advice

[Hoang Le Truong]

Thank you I fix it.

[Hoang Le Truong]

I have the following code

variables {α : Type}

definition  f : α → list α→ ℕ
| a     []          := 0
| a     (b :: l)  :=   if a = b then  (f a l)+1  else f a l

and I received messages

failed to synthesize type class instance for α : Type, f : α → list α→ ℕ, a b: α, l: list α ⊢ decidable (a=b)

If I used type char then it run. Please can you explain it and how to use type α in such cases

[Sean Leather]

The if a = b then t else f is notation for ite (a = b) t f, where:

def ite (c : Prop) [h : decidable c] {α : Sort u} (t e : α) : α

So, Lean is looking for an instance decidable (a = b). You can tell Lean to wait for an instance to appear until you actually use f by putting [decidable_eq α] before the colon (:).

[Sean Leather]

Note how decidable_eq reduces:

#reduce decidable_eq -- λ (α : Sort u_1), Π (a b : α), decidable (a = b)

[Hoang Le Truong]

Thank you for that, Sean

variables {α : Type} [decidable_eq α]

definition  f : α → list α→ ℕ
| a     []        := 0
| a     (b :: l)  :=   if a = b then  (f a l)+1  else f a l

It is Ok

[Sean Leather]

Yes, that also works.

[Sean Leather]

If you put variables [decidable_eq α] while learning, it's fine. But note that if you write other definitions or theorems using α after that, they will all have [decidable_eq α] in their type signatures, whether you want it that way or not.

[Hoang Le Truong]

How to repair it

[Sean Leather]

That's one of those things that can trip you up when you're writing larger collections of Lean code.

[Sean Leather]

You can use section or namespace to make the variables local to a region.

[Sean Leather]

So, if you know you want to write a bunch of things that need decidable_eq, you can:

section
variables {α : Type} [decidable_eq α]
def f ...
theorem p ...
end -- variables {α : Type} [decidable_eq α] not valid after this.

[Hoang Le Truong]

Thank you for that. I used it. I have more question

variables {α : Type}

definition f (l:list α):Prop := head l = last l

and I received messages

type mismatch at application head l = last l term last l has type l  ≠ nil →  α but is expected have type α

How use type which have condition as function last?

[Sean Leather]

You should first check the types:

#check @list.head
#check @list.last

list.head : Π {α : Type u_1} [_inst_1 : inhabited α], list α → α
list.last : Π {α : Type u_1} (l : list α), l ≠ list.nil → α

[Hoang Le Truong]

Yes I used it

[Hoang Le Truong]

import data.list
open list

[Sean Leather]

So, in order to use last, you will need to prove l ≠ list.nil.

[Sean Leather]

I'm not sure what you want to do, but you could have that condition as a parameter to f.

[Sean Leather]

definition head_eq_last (l : list α) (h : l ≠ list.nil) : Prop := head l = last l h

[Hoang Le Truong]

In fact I want definition f such that head of l equal tail of l. In general, I want used type have condition

[Mario Carneiro]

should the empty list satisfy the definition?

[Hoang Le Truong]

the empty list is not satisfy definition

[Mario Carneiro]

Then you can write

definition head_eq_last (l : list α) : Prop := ∃ (h : l ≠ list.nil), head l = last l h

[Hoang Le Truong]

I try it but I received messages

failed to synthesize type class instance for α: Type, l: list α, h : l ≠ list.nil ⊢inhibited α

[Sean Leather]

That's a consequence of the type of head. Easy to fix:

def head_eq_last [inhabited α] (l : list α) : Prop := ∃ (h : l ≠ list.nil), head l = last l h

[Hoang Le Truong]

Thank you for that, I understood

[Sean Leather]

Any time you see this message pattern:

failed to synthesize type class instance for ... ⊢ C

Lean is looking for either an existing instance C or a parameter such as [C].

[Sean Leather]

So, when you used char, it used the existing instance decidable_eq char.

[Hoang Le Truong]

when I restrict type α to type fintype α , I have problem. My code is

variables {α : Type}

def preimage (f:α → ℕ ) (u:ℕ ):set α  := λ x, f x=u

def card_image (f:(fintype α) → ℕ) (u:ℕ ):ℕ
:= fintype.card (preimage g u)

and I received messages

failed to synthesize type class instance for α : Type, f : fintype α → ℕ, u : ℕ ⊢ fintype ↥(preimage f u)

I understand that Lean find fintype ↥(preimage f u). What mean is ↥? can we show that preimage f u have type fintype? How I fix it

[Chris Hughes]

This code should work. In the function card_image, the type of f should probably be α → ℕ. fintype α is more or less just the statement that α is finite. I also made decidable_eq an argument to the function as this is necessary to compute the fintype instance. You could also use the linelocal attribute [instance] classical.prop_decidable to achieve the same thing without decidable_eq.

import data.fintype

variables {α : Type}

def preimage (f : α → ℕ) (u : ℕ) : set α  := λ x, f x=u

instance [fintype α] [decidable_eq α] (f : α → ℕ) (u : ℕ) : fintype (preimage f u) :=
by unfold preimage; apply_instance

def card_image [fintype α] [decidable_eq α] (f : α → ℕ) (u : ℕ) : ℕ :=
fintype.card (preimage f u)

[Hoang Le Truong]

Thank @Chris Hughes for that. :thumbs_up:

[Hoang Le Truong]

What mean is messages

maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

[Simon Hudon]

That means that you need an instance for a certain type class. Lean is trying to find one for you but gives up. It might be because none exists or because the one that would work is, in a sense, unattainable by Lean. Do you know what type class you're trying to find an instance for?

[Hoang Le Truong]

my type class is fintype . I have code 50 line. when I break it to two file then it run. But I run one file. it give messages

[Simon Hudon]

Can you great a gist on github and show me where you break it into two files?

[Hoang Le Truong]

https://gist.github.com/truonghoangle/b9fa69e939bcb6c20fcf96affc0fd965
I break it after end direct_graph

[Simon Hudon]

Great! When you break it, what import do you give the new file?

[Hoang Le Truong]

I use only import data.fintype

[Simon Hudon]

try copying all the imports. You probably use instances from the other modules

[Simon Hudon]

You can remove one at a time until it breaks

[Hoang Le Truong]

Ok it is run. Thank you for that