blob: 0a1f65e29846be86b10a744713cd4a5be5ee68f3 (
plain)
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
|
Require Import Coq.omega.Omega.
Require Import Coq.Classes.Morphisms.
Require Import Crypto.Util.ForLoop.
Require Import Crypto.Util.Notations.
Lemma repeat_function_Proper_rel_le {stateT} R f g n
(Hfg : forall c, 0 < c <= n -> forall s1 s2, R s1 s2 -> R (f c s1) (g c s2))
s1 s2 (Hs : R s1 s2)
: R (@repeat_function stateT f n s1) (@repeat_function stateT g n s2).
Proof.
revert s1 s2 Hs.
induction n; simpl; auto.
intros; apply IHn; auto;
intros; apply Hfg; auto;
omega.
Qed.
Global Instance repeat_function_Proper_rel {stateT} R
: Proper (pointwise_relation _ (R ==> R) ==> eq ==> R ==> R) (@repeat_function stateT) | 10.
Proof.
unfold pointwise_relation, respectful.
intros body1 body2 Hbody c y ?; subst y.
induction c; simpl; auto.
Qed.
Lemma repeat_function_Proper_le {stateT} f g n
(Hfg : forall c, 0 < c <= n -> forall st, f c st = g c st)
st
: @repeat_function stateT f n st = @repeat_function stateT g n st.
Proof.
apply repeat_function_Proper_rel_le; try reflexivity; intros; subst; auto.
Qed.
Global Instance repeat_function_Proper {stateT}
: Proper (pointwise_relation _ (pointwise_relation _ eq) ==> eq ==> eq ==> eq) (@repeat_function stateT).
Proof.
intros ???; eapply repeat_function_Proper_rel; repeat intro; subst.
unfold pointwise_relation, respectful in *; auto.
Qed.
About for_loop.
Global Instance for_loop_Proper_rel {stateT} R i0 final step
: Proper (R ==> pointwise_relation _ (R ==> R) ==> R) (@for_loop stateT i0 final step) | 10.
Proof.
intros ?? Hinitial ?? Hbody; revert Hinitial.
unfold for_loop; eapply repeat_function_Proper_rel;
unfold pointwise_relation, respectful in *; auto.
Qed.
Global Instance for_loop_Proper_rel_full {stateT} R
: Proper (eq ==> eq ==> eq ==> R ==> pointwise_relation _ (R ==> R) ==> R) (@for_loop stateT) | 20.
Proof.
intros ?????????; subst; apply for_loop_Proper_rel.
Qed.
Global Instance for_loop_Proper {stateT} i0 final step initial
: Proper (pointwise_relation _ (pointwise_relation _ eq) ==> eq) (@for_loop stateT i0 final step initial).
Proof.
unfold pointwise_relation.
intros ???; eapply for_loop_Proper_rel; try reflexivity; repeat intro; subst; auto.
Qed.
Global Instance for_loop_Proper_full {stateT}
: Proper (eq ==> eq ==> eq ==> eq ==> pointwise_relation _ (pointwise_relation _ eq) ==> eq) (@for_loop stateT) | 5.
Proof.
intros ????????????; subst; apply for_loop_Proper.
Qed.
|
