Quelle bug_11011.v Sprache: Coq

Require Import Setoid.
Require Import Corelib.Classes.CRelationClasses.
Require Import Corelib.Classes.CMorphisms.

Parameter B C : Type.
Parameter P : Type -> Type -> Type.

(* This is used for rewrites for lem_P and lem_P_iffT. *)
#[export] Instance P_Proper : Proper (iffT ==> iffT ==> iffT) (P).
Admitted.

Lemma lem_P : forall A, iffT A B -> P A C -> P B C.
Proof.
  intros A H1 H2.
  rewrite H1 in H2. (* Comment out iffT_P_Proper to see this fail. *)
Abort.

Lemma lem_P_iffT : forall A, iffT A B -> P A C -> iffT B C.
Proof.
  intros A H1 H2.
  setoid_rewrite H1 in H2.  (* Comment out iffT_P_Proper to see this fail. *)
Abort.

(* Trying to do the same with iffT instead of P. *)
#[export] Instance iffT_Proper : Proper (iffT ==> iffT ==> iffT) iffT.
Admitted.

(* Just in case? *)
#[export] Instance arrow_Proper  : Proper (iffT ==> iffT ==> iffT ) (arrow).
Admitted.

Lemma lem_iffT_P : forall A, iffT A B -> iffT A C -> P B C.
Proof.
  intros A H1 H2.
  rewrite H1 in H2.
Abort.

Lemma lem_iffT : forall A, iffT A B -> iffT A C -> iffT B C.
Proof.
  intros A H1 H2.
  setoid_rewrite H1 in H2.
Abort.

quality100%

¤ Dauer der Verarbeitung: 0.5 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.