Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Incorrect elimination (defining function within proof)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Incorrect elimination (defining function within proof)


Chronological Thread 
  • From: Cedric Auger <sedrikov AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Incorrect elimination (defining function within proof)
  • Date: Fri, 13 Feb 2015 10:16:37 +0100

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




Archive powered by MHonArc 2.6.18.

Top of Page