如何用destruct代替inversion完成Coq中爆炸原理的证明？

Great question! Let's unpack why destruct works on False and how it completes the proof of the explosion principle.

First: What is False in Coq? #

In Coq, False is defined as an inductive type with no constructors:

Inductive False : Prop := .

That means there's no valid way to create a term of type False in a consistent logical context. If you have a term contra : False in your context, it's a direct contradiction—something that shouldn't exist if your assumptions are consistent.

How does destruct work here? #

The destruct strategy is designed to break down terms of inductive types. When you run destruct X on a term X of an inductive type:

• Coq generates a separate subgoal for each constructor of that type.
• If the inductive type has no constructors (like False), there are zero subgoals left to prove.

Let's walk through your proof step by step:

1. intros P contra: This brings the universal proposition P and the contradictory term contra : False into your context. Your goal is still to prove P.
2. destruct contra: Coq checks the definition of False and sees there are no constructors. Since there are no possible cases to validate, the contradiction in your context (contra : False) already makes the goal trivially true (by the explosion principle). Coq closes the proof immediately because there's nothing left to show.

How does this compare to inversion? #

inversion is a more powerful strategy that digs into the structure of inductive terms to find contradictions or infer logical equalities. In this specific case, both inversion contra and destruct contra achieve the same result because False has no constructors—both strategies recognize the contradiction and close the goal. The key difference is that inversion can handle more complex inductive types (like those with multiple constructors or nested structures), while destruct is a simpler tool that works perfectly here.

To sum up: #

• False counts as an inductive type (even without constructors), so destruct can operate on it.
• Destructing a False term eliminates all subgoals because such a term can't exist in a consistent context. This lets us conclude any proposition P from the contradiction—exactly what the explosion principle states.

内容的提问来源于stack exchange，提问作者Waiting for Dev...