The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello. You can find something similar in http://color.inria.fr/ in the 
file Util/Relation/DepChoicePrf.v (see 
http://color.inria.fr/doc/CoLoR.Util.Logic.DepChoicePrf.html for the 
statements only). Best regards, Frédéric.


Le 13/02/2015 03:10, Andrew Gacek a écrit :
> 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