Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: guard_cofix.v Sprache: Coq

Original von: Coq^©

(* This script shows, in two different ways, the inconsistency of the
propositional extensionality axiom with the guard condition for cofixpoints. It
is the dual of the problem on fixpoints (cf subterm.v, subterm2.v,
subterm3.v). Posted on Coq-club by Maxime Dénès (02/26/2014). *)

(* First example *)

CoInductive CoFalse : Prop := CF : CoFalse -> False -> CoFalse.

CoInductive Pandora : Prop := C : CoFalse -> Pandora.

Axiom prop_ext : forall P Q : Prop, (P<->Q) -> P = Q.

Lemma foo : Pandora = CoFalse.
apply prop_ext.
constructor.
intro x; destruct x; assumption.
exact C.
Qed.

Fail CoFixpoint loop : CoFalse :=
match foo in (_ = T) return T with eq_refl => C loop end.

Fail Definition ff : False := match loop with CF _ t => t end.

(* Second example *)

Inductive omega : Prop := Omega : omega -> omega.

Lemma H : omega = CoFalse.
Proof.
apply prop_ext; constructor.
  induction 1; assumption.
destruct 1; destruct H0.
Qed.

Fail CoFixpoint loop' : CoFalse :=
  match H in _ = T return T with
    eq_refl =>
    Omega match eq_sym H in _ = T return T with eq_refl => loop' end
  end.

Fail Definition ff' : False := match loop' with CF _ t => t end.

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.