Quelle bug_15753_1.v Sprache: Coq

Require Import Corelib.ssr.ssreflect.

Axiom R : Type.

Variant extended := EFin of R | EPInf | ENInf.

Definition le_ereal (x1 x2 : extended) :=
  match x1, x2 with
  | ENInf, EFin r | EFin r, EPInf => true
  | EFin r1, EFin r2 => true
  | ENInf, _    | _, EPInf => true
  | EPInf, _    | _, ENInf => false
  end.

Axiom lee_pinfty : forall (x : extended), is_true (le_ereal x (EPInf)).

Definition adde_subdef (x y : extended) :=
  match x, y with
  | EFin _, EFin _  => x
  | ENInf, _     => ENInf
  | _    , ENInf => ENInf
  | EPInf, _     => EPInf
  | _    , EPInf => EPInf
  end.

Definition adde := nosimpl adde_subdef.

Goal forall (x : R),
  (forall e : R, is_true (le_ereal (EFin x) (adde (EPInf) (EFin e)))) -> True.
Proof.
intros x.
Fail rewrite (lee_pinfty (EFin x)).
constructor.
Qed.

quality100%

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

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.