Quelle bug_16362.v Sprache: Coq

Require Corelib.Setoids.Setoid.
Export Corelib.Classes.Morphisms.
Export Corelib.Setoids.Setoid.

Axiom A : Type.
Axiom equiv : relation A.
Axiom sg_op : A -> A -> A.
Axiom mon_unit : A.
Axiom negate : A -> A.

#[export] Declare Instance sg_setoid : Equivalence equiv.
#[export] Declare Instance sg_op_proper : Proper (equiv ==> equiv ==> equiv) sg_op.
Axiom right_identity : forall x, equiv (sg_op x mon_unit) x.
Axiom left_inverse : forall x, equiv (sg_op (negate x) x) mon_unit.

#[global] Hint Rewrite @right_identity @left_inverse using apply _: group_cancellation.

(* Check that the rewrite hints are considered in the right order. *)

Goal equiv mon_unit (sg_op (negate mon_unit) mon_unit).
Proof.
rewrite_strat (try bottomup (hints group_cancellation)). (* should select left_inverse rather than right_identity *)
reflexivity.
Qed.

quality94%

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