Stream: math-comp users

Topic: Where does the phrase "defective tactic" come from?

Li-yao (Apr 24 2022 at 19:17):

move, elim, case are referred to as "defective tactics": https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#the-defective-tactics

I'm curious what's "defective" about them.

Paolo Giarrusso (Apr 24 2022 at 19:37):

Here, "defective" = lack "arguments".

Paolo Giarrusso (Apr 24 2022 at 19:38):

So when the manual describes the defective move, it adds:

Of course this tactic is most often used in combination with the bookkeeping tacticals

Paolo Giarrusso (Apr 24 2022 at 19:43):

I won’t claim that “defective” can mean “missing something” in English — but maybe in Latin/French?

Paolo Giarrusso (Apr 24 2022 at 19:44):

back to ssreflect, I can’t remember/find where I read that “defective” is used in this sense (maybe in the ssreflect tutorial?), so a clarification in the manual would IMHO be welcome.

Last updated: Feb 08 2023 at 04:04 UTC