File: bug_18126.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (33 lines) | stat: -rw-r--r-- 1,105 bytes parent folder | download | duplicates (2)
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.