# What I'm doing wrong? Smth not computing

**URL:** <https://discourse.rocq-prover.org/t/what-im-doing-wrong-smth-not-computing/507>\
**Category:** Using Rocq\
**Created:** [November 24, 2019, 2:15pm UTC](https://discourse.rocq-prover.org/t/what-im-doing-wrong-smth-not-computing/507 "2019-11-24T14:15:17Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![LessnessR](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lessnessr/32/783_2.png) [@LessnessR](https://discourse.rocq-prover.org/u/LessnessR)\
**Post date:** [November 24, 2019, 2:15pm UTC](https://discourse.rocq-prover.org/t/what-im-doing-wrong-smth-not-computing/507/1 "2019-11-24T14:15:17Z")

</div>

```
Require Import List Arith Utf8.
Set Implicit Arguments.

Definition dec (P: Prop) := { P } + { ~ P }.
Definition eq_dec A := ∀ (x y: A), { x = y } + { x ≠ y }.
Definition fmap A B (Da: eq_dec A) (Db: eq_dec B) :=
  { L: list (A * B) | NoDup (map fst L) }.

Definition fmap_value A B Da Db (m: @fmap A B Da Db) (key: A): option B.
Proof.
  destruct m. induction x.
  + simpl in *. exact None.
  + simpl in *. apply NoDup_cons_iff in n. destruct n.
    destruct (IHx H0).
    - exact (Some b).
    - destruct a. destruct (Da a key).
      * exact (Some b).
      * exact None.
Defined.
Definition all_keys A B Da Db (m: @fmap A B Da Db) :=
  map fst (proj1_sig m).

Definition test_fmap: fmap Nat.eq_dec Nat.eq_dec.
Proof.
  exists ((1,2)::(2,3)::(3,5)::nil).
  simpl. apply NoDup_cons.
  + intro. simpl in H. intuition; congruence.
  + apply NoDup_cons.
    - intro. simpl in H. intuition; congruence.
    - apply NoDup_cons.
      * intro. simpl in H. auto.
      * apply NoDup_nil.
Defined.
Eval compute in (fmap_value test_fmap 2).
```

The “Eval compute” doesn’t return Some 3 somehow. 😑

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [November 24, 2019, 2:35pm UTC](https://discourse.rocq-prover.org/t/what-im-doing-wrong-smth-not-computing/507/2 "2019-11-24T14:35:59Z")

</div>

As you can see it blocks on NoDup\_cons\_iff which is opaque.  
You can change your definition to avoid this:

```diff
- + simpl in *. apply NoDup_cons_iff in n. destruct n.
- destruct (IHx H0).
+ + simpl in *. destruct IHx.
+ - apply NoDup_cons_iff in n. destruct n as [_ H0];apply H0.

```

The main point is that the `destruct n` where `n` comes from the opaque proof is moved from the “main stream” of the definition (where it blocks everything) to only a subproof (where it only blocks the proof part).