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.

Julin Shaji (Nov 13 2023 at 06:17):

I was wondering about this now as well.

So a tactic 'in its defective form' means no arguments?
I too wonder why the name 'defective' was chosen for that.

Karl Palmskog (Nov 13 2023 at 07:14):

the etymology of "defective" is "un" + "do". My guess is that it refers to manipulating something in the context, thus "undoing" it.

Last updated: Apr 18 2024 at 15:01 UTC