3

The Finite_sets library of Coq has an inductive type, specifying that some ensemble is finite:

Inductive Finite : Ensemble U -> Prop :=
| Empty_is_finite : Finite (Empty_set U)
| Union_is_finite :
  forall A:Ensemble U,
    Finite A -> forall x:U, ~ In U A x -> Finite (Add U A x).

I am trying to prove that membership in a finite set is decidable as follows:

Lemma Finite_dec (A:Type) : forall f:Ensemble A, Finite A f ->
  forall x:A, {In A f x} + {~In A f x}.
Proof.
intros.
induction H.

However, Coq produces the following error message: 

Cannot find the elimination combinator Finite_rec, the
elimination of the inductive definition Finite on sort Set is
probably not allowed.

My question is, why is Coq not able to generate an elimination combinator for Finite? What is required of an inductive type for this to be possible?

Note: I need an elimination combinator for a different type, which is very similar to Finite, but do not know how to construct this.

Myrthe van Delft
  • 53
  • 4
  • 2
    In this case the particular problem is that the `Finite` inductive is of type prop, thus you cannot extract "true" information from it, which your decidability is. If you change your goal to `In A f x \/ ~In A f x` it will go throu. You could obtain your result over different hypotheses but I would particularly use other approach altogether, namely encoding my finite sets as lists with a quotient. – ejgallego Sep 29 '16 at 13:00
  • In [this](http://stackoverflow.com/a/27324790/2747511) answer to a related [question](http://stackoverflow.com/questions/27322979/why-coq-doesnt-allow-inversion-destruct-etc-when-the-goal-is-a-type) Arthur Azevedo De Amorim perfectly explains the reason. Just replace `inversion` with `induction` in his explanation. – Anton Trunov Sep 29 '16 at 15:07
  • Thank you, but I need the sumbool to be able to use the lemma in a function which I am defining, so proving it only for propositions is not sufficient. – Myrthe van Delft Sep 30 '16 at 11:51

2 Answers2

2

One problem, as @ejgallego pointed out, is that you cannot do induction on something propositional, such as Finite, to obtain something computational such as {P} + {~ P}. There's a deeper issue, however: your result is not provable without assuming some form of the excluded middle, because it implies that all types have decidable equality.

Goal (forall (A : Type) (f : Ensemble A),
        Finite A f -> forall x, In A f x \/ ~ In A f x) ->
     forall (A : Type) (x y : A), x = y \/ x <> y.
Proof.
intros fin_dec A x y.
assert (fin : Finite A (Add A (Empty_set A) x)).
{ apply Union_is_finite.
  - apply Empty_is_finite.
  - intros []. }
specialize (fin_dec _ _ fin y).
destruct fin_dec as [H | H].
- destruct H.
  + destruct H.
  + destruct H. now left.
- right.
  contradict H. rewrite H. right. constructor.
Qed.

If you don't want to work with extra axioms, I would advise you to use lists instead of the ensemble library, and work with types that have decidable equality.

Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39
  • I realized the problem of decidable equality, but trying to prove this only for types with decidable equality still left me in a state where I couldn't prove the property. Though I could change to lists, as proposed above, I would still like to know if it would be possible to prove using something like Finite, even if only for types with decidable equality. – Myrthe van Delft Sep 30 '16 at 11:49
0

After trying some things, I got some inspiration from one of the error messages

Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs

This gave me the inspiration of trying to change the return type from Prop to Type. In this case, I am capable of calling induction, and the proof of the following is straightforward. 

Inductive Finite (U:Type) : Ensemble U -> Type :=
| Empty_is_finite : Finite U (Empty_set U)
| Union_is_finite :
  forall A:Ensemble U,
    Finite U A -> forall x:U, ~ In U A x -> Finite U (Add U A x).

Definition eq_dec (U:Type) : forall x y:U, {x=y} + {x<>y}.

Lemma Finite_dec (A:Type) : forall f:Ensemble A, Finite A f ->
  forall x:A, {In A f x} + {~In A f x}.
Proof.
intros.
induction X.

Though I do not fully understand the reasons for this.

Myrthe van Delft
  • 53
  • 4
  • [This](http://cstheory.stackexchange.com/questions/21836/why-does-coq-have-prop) might clarify some things for you. – Anton Trunov Oct 17 '16 at 15:29