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
|
From stdpp Require Import prelude fin_maps propset.
Global Instance from_option_proper_test1 `{Equiv A} {B} (R : relation B) (f : A → B) :
Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
Proof. apply _. Qed.
Global Instance from_option_proper_test2 `{Equiv A} {B} (R : relation B) (f : A → B) :
Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
Proof. solve_proper. Qed.
Section map_tests.
Context `{FinMap K M} `{Equiv A}.
(** For higher-order functions on maps (like [map_with_with], [fmap], etc)
we use "higher-order [Proper] instances" [Proper ((≡) ==> (≡)) ==> ...)]
that also allow the function to differ. We test that we can derive simpler
[Proper]s for a fixed function using both type class inference ([apply _])
and std++'s [solve_proper] tactic. *)
Global Instance map_alter_proper_test (f : A → A) i :
Proper ((≡) ==> (≡)) f →
Proper ((≡) ==> (≡)) (alter (M:=M A) f i).
Proof.
apply _.
Restart. Proof.
solve_proper.
Abort.
Global Instance map_zip_proper_test `{Equiv B} :
Proper ((≡@{M A}) ==> (≡@{M B}) ==> (≡@{M (A * B)})) map_zip.
Proof.
apply _.
Restart. Proof.
solve_proper.
Abort.
Global Instance map_zip_with_proper_test `{Equiv B, Equiv C} (f : A → B → C) :
Proper ((≡) ==> (≡) ==> (≡)) f →
Proper ((≡) ==> (≡) ==> (≡)) (map_zip_with (M:=M) f).
Proof.
apply _.
Restart. Proof.
solve_proper.
Abort.
Global Instance map_fmap_proper_test `{Equiv B} (f : A → B) :
Proper ((≡) ==> (≡)) f →
Proper ((≡) ==> (≡@{M _})) (fmap f).
Proof.
apply _.
Restart. Proof.
solve_proper.
Abort.
Global Instance map_omap_proper_test `{Equiv B} (f : A → option B) :
Proper ((≡) ==> (≡)) f →
Proper ((≡) ==> (≡@{M _})) (omap f).
Proof.
apply _.
Restart. Proof.
solve_proper.
Abort.
End map_tests.
(** And similarly for lists *)
Global Instance list_alter_proper_test `{!Equiv A} (f : A → A) i :
Proper ((≡) ==> (≡)) f →
Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
Proof.
apply _.
Restart. Proof.
solve_proper.
Abort.
Global Instance list_fmap_proper_test `{!Equiv A, !Equiv B} (f : A → B) :
Proper ((≡) ==> (≡)) f → Proper ((≡@{list A}) ==> (≡)) (fmap f).
Proof.
apply _.
Restart. Proof.
solve_proper.
Abort.
Global Instance list_bind_proper_test `{!Equiv A, !Equiv B} (f : A → list B) :
Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (mbind f).
Proof.
apply _.
Restart. Proof.
solve_proper.
Abort.
Global Instance mapM_proper_test `{!Equiv A, !Equiv B} (f : A → option B) :
Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (mapM f).
Proof.
apply _.
Restart. Proof.
solve_proper.
Abort.
Lemma test_prod_equivalence (X1 X2 X3 Y : propset nat * propset nat) :
X3 ≡ X2 → X2 ≡ X1 → (X1,Y) ≡ (X3,Y).
Proof. intros H1 H2. by rewrite H1, <-H2. Qed.
|
