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 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 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 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* G. Huet 1-9-95 *)
Require Import PeanoNat Permut Setoid.
Set Implicit Arguments.
Section multiset_defs.
Variable A : Type.
Variable eqA : A -> A -> Prop.
Hypothesis eqA_equiv : Equivalence eqA.
Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
Inductive multiset : Type :=
Bag : (A -> nat) -> multiset.
Definition EmptyBag := Bag (fun a:A => 0).
Definition SingletonBag (a:A) :=
Bag (fun a':A => match Aeq_dec a a' with
| left _ => 1
| right _ => 0
end).
Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a.
(** multiset equality *)
Definition meq (m1 m2:multiset) :=
forall a:A, multiplicity m1 a = multiplicity m2 a.
Lemma meq_refl : forall x:multiset, meq x x.
Proof.
destruct x; unfold meq; reflexivity.
Qed.
Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z.
Proof.
unfold meq.
destruct x; destruct y; destruct z.
intros; rewrite H; auto.
Qed.
Lemma meq_sym : forall x y:multiset, meq x y -> meq y x.
Proof.
unfold meq.
destruct x; destruct y; auto.
Qed.
(** multiset union *)
Definition munion (m1 m2:multiset) :=
Bag (fun a:A => multiplicity m1 a + multiplicity m2 a).
Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x).
Proof.
unfold meq; unfold munion; simpl; auto.
Qed.
Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag).
Proof.
unfold meq; unfold munion; simpl; auto.
Qed.
Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
Proof.
unfold meq; unfold multiplicity; unfold munion.
destruct x; destruct y; intros; apply Nat.add_comm.
Qed.
Lemma munion_ass :
forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)).
Proof.
unfold meq; unfold munion; unfold multiplicity.
destruct x; destruct y; destruct z; intros; symmetry; apply Nat.add_assoc.
Qed.
Lemma meq_left :
forall x y z:multiset, meq x y -> meq (munion x z) (munion y z).
Proof.
unfold meq; unfold munion; unfold multiplicity.
destruct x; destruct y; destruct z.
intros; elim H; reflexivity.
Qed.
Lemma meq_right :
forall x y z:multiset, meq x y -> meq (munion z x) (munion z y).
Proof.
unfold meq; unfold munion; unfold multiplicity.
destruct x; destruct y; destruct z.
intros; elim H; auto.
Qed.
(** Here we should make multiset an abstract datatype, by hiding [Bag],
[munion], [multiplicity]; all further properties are proved abstractly *)
Lemma munion_rotate :
forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)).
Proof.
intros; apply (op_rotate multiset munion meq).
apply munion_comm.
apply munion_ass.
exact meq_trans.
exact meq_sym.
trivial.
Qed.
Lemma meq_congr :
forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t).
Proof.
intros; apply (cong_congr multiset munion meq); auto using meq_left, meq_right.
exact meq_trans.
Qed.
Lemma munion_perm_left :
forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)).
Proof.
intros; apply (perm_left multiset munion meq); auto using munion_comm, munion_ass, meq_left, meq_right, meq_sym.
exact meq_trans.
Qed.
Lemma multiset_twist1 :
forall x y z t:multiset,
meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z).
Proof.
intros; apply (twist multiset munion meq); auto using munion_comm, munion_ass, meq_sym, meq_left, meq_right.
exact meq_trans.
Qed.
Lemma multiset_twist2 :
forall x y z t:multiset,
meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t).
Proof.
intros; apply meq_trans with (munion (munion x (munion y z)) t).
apply meq_sym; apply munion_ass.
apply meq_left; apply munion_perm_left.
Qed.
(** specific for treesort *)
Lemma treesort_twist1 :
forall x y z t u:multiset,
meq u (munion y z) ->
meq (munion x (munion u t)) (munion (munion y (munion x t)) z).
Proof.
intros; apply meq_trans with (munion x (munion (munion y z) t)).
apply meq_right; apply meq_left; trivial.
apply multiset_twist1.
Qed.
Lemma treesort_twist2 :
forall x y z t u:multiset,
meq u (munion y z) ->
meq (munion x (munion u t)) (munion (munion y (munion x z)) t).
Proof.
intros; apply meq_trans with (munion x (munion (munion y z) t)).
apply meq_right; apply meq_left; trivial.
apply multiset_twist2.
Qed.
(** SingletonBag *)
Lemma meq_singleton : forall a a',
eqA a a' -> meq (SingletonBag a) (SingletonBag a').
Proof.
intros; red; simpl; intro a0.
destruct (Aeq_dec a a0) as [Ha|Ha]; rewrite H in Ha;
decide (Aeq_dec a' a0) with Ha; reflexivity.
Qed.
(*i theory of minter to do similarly
(* multiset intersection *)
Definition minter := [m1,m2:multiset]
(Bag [a:A](min (multiplicity m1 a)(multiplicity m2 a))).
i*)
End multiset_defs.
Unset Implicit Arguments.
#[global]
Hint Unfold meq multiplicity: datatypes.
#[global]
Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right
munion_empty_left: datatypes.
#[global]
Hint Immediate meq_sym: datatypes.
(* TODO #14736 for compatibility only, should be removed after deprecation *)
Require Plus.
|