The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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