Stream: Coq users

Topic: "Cannot remove" warning


view this post on Zulip Joshua Grosso (Jul 09 2021 at 03:53):

If induction gives me Warning: Cannot remove foo. [cannot-remove-as-expected,tactics] but the proof goes through anyway, do I need to worry about e.g. unsoundness?

view this post on Zulip Yannick Forster (Jul 09 2021 at 06:48):

No, you never have to worry about unsoundness introduced by a tactic. The proof term the tactic generates is a correct proof term as indicated by the working Qed, meaning the kernel checked your proof term successfully. Can you give some context where the error occurs? In particular, are you doing induction on foo or does any of your intro patterns use the name foo?

view this post on Zulip Joshua Grosso (Jul 09 2021 at 18:16):

I'm not sure why, but removing From Equations Require Import Equations gets rid of the warning. Regardless, I'm glad to hear it's not the end of the world!

view this post on Zulip Pierre-Marie Pédrot (Jul 09 2021 at 18:25):

This might be related to the Keep Proof Equalities flag.

view this post on Zulip Pierre-Marie Pédrot (Jul 09 2021 at 18:25):

This warning typically applies when induction tries to apply a non-dependent induction principle because the inductive type lives in Prop.

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 18:54):

but Keep Proof Equalities only impacts injection users, not induction?


Last updated: Feb 04 2023 at 21:02 UTC