Joshua Grosso (Jul 09 2021 at 03:53): 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?
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?
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!
Pierre-Marie Pédrot (Jul 09 2021 at 18:25):This might be related to the Keep Proof Equalities flag.
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.
Gaëtan Gilbert (Jul 09 2021 at 18:54):but Keep Proof Equalities only impacts injection users, not induction?
Last updated: Sep 23 2023 at 14:01 UTC