Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_4679.v Sprache: Coq

Original von: Coq^©

Require Import TestSuite.admit.
Require Coq.Lists.List.
Require Coq.Sets.Ensembles.
Import Coq.Sets.Ensembles.
Global Set Implicit Arguments.
Delimit Scope comp_scope with comp.
Inductive Comp : Type -> Type :=
| Return : forall A, A -> Comp A
| Bind : forall A B, Comp A -> (A -> Comp B) -> Comp B
| Pick : forall A, Ensemble A -> Comp A.
Notation ret := Return.
Notation "x <- y ; z" := (Bind y%comp (fun x => z%comp))
                           (at level 81, right associativity,
                            format "'[v' x <- y ; '/' z ']'") : comp_scope.
Axiom refine : forall {A} (old : Comp A) (new : Comp A), Prop.
Open Scope comp.
Axiom elements : forall {A} (ls : list A), Ensemble A.
Axiom to_list : forall {A} (S : Ensemble A), Comp (list A).
Axiom finite_set_handle_cardinal : refine (ret 0) (ret 0).
Definition sumUniqueSpec (ls : list nat) : Comp nat.
  exact (ls' <- to_list (elements ls);
         List.fold_right (fun a b' => Bind b' ((fun a b => ret (a + b)) a)) (ret 0) ls').
Defined.
Axiom admit : forall {T}, T.
Definition sumUniqueImpl (ls : list nat)
: { c : _ | refine (sumUniqueSpec ls) (ret c) }%type.
Proof.
  eexists.
  match goal with
    | [ |- refine ?a ?b ] => let a' := eval hnf in a in change (refine a' b)
  end.
  try setoid_rewrite (@finite_set_handle_cardinal).
Abort.

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.