`PartialMap` typeclass에`Map` typeclass를 특화하십시오

Question

Map 및 PartialMap이라는 두 가지 유형의 안경을 정의했으며 이러한 데이터 구조에 대한 명확한 규칙이 있습니다. 특히, 이들은 단지 V 또는 option V을 초과하는지 여부에서만 차이가납니다.

PartialMap은 본질적으로 Map의 특별한 경우입니다. 그러나, 나는 그것을 인코딩하는 방법을 잘 모르겠습니다.

Class Map M K V: Type := { 
    get: M K V -> K -> V; 
    set: M K V -> K -> V -> M K V; 
    map_get_set_idem: forall (m: M K V) (k: K) (v: V), get (set m k v) k = v; 
    map_get_set_comm: forall (m: M K V) (k1 k2: K) (v: V), ~(k1 = k2) -> get (set m k1 v) k2 = get m k2; 
}. 

Class PartialMap M K V: Type := { 
    pget: M K V -> K -> option V; 
    pset: M K V -> K -> option V -> M K V; 
    pmap_pget_pset_idem: forall (m: M K V) (k: K) (v: option V), pget (pset m k v) k = v; 
    pmap_pget_pset_comm: forall (m: M K V) (k1 k2: K) (v: option V), ~(k1 = k2) -> pget (pset m k1 v) k2 = pget m k2; 
}. 

Answer 1

는 K 및 V에 의해 M을 매개 변수화하는 것은 완전히 불필요한 것으로 밝혀졌습니다.

Class Map M K V: Type := { 
    get: M -> K -> V; 
    set: M -> K -> V -> M; 
    map_get_set_idem: forall m k v, get (set m k v) k = v; 
    map_get_set_comm: forall m k1 k2 v, ~(k1 = k2) -> get (set m k1 v) k2 = get m k2; 
}. 

Class PartialMap M K V: Type := { 
    PartialMapIsMap :> Map M K (option V) 
}.