From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- lib/Maps.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/Maps.v') diff --git a/lib/Maps.v b/lib/Maps.v index 9e44a7fe..54d92897 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -1395,7 +1395,7 @@ Theorem cardinal_remove: Proof. unfold cardinal; intros. exploit T.elements_remove; eauto. intros (l1 & l2 & P & Q). - rewrite P, Q. rewrite ! app_length. simpl. omega. + rewrite P, Q. rewrite ! app_length. simpl. lia. Qed. Theorem cardinal_set: -- cgit From bbf3b4140f4263cdcb7dcb9c9a32c8c7651818d8 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 15 Dec 2020 11:11:15 +0100 Subject: Add new fold_ind induction principle for folds fold_inv is in Type, hence can prove goals such as `{ x | P x }`. Also, no extensionality property is needed. fold_rec is now derived from fold_inv. --- lib/Maps.v | 145 ++++++++++++++++++++++++++++++++++--------------------------- 1 file changed, 82 insertions(+), 63 deletions(-) (limited to 'lib/Maps.v') diff --git a/lib/Maps.v b/lib/Maps.v index 54d92897..092ab6ea 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -1285,103 +1285,122 @@ Module ZTree := ITree(ZIndexed). Module Tree_Properties(T: TREE). -(** An induction principle over [fold]. *) +(** Two induction principles 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 P: T.t V -> A -> Type. 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. + forall m, + (forall k, T.get k m = None) -> + P m 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). + T.get k m = Some v -> T.get k m_final = Some v -> + P (T.remove k m) a -> P m (f a k v). -Let f' (a: A) (p : T.elt * V) := f a (fst p) (snd p). +Let f' (p : T.elt * V) (a: A) := f a (fst p) (snd p). -Let P' (l: list (T.elt * V)) (a: A) : Prop := - forall m, list_equiv l (T.elements m) -> P m a. +Let P' (l: list (T.elt * V)) (a: A) : Type := + forall m, (forall k v, In (k, v) l <-> T.get k m = Some v) -> P m a. -Remark H_base': +Let 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. + intros m EQV. apply H_base. + intros. destruct (T.get k m) as [v|] eqn:G; auto. + apply EQV in G. contradiction. Qed. -Remark H_rec': +Let H_rec': forall k v l a, - ~In k (List.map (@fst T.elt V) l) -> - In (k, v) (T.elements m_final) -> + ~In k (List.map fst l) -> + T.get k m_final = Some v -> P' l a -> - P' (l ++ (k, v) :: nil) (f a k v). + P' ((k, v) :: l) (f a k v). Proof. - unfold P'; intros. + unfold P'; intros k v l a NOTIN FINAL HR m EQV. 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. + apply H_rec. +- apply EQV. simpl; auto. +- auto. +- apply HR. intros k' v'. rewrite T.grspec. split; intros; destruct (T.elt_eq k' k). + + subst k'. elim NOTIN. change k with (fst (k, v')). apply List.in_map; auto. + + apply EQV. simpl; auto. + + congruence. + + apply EQV in H. simpl in H. 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). +Lemma fold_ind_aux: + forall l, + (forall k v, In (k, v) l -> T.get k m_final = Some v) -> + list_norepet (List.map fst l) -> + P' l (List.fold_right f' init l). 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. + induction l as [ | [k v] l ]; simpl; intros FINAL NOREPET. +- apply H_base'. +- apply H_rec'. + + inv NOREPET. auto. + + apply FINAL. auto. + + apply IHl. auto. inv NOREPET; auto. Qed. -Theorem fold_rec: +Theorem fold_ind: 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. + intros. + set (l' := List.rev (T.elements m_final)). + assert (P' l' (List.fold_right f' init l')). + { apply fold_ind_aux. + intros. apply T.elements_complete. apply List.in_rev. auto. + unfold l'; rewrite List.map_rev. apply list_norepet_rev. apply T.elements_keys_norepet. } + unfold l', f' in X; rewrite fold_left_rev_right in X. + rewrite T.fold_spec. apply X. + intros; simpl. rewrite <- List.in_rev. + split. apply T.elements_complete. apply T.elements_correct. Qed. End TREE_FOLD_IND. +Section TREE_FOLD_REC. + +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). + +Theorem fold_rec: + P m_final (T.fold f m_final init). +Proof. + apply fold_ind. +- intros. apply P_compat with (T.empty V); auto. + + intros. rewrite T.gempty. auto. +- intros. apply P_compat with (T.set k v (T.remove k m)). + + intros. rewrite T.gsspec, T.grspec. destruct (T.elt_eq x k); auto. congruence. + + apply H_rec; auto. apply T.grs. +Qed. + +End TREE_FOLD_REC. + (** A nonnegative measure over trees *) Section MEASURE. -- cgit From eca149363d20d94198a4b1e1ae4f9f964e468098 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 16:07:24 +0100 Subject: Define `fold_ind_aux` and `fold_ind` transparently The extraction mechanism wants to extract them (because they are in Type, probably). The current opaque definition causes a warning at extraction-time. --- lib/Maps.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib/Maps.v') diff --git a/lib/Maps.v b/lib/Maps.v index 092ab6ea..c617d488 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -1349,7 +1349,7 @@ Proof. + inv NOREPET. auto. + apply FINAL. auto. + apply IHl. auto. inv NOREPET; auto. -Qed. +Defined. Theorem fold_ind: P m_final (T.fold f m_final init). @@ -1364,7 +1364,7 @@ Proof. rewrite T.fold_spec. apply X. intros; simpl. rewrite <- List.in_rev. split. apply T.elements_complete. apply T.elements_correct. -Qed. +Defined. End TREE_FOLD_IND. -- cgit From 04f499c632a76e460560fc9ec4e14d8216e7fc18 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 4 May 2021 10:46:17 +0200 Subject: Use the LGPL instead of the GPL for dual-licensed files The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate. --- lib/Maps.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'lib/Maps.v') diff --git a/lib/Maps.v b/lib/Maps.v index c617d488..6bc6e14b 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) -- cgit