blob: 5a1241151c618c0c6b6c1b0723a8c1ed99cb9985 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
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 refine (_ : refine a' b)
end;
try setoid_rewrite (@finite_set_handle_cardinal).
Undo.
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). (* Anomaly: Uncaught exception Invalid_argument("decomp_pointwise").
Please report. *)
instantiate (1 := admit).
admit.
Defined.
|
