failing to instantiate, type mismatch

Stream: general

[Bruno Bandeira Monteiro]

Hi,
use is giving me a weird error in a particular situation. I'm trying to formalize a proof that a set of axioms is satisfiable. Satisfiability is an existential, so Im starting the proof with use \N. I believe this should type check with my definition of satisfiability:

def satisfiable (A : set Ax) := ∃ (N : Type*) (S : N → N) (z : N), ∀φ : Ax, φ ∈ A → φ N S z

the goal is satisfiable {Zer, Sur, Dni}. Am I misusing Type* or the existential quantifier?

existsi tells me the expected type is Type, but even though nat has type Type, it tells me there is a type mismatch.

[Kevin Buzzard]

Can you post a #mwe? If I cut and paste your code as it stands I get errors (different to the errors you're seeing)

[Kevin Buzzard]

i.e. can you post enough so that I can see the error you want me to see, and not random unrelated errors about not knowing what Ax is.

[Bruno Bandeira Monteiro]

ok,

import data.set.basic
import data.nat.basic
open nat

def Ax := Π (N : Type*), (N → N) → N → Prop
def satisfiable (A : set Ax) := ∃ (N : Type*) (S : N → N) (z : N), ∀φ : Ax, φ ∈ A → φ N S z
def Zer := λ (N : Type*) (S : N → N) (z : N), ∀ (x : N), S x ≠ z

lemma ex1 : satisfiable {Zer} :=
begin
  use ℕ,
end

edit : fixed the mwe

[Bruno Bandeira Monteiro]

ah sorry, 1 moment

[Bruno Bandeira Monteiro]

there

[Reid Barton]

use generally provides poor error messages. If you get an error from use, better try:

  refine ⟨ℕ, _⟩,

and now we get a better error message:

type mismatch at application
  Exists.intro ℕ
term
  ℕ
has type
  Type : Type 1
but is expected to have type
  Type u_1 : Type (u_1+1)
state:
⊢ satisfiable {Zer}

[Reid Barton]

I suggest not using Type* in situations like this, under an existential, unless you really know what you're doing (and probably even not then).

[Reid Barton]

In short the error is because Lean determines the type of a lemma before looking at its definition, and here it thinks the type should be universe-polymorphic because there is nothing to determine the universe variable in satisfiable. But then the proof beginning with ℕ only works for a specific universe.

[Reid Barton]

Bruno Bandeira Monteiro said:

existsi tells me the expected type is Type, but even though nat has type Type, it tells me there is a type mismatch.

Oh yes, and existsi is also known to give poor errors...

[Bruno Bandeira Monteiro]

Ok,
I'm not sure I understood what lean is doing there. But I changed Type* to Type and it worked. I guess using Type* would be unnecessarily general, and maybe I misunderstood what Type* actually is.

[Bruno Bandeira Monteiro]

Thanks for the help!

[Reid Barton]

def satisfiable (A : set Ax) := ∃ (N : Type*) ... doesn't mean
"A is satisfiable if there is a type N in some universe such that ..."

[Reid Barton]

instead, it means
def {u} satisfiable (A : set Ax) := ∃ (N : Type u) ... which is
"for each universe u, A is satisfiable with respect to universe u if there is a type N in universe u such that ..."

[Bruno Bandeira Monteiro]

Really? What does it mean then?

[Bruno Bandeira Monteiro]

ahh

[Bruno Bandeira Monteiro]

Ok, I think I see

[Reid Barton]

and then
lemma ex1 : satisfiable {Zer} := ...
was inferred as lemma {u} ex1 : satisfiable.{u} {Zer} := ..., i.e., {Zer} is satisfiable with respect to any universe u, so you had better come up with a type in an arbitrary universe u (which is possible to do, but probably not what you are interested in)

[Reid Barton]

In fact Type* is just another way to write Type _, meaning "Lean please figure out what univese goes here". The name Type* can be misleading.

[Bruno Bandeira Monteiro]

ah ok,
I thought it was the 'union' of Type n for all n \in \N

[Bruno Bandeira Monteiro]

Thanks a lot for the explanations.