Why does Coq not allow inversion, destruction, etc., when the goal is a type?

Question

When refine with the program, I tried to complete the proof of inversion in the False hypothesis when the target was Type . Here is the version of the proof I was trying to make.

 Lemma strange1: forall T:Type, 0>0 -> T. intros T H. inversion H. (* Coq refuses inversion on 'H : 0 > 0' *) 

Coq complained

 Error: Inversion would require case analysis on sort Type which is not allowed for inductive definition le 

However, since I am not doing anything with T , it does not matter, ... or?

I got rid of T like this, and the proof passed:

 Lemma ex_falso: forall T:Type, False -> T. inversion 1. Qed. Lemma strange2: forall T:Type, 0>0 -> T. intros T H. apply ex_falso. (* this changes the goal to 'False' *) inversion H. Qed. 

What is the reason Kok complained? Is it just a flaw in inversion , destruct , etc.?

Answer 1

I have never seen this problem before, but it makes sense, although it can probably be argued that this is a bug in inversion .

This problem is due to the fact that inversion is implemented by case analysis. In Coq logic, it is impossible to analyze data by a logical hypothesis (i.e., something like Prop ) if the result is something computational (i.e. if the type of the return type is a Type ). One of the reasons for this is that Coq developers wanted to make it possible to erase evidence-based arguments from programs by extracting them into code in sound form: in this way, random analysis can be allowed only for a hypothesis, to do something computational if the destructible thing isn’t may change the result. It includes:

• Sentences without constructors, for example False .
• Suggestions with a single constructor, if this constructor does not accept arguments of a computational nature. This includes True , Acc (the accessibility predicate used to perform reasonable recursion), but excludes the existential quantifier ex .

As you noticed, however, you can get around this rule by converting some sentence that you want to use to create your result to another, which you can do case analysis directly. Thus, if you have a conflicting assumption, as in your case, you can first use it to prove False (which is allowed, since False is Prop ), and then exclude False to get the result (which is allowed by the above rules).

In your example, inversion too conservative, refusing only because in this context it cannot analyze the case with something like 0 < 0 . It is true that he cannot analyze data on it directly according to the rules of logic, as explained above; however, you might consider making a smarter implementation of inversion , which recognizes that we eliminate the conflicting hypothesis and add False as an intermediate step, just like you do. Unfortunately, it seems to us that we need to do this trick manually in order for it to work.