Why Coq doesn't allow inversion, destruct, etc. when the goal is a Type?

Question

When refineing a program, I tried to end proof by inversion on a False hypothesis when the goal was a Type. Here is a reduced version of the proof I tried to do.

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 do nothing with T, it shouldn't matter, ... or ?

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

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 Coq complained? Is it just a deficiency in inversion, destruct, etc. ?

Heavyarmed

An enlightening discussion at the coq-club mailing list: sympa.inria.fr/sympa/arc/coq-club/2014-12/msg00036.html – Heavyarmed

Answer 1

I had never seen this issue before, but it makes sense, although one could probably argue that it is a bug in inversion.

This problem is due to the fact that inversion is implemented by case analysis. In Coq's logic, one cannot in general perform case analysis on a logical hypothesis (i.e., something whose type is a Prop) if the result is something of computational nature (i.e., if the sort of the type of the thing being returned is a Type). One reason for this is that the designers of Coq wanted to make it possible to erase proof arguments from programs when extracting them into code in a sound way: thus, one is only allowed to do case analysis on a hypothesis to produce something computational if the thing being destructed cannot alter the result. This includes:

1. Propositions with no constructors, such as False.
2. Propositions with only one constructor, as long as that constructor takes no arguments of computational nature. This includes True, Acc (the accessibility predicated used for doing well-founded recursion), but excludes the existential quantifier ex.

As you noticed, however, it is possible to circumvent that rule by converting some proposition you want to use for producing your result to another one you can do case analysis on directly. Thus, if you have a contradictory assumption, like in your case, you can first use it to prove False (which is allowed, since False is a Prop), and then eliminating False to produce your result (which is allowed by the above rules).

In your example, inversion is being too conservative by giving up just because it cannot do case analysis on something of type 0 < 0 in that context. It is true that it can't do case analysis on it directly by the rules of the logic, as explained above; however, one could think of making a slightly smarter implementation of inversion that recognizes that we are eliminating a contradictory hypothesis and adds False as an intermediate step, just like you did. Unfortunately, it seems that we need to do this trick by hand to make it work.

Lovesome

Isn't the fact that < is in Prop so you can't case analyse it to build a Type the real issue ? Am I missing something here ? – Scleritis

Hmmm I guess I miss-interpreted your "bug in inversion". I would call this a feature, to prevent universe inconsistency. Even if in this particular case the result of inversion is not used to compute the result, I'm glad that Coq prevents this kind of escalation. If the result does not depend on the inversion, do not perform it ;) – Scleritis

@Scleritis how does this prevent universe inconsistency? – Lovesome

I don't remember the details, it's been a long time since I thought about this kind of issues. I'll try to dig up some old papers on the subject, and see if I can answer that :) – Scleritis

@Scleritis regardless of consistency issues, inversion could still try to be smarter in that case without changing the basic logic -- I guess I was not very clear about that. It could do automatically what one would do by hand in this case, which is to produce a proof of False first. – Lovesome

Answer 2

In addition to Arthur's answer, there is a workaround using constructive_definite_description axiom. Using this axiom in a function would not allow to perform calculations and extract code from it, but it still could be used in other proofs:

From Coq Require Import Description.

Definition strange1: forall T:Type, 0>0 -> T.
  intros T H.
  assert (exists! t:T, True) as H0 by inversion H.
  apply constructive_definite_description in H0.
  destruct H0 as [x ?].
  exact x.
Defined.

Or same function without proof editing mode:

Definition strange2 (T: Type) (H: 0 > 0): T :=
  proj1_sig (constructive_definite_description (fun _ => True) ltac: (inversion H)).

Also there's a stronger axiom constructive_indefinite_description that converts a proposition exists x:T, P x (without uniqueness) into a corresponding sigma-type {x:T | P x}.

Guanabara