Quelle bug_8004.v Sprache: Coq

Require Export Corelib.Program.Tactics Corelib.Classes.SetoidTactics Corelib.Classes.CMorphisms .

Set Universe Polymorphism.

Delimit Scope category_theory_scope with category_theory.
Open Scope category_theory_scope.

Infix "∧" := prod (at level 80, right associativity) : category_theory_scope.

Class Setoid A := {
  equiv : crelation A;
  setoid_equiv :: Equivalence equiv
}.

Notation "f ≈ g" := (equiv f g) (at level 79) : category_theory_scope.

Open Scope list_scope.

Generalizable All Variables.

Fixpoint list_equiv `{Setoid A} (xs ys : list A) : Type :=
  match xs, ys with
  | nil, nil => True
  | x :: xs, y :: ys => x ≈ y ∧ list_equiv xs ys
  | _, _ => False
  end.

Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.

#[export] Program Instance list_equivalence `{Setoid A} : Equivalence list_equiv.
Next Obligation.
  repeat intro.
  induction x; simpl; split; auto.
  reflexivity.
Qed.
Next Obligation.
  repeat intro.
  generalize dependent y.
  induction x, y; simpl; intros; auto.
  destruct X; split.
    now symmetry.
  intuition.
Qed.
Next Obligation.
admit.
Defined.

quality98%

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