Quelle bug_12240.v Sprache: Coq

Require Import Setoid CMorphisms.

Set Implicit Arguments.

Inductive R A : A -> A -> Type :=
   (* with A -> A -> Prop here and Morphisms on top: no failure *)
   (* with relation A here and Morphisms on top: no failure *)
   (* with crelation A here and CMorphisms on top: no failure *)
| cR1 l : R l l
| cR2 l : R l l.  (* with only one constructor, only Fail 1 fails *)
#[export] Hint Constructors R : core.

#[export] Instance R_refl A : Reflexive (@R A).
Proof. auto. Qed.
#[export] Instance R_trans A : Transitive (@R A).
Proof. intros x y z HR1 HR2; destruct HR1, HR2; auto. Qed.

Goal forall (a b : nat), R a b -> R (id a) (id b).
Proof. intros a b H.
  (** This still fails but should be fixed when #7675 is. *)
  Fail rewrite H; reflexivity. (* does not fail with nat inlined in the definition of R *)
    (* Fail 1 *)
    (* Tactic failure: setoid rewrite failed: ... *)
Abort.

Goal forall A (a b : A), R a b -> R (id a) (id b).
Proof. intros A a b H.
  rewrite H; reflexivity.
Abort.

Definition GuR A (uu : unit) := match uu with unit => @R A end.

#[export] Instance GuR_refl A uu : Reflexive (@GuR A uu).
Proof. destruct uu; apply R_refl. Qed.
#[export] Instance GuR_trans A uu : Transitive (@GuR A uu).
Proof. destruct uu; apply R_trans. Qed.

Goal forall uu (a b : nat), GuR uu a b -> GuR uu (id a) (id b).
Proof. intros uu a b H.
  rewrite H; reflexivity.
Abort.

Goal forall A uu (a b : A), GuR uu a b -> GuR uu (id a) (id b).
Proof. intros A uu a b H.
  rewrite H; reflexivity.
Abort.

Definition GbR A (bb : bool) := if bb then @R A else @R A.

#[export] Instance GbR_refl A bb : Reflexive (@GbR A bb).
Proof. destruct bb; apply R_refl. Qed.
#[export] Instance GbR_trans A bb : Transitive (@GbR A bb).
Proof. destruct bb; apply R_trans. Qed.

Goal forall bb (a b : nat), GbR bb a b -> GbR bb (id a) (id b).
Proof. intros bb a b H.
  rewrite H; reflexivity.
Qed.

Goal forall A bb (a b : A), GbR bb a b -> GbR bb (id a) (id b).
Proof. intros A bb a b H.
  rewrite H; reflexivity.
Qed.

quality99%

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