The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

If you do not want to use extra axiom, by changing total into:

Definition total : Prop := exists (step:state->state), forall s, T s (step s),

you can prove your lemma.
My definition implies yours, but yours requires an axiom (choice axiom) to prove mine.
And your first step in the proof would be "intros [step Hstep] s." rather than simply "intros."

2015-02-13 2:16 GMT+01:00 Andrew Gacek <andrew.gacek AT gmail.com>:

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.

Thanks,
Andrew Gacek