diff options
Diffstat (limited to 'test-suite/bugs/closed/3344.v')
-rw-r--r-- | test-suite/bugs/closed/3344.v | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3344.v b/test-suite/bugs/closed/3344.v new file mode 100644 index 00000000..8255fd6c --- /dev/null +++ b/test-suite/bugs/closed/3344.v @@ -0,0 +1,58 @@ +(* 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. *) |