Zulip Chat Archive

Stream: new members

Topic: failed to instantiate goal with subtypes

Nir Paz (Mar 06 2023 at 18:43):

This code produces a "failed to instantiate goal" error:

example :  (f : {x :  | true}  {x :  | true}), true :=
  use λ x, if ( (n : ), n > 0) then 0 else 0, sorry⟩,

But when I change ∃ (n : ℕ), n > 0 to something simpler, like 0 = 0, then it works. Obviously I'm working on something a bit different than this (this is the minimalistiest example I found), but I need to define a function with "if" for it, and then because of this problem I can't even try to fill the sorry.
I think maybe I'm just misunderstanding something basic about subtypes or defining functions this way, so any clarification is welcome (:

Eric Wieser (Mar 06 2023 at 19:18):

This is just use being annoying

Kyle Miller (Mar 06 2023 at 19:18):

I haven't tested your example, but one thing that seems possible is that since if requires a decidable instances (and there's not immediately one here), use fails, and use can be unfriendly like that. Maybe try using the classical tactic first? This adds the classical decidable instances.

Eric Wieser (Mar 06 2023 at 19:18):

Use refine instead of use and you'll get a better error message

Kevin Buzzard (Mar 06 2023 at 19:20):

By the way, functions go from types to types and the domain and codomain of your f are terms (because they're subsets), so they're being coerced into types which causes a bit of obfuscation. You can use {x : \R // true} to make the subtype directly.

Nir Paz (Mar 06 2023 at 23:03):

using classical worked, thanks!

Last updated: Dec 20 2023 at 11:08 UTC