collections.v 9.05 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
Require Export base orders.

Section collection.
  Context `{Collection A B}.

  Lemma elem_of_empty_iff x : x    False.
  Proof. split. apply elem_of_empty. easy. Qed.

  Lemma elem_of_union_l x X Y : x  X  x  X  Y.
  Proof. intros. apply elem_of_union. auto. Qed.
  Lemma elem_of_union_r x X Y : x  Y  x  X  Y.
  Proof. intros. apply elem_of_union. auto. Qed.

  Global Instance collection_subseteq: SubsetEq B := λ X Y,  x, x  X  x  Y.
  Global Instance: BoundedJoinSemiLattice B.
  Proof. firstorder. Qed.
  Global Instance: MeetSemiLattice B.
  Proof. firstorder. Qed.

  Lemma elem_of_subseteq X Y : X  Y   x, x  X  x  Y.
  Proof. easy. Qed.
  Lemma elem_of_equiv X Y : X  Y   x, x  X  x  Y.
  Proof. firstorder. Qed.
24 25
  Lemma elem_of_equiv_alt X Y :
    X  Y  ( x, x  X  x  Y)  ( x, x  Y  x  X).
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27 28 29 30
  Proof. firstorder. Qed.

  Global Instance: Proper ((=) ==> () ==> iff) ().
  Proof. intros ???. subst. firstorder. Qed.

31 32 33 34 35
  Lemma empty_ne_singleton x :    {[ x ]}.
  Proof.
    intros [_ E]. destruct (elem_of_empty x).
    apply E. now apply elem_of_singleton.
  Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
36 37 38 39 40
End collection.

Section cmap.
  Context `{Collection A C}.

41 42
  Lemma elem_of_map_1 (f : A  A) (X : C) (x : A) :
    x  X  f x  map f X.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  Proof. intros. apply (elem_of_map _). eauto. Qed.
44 45
  Lemma elem_of_map_1_alt (f : A  A) (X : C) (x : A) y :
    x  X  y = f x  y  map f X.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
  Proof. intros. apply (elem_of_map _). eauto. Qed.
47 48
  Lemma elem_of_map_2 (f : A  A) (X : C) (x : A) :
    x  map f X   y, x = f y  y  X.
Robbert Krebbers's avatar
Robbert Krebbers committed
49 50 51
  Proof. intros. now apply (elem_of_map _). Qed.
End cmap.

52 53
Definition fresh_sig `{FreshSpec A C} (X : C) : { x : A | x  X } :=
  exist ( X) (fresh X) (is_fresh X).
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55 56 57 58 59 60 61 62

Lemma elem_of_fresh_iff `{FreshSpec A C} (X : C) : fresh X  X  False.
Proof. split. apply is_fresh. easy. Qed.

Ltac split_elem_ofs := repeat
  match goal with
  | H : context [ _  _ ] |- _ => setoid_rewrite elem_of_subseteq in H
  | H : context [ _  _ ] |- _ => setoid_rewrite elem_of_equiv_alt in H
  | H : context [ _   ] |- _ => setoid_rewrite elem_of_empty_iff in H
63
  | H : context [ _  {[ _ ]} ] |- _ => setoid_rewrite elem_of_singleton in H
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65 66 67 68 69 70
  | H : context [ _  _  _ ] |- _ => setoid_rewrite elem_of_union in H
  | H : context [ _  _  _ ] |- _ => setoid_rewrite elem_of_intersection in H
  | H : context [ _  _  _ ] |- _ => setoid_rewrite elem_of_difference in H
  | H : context [ _  map _ _ ] |- _ => setoid_rewrite elem_of_map in H
  | |- context [ _  _ ] => setoid_rewrite elem_of_subseteq
  | |- context [ _  _ ] => setoid_rewrite elem_of_equiv_alt
  | |- context [ _   ] => setoid_rewrite elem_of_empty_iff
71
  | |- context [ _  {[ _ ]} ] => setoid_rewrite elem_of_singleton
Robbert Krebbers's avatar
Robbert Krebbers committed
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 97 98 99 100 101 102 103 104 105 106 107
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_union
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_intersection
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_difference
  | |- context [ _  map _ _ ] => setoid_rewrite elem_of_map
  end.

Ltac destruct_elem_ofs := repeat
  match goal with
  | H : context [ @elem_of (_ * _) _ _ ?x _ ] |- _ => is_var x; destruct x
  | H : context [ @elem_of (_ + _) _ _ ?x _] |- _ => is_var x; destruct x
  end.

Tactic Notation "simplify_elem_of" tactic(t) :=
  intros; (* due to bug #2790 *)
  simpl in *;
  split_elem_ofs;
  destruct_elem_ofs;
  intuition (simplify_eqs; t).
Tactic Notation "simplify_elem_of" := simplify_elem_of auto.

Ltac naive_firstorder t :=
  match goal with
  (* intros *)
  | |-  _, _ => intro; naive_firstorder t
  (* destructs without information loss *)
  | H : False |- _ => destruct H
  | H : ?X, Hneg : ¬?X|- _ => now destruct Hneg
  | H : _  _ |- _ => destruct H; naive_firstorder t
  | H :  _, _  |- _ => destruct H; naive_firstorder t
  (* simplification *)
  | |- _ => progress (simplify_eqs; simpl in *); naive_firstorder t
  (* constructs *)
  | |- _  _ => split; naive_firstorder t
  (* solve *)
  | |- _ => solve [t]
  (* dirty destructs *)
108 109 110 111 112 113
  | H : context [  _, _ ] |- _ =>
    edestruct H; clear H;naive_firstorder t || clear H; naive_firstorder t
  | H : context [ _  _ ] |- _ => 
    destruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
  | H : context [ _  _ ] |- _ =>
    edestruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
  (* dirty constructs *)
  | |-  x, _ => eexists; naive_firstorder t
  | |- _  _ => left; naive_firstorder t || right; naive_firstorder t
  | H : _  False |- _ => destruct H; naive_firstorder t
  end.
Tactic Notation "naive_firstorder" tactic(t) :=
  unfold iff, not in *; 
  naive_firstorder t.

Tactic Notation "esimplify_elem_of" tactic(t) := 
  (simplify_elem_of t); 
  try naive_firstorder t.
Tactic Notation "esimplify_elem_of" := esimplify_elem_of (eauto 5).

Section no_dup.
  Context `{Collection A B} (R : relation A) `{!Equivalence R}.

  Definition elem_of_upto (x : A) (X : B) :=  y, y  X  R x y.
  Definition no_dup (X : B) :=  x y, x  X  y  X  R x y  x = y.

  Global Instance: Proper (() ==> iff) (elem_of_upto x).
  Proof. firstorder. Qed.
  Global Instance: Proper (R ==> () ==> iff) elem_of_upto.
  Proof.
    intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
139 140
    * rewrite <-E1, <-E2; intuition.
    * rewrite E1, E2; intuition.
Robbert Krebbers's avatar
Robbert Krebbers committed
141 142 143 144 145 146 147 148
  Qed.
  Global Instance: Proper (() ==> iff) no_dup.
  Proof. firstorder. Qed.

  Lemma elem_of_upto_elem_of x X : x  X  elem_of_upto x X.
  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
  Lemma elem_of_upto_empty x : ¬elem_of_upto x .
  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
149
  Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]}  R x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
150 151
  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.

152 153
  Lemma elem_of_upto_union X Y x :
    elem_of_upto x (X  Y)  elem_of_upto x X  elem_of_upto x Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
154 155 156 157 158 159
  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
  Lemma not_elem_of_upto x X : ¬elem_of_upto x X   y, y  X  ¬R x y.
  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.

  Lemma no_dup_empty: no_dup .
  Proof. unfold no_dup. simplify_elem_of. Qed.
160
  Lemma no_dup_add x X : ¬elem_of_upto x X  no_dup X  no_dup ({[ x ]}  X).
Robbert Krebbers's avatar
Robbert Krebbers committed
161
  Proof. unfold no_dup, elem_of_upto. esimplify_elem_of. Qed.
162 163 164 165 166
  Lemma no_dup_inv_add x X : x  X  no_dup ({[ x ]}  X)  ¬elem_of_upto x X.
  Proof.
    intros Hin Hnodup [y [??]].
    rewrite (Hnodup x y) in Hin; simplify_elem_of.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
167 168 169 170 171 172 173 174 175 176 177 178 179 180
  Lemma no_dup_inv_union_l X Y : no_dup (X  Y)  no_dup X.
  Proof. unfold no_dup. simplify_elem_of. Qed.
  Lemma no_dup_inv_union_r X Y : no_dup (X  Y)  no_dup Y.
  Proof. unfold no_dup. simplify_elem_of. Qed.
End no_dup.

Section quantifiers.
  Context `{Collection A B} (P : A  Prop).

  Definition cforall X :=  x, x  X  P x.
  Definition cexists X :=  x, x  X  P x.

  Lemma cforall_empty : cforall .
  Proof. unfold cforall. simplify_elem_of. Qed.
181
  Lemma cforall_singleton x : cforall {[ x ]}  P x.
Robbert Krebbers's avatar
Robbert Krebbers committed
182 183 184 185 186 187 188 189 190 191
  Proof. unfold cforall. simplify_elem_of. Qed.
  Lemma cforall_union X Y : cforall X  cforall Y  cforall (X  Y).
  Proof. unfold cforall. simplify_elem_of. Qed.
  Lemma cforall_union_inv_1 X Y : cforall (X  Y)  cforall X.
  Proof. unfold cforall. simplify_elem_of. Qed.
  Lemma cforall_union_inv_2 X Y : cforall (X  Y)  cforall Y.
  Proof. unfold cforall. simplify_elem_of. Qed.

  Lemma cexists_empty : ¬cexists .
  Proof. unfold cexists. esimplify_elem_of. Qed.
192
  Lemma cexists_singleton x : cexists {[ x ]}  P x.
Robbert Krebbers's avatar
Robbert Krebbers committed
193 194 195 196 197 198 199 200 201
  Proof. unfold cexists. esimplify_elem_of. Qed.
  Lemma cexists_union_1 X Y : cexists X  cexists (X  Y).
  Proof. unfold cexists. esimplify_elem_of. Qed.
  Lemma cexists_union_2 X Y : cexists Y  cexists (X  Y).
  Proof. unfold cexists. esimplify_elem_of. Qed.
  Lemma cexists_union_inv X Y : cexists (X  Y)  cexists X  cexists Y.
  Proof. unfold cexists. esimplify_elem_of. Qed.
End quantifiers.

202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241
Section more_quantifiers.
  Context `{Collection A B}.
  
  Lemma cforall_weak (P Q : A  Prop) (Hweak :  x, P x  Q x) X :
    cforall P X  cforall Q X.
  Proof. firstorder. Qed.
  Lemma cexists_weak (P Q : A  Prop) (Hweak :  x, P x  Q x) X :
    cexists P X  cexists Q X.
  Proof. firstorder. Qed.
End more_quantifiers.

Section fresh.
  Context `{Collection A C} `{Fresh A C} `{!FreshSpec A C} .

  Fixpoint fresh_list (n : nat) (X : C) : list A :=
    match n with
    | 0 => []
    | S n => let x := fresh X in x :: fresh_list n ({[ x ]}  X)
    end.

  Lemma fresh_list_length n X : length (fresh_list n X) = n.
  Proof. revert X. induction n; simpl; auto. Qed.

  Lemma fresh_list_is_fresh n X x : In x (fresh_list n X)  x  X.
  Proof.
    revert X. induction n; simpl.
    * easy.
    * intros X [?| Hin]. subst.
      + apply is_fresh.
      + apply IHn in Hin. simplify_elem_of.
  Qed.

  Lemma fresh_list_nodup n X : NoDup (fresh_list n X).
  Proof.
    revert X.
    induction n; simpl; constructor; auto.
    intros Hin. apply fresh_list_is_fresh in Hin.
    simplify_elem_of.
  Qed.
End fresh.