Zulip Chat Archive

Stream: general

Topic: Type


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 02 2018 at 18:36):

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

view this post on Zulip Reid Barton (Jul 02 2018 at 18:37):

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

view this post on Zulip Kenny Lau (Jul 02 2018 at 18:38):

oh lol alpha is explicit

view this post on Zulip Simon Hudon (Jul 02 2018 at 18:38):

Good catch

view this post on Zulip 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

view this post on Zulip 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 )

view this post on Zulip Kevin Buzzard (Jul 02 2018 at 18:50):

If you use { } then beta is implicit

view this post on Zulip Kevin Buzzard (Jul 02 2018 at 18:51):

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

view this post on Zulip Kevin Buzzard (Jul 02 2018 at 18:51):

so then you have to give it.

view this post on Zulip Kevin Buzzard (Jul 02 2018 at 18:52):

#check f α x -- α → Prop

view this post on Zulip 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

view this post on Zulip Hoang Le Truong (Jul 02 2018 at 18:58):

Thank you I fix it.

view this post on Zulip 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

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

view this post on Zulip 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 (:).

view this post on Zulip Sean Leather (Jul 03 2018 at 11:49):

Note how decidable_eq reduces:

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

view this post on Zulip 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

view this post on Zulip Sean Leather (Jul 03 2018 at 11:55):

Yes, that also works.

view this post on Zulip 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.

view this post on Zulip Hoang Le Truong (Jul 03 2018 at 11:57):

How to repair it

view this post on Zulip 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.

view this post on Zulip Sean Leather (Jul 03 2018 at 11:58):

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

view this post on Zulip 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.

view this post on Zulip 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

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?

view this post on Zulip 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  α

view this post on Zulip Hoang Le Truong (Jul 03 2018 at 12:09):

Yes I used it

view this post on Zulip Hoang Le Truong (Jul 03 2018 at 12:10):

import data.list
open list

view this post on Zulip Sean Leather (Jul 03 2018 at 12:10):

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

view this post on Zulip 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.

view this post on Zulip Sean Leather (Jul 03 2018 at 12:13):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 03 2018 at 12:16):

should the empty list satisfy the definition?

view this post on Zulip Hoang Le Truong (Jul 03 2018 at 12:17):

the empty list is not satisfy definition

view this post on Zulip 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

view this post on Zulip 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 α

view this post on Zulip 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

view this post on Zulip Hoang Le Truong (Jul 03 2018 at 12:32):

Thank you for that, I understood

view this post on Zulip 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].

view this post on Zulip Sean Leather (Jul 03 2018 at 12:33):

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

view this post on Zulip 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)

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

view this post on Zulip 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)

view this post on Zulip Hoang Le Truong (Jul 05 2018 at 09:45):

Thank @Chris Hughes for that. :thumbs_up:

view this post on Zulip 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')

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Hoang Le Truong (Jul 05 2018 at 19:25):

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

view this post on Zulip Simon Hudon (Jul 05 2018 at 19:26):

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

view this post on Zulip Hoang Le Truong (Jul 05 2018 at 19:29):

I use only import data.fintype

view this post on Zulip Simon Hudon (Jul 05 2018 at 19:30):

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

view this post on Zulip Simon Hudon (Jul 05 2018 at 19:30):

You can remove one at a time until it breaks

view this post on Zulip 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