Newbie error

Stream: general

[Johan Commelin]

I've got the following code

import algebra.ring data.finsupp

variables {R : Type*} [ring R]

section free_module
definition free_module (S : Type*) := finsupp S R
variables {S : Type*}

instance : module R (free_module S) := sorry

end free_module

[Johan Commelin]

And this is the error

don't know how to synthesize placeholder
context:
R : Type u_1,
_inst_1 : ring R,
S : Type u_2
⊢ Type ?

[Johan Commelin]

Aah, I should point out that the red squiggles are under free_module in the line with sorry

[Mario Carneiro]

Shouldn't R be explicit in free_module? It is not inferrable

[Johan Commelin]

I think the error means that it can't figure out in which universe free_module S lives

[Johan Commelin]

Aah, Ok, is that the problem. I thought it was automatically included, since I declared it a variable

[Johan Commelin]

Or should I then use () instead of {}

[Kenny Lau]

it isn't a parameter

[Mario Carneiro]

it is included, but the later use might refer to a different R

[Johan Commelin]

Ok... well, that fixed my problem. Thanks a lot!

[Kenny Lau]

no, don't use parameter

[Kenny Lau]

you won't be able to use it once you leave the section

[Johan Commelin]

Hmm, what do you mean?

[Johan Commelin]

I now have

import algebra.ring data.finsupp

variables {R : Type*} [ring R]

section free_module
definition free_module (R : Type*) [ring R] (S : Type*) := finsupp S R
variables {S : Type*}

instance : module R (free_module R S) :=
begin
split, -- tactic fails
end

end free_module

[Johan Commelin]

Is that wrong?

[Kenny Lau]

never mind

[Kenny Lau]

that isn't wrong

[Johan Commelin]

Ok, I don't mind learning a better way (-;

[Johan Commelin]

So, why is split failing? I expected to get 4 goals, according to the 4 axioms of a module

[Kenny Lau]

constructor

[Kenny Lau]

but you don't want to use it since it extends something

[Kenny Lau]

maybe if you really want to stay in tactic mode, do refine {..}

[Johan Commelin]

Well, I don't want to stay in tactic mode. It is just that I have no clue how to do things in term mode. And tactic mode helps me a bit (-;

[Johan Commelin]

So what would be the proper way to prove this instance?

[Kenny Lau]

instance : module R (free_module R S) :=
{ smul := _,
  smul_add := _ }

etc

[Johan Commelin]

Ok, thanks! I'll try to do that.

[Johan Commelin]

Lol, this is already in finsupp: to_module

[Kenny Lau]

lol

[Johan Commelin]

The errors continue:

import algebra.ring data.finsupp

variables {R : Type*} [decidable_eq R] [ring R]

section free_module
definition free_module (R : Type*) [ring R] (S : Type*) := finsupp S R
variables {S : Type*} [decidable_eq S]

instance : add_comm_monoid (free_module R S) := finsupp.add_comm_monoid
instance : module R (free_module R S) := finsupp.to_module
end free_module

section generators
variables {M : Type*} [module R M]

definition natural_map (S : set M) : free_module R S → M :=
λ x, x.sum (λ s r, r • s)

definition generated_submodule (S : set M) := set.range (natural_map S) -- fails

definition is_finitely_generated (M : Type*) [module R M] : Prop :=
∃ S : finset M, generated_submodule {x | x ∈ S} = set.univ M -- fails

end generators

[Johan Commelin]

Errors:

generators.lean:19:57: error

failed to synthesize type class instance for
M : Type u_2,
S : set M
⊢ module ?m_1 M
generators.lean:19:57: error

don't know how to synthesize placeholder
context:
M : Type u_2,
S : set M
⊢ Type ?

[Johan Commelin]

But I am telling it that M is a module over R, so why can't it unify ?m_1 with R?

[Kevin Buzzard]

You started a new section so Lean has forgotten about the variable R

[Kevin Buzzard]

wait

[Kevin Buzzard]

that doesn't seem to be true

[Kevin Buzzard]

It seems to be because you don't ever mention R so the type class inference doesn't kick in

[Kevin Buzzard]

definition generated_submodule (S : set M) [module R M] := set.range (natural_map S) -- works

[Kevin Buzzard]

Type class inference is a strange thing

[Kenny Lau]

include R

[Kevin Buzzard]

I would still not say I had completely got the hang of it

[Kevin Buzzard]

include R
definition generated_submodule (S : set M) := set.range (natural_map S) -- works

[Kevin Buzzard]

Kenny's fix

[Kevin Buzzard]

What does include do?

[Kevin Buzzard]

I thought this was for including variable names in tactic proofs

[Kevin Buzzard]

As for the equality failing

[Kevin Buzzard]

set.univ : Π {α : Type u}, set α

[Kevin Buzzard]

set.univ doesn't take M, it guesses it.

[Kevin Buzzard]

definition is_finitely_generated (M : Type*) [module R M] : Prop :=
∃ S : finset M, generated_submodule {x | x ∈ S} = set.univ -- works

[Kevin Buzzard]

Recently I realised that I pretty fully understood most Lean errors

[Kevin Buzzard]

i.e. I can look at the error and actually figure out what is wrong with my code, in many cases

[Kevin Buzzard]

type mismatch at application
  generated_submodule {x : M | x ∈ S} = set.univ M
term
  set.univ M
has type
  Prop : Type
but is expected to have type
  set M : Type ?

[Kevin Buzzard]

says "the right hand side is supposed to have type set M but it has type Prop so you have not written what you meant to write -- it doesn't typecheck."

[Kevin Buzzard]

You are attempting to assert that two sets are equal

[Kevin Buzzard]

so the correct type is set M

[Kevin Buzzard]

so the problem is that set.univ M has type Prop instead of type set M

[Kevin Buzzard]

and now you look at what set.univ actually does by hovering your mouse over set.univ

[Kevin Buzzard]

and you see your error

[Kevin Buzzard]

I would urge you @Johan Commelin to learn to read errors so you can find out the problem.

[Kevin Buzzard]

Sometimes the problem is that type class inference has failed. Type class inference is just something you have to get the hang of and I had to ask and ask here about it -- see my typeclass inference woes thread

[Kevin Buzzard]

But for other errors, try and make it so that there is exactly one error (i.e put sorry everywhere else) and then try and read the error.

[Kevin Buzzard]

And then hope that you can fix it

[Johan Commelin]

Ok, thanks! I hope to get the hang of it as well...

[Chris Hughes]

set.univ : set M should help

[Chris Hughes]

Or perhaps @set.univ M