Added 'going wrong' behaviors

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 120 insertions, 0 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 9e2199c..416afa9 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -781,6 +781,11 @@ Proof.
   right; red; intros. elim n0. eapply list_disjoint_cons_left; eauto.
 Defined.
 
+(** [list_equiv l1 l2] holds iff the lists [l1] and [l2] contain the same elements. *)
+
+Definition list_equiv (A : Type) (l1 l2: list A) : Prop :=
+  forall x, In x l1 <-> In x l2.
+
 (** [list_norepet l] holds iff the list [l] contains no repetitions,
   i.e. no element occurs twice. *)
 
diff --git a/lib/Maps.v b/lib/Maps.v
index a277e67..766168a 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -74,6 +74,9 @@ Module Type TREE.
   Hypothesis gro:
     forall (A: Type) (i j: elt) (m: t A),
     i <> j -> get i (remove j m) = get i m.
+  Hypothesis grspec:
+    forall (A: Type) (i j: elt) (m: t A),
+    get i (remove j m) = if elt_eq i j then None else get i m.
 
   (** Extensional equality between trees. *)
   Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool.
@@ -333,6 +336,13 @@ Module PTree <: TREE.
         auto.
   Qed.
 
+  Theorem grspec:
+    forall (A: Type) (i j: elt) (m: t A),
+    get i (remove j m) = if elt_eq i j then None else get i m.
+  Proof.
+    intros. destruct (elt_eq i j). subst j. apply grs. apply gro; auto.
+  Qed.
+
   Section EXTENSIONAL_EQUALITY.
 
     Variable A: Type.
@@ -1127,6 +1137,111 @@ Module EMap(X: EQUALITY_TYPE) <: MAP.
   Qed.
 End EMap.
 
+(** * Additional properties over trees *)
+
+Module Tree_Properties(T: TREE).
+
+(** An induction principle over [fold]. *)
+
+Section TREE_FOLD_IND.
+
+Variables V A: Type.
+Variable f: A -> T.elt -> V -> A.
+Variable P: T.t V -> A -> Prop.
+Variable init: A.
+Variable m_final: T.t V.
+
+Hypothesis P_compat:
+  forall m m' a,
+  (forall x, T.get x m = T.get x m') ->
+  P m a -> P m' a.
+
+Hypothesis H_base: 
+  P (T.empty _) init.
+
+Hypothesis H_rec:
+  forall m a k v,
+  T.get k m = None -> T.get k m_final = Some v -> P m a -> P (T.set k v m) (f a k v).
+
+Definition f' (a: A) (p : T.elt * V) := f a (fst p) (snd p).
+
+Definition P' (l: list (T.elt * V)) (a: A) : Prop :=
+  forall m, list_equiv l (T.elements m) -> P m a.
+
+Remark H_base':
+  P' nil init.
+Proof.
+  red; intros. apply P_compat with (T.empty _); auto.
+  intros. rewrite T.gempty. symmetry. case_eq (T.get x m); intros; auto.
+  assert (In (x, v) nil). rewrite (H (x, v)). apply T.elements_correct. auto.
+  contradiction.
+Qed.
+
+Remark H_rec':
+  forall k v l a,
+  ~In k (List.map (@fst T.elt V) l) ->
+  In (k, v) (T.elements m_final) ->
+  P' l a ->
+  P' (l ++ (k, v) :: nil) (f a k v).
+Proof.
+  unfold P'; intros.  
+  set (m0 := T.remove k m). 
+  apply P_compat with (T.set k v m0).
+    intros. unfold m0. rewrite T.gsspec. destruct (T.elt_eq x k).
+    symmetry. apply T.elements_complete. rewrite <- (H2 (x, v)).
+    apply in_or_app. simpl. intuition congruence.
+    apply T.gro. auto.
+  apply H_rec. unfold m0. apply T.grs. apply T.elements_complete. auto. 
+  apply H1. red. intros [k' v']. 
+  split; intros. 
+  apply T.elements_correct. unfold m0. rewrite T.gro. apply T.elements_complete. 
+  rewrite <- (H2 (k', v')). apply in_or_app. auto. 
+  red; intro; subst k'. elim H. change k with (fst (k, v')). apply in_map. auto.
+  assert (T.get k' m0 = Some v'). apply T.elements_complete. auto.
+  unfold m0 in H4. rewrite T.grspec in H4. destruct (T.elt_eq k' k). congruence.
+  assert (In (k', v') (T.elements m)). apply T.elements_correct; auto.
+  rewrite <- (H2 (k', v')) in H5. destruct (in_app_or _ _ _ H5). auto. 
+  simpl in H6. intuition congruence.
+Qed.
+
+Lemma fold_rec_aux:
+  forall l1 l2 a,
+  list_equiv (l2 ++ l1) (T.elements m_final) ->
+  list_disjoint (List.map (@fst T.elt V) l1) (List.map (@fst T.elt V) l2) ->
+  list_norepet (List.map (@fst T.elt V) l1) ->
+  P' l2 a -> P' (l2 ++ l1) (List.fold_left f' l1 a).
+Proof.
+  induction l1; intros; simpl.
+  rewrite <- List.app_nil_end. auto.
+  destruct a as [k v]; simpl in *. inv H1. 
+  change ((k, v) :: l1) with (((k, v) :: nil) ++ l1). rewrite <- List.app_ass. apply IHl1.
+  rewrite app_ass. auto.
+  red; intros. rewrite map_app in H3. destruct (in_app_or _ _ _ H3). apply H0; auto with coqlib. 
+  simpl in H4. intuition congruence.
+  auto.
+  unfold f'. simpl. apply H_rec'; auto. eapply list_disjoint_notin; eauto with coqlib.
+  rewrite <- (H (k, v)). apply in_or_app. simpl. auto.
+Qed.
+
+Theorem fold_rec:
+  P m_final (T.fold f m_final init).
+Proof.
+  intros. rewrite T.fold_spec. fold f'.
+  assert (P' (nil ++ T.elements m_final) (List.fold_left f' (T.elements m_final) init)).
+    apply fold_rec_aux.
+    simpl. red; intros; tauto.
+    simpl. red; intros. elim H0.
+    apply T.elements_keys_norepet. 
+    apply H_base'. 
+  simpl in H. red in H. apply H. red; intros. tauto.
+Qed.
+
+End TREE_FOLD_IND.
+
+End Tree_Properties.
+
+Module PTree_Properties := Tree_Properties(PTree).
+
 (** * Useful notations *)
 
 Notation "a ! b" := (PTree.get b a) (at level 1).