subtype_instance

Stream: general

[Scott Morrison]

I'm having trouble using subtype_instance.

With a state of

R S : examples.CommRing,
f g : R ⟶ S,
h : is_subring {r : ↥R | ⇑f r = ⇑g r}
⊢ comm_ring ↥{r : ↥R | ⇑f r = ⇑g r}

running subtype_instance reports:

assumption tactic failed
state:
R S : examples.CommRing,
f g : R ⟶ S,
h : is_subring {r : ↥R | ⇑f r = ⇑g r}
⊢ set ?m_1

Is this expected? I appreciate I may be asking too much from subtype_instance there.

[Mario Carneiro]

isn't this a theorem?

[Mario Carneiro]

A subring of a comm_ring yields a comm_ring

[Scott Morrison]

Hi @Simon Hudon, did you write subtype_instance? I think I need some help with it.

[Scott Morrison]

Sorry, problem solved.

[Simon Hudon]

Oh! I just saw that! What was the issue?

[Kenny Lau]

RIP subtype_instance 2018-2020

[Kenny Lau]

where did it go?

[Kenny Lau]

(to be clear, the tactic by subtype_instance is still there, but it is never used)

[Yury G. Kudryashov]

AFAIR, we found out that the tactic creates bad definitions, and I rewrote all 2-3 instances by hand.

[Yury G. Kudryashov]

The instances provided by subtype_instance created diamonds that Lean failed to unify.

[Kenny Lau]

then is it time to kill the tactic itself?