Relationship between existential and universal quantifier in an inductive Coq definition

Question

Suppose I want an inductive definiton of a substring (with string being just a synonym for list).

Inductive substring {A : Set} (w : string A) :
                    (string A) -> Prop :=
  | SS_substr : forall x y z : string A,
                  x ++ y ++ z = w ->
                  substring w y.

Here I can for example prove the following:

Theorem test : substring [3;4;1] [4].
Proof.
  eapply SS_substr.
  cbn.
  instantiate (1:=[1]).
  instantiate (1:=[3]).
  reflexivity.
Qed.

However, the proof is "existential" rather than "universal", in spite of the fact that the inductive definition states forall x y z and only then constrains their shapes. This seems somewhat unintuitive to me. What gives?

Also, is it possible to make an inductive definition using exists x : string A, exists y : string A, exists z : string, x ++ y ++ z = w -> substring w y?

eponier eponier · Accepted Answer · 2016-11-08T09:26:00

One important thing to note is that exists is not a built-in functionality of Coq (contrary to forall). Actually, exists itself is a notation, but behind there is an inductive type named ex. The notation and the inductive type are defined in the Coq standard library. Here is the definition of ex:

Inductive ex (A:Type) (P:A -> Prop) : Prop :=
    ex_intro : forall x:A, P x -> ex (A:=A) P.

It is defined using one constructor and a universal quantification, like your substring type, so it is not surprising that your susbtring type seems to be "existential" at some point.

Of course, you can define your type using exists, and you do not even need Inductive.

Definition substring' {A : Set} (w y : string A) : Prop :=
    exists x z, x ++ y ++ z = w.

Relationship between existential and universal quantifier in an inductive Coq definition

1 Answers