diff options
author | 2015-07-15 13:15:50 +0200 | |
---|---|---|
committer | 2015-07-15 13:15:50 +0200 | |
commit | e347929583f820a2cc0296597b6382309e930989 (patch) | |
tree | cdc3f18fc5c66a9d3d7cc8404c6a295169e41fcc /test-suite/bugs/closed/3786.v | |
parent | c01be74d81a5466c58f8dc6c568db286b0979997 (diff) | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 8.5~beta2+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3786.v')
-rw-r--r-- | test-suite/bugs/closed/3786.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3786.v b/test-suite/bugs/closed/3786.v new file mode 100644 index 00000000..23d19e94 --- /dev/null +++ b/test-suite/bugs/closed/3786.v @@ -0,0 +1,33 @@ +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. |