Stream: Coq users

Topic: Injection for dependent constructors


view this post on Zulip Li-yao (Jan 07 2021 at 21:34):

existT _ x f = existT _ y g is something you can actually invert if y and g are variables. Is there a tactic for doing that? I'm actually looking for a way that would work for any inductive type, but I'm not sure how to turn a constructor into a pattern.

One other step that seems useful for that is to generalize all hypotheses depending on y and g, but generalize dependent y mixes g and the aforementioned equality with everything else. Is there a tactic that would generalize everything that depends on multiple given variables, and either keeps those variables in the context or at least at the head of the goal?

view this post on Zulip Paolo Giarrusso (Jan 07 2021 at 22:45):

Was inversion_sigma related?

view this post on Zulip Paolo Giarrusso (Jan 07 2021 at 22:45):

(To the first)

view this post on Zulip Li-yao (Jan 07 2021 at 22:49):

Indeed that looks like it for sigma!


Last updated: Mar 29 2024 at 04:02 UTC