What I'm doing wrong? Smth not computing

Using Rocq
1 
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. :expressionless:

2

As you can see it blocks on NoDup_cons_iff which is opaque.
You can change your definition to avoid this:

-  + 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).

1 Like