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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 716 lines to 197 lines, then from 206 lines to 162 lines, then from 163 lines to 73 lines *)
Require Import Coq.Sets.Ensembles.
Require Import Coq.Strings.String.
Global Set Implicit Arguments.
Global Set Asymmetric Patterns.
Ltac clearbodies := repeat match goal with | [ H := _ |- _ ] => clearbody H end.
Inductive Comp : Type -> Type :=
| Return : forall A, A -> Comp A
| Bind : forall A B, Comp A -> (A -> Comp B) -> Comp B.
Inductive computes_to : forall A, Comp A -> A -> Prop :=
| ReturnComputes : forall A v, @computes_to A (Return v) v
| BindComputes : forall A B comp_a f comp_a_value comp_b_value,
@computes_to A comp_a comp_a_value
-> @computes_to B (f comp_a_value) comp_b_value
-> @computes_to B (Bind comp_a f) comp_b_value.
Inductive is_computational : forall A, Comp A -> Prop :=
| Return_is_computational : forall A (x : A), is_computational (Return x)
| Bind_is_computational : forall A B (cA : Comp A) (f : A -> Comp B),
is_computational cA
-> (forall a,
@computes_to _ cA a -> is_computational (f a))
-> is_computational (Bind cA f).
Theorem is_computational_inv A (c : Comp A)
: is_computational c
-> match c with
| Return _ _ => True
| Bind _ _ x f => is_computational x
/\ forall v, computes_to x v
-> is_computational (f v)
end.
admit.
Defined.
Fixpoint is_computational_unique_val A (c : Comp A) {struct c}
: is_computational c -> { a | unique (computes_to c) a }.
Proof.
refine match c as c return is_computational c -> { a | unique (computes_to c) a } with
| Return T x => fun _ => exist (unique (computes_to (Return x)))
x
_
| Bind _ _ x f
=> fun H
=> let H' := is_computational_inv H in
let xv := @is_computational_unique_val _ _ (proj1 H') in
let fxv := @is_computational_unique_val _ _ (proj2 H' _ (proj1 (proj2_sig xv))) in
exist (unique (computes_to _))
(proj1_sig fxv)
_
end;
clearbodies;
clear is_computational_unique_val;
clear;
first [ abstract admit
| abstract admit ].
(* [Fail] does not catch the anomaly *)
Defined.
(* Anomaly: Uncaught exception Not_found(_). Please report. *)
|
