Extras.v 5.25 KB
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
2
(* This file implements various helper functions and proofs *)

3
From Coq Require Import ZArith.
4
From Coq Require Import List.
5
6
7
8
9
From Coq Require Import Permutation.
From Coq Require Import Morphisms.
From Coq Require Import Psatz.
From Coq Require Import Eqdep_dec.
From SmartContracts Require Import Automation.
10
11
12
13
14
15
16
17
18
19
20
Import ListNotations.

Fixpoint find_first {A B : Type} (f : A -> option B) (l : list A)
  : option B :=
  match l with
  | hd :: tl => match f hd with
                | Some b => Some b
                | None => find_first f tl
                end
  | [] => None
  end.
21
22
23
24
25
26
27
28
29
30

Fixpoint map_option {A B : Type} (f : A -> option B) (l : list A)
  : list B :=
  match l with
  | hd :: tl => match f hd with
                  | Some b => b :: map_option f tl
                  | None => map_option f tl
                end
  | [] => []
  end.
31
32
33
34
35
36
37

Definition with_default {A : Type} (a : A) (o : option A) : A :=
  match o with
  | Some v => v
  | None => a
  end.

38
39
40
41
42
43
44
45
46
Definition unpack_option {A : Type} (a : option A) :=
  match a return match a with
                  | Some _ => A
                  | None => unit
                  end with
  | Some x => x
  | None => tt
  end.

47
48
49
50
51
52
Fixpoint sumZ {A : Type} (f : A -> Z) (xs : list A) : Z :=
  match xs with
  | [] => 0
  | x :: xs' => f x + sumZ f xs'
  end.

53
54
55
56
57
58
59
60
61
62
63
64
Fixpoint sumnat {A : Type} (f : A -> nat) (xs : list A) : nat :=
  match xs with
  | [] => 0
  | x :: xs' => f x + sumnat f xs'
  end.

Lemma sumnat_app
      {A : Type} {f : A -> nat} {xs ys : list A} :
  sumnat f (xs ++ ys) = sumnat f xs + sumnat f ys.
Proof.
  revert ys.
  induction xs as [| x xs IH]; intros ys; auto.
65
  cbn.
66
67
68
69
70
71
72
73
74
75
  rewrite IH.
  lia.
Qed.

Lemma sumnat_permutation
      {A : Type} {f : A -> nat} {xs ys : list A}
      (perm_eq : Permutation xs ys) :
  sumnat f xs = sumnat f ys.
Proof. induction perm_eq; perm_simplify; lia. Qed.

76
77
78
Instance sumnat_perm_proper {A : Type} :
  Proper (eq ==> Permutation (A:=A) ==> eq) sumnat.
Proof. repeat intro. subst. now apply sumnat_permutation. Qed.
79

80
81
82
83
Lemma sumZ_permutation
      {A : Type} {f : A -> Z} {xs ys : list A}
      (perm_eq : Permutation xs ys) :
  sumZ f xs = sumZ f ys.
84
Proof. induction perm_eq; perm_simplify; lia. Qed.
85

86
87
88
Instance sumZ_perm_proper {A : Type} :
  Proper (eq ==> Permutation (A:=A) ==> eq) sumZ.
Proof. repeat intro. subst. now apply sumZ_permutation. Qed.
89
90
91
92
93
94
95
96

Local Open Scope Z.
Lemma sumZ_app
      {A : Type} {f : A -> Z} {xs ys : list A} :
  sumZ f (xs ++ ys) = sumZ f xs + sumZ f ys.
Proof.
  revert ys.
  induction xs as [| x xs IH]; intros ys; auto.
97
  cbn.
98
99
100
101
102
103
104
105
106
107
108
109
  rewrite IH.
  lia.
Qed.

Lemma in_app_cons_or {A : Type} (x y : A) (xs ys : list A) :
  x <> y ->
  In x (xs ++ y :: ys) ->
  In x (xs ++ ys).
Proof.
  intros x_neq_y x_in.
  apply in_or_app.
  apply in_app_or in x_in.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
110
111
  destruct x_in as [?|x_in]; auto.
  destruct x_in; auto; congruence.
112
113
114
115
Qed.

Lemma incl_split {A : Type} (l m n : list A) :
  incl (l ++ m) n -> incl l n /\ incl m n.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
116
117
118
119
120
121
Proof.
  intros H.
  unfold incl in *.
  Hint Resolve in_or_app : core.
  auto.
Qed.
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144

Lemma NoDup_incl_reorganize
      {A : Type}
      (l l' : list A) :
  NoDup l' ->
  incl l' l ->
  exists suf, Permutation (l' ++ suf) l.
Proof.
  revert l.
  induction l' as [| x xs IH]; intros l nodup_l' incl_l'_l.
  - exists l. apply Permutation_refl.
  - assert (x_in_l: In x l).
    + apply (incl_l'_l x). left. constructor.
    + destruct (in_split _ _ x_in_l) as [pref [suf eq]]; subst.
      inversion nodup_l'; subst.
      assert (incl xs (pref ++ suf)).
      * intros a a_in.
        apply in_or_app.
        apply (incl_split [x] xs _) in incl_l'_l.
        destruct incl_l'_l as [incl_x incl_xs].
        intuition.
        specialize (incl_xs a a_in).
        apply in_app_or in incl_xs.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
145
146
        destruct incl_xs as [in_pref | [in_x | in_suf]]; auto.
        congruence.
147
148
      * destruct (IH _ H2 H) as [suf' perm_suf'].
        exists suf'.
149
        perm_simplify.
150
151
152
153
154
155
156
Qed.

Lemma in_NoDup_app {A : Type} (x : A) (l m : list A) :
  In x l -> NoDup (l ++ m) -> ~In x m.
Proof.
  intros in_x_l nodup_l_app_m in_x_m.
  destruct (in_split _ _ in_x_l) as [l1 [l2 eq]]; subst.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
157
158
159
160
161
162
163
  replace ((l1 ++ x :: l2) ++ m) with (l1 ++ x :: (l2 ++ m)) in nodup_l_app_m.
  - apply (NoDup_remove_2 _ _ _) in nodup_l_app_m.
    rewrite app_assoc in nodup_l_app_m.
    auto.
  - rewrite app_comm_cons.
    appify.
    now rewrite app_assoc.
164
165
166
167
168
169
170
171
Qed.

Lemma seq_app start len1 len2 :
  seq start (len1 + len2) = seq start len1 ++ seq (start + len1) len2.
Proof.
  revert start.
  induction len1 as [| len1 IH]; intros start.
  - now rewrite Nat.add_0_r.
172
  - cbn.
173
174
175
176
177
178
179
180
181
182
183
    rewrite IH.
    f_equal; f_equal; f_equal.
    lia.
Qed.

Lemma sumZ_seq_S f start len :
  sumZ f (seq start (S len)) = sumZ f (seq start len) + f (start + len)%nat.
Proof.
  replace (S len) with (len + 1)%nat by lia.
  rewrite (seq_app start len 1).
  rewrite sumZ_app.
184
  cbn.
185
186
  lia.
Qed.
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205

Lemma forall_respects_permutation {A} (xs ys : list A) P :
  Permutation xs ys -> Forall P xs -> Forall P ys.
Proof.
  intros perm all.
  apply Forall_forall.
  intros y y_in.
  pose proof (proj1 (Forall_forall P xs) all).
  apply H.
  apply Permutation_in with ys; symmetry in perm; auto.
Qed.

Instance Forall_Permutation_proper {A} :
  Proper (eq ==> @Permutation A ==> iff) (@Forall A).
Proof.
  intros f f' ? xs ys perm.
  subst f'.
  split; apply forall_respects_permutation; auto; symmetry; auto.
Qed.