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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
From iris.algebra Require Import auth excl lib.gmap_view.
From iris.base_logic.lib Require Import invariants.
From iris.prelude Require Import options.
Section test_dist_equiv_mode.
(* check that the mode for [Dist] does not trigger https://github.com/coq/coq/issues/14441.
From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)
Lemma list_dist_lookup {A : ofe} n (l1 l2 : list A) :
l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
Abort.
(* analogous test for [Equiv] and https://github.com/coq/coq/issues/14441.
From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)
Lemma list_equiv_lookup_ofe {A : ofe} (l1 l2 : list A) :
l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
Abort.
End test_dist_equiv_mode.
(** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs
with carriers that are definitionally equal. See also
https://gitlab.mpi-sws.org/iris/iris/issues/299 *)
Definition tag := nat.
Canonical Structure tagO := leibnizO tag.
Goal tagO = natO.
Proof. reflexivity. Qed.
Global Instance test_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Section tests.
Context `{!invGS_gen hlc Σ}.
Program Definition test : (iPropO Σ -n> iPropO Σ) -n> (iPropO Σ -n> iPropO Σ) :=
λne P v, (▷ (P v))%I.
Solve Obligations with solve_proper.
End tests.
(** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
Really, we want to set [Hint Mode Reflexive] in a way that this fails, but
we cannot [1]. So at least we try to make sure the first solution found
is the right one, to not pay performance in the success case [2].
[1] https://github.com/coq/coq/issues/7916
[2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
*)
Lemma test_setoid_rewrite :
∃ R, @Reflexive Prop R ∧ R = iff.
Proof.
eexists. split.
- apply _.
- reflexivity.
Qed.
(** Regression test for <https://gitlab.mpi-sws.org/iris/iris/issues/255>. *)
Definition testR := authR (prodUR
(prodUR
(optionUR (exclR unitO))
(optionUR (exclR unitO)))
(optionUR (agreeR (boolO)))).
Section test_prod.
Context `{!inG Σ testR}.
Lemma test_prod_persistent γ :
Persistent (PROP:=iPropI Σ) (own γ (◯((None, None), Some (to_agree true)))).
Proof. apply _. Qed.
End test_prod.
(** Make sure the [auth]/[gmap_view] notation does not mix up its arguments. *)
Definition auth_check {A : ucmra} :
auth A = authO A := eq_refl.
Definition gmap_view_check {K : Type} `{Countable K} {V : cmra} :
gmap_view K V = gmap_viewO K V := eq_refl.
Lemma uncurry_ne_test {A B C : ofe} (f : A → B → C) :
NonExpansive2 f → NonExpansive (uncurry f).
Proof. apply _. Qed.
Lemma uncurry3_ne_test {A B C D : ofe} (f : A → B → C → D) :
NonExpansive3 f → NonExpansive (uncurry3 f).
Proof. apply _. Qed.
Lemma uncurry4_ne_test {A B C D E : ofe} (f : A → B → C → D → E) :
NonExpansive4 f → NonExpansive (uncurry4 f).
Proof. apply _. Qed.
Lemma curry_ne_test {A B C : ofe} (f : A * B → C) :
NonExpansive f → NonExpansive2 (curry f).
Proof. apply _. Qed.
Lemma curry3_ne_test {A B C D : ofe} (f : A * B * C → D) :
NonExpansive f → NonExpansive3 (curry3 f).
Proof. apply _. Qed.
Lemma curry4_ne_test {A B C D E : ofe} (f : A * B * C * D → E) :
NonExpansive f → NonExpansive4 (curry4 f).
Proof. apply _. Qed.
(** Regression test for https://gitlab.mpi-sws.org/iris/iris/-/issues/577 *)
Lemma list_bind_ne_test {A B : ofe} (f : A → list B) :
NonExpansive f → NonExpansive (mbind f : list A → list B).
Proof. apply _. Qed.
|
