The Coq mailing list

[Andrew Gacek <andrew.gacek AT gmail.com>]

Thanks Daniel. You are right, the axiom of choice proves this fairly easily:

Variable state : Set.

Definition transition := state -> state -> Prop.
Variable T : transition.

Definition trace := nat -> state.

Definition total : Prop :=
  forall s, exists s', T s s'.

Require Import ClassicalChoice.

Theorem total_has_trace :
  total -> forall s, exists P, P 0 = s /\ forall n, T (P n) (P (S n)).
intros.
apply choice in H as [f Hf].
exists (fix p n := match n with
                   | 0 => s
                   | S n' => f (p n')
                   end).
auto.
Qed.

On Thu, Feb 12, 2015 at 8:00 PM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:
> On Thu, Feb 12, 2015 at 5:16 PM, Andrew Gacek 
> <andrew.gacek AT gmail.com>
> wrote:
>>
>> I'm trying to prove that a total transition system has an infinite
>> trace starting from any state. The problem is that I need to provide a
>> witness for the trace which involves defining a fixed point. This
>> fixed point needs to destruct an existential, but that results in an
>> error about incorrect elimination. I thought there might be a way
>> around this since I'm still doing everything within the context of a
>> proof. Or perhaps what I'm trying to prove isn't intuitionistically
>> true?
>>
>> Variable state : Set.
>>
>> Definition transition := state -> state -> Prop.
>> Variable T : transition.
>>
>> Definition trace := nat -> state.
>>
>> Definition total : Prop :=
>>   forall s, exists s', T s s'.
>>
>> Theorem total_has_trace :
>>   total -> forall s, exists P, P 0 = s /\ forall n, T (P n) (P (S n)).
>> intros.
>> exists (fix p n := match n with
>>                    | 0 => s
>>                    | S n' => match H (p n') with
>>                              | ex_intro s' Hs' => s'
>>                              end
>>                    end).
>>
>>
>> The last line here results in:
>>
>> Error:
>> Incorrect elimination of "H (p n'0)" in the inductive type "ex":
>> the return type has sort "Set" while it should be "Prop".
>> Elimination of an inductive object of sort Prop
>> is not allowed on a predicate in sort Set
>> because proofs can be eliminated only to build proofs.
>>
>> Please let me know if you have any ideas about how to go about proving
>> this.
>
>
> This is fairly close to the axiom of (countable) dependent choice, which
> isn't even provable assuming excluded middle.  You might look into using the
> axiom of choice (Require Import Choice.)  To prove your statement, the major
> stepping stone would be to use the axiom of choice to prove (exists totalT :
> state -> state, forall s, T s (totalT s)).  The first step of
> total_has_trace would then be to destruct the exists statement, and then
> construct a fixpoint function similarly to what you did above.
> --
> Daniel Schepler
>