Quelle bug_10175.v Sprache: Coq

From Corelib Require Import ssreflect ssrbool ssrfun.
From Corelib Require Import ListDef.

Import Nat.

Fixpoint filter A (f : A -> bool) (l:list A) : list A :=
  match l with
  | nil => nil
  | x :: l => if f x then x::(filter A f l) else filter A f l
  end.
Arguments filter {_}.

Definition partition {X : Type}
                     (test : X -> bool)
                     (l : list X)
                   : list X * list X
  := (filter test l, filter (fun x => negb (test x)) l).

Section Fold_Right_Recursor.
  Variables (A : Type) (B : Type).
  Variable f : B -> A -> A.
  Variable a0 : A.

  Fixpoint fold_right (l:list B) : A :=
    match l with
      | nil => a0
      | cons b t => f b (fold_right t)
    end.
End Fold_Right_Recursor.
Arguments fold_right {_ _}.

Definition fold (A B: Type) f l b:= @fold_right B A f b l.

Theorem partition_fst: forall (X : Type)  (test : X -> bool) (l : list X),
                         fold_right andb true (map test (fst (partition test l))) = true.
Proof.
  move => ? test.
  elim => [|x xs IHxs] //.
  case H: eqb (test x) true.  (* <-- anomaly here! *)
Abort.

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.