coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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."
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
- [Coq-Club] Incorrect elimination (defining function within proof), Andrew Gacek, 02/13/2015
- Re: [Coq-Club] Incorrect elimination (defining function within proof), Daniel Schepler, 02/13/2015
- Re: [Coq-Club] Incorrect elimination (defining function within proof), Andrew Gacek, 02/13/2015
- Re: [Coq-Club] Incorrect elimination (defining function within proof), Frédéric Blanqui, 02/13/2015
- Re: [Coq-Club] Incorrect elimination (defining function within proof), Andrew Gacek, 02/13/2015
- Re: [Coq-Club] Incorrect elimination (defining function within proof), Cedric Auger, 02/13/2015
- Re: [Coq-Club] Incorrect elimination (defining function within proof), Daniel Schepler, 02/13/2015
Archive powered by MHonArc 2.6.18.