## Stream: general

### Topic: Type

#### Hoang Le Truong (Jul 02 2018 at 18:31):

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 (Jul 02 2018 at 18:36):

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 (Jul 02 2018 at 18:36):

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

#### Reid Barton (Jul 02 2018 at 18:37):

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

#### Kenny Lau (Jul 02 2018 at 18:38):

oh lol alpha is explicit

Good catch

#### Kevin Buzzard (Jul 02 2018 at 18:50):

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 (Jul 02 2018 at 18:50):

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 (Jul 02 2018 at 18:50):

If you use { } then beta is implicit

#### Kevin Buzzard (Jul 02 2018 at 18:51):

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

#### Kevin Buzzard (Jul 02 2018 at 18:51):

so then you have to give it.

#### Kevin Buzzard (Jul 02 2018 at 18:52):

#check f α x -- α → Prop 

#### Simon Hudon (Jul 02 2018 at 18:52):

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

#### Hoang Le Truong (Jul 02 2018 at 18:58):

Thank you I fix it.

#### Hoang Le Truong (Jul 03 2018 at 11:43):

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


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 (Jul 03 2018 at 11:46):

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 (Jul 03 2018 at 11:49):

Note how decidable_eq reduces:

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


#### Hoang Le Truong (Jul 03 2018 at 11:54):

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 (Jul 03 2018 at 11:55):

Yes, that also works.

#### Sean Leather (Jul 03 2018 at 11:57):

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.

How to repair it

#### Sean Leather (Jul 03 2018 at 11:57):

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

#### Sean Leather (Jul 03 2018 at 11:58):

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

#### Sean Leather (Jul 03 2018 at 11:59):

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 (Jul 03 2018 at 12:06):

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

variables {α : Type}

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


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 (Jul 03 2018 at 12:08):

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 → α


Yes I used it

#### Hoang Le Truong (Jul 03 2018 at 12:10):

import data.list
open list


#### Sean Leather (Jul 03 2018 at 12:10):

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

#### Sean Leather (Jul 03 2018 at 12:11):

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

#### Sean Leather (Jul 03 2018 at 12:13):

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


#### Hoang Le Truong (Jul 03 2018 at 12:15):

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 (Jul 03 2018 at 12:16):

should the empty list satisfy the definition?

#### Hoang Le Truong (Jul 03 2018 at 12:17):

the empty list is not satisfy definition

#### Mario Carneiro (Jul 03 2018 at 12:17):

Then you can write

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


#### Hoang Le Truong (Jul 03 2018 at 12:23):

I try it but I received messages

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


#### Sean Leather (Jul 03 2018 at 12:30):

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 (Jul 03 2018 at 12:32):

Thank you for that, I understood

#### Sean Leather (Jul 03 2018 at 12:33):

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 (Jul 03 2018 at 12:33):

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

#### Hoang Le Truong (Jul 05 2018 at 09:19):

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)


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 (Jul 05 2018 at 09:37):

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 (Jul 05 2018 at 09:45):

Thank @Chris Hughes for that. :thumbs_up:

#### Hoang Le Truong (Jul 05 2018 at 18:40):

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 (Jul 05 2018 at 18:44):

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 (Jul 05 2018 at 18:53):

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 (Jul 05 2018 at 19:03):

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

#### Hoang Le Truong (Jul 05 2018 at 19:25):

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

#### Simon Hudon (Jul 05 2018 at 19:26):

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

#### Hoang Le Truong (Jul 05 2018 at 19:29):

I use only  import data.fintype `

#### Simon Hudon (Jul 05 2018 at 19:30):

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

#### Simon Hudon (Jul 05 2018 at 19:30):

You can remove one at a time until it breaks

#### Hoang Le Truong (Jul 05 2018 at 19:33):

Ok it is run. Thank you for that

Last updated: May 08 2021 at 18:17 UTC