Quelle subterm3.v Sprache: Coq

(* An example showing that prop-extensionality is incompatible with
   powerful extensions of the guard condition.
   This is a variation on the example in subterm2, exploiting
   missing typing constraints in the commutative cut subterm rule
   (subterm2 is using the same flaw but for the match rule).

   Example due to Cristóbal Camarero on Coq-Club.
*)

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

Inductive True2 : Prop := I3 : (False -> True2) -> True2.

Theorem T3T: True2 = True.
Proof.
apply prop_ext; split; auto.
intros; constructor; apply False_rect.
Qed.

Theorem T3F_FT3F : (True2 -> False) = ((False -> True2) -> False).
Proof.
rewrite T3T.
apply prop_ext; split; auto.
Qed.

Fail Fixpoint loop (x : True2) : False :=
match x with
I3 f => (match T3F_FT3F in _=T return T with eq_refl=> loop end) f
end.

quality100%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.