failed to instantiate goal

Stream: new members

[Huỳnh Trần Khanh]

what does this error mean?

failed to instantiate goal with function.embedding.mk (fun (x : 4._.10), (dite ((frozen_name has_mem.mem) x a) (fun (h : (frozen_name has_mem.mem) x a), (b.to_fun (subtype.mk x h))) (fun (h : not ((frozen_name has_mem.mem) x a)), (dite (nonempty a) (fun (h : nonempty a), (a.max' h)) (fun (h : not (nonempty a)), x)))))

this is the proof that i got

lemma goal_injective : ∀ {S : finset ℕ} (f : ↥(↑S : set ℕ) ↪ ℕ), ∃ (h : ℕ ↪ ℕ), set.restrict h S = f := begin
  intros a b,
  rw [finset.set_of_mem.symm, set.set_coe_eq_subtype] at b,
  classical,
  use function.embedding.mk (λ x, if h : x ∈ a then b.to_fun (subtype.mk x h)
    else if h : nonempty a then a.max' h else x),
  sorry,
end

here is the room numbering scheme that i'm trying to implement: if the set of VIP people is empty then the room number is equal to the person number. otherwise, if the person is VIP then the room number is retrieved from the ↥(↑S : set ℕ) ↪ ℕ bundle. if the person is not VIP then the room number is equal to the max room number that is assigned to a VIP person, plus 1, plus that person's number.

[Kevin Buzzard]

If you break this up a bit and try

let g := function.embedding.mk (λ x, if h : x ∈ a then b.to_fun (subtype.mk x h)
    else if h : nonempty a then a.max' h else x),

then you can see your error, this term doesn't quite typecheck.

[Kevin Buzzard]

I don't know why the error use gives is so obfuscated; somehow the term has been partially translated into some more primitive form before stuff bombs out. If you look at the code which defines use (e.g. by right clicking on it) you might be able to work out what's going on better than I can!

[Anne Baanen]

tactic#use and tactic#show are two tactics that I almost never use because their error messages are useless. Instead there is refine \<something, _\> or tactic#change

[Kevin Buzzard]

use is absolutely great for beginners though, and I use show a lot in my teaching when Lean decides to obfuscate the goal for whatever reason and I use show to tidy it up before the sorry that the students then have to deal with.

[Anne Baanen]

Sure, refine \<something, _\> is a bit more complicated, but the basic use of change is exactly the same as show except the error change reports is not just literally show tactic failed

[Anne Baanen]

(I just remembered show has a secondary use where you can choose which goal to work on. Still the basic purpose of show and change is identical.)

[Vasily Ilin]

I am getting an error failed to instantiate goal with polynomial K after use polynomial K when my goal is ∃ (X : (Algebra K)ᵒᵖ) (f : coyoneda.obj X ⟶ forget (Algebra K)), is_iso f. Why could this be? The file is below

import category_theory.types
import algebra.category.Algebra.basic
import algebra.category.Group.basic
import data.polynomial.basic

open_locale polynomial
open polynomial
open category_theory

variables (K : Type*) [comm_ring K]

class affine_scheme :=
(scheme : Algebra K ⥤ Type*)
(corepresentable : scheme.corepresentable)

class affine_group_scheme :=
(scheme : Algebra K ⥤ Group)
(corepresentable : (scheme ⋙ forget Group).corepresentable)

-- DEFINING G_a
instance G_a : affine_scheme K :=
{
  scheme := forget (Algebra K),
  corepresentable := begin
    refine {has_corepresentation := _},
    use polynomial K, -- failed to instantiate goal with polynomial K
  end,
}

[Eric Wieser]

I would guess you need to use docs#Algebra.of

[Kevin Buzzard]

If you want to see what use exists you can always try refine \<_, _\>

[Vasily Ilin]

@Kevin Buzzard I do not understand what refine \<_, _\> does. It splits goal ⊢ ∃ (X : (Algebra K)ᵒᵖ), Exists is_iso into ⊢ (Algebra K)ᵒᵖ and ⊢ Exists is_iso. But I don't understand what it means to prove ⊢ (Algebra K)ᵒᵖ.

[Vasily Ilin]

@Eric Wieser , this is a good suggestion but it did not work for me. I'm getting failed to instantiate goal with Algebra.of K ((frozen_name polynomial) K) error.

[Alex J. Best]

It means you have to give an element of Algebra K^op, which is as per https://leanprover-community.github.io/mathlib_docs/algebra/category/Algebra/basic.html#Algebra a triple of a Type a ring structure and an algebra structure.

[Eric Wieser]

Alex, I think your parens are missing there

[Alex J. Best]

Sure, its also not unicode

[Vasily Ilin]

But this does not work:

instance G_a : affine_scheme K :=
{
  scheme := forget (Algebra K),
  corepresentable := begin
    refine {has_corepresentation := _},
    simp only,
    have : algebra K K[X],
      refine ring_hom.to_algebra _,
      exact C,
    refine ⟨_, _⟩,
    refine opposite.op _,
    use Algebra.of K (K[X]) -- failed to instantiate goal with Algebra.of K ((frozen_name polynomial) K)

  end,
}

[Eric Wieser]

Can you change that use to a refine?

[Eric Wieser]

You'll get a better error message

[Alex J. Best]

Or existsi instead of use

[Eric Wieser]

It's not even an existential at that point

[Vasily Ilin]

Error: failed to synthesize type class instance for K : Type u_1, _inst_1 : comm_ring K, this : algebra K K[X] ⊢ algebra K K[X]

[Alex J. Best]

Eric Wieser said:

It's not even an existential at that point

I'm confused why we are using use instead of exact then?

[Eric Wieser]

I think tactic#use tries to be clever

[Vasily Ilin]

Actually, this also errors: #check Algebra.of K K[X]. Not sure what's going on

[Eric Wieser]

Do you have data.polynomial.algebra_map imported?

[Eric Wieser]

You need to have docs#polynomial.algebra_of_algebra imported

[Vasily Ilin]

I did not. I thought it would be part of polyonmial.basic. Now #check Algebra.of K K[X] works. But the proof still does not

[Vasily Ilin]

I am not getting an error any more though

[Eric Wieser]

Surely if the proof doesn't work, then you're still getting an error?

[Vasily Ilin]

instance G_a : affine_scheme K :=
{
  scheme := forget (Algebra K),
  corepresentable := begin
    refine {has_corepresentation := _},
    simp only,
    have : algebra K K[X],
      refine ring_hom.to_algebra _,
      exact C,
    refine ⟨_, _⟩,
    refine opposite.op _, -- ⊢ Algebra K
    refine Algebra.of K (K[X]) -- ⊢ Algebra K
  end,
}

[Eric Wieser]

Add a comma

[Vasily Ilin]

This is what I have. I give it a K-algebra but it doesn't wanna take it

[Eric Wieser]

You're not done, you have another goal to prove

[Vasily Ilin]

Well, that worked

[Vasily Ilin]

What does the goal ⊢ Exists is_iso mean? Mathematically, I need to prove the isomorphism Hom(K[X], A) = abelian group of A. But I don't understand how this goal expresses that

[Alex J. Best]

The goal state after

-- DEFINING G_a
instance G_a : affine_scheme K :=
{
  scheme := forget (Algebra K),
  corepresentable := begin
    refine {has_corepresentation := _},
    refine ⟨opposite.op (Algebra.of K (K[X])), _⟩,

  end,
}

might be more clear