Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_3477.v Sprache: Coq

Original von: Coq^©

Require Import TestSuite.admit.

Require Import Relations Program Setoid Morphisms.

Section S1.
  Variable R: nat -> relation bool.
  Instance HR1: forall n, Transitive (R n). Admitted.
  Instance HR2: forall n, Symmetric (R n).  Admitted.
  Hypothesis H: forall n a, R n (andb a a) a.
  Goal forall n a b, R n b a.
   intros.
   (* rewrite <- H. *) (* Anomaly: Evar ?.. was not declared. Please report. *)
   (* idem with setoid_rewrite *)
(*    assert (HR2' := HR2 n). *)
   rewrite <- H.                (* ok *)
   admit.
  Qed.
End S1.

Section S2.
  Variable R: nat -> relation bool.
  Instance HR: forall n, Equivalence (R n). Admitted.
  Hypothesis H: forall n a, R n (andb a a) a.
  Goal forall n a b, R n a b.
   intros. rewrite <- H. admit.
  Qed.
End S2.

(* the parametrised relation is required to get the problem *)
Section S3.
  Variable R: relation bool.
  Instance HR1': Transitive R. Admitted.
  Instance HR2': Symmetric R.  Admitted.
  Hypothesis H: forall a, R (andb a a) a.
  Goal forall a b, R b a.
   intros.
   rewrite <- H.                (* ok *)
   admit.
  Qed.
End S3.

¤ 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.