Quelle subterm2.v Sprache: Coq

(* An example showing that prop-extensionality is incompatible with
   powerful extensions of the guard condition.
   Unlike the example in guard2, it is not exploiting the fact that
   the elimination of False always produces a subterm.

   Example due to Cristobal Camarero on Coq-Club.
   Adapted to nested types by Bruno Barras.
*)

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

Module Unboxed.

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

Theorem Heq: (False->True2)=True2.
Proof.
apply prop_ext. split.
- intros. constructor. exact H.
- intros. exact H.
Qed.

Fail Fixpoint con (x:True2) :False :=
match x with
I2 f => con (match Heq in _=T return T with eq_refl => f end)
end.

End Unboxed.

(* This boxed example shows that it is not enough to just require
   that the return type of the match on Heq is an inductive type
*)
Module Boxed.

Inductive box (T:Type) := Box (_:T).
Definition unbox {T} (b:box T) : T := let (x) := b in x.

Inductive True2:Prop:= I2: box(False->True2)->True2.

Definition Heq: (False->True2) <-> True2 :=
  conj (fun f => I2 (Box _ f)) (fun x _ => x).

Fail Fixpoint con (x:True2) :False :=
match x with
I2 f => con (unbox(match prop_ext _ _ Heq in _=T return box T with eq_refl => f end))
end.

End Boxed.

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.