summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-03-12 10:10:19 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-03-12 10:10:19 +0000
commit644bd3cfc92fa0ddded80566b25b8a11957f6edf (patch)
treeb393e62ca40e3c8632f95270caec96ce2b7f3ee2
parent45fc4cc348d2b8c4cc151a5e3ce3483f21a6ef78 (diff)
Maps: revised TREE interface; added mucho derived properties and operations in Tree_Properties.
Lattice: adapted accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2147 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--lib/Lattice.v12
-rw-r--r--lib/Maps.v307
2 files changed, 256 insertions, 63 deletions
diff --git a/lib/Lattice.v b/lib/Lattice.v
index fd05b34..c4b55e9 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -141,11 +141,15 @@ Lemma beq_correct: forall x y, beq x y = true -> eq x y.
Proof.
destruct x; destruct y; simpl; intro; try congruence.
red; intro; simpl.
- generalize (PTree.beq_correct L.eq L.beq L.beq_correct t0 t1 H p).
- destruct (t0!p); destruct (t1!p); intuition. apply L.eq_refl.
+ rewrite PTree.beq_correct in H. generalize (H p).
+ destruct (t0!p); destruct (t1!p); intuition.
+ apply L.beq_correct; auto.
+ apply L.eq_refl.
red; intro; simpl.
- generalize (PTree.beq_correct L.eq L.beq L.beq_correct t0 t1 H p).
- destruct (t0!p); destruct (t1!p); intuition. apply L.eq_refl.
+ rewrite PTree.beq_correct in H. generalize (H p).
+ destruct (t0!p); destruct (t1!p); intuition.
+ apply L.beq_correct; auto.
+ apply L.eq_refl.
Qed.
Definition ge (x y: t) : Prop :=
diff --git a/lib/Maps.v b/lib/Maps.v
index 82888d5..9aa59d0 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -32,6 +32,7 @@
inefficient implementation of maps as functions is also provided.
*)
+Require Import Equivalence EquivDec.
Require Import Coqlib.
(* To avoid useless definitions of inductors in extracted code. *)
@@ -83,15 +84,14 @@ Module Type TREE.
(** Extensional equality between trees. *)
Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool.
Hypothesis beq_correct:
- forall (A: Type) (P: A -> A -> Prop) (cmp: A -> A -> bool),
- (forall (x y: A), cmp x y = true -> P x y) ->
- forall (t1 t2: t A), beq cmp t1 t2 = true ->
- forall (x: elt),
- match get x t1, get x t2 with
- | None, None => True
- | Some y1, Some y2 => P y1 y2
- | _, _ => False
- end.
+ forall (A: Type) (eqA: A -> A -> bool) (t1 t2: t A),
+ beq eqA t1 t2 = true <->
+ (forall (x: elt),
+ match get x t1, get x t2 with
+ | None, None => True
+ | Some y1, Some y2 => eqA y1 y2 = true
+ | _, _ => False
+ end).
(** Applying a function to all data of a tree. *)
Variable map:
@@ -107,24 +107,16 @@ Module Type TREE.
forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
get i (map1 f m) = option_map f (get i m).
- (** Filtering data that match a given predicate. *)
- Variable filter1:
- forall (A: Type), (A -> bool) -> t A -> t A.
- Hypothesis gfilter1:
- forall (A: Type) (pred: A -> bool) (i: elt) (m: t A),
- get i (filter1 pred m) =
- match get i m with None => None | Some x => if pred x then Some x else None end.
-
(** Applying a function pairwise to all data of two trees. *)
Variable combine:
- forall (A: Type), (option A -> option A -> option A) -> t A -> t A -> t A.
+ forall (A B C: Type), (option A -> option B -> option C) -> t A -> t B -> t C.
Hypothesis gcombine:
- forall (A: Type) (f: option A -> option A -> option A),
+ forall (A B C: Type) (f: option A -> option B -> option C),
f None None = None ->
- forall (m1 m2: t A) (i: elt),
+ forall (m1: t A) (m2: t B) (i: elt),
get i (combine f m1 m2) = f (get i m1) (get i m2).
Hypothesis combine_commut:
- forall (A: Type) (f g: option A -> option A -> option A),
+ forall (A B: Type) (f g: option A -> option A -> option B),
(forall (i j: option A), f i j = g j i) ->
forall (m1 m2: t A),
combine f m1 m2 = combine g m2 m1.
@@ -359,10 +351,9 @@ Module PTree <: TREE.
intros. destruct (elt_eq i j). subst j. apply grs. apply gro; auto.
Qed.
- Section EXTENSIONAL_EQUALITY.
+ Section BOOLEAN_EQUALITY.
Variable A: Type.
- Variable eqA: A -> A -> Prop.
Variable beqA: A -> A -> bool.
Fixpoint bempty (m: t A) : bool :=
@@ -405,20 +396,19 @@ Module PTree <: TREE.
intros; apply (H (xO x)).
Qed.
- Hypothesis beqA_correct: forall x y, beqA x y = true -> eqA x y.
-
- Definition exteq (m1 m2: t A) : Prop :=
- forall (x: elt),
- match get x m1, get x m2 with
- | None, None => True
- | Some y1, Some y2 => eqA y1 y2
- | _, _ => False
- end.
-
Lemma beq_correct:
- forall m1 m2, beq m1 m2 = true -> exteq m1 m2.
+ forall m1 m2,
+ beq m1 m2 = true <->
+ (forall (x: elt),
+ match get x m1, get x m2 with
+ | None, None => True
+ | Some y1, Some y2 => beqA y1 y2 = true
+ | _, _ => False
+ end).
Proof.
- induction m1; destruct m2; simpl.
+ intros; split.
+ - (* beq = true -> exteq *)
+ revert m1 m2. induction m1; destruct m2; simpl.
intros; red; intros. change (@Leaf A) with (empty A).
repeat rewrite gempty. auto.
destruct o; intro. congruence.
@@ -429,21 +419,14 @@ Module PTree <: TREE.
rewrite bempty_correct. auto. assumption.
destruct o; destruct o0; simpl; intro; try congruence.
destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0).
- red; intros. destruct x; simpl.
- apply IHm1_2; auto. apply IHm1_1; auto.
- apply beqA_correct; auto.
+ destruct x; simpl.
+ apply IHm1_2; auto. apply IHm1_1; auto. auto.
destruct (andb_prop _ _ H).
red; intros. destruct x; simpl.
apply IHm1_2; auto. apply IHm1_1; auto.
auto.
- Qed.
-
- Hypothesis beqA_complete: forall x y, eqA x y -> beqA x y = true.
-
- Lemma beq_complete:
- forall m1 m2, exteq m1 m2 -> beq m1 m2 = true.
- Proof.
- induction m1; destruct m2; simpl; intros.
+ - (* exteq -> beq = true *)
+ revert m1 m2. induction m1; destruct m2; simpl; intros.
auto.
change (bempty (Node m2_1 o m2_2) = true).
apply bempty_complete. intros. generalize (H x). rewrite gleaf.
@@ -453,11 +436,11 @@ Module PTree <: TREE.
destruct (get x (Node m1_1 o m1_2)); tauto.
apply andb_true_intro. split. apply andb_true_intro. split.
generalize (H xH); simpl. destruct o; destruct o0; auto.
- apply IHm1_1. red; intros. apply (H (xO x)).
- apply IHm1_2. red; intros. apply (H (xI x)).
+ apply IHm1_1. intros. apply (H (xO x)).
+ apply IHm1_2. intros. apply (H (xI x)).
Qed.
- End EXTENSIONAL_EQUALITY.
+ End BOOLEAN_EQUALITY.
Fixpoint append (i j : positive) {struct i} : positive :=
match i with
@@ -576,11 +559,11 @@ Module PTree <: TREE.
Section COMBINE.
- Variable A: Type.
- Variable f: option A -> option A -> option A.
+ Variable A B C: Type.
+ Variable f: option A -> option B -> option C.
Hypothesis f_none_none: f None None = None.
- Fixpoint xcombine_l (m : t A) {struct m} : t A :=
+ Fixpoint xcombine_l (m : t A) {struct m} : t C :=
match m with
| Leaf => Leaf
| Node l o r => Node' (xcombine_l l) (f o None) (xcombine_l r)
@@ -595,14 +578,14 @@ Module PTree <: TREE.
rewrite gnode'. destruct i; simpl; auto.
Qed.
- Fixpoint xcombine_r (m : t A) {struct m} : t A :=
+ Fixpoint xcombine_r (m : t B) {struct m} : t C :=
match m with
| Leaf => Leaf
| Node l o r => Node' (xcombine_r l) (f None o) (xcombine_r r)
end.
Lemma xgcombine_r :
- forall (m: t A) (i : positive),
+ forall (m: t B) (i : positive),
get i (xcombine_r m) = f None (get i m).
Proof.
induction m; intros; simpl.
@@ -610,7 +593,7 @@ Module PTree <: TREE.
rewrite gnode'. destruct i; simpl; auto.
Qed.
- Fixpoint combine (m1 m2 : t A) {struct m1} : t A :=
+ Fixpoint combine (m1: t A) (m2: t B) {struct m1} : t C :=
match m1 with
| Leaf => xcombine_r m2
| Node l1 o1 r1 =>
@@ -621,7 +604,7 @@ Module PTree <: TREE.
end.
Theorem gcombine:
- forall (m1 m2: t A) (i: positive),
+ forall (m1: t A) (m2: t B) (i: positive),
get i (combine m1 m2) = f (get i m1) (get i m2).
Proof.
induction m1; intros; simpl.
@@ -634,7 +617,7 @@ Module PTree <: TREE.
End COMBINE.
Lemma xcombine_lr :
- forall (A : Type) (f g : option A -> option A -> option A) (m : t A),
+ forall (A B: Type) (f g : option A -> option A -> option B) (m : t A),
(forall (i j : option A), f i j = g j i) ->
xcombine_l f m = xcombine_r g m.
Proof.
@@ -645,12 +628,12 @@ Module PTree <: TREE.
Qed.
Theorem combine_commut:
- forall (A: Type) (f g: option A -> option A -> option A),
+ forall (A B: Type) (f g: option A -> option A -> option B),
(forall (i j: option A), f i j = g j i) ->
forall (m1 m2: t A),
combine f m1 m2 = combine g m2 m1.
Proof.
- intros A f g EQ1.
+ intros A B f g EQ1.
assert (EQ2: forall (i j: option A), g i j = f j i).
intros; auto.
induction m1; intros; destruct m2; simpl;
@@ -1499,6 +1482,212 @@ Qed.
End MEASURE.
+(** Forall and exists *)
+
+Section FORALL_EXISTS.
+
+Variable A: Type.
+
+Definition for_all (m: T.t A) (f: T.elt -> A -> bool) : bool :=
+ T.fold (fun b x a => b && f x a) m true.
+
+Lemma for_all_correct:
+ forall m f,
+ for_all m f = true <-> (forall x a, T.get x m = Some a -> f x a = true).
+Proof.
+ intros m0 f.
+ unfold for_all. apply fold_rec; intros.
+- (* Extensionality *)
+ rewrite H0. split; intros. rewrite <- H in H2; auto. rewrite H in H2; auto.
+- (* Base case *)
+ split; intros. rewrite T.gempty in H0; congruence. auto.
+- (* Inductive case *)
+ split; intros.
+ destruct (andb_prop _ _ H2). rewrite T.gsspec in H3. destruct (T.elt_eq x k).
+ inv H3. auto.
+ apply H1; auto.
+ apply andb_true_intro. split.
+ rewrite H1. intros. apply H2. rewrite T.gso; auto. congruence.
+ apply H2. apply T.gss.
+Qed.
+
+Definition exists_ (m: T.t A) (f: T.elt -> A -> bool) : bool :=
+ T.fold (fun b x a => b || f x a) m false.
+
+Lemma exists_correct:
+ forall m f,
+ exists_ m f = true <-> (exists x a, T.get x m = Some a /\ f x a = true).
+Proof.
+ intros m0 f.
+ unfold exists_. apply fold_rec; intros.
+- (* Extensionality *)
+ rewrite H0. split; intros (x0 & a0 & P & Q); exists x0; exists a0; split; auto; congruence.
+- (* Base case *)
+ split; intros. congruence. destruct H as (x & a & P & Q). rewrite T.gempty in P; congruence.
+- (* Inductive case *)
+ split; intros.
+ destruct (orb_true_elim _ _ H2).
+ rewrite H1 in e. destruct e as (x1 & a1 & P & Q).
+ exists x1; exists a1; split; auto. rewrite T.gso; auto. congruence.
+ exists k; exists v; split; auto. apply T.gss.
+ destruct H2 as (x1 & a1 & P & Q). apply orb_true_intro.
+ rewrite T.gsspec in P. destruct (T.elt_eq x1 k).
+ inv P. right; auto.
+ left. apply H1. exists x1; exists a1; auto.
+Qed.
+
+Remark exists_for_all:
+ forall m f,
+ exists_ m f = negb (for_all m (fun x a => negb (f x a))).
+Proof.
+ intros. unfold exists_, for_all. rewrite ! T.fold_spec.
+ change false with (negb true). generalize (T.elements m) true.
+ induction l; simpl; intros.
+ auto.
+ rewrite <- IHl. f_equal.
+ destruct b; destruct (f (fst a) (snd a)); reflexivity.
+Qed.
+
+Remark for_all_exists:
+ forall m f,
+ for_all m f = negb (exists_ m (fun x a => negb (f x a))).
+Proof.
+ intros. unfold exists_, for_all. rewrite ! T.fold_spec.
+ change true with (negb false). generalize (T.elements m) false.
+ induction l; simpl; intros.
+ auto.
+ rewrite <- IHl. f_equal.
+ destruct b; destruct (f (fst a) (snd a)); reflexivity.
+Qed.
+
+Lemma for_all_false:
+ forall m f,
+ for_all m f = false <-> (exists x a, T.get x m = Some a /\ f x a = false).
+Proof.
+ intros. rewrite for_all_exists.
+ rewrite negb_false_iff. rewrite exists_correct.
+ split; intros (x & a & P & Q); exists x; exists a; split; auto.
+ rewrite negb_true_iff in Q. auto.
+ rewrite Q; auto.
+Qed.
+
+Lemma exists_false:
+ forall m f,
+ exists_ m f = false <-> (forall x a, T.get x m = Some a -> f x a = false).
+Proof.
+ intros. rewrite exists_for_all.
+ rewrite negb_false_iff. rewrite for_all_correct.
+ split; intros. apply H in H0. rewrite negb_true_iff in H0. auto. rewrite H; auto.
+Qed.
+
+End FORALL_EXISTS.
+
+(** More about [beq] *)
+
+Section BOOLEAN_EQUALITY.
+
+Variable A: Type.
+Variable beqA: A -> A -> bool.
+
+Theorem beq_false:
+ forall m1 m2,
+ T.beq beqA m1 m2 = false <->
+ exists x, match T.get x m1, T.get x m2 with
+ | None, None => False
+ | Some a1, Some a2 => beqA a1 a2 = false
+ | _, _ => True
+ end.
+Proof.
+ intros; split; intros.
+- (* beq = false -> existence *)
+ set (p1 := fun x a1 => match T.get x m2 with None => false | Some a2 => beqA a1 a2 end).
+ set (p2 := fun x a2 => match T.get x m1 with None => false | Some a1 => beqA a1 a2 end).
+ destruct (for_all m1 p1) eqn:F1; [destruct (for_all m2 p2) eqn:F2 | idtac].
+ + cut (T.beq beqA m1 m2 = true). congruence.
+ rewrite for_all_correct in *. rewrite T.beq_correct; intros.
+ destruct (T.get x m1) as [a1|] eqn:X1.
+ generalize (F1 _ _ X1). unfold p1. destruct (T.get x m2); congruence.
+ destruct (T.get x m2) as [a2|] eqn:X2; auto.
+ generalize (F2 _ _ X2). unfold p2. rewrite X1. congruence.
+ + rewrite for_all_false in F2. destruct F2 as (x & a & P & Q).
+ exists x. rewrite P. unfold p2 in Q. destruct (T.get x m1); auto.
+ + rewrite for_all_false in F1. destruct F1 as (x & a & P & Q).
+ exists x. rewrite P. unfold p1 in Q. destruct (T.get x m2); auto.
+- (* existence -> beq = false *)
+ destruct H as [x P].
+ destruct (T.beq beqA m1 m2) eqn:E; auto.
+ rewrite T.beq_correct in E.
+ generalize (E x). destruct (T.get x m1); destruct (T.get x m2); tauto || congruence.
+Qed.
+
+End BOOLEAN_EQUALITY.
+
+(** Extensional equality between trees *)
+
+Section EXTENSIONAL_EQUALITY.
+
+Variable A: Type.
+Variable eqA: A -> A -> Prop.
+Hypothesis eqAeq: Equivalence eqA.
+
+Definition Equal (m1 m2: T.t A) : Prop :=
+ forall x, match T.get x m1, T.get x m2 with
+ | None, None => True
+ | Some a1, Some a2 => a1 === a2
+ | _, _ => False
+ end.
+
+Lemma Equal_refl: forall m, Equal m m.
+Proof.
+ intros; red; intros. destruct (T.get x m); auto. reflexivity.
+Qed.
+
+Lemma Equal_sym: forall m1 m2, Equal m1 m2 -> Equal m2 m1.
+Proof.
+ intros; red; intros. generalize (H x). destruct (T.get x m1); destruct (T.get x m2); auto. intros; symmetry; auto.
+Qed.
+
+Lemma Equal_trans: forall m1 m2 m3, Equal m1 m2 -> Equal m2 m3 -> Equal m1 m3.
+Proof.
+ intros; red; intros. generalize (H x) (H0 x).
+ destruct (T.get x m1); destruct (T.get x m2); try tauto;
+ destruct (T.get x m3); try tauto.
+ intros. transitivity a0; auto.
+Qed.
+
+Instance Equal_Equivalence : Equivalence Equal := {
+ Equivalence_Reflexive := Equal_refl;
+ Equivalence_Symmetric := Equal_sym;
+ Equivalence_Transitive := Equal_trans
+}.
+
+Hypothesis eqAdec: EqDec A eqA.
+
+Program Definition Equal_dec (m1 m2: T.t A) : { m1 === m2 } + { m1 =/= m2 } :=
+ match T.beq (fun a1 a2 => proj_sumbool (a1 == a2)) m1 m2 with
+ | true => left _
+ | false => right _
+ end.
+Next Obligation.
+ rename Heq_anonymous into B.
+ symmetry in B. rewrite T.beq_correct in B.
+ red; intros. generalize (B x).
+ destruct (T.get x m1); destruct (T.get x m2); auto.
+ intros. eapply proj_sumbool_true; eauto.
+Qed.
+Next Obligation.
+ assert (T.beq (fun a1 a2 => proj_sumbool (a1 == a2)) m1 m2 = true).
+ apply T.beq_correct; intros.
+ generalize (H x).
+ destruct (T.get x m1); destruct (T.get x m2); try tauto.
+ intros. apply proj_sumbool_is_true; auto.
+ unfold equiv, complement in H0. congruence.
+Qed.
+
+Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec.
+
+End EXTENSIONAL_EQUALITY.
+
End Tree_Properties.
Module PTree_Properties := Tree_Properties(PTree).