1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
From Coq Require Export Morphisms Setoid Utf8.
Class Empty A := empty : A.
Class MapFold K A M := map_fold B : (K → A → B → B) → B → M → B.
Global Arguments map_fold {_ _ _ _ _}.
Class FinMap K M `{∀ A, Empty (M A), ∀ A, MapFold K A (M A)} := { }.
Definition map_filter {K A M} `{MapFold K A M, Empty M} (P : A → Prop) : M → M :=
map_fold (λ k v m, m) empty.
Global Instance map_filter_proper {K A M} `{FinMap K M} (P : A → Prop) :
Proper (@eq (M A) ==> eq) (map_filter P).
Proof. Admitted.
#[projections(primitive=yes)]
Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
Global Arguments unseal {_ _}.
Record ofe := { ofe_car :> Type }.
Definition iProto (Σ V : Type) : ofe. Admitted.
Definition iProto_dual_def {Σ V} (p : iProto Σ V) : iProto Σ V := p.
Definition iProto_dual_aux : seal (@iProto_dual_def). Proof. eexists. reflexivity. Qed.
Definition iProto_dual : ∀ {Σ V}, iProto Σ V → iProto Σ V := iProto_dual_aux.(unseal).
Lemma test {Σ V} (p q q' : iProto Σ V) (Hq : q = q') :
iProto_dual q = p.
Proof.
setoid_rewrite Hq.
Abort.
|
