The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

As a theoretical point: there are two kinds of things from Prop which cannot be eliminated to produce something in Type.

• Disjunctions P\/Q
• Existentials exists x:A, P

Their elimination is disallowed because it would expose “information” from the proof of a proposition to a computation (it would prevent things like extraction, for instance). But the case of existential is a bit different because allowing elimination would be inconsistent (in that False would be provable).

This is a rather technical result. It is an instance of https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.Hurkens.html#NoRetractFromTypeToProp where you would use exists x:A, True for down A then up would be the elimination of the existential.

​

On 31 May 2016 at 11:18, Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Dear Michael,

>
>
> I am way stuck trying to use an existential hypothesis with elim:
>
>
> 1 subgoal
>
> t : Type
>
> p : list t -> Type
>
> H0 : p [ ]
>
> HS : forall (x : t) (l : list t), p (l ++ [x])
>
> x : t
>
> l : list t
>
> HM : exists (x2 : t) (l2 : list t), l ++ [x] = [x2] ++ l2
>
> ______________________________________(1/1)
>
> p ([x] ++ l)
>
>
>
> now I want to elim HM to get the equation to rewrite the goal, so that I
> can use HS to solve it. But when I try “elim HM” I get the error “Error:
> Cannot find the elimination combinator ex_rect, the elimination of the
> inductive definition ex on sort Type is probably not allowed.”.
>
>

As Adam said, it is a useful feature of Coq to NOT allow the destruction
of an inductively defined term of type Prop to build a term of type
Type (or Set).

This way, you can add axioms in Prop without having to realize those
axioms during the extraction process. The idea is that propositions
cannot contribute to computations but only to (show) their correctness.

There are some exceptions though: when the inductive Prop is defined
by either 0 (eg False) or 1 (eg conj) constructor/rule, you can destruct
the constructor because it contains no computational content (ie choice)
in those two cases (0 or 1).

Regarding the solution to your problem, notice that you can prove
HM (or the reversed version I suggest here) directly for any l x.

(***********)

Require Import List.

Section test.

  Variables (t : Type).

  Implicit Type (l : list t).

  Fact invert_Prop l : forall x, exists x2 l2, l2 ++ x2::nil = (x::nil)
++ l.
  Proof.
    induction l as [ | y l IHl ]; intros x.
    exists x, nil; auto.
    destruct (IHl y) as (x2 & l2 & H).
    exists x2, (x::l2); auto.
    simpl; f_equal; auto.
  Qed.

  Fact invert_Type l : forall x, { x2 : _ & { l2 | l2 ++ x2::nil =
(x::nil) ++ l } }.
  Proof.
    induction l as [ | y l IHl ]; intros x.
    exists x, nil; auto.
    destruct (IHl y) as (x2 & l2 & H).
    exists x2, (x::l2); auto.
    simpl; f_equal; auto.
  Qed.

  Variables (p : list t -> Type) (H0 : p nil)
     (HS : forall (x : t) (l : list t), p (l ++ x :: nil))
     (x : t) (l : list t).

  Goal p ((x :: nil) ++ l).
  Proof.
    destruct (invert_Type l x) as (x2 & l2 & H2).
    rewrite <- H2; auto.
  Qed.

End test.

(***********)

You cannot destruct invert_Prop while proving the goal
but you can destruct invert_Type ...

Both invert_Prop and invert_Type have the very
same proof script (which does not mean that they
share the same proof term). Of course this corresponds
to the idea of replacing exists with either sig or sigT.

({ ... & ...} is a notation for sigT
and { ... | ... } a notation for sig.

Best regards,

Dominique