2
$\begingroup$

Consider the following definition of a record R, parametrized over an arbitrary eqType:

From mathcomp Require Import ssreflect ssrbool ssrnat eqtype.
From Coq Require Import DecidableType DecidableTypeEx FMapWeakList.


Record R {s : eqType}  := mkR {
    a : nat;
    b : s
}.

Now, I want to use R as a UsualDecidableType to index weak maps. Following examples here, a create a module R_as_DT:

Module R_as_DT <: UsualDecidableType.

    Parameter s : eqType.

    Definition t := @R s.
    Definition eq := @Logic.eq t.
    Definition eq_refl := @Logic.eq_refl t.
    Definition eq_sym := @Logic.eq_sym t.
    Definition eq_trans := @Logic.eq_trans t.

    Definition eq_dec : forall (x y : t), {eq x y} + {~ eq x y}.
        intros x y.
        destruct (x.(a) == y.(a)) eqn:Ha.
        2 : { 
            right; unfold eq; destruct x,y; cbv; intro H; inversion H.
            simpl in Ha; rewrite H1 in Ha; contradict Ha.
            apply Bool.not_false_iff_true; apply /eqP; reflexivity.
        }
        destruct (x.(b) == y.(b)) eqn:Hb.
        2 : { 
            right; unfold eq; destruct x,y; cbv; intro H; inversion H.
            simpl in Hb; rewrite H2 in Hb; contradict Hb.
            apply Bool.not_false_iff_true; apply /eqP; reflexivity.
        }
        destruct x,y; left; simpl in Ha,Hb; 
        move: Ha => /eqP Ha; move: Hb => /eqP Hb; subst.
        reflexivity.
    Defined.
    
End R_as_DT.

Then, I import the FMapWeakList module passing R_as_DT as parameter.

Module Import RMap := FMapWeakList.Make(R_as_DT).

Problem is that now, Coq does not understand that R is the same as key.

Definition R1 : R := mkR nat_eqType 0 0.

Fail Definition test := RMap.add R1 2.

Do I need to somehow specify explicitely that parameter s of module R_as_DT is instantiated with nat_eqType ? The problem does not happen if R does not contain a type parameter.

$\endgroup$

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.