Quelle bug_17100.v Sprache: Coq

SetSet "bad-relevance".

Module

  : Prop1> Prop2.
Axiom buggy  ) :  ->
Axiom : <-.

Lemma buggyapply in.
Proof.
  intros. (* Bad relevance in case annotation. [bad-relevance,debug] *)
  apply in.
  refinefun>)
Qed : Type:Type.

java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0

Module Test2.

Axiom Type1 : Type.
Axiom Type2 : Type.
Axiom equiv : inhabited (Type1 -> Type1).

Lemma buggy (P : Prop) : Type1 -> True.
Proof.
  intros H.
  Fail apply equiv in H.
Abort.

End Test2.

Module Test3.

Axiom In : forall [A : Type] (a : A) (l : list A), Prop.
Definition all_equiv (l: list Prop) := forall x y, In x l -> In y l -> (x <-> y).

Axiom last : forall [A : Type], list A -> A -> A.
Axiom in_eq : forall [A : Type] (a : A) (l : list A), In a (a :: l).
Axiom in_last : forall [A : Type] (a b : A) (l : list A), In (last (b :: l) a) (a :: b :: l).

(* Check that apply in handles correctly binders in the lemma *)
Goal forall (b : Prop) (l : list Prop) (a : Prop)
  (H : all_equiv (a :: b :: l)), last (b :: l) a -> a.
Proof.
intros b l a H.
apply H.
+ apply in_eq.
+ apply in_last.
Qed.

End Test3.

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

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.