diff options
Diffstat (limited to 'theories')
38 files changed, 767 insertions, 917 deletions
diff --git a/theories/Arith/Cantor.v b/theories/Arith/Cantor.v new file mode 100644 index 0000000000..b63d970db7 --- /dev/null +++ b/theories/Arith/Cantor.v @@ -0,0 +1,88 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(** Implementation of the Cantor pairing and its inverse function *) + +Require Import PeanoNat Lia. + +(** Bijections between [nat * nat] and [nat] *) + +(** Cantor pairing [to_nat] *) + +Definition to_nat '(x, y) : nat := + y + (nat_rec _ 0 (fun i m => (S i) + m) (y + x)). + +(** Cantor pairing inverse [of_nat] *) + +Definition of_nat (n : nat) : nat * nat := + nat_rec _ (0, 0) (fun _ '(x, y) => + match x with | S x => (x, S y) | _ => (S y, 0) end) n. + +(** [of_nat] is the left inverse for [to_nat] *) + +Lemma cancel_of_to p : of_nat (to_nat p) = p. +Proof. + enough (H : forall n p, to_nat p = n -> of_nat n = p) by now apply H. + intro n. induction n as [|n IHn]. + - now intros [[|?] [|?]]. + - intros [x [|y]]. + + destruct x as [|x]; [discriminate|]. + intros [=H]. cbn. fold (of_nat n). + rewrite (IHn (0, x)); [reflexivity|]. + rewrite <- H. cbn. now rewrite PeanoNat.Nat.add_0_r. + + intros [=H]. cbn. fold (of_nat n). + rewrite (IHn (S x, y)); [reflexivity|]. + rewrite <- H. cbn. now rewrite Nat.add_succ_r. +Qed. + +(** [to_nat] is injective *) + +Corollary to_nat_inj p q : to_nat p = to_nat q -> p = q. +Proof. + intros H %(f_equal of_nat). now rewrite ?cancel_of_to in H. +Qed. + +(** [to_nat] is the left inverse for [of_nat] *) + +Lemma cancel_to_of n : to_nat (of_nat n) = n. +Proof. + induction n as [|n IHn]; [reflexivity|]. + cbn. fold (of_nat n). destruct (of_nat n) as [[|x] y]. + - rewrite <- IHn. cbn. now rewrite PeanoNat.Nat.add_0_r. + - rewrite <- IHn. cbn. now rewrite (Nat.add_succ_r y x). +Qed. + +(** [of_nat] is injective *) + +Corollary of_nat_inj n m : of_nat n = of_nat m -> n = m. +Proof. + intros H %(f_equal to_nat). now rewrite ?cancel_to_of in H. +Qed. + +(** Polynomial specifications of [to_nat] *) + +Lemma to_nat_spec x y : + to_nat (x, y) * 2 = y * 2 + (y + x) * S (y + x). +Proof. + cbn. induction (y + x) as [|n IHn]; cbn; lia. +Qed. + +Lemma to_nat_spec2 x y : + to_nat (x, y) = y + (y + x) * S (y + x) / 2. +Proof. + now rewrite <- Nat.div_add_l, <- to_nat_spec, Nat.div_mul. +Qed. + +(** [to_nat] is non-decreasing in (the sum of) pair components *) + +Lemma to_nat_non_decreasing x y : y + x <= to_nat (x, y). +Proof. + pose proof (to_nat_spec x y). nia. +Qed. diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 6978fa1ddf..a1a4da6f37 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -87,7 +87,7 @@ Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left. Next Obligation. Proof. - destruct x ; destruct y. + do 2 match goal with [ x : () |- _ ] => destruct x end. reflexivity. Qed. @@ -142,7 +142,10 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq := | _, _ => in_right end }. - Next Obligation. destruct y ; unfold not in *; eauto. Defined. + Next Obligation. + match goal with y : list _ |- _ => destruct y end ; + unfold not in *; eauto. + Defined. Solve Obligations with unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 6a98af39aa..3e71a60fa6 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -87,7 +87,7 @@ Tactic Notation "clsubst" "*" := clsubst_nofail. Lemma nequiv_equiv_trans : forall `{Setoid A} (x y z : A), x =/= y -> y == z -> x =/= z. Proof with auto. - intros; intro. + intros A ? x y z H H0 H1. assert(z == y) by (symmetry ; auto). assert(x == y) by (transitivity z ; eauto). contradiction. @@ -95,7 +95,7 @@ Qed. Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z. Proof. - intros; intro. + intros A ? x y z **; intro. assert(y == x) by (symmetry ; auto). assert(y == z) by (transitivity x ; eauto). contradiction. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 2947c4831f..f4220e3aa1 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -96,7 +96,7 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) := Next Obligation. Proof. - destruct x ; destruct y. + do 2 match goal with x : () |- _ => destruct x end. reflexivity. Qed. diff --git a/theories/Compat/Coq813.v b/theories/Compat/Coq813.v index fe7431dcd3..5cfb9d84c7 100644 --- a/theories/Compat/Coq813.v +++ b/theories/Compat/Coq813.v @@ -11,3 +11,13 @@ (** Compatibility file for making Coq act similar to Coq v8.13 *) Require Export Coq.Compat.Coq814. + +Require Coq.micromega.Lia. +Module Export Coq. + Module Export omega. + Module Export Omega. + #[deprecated(since="8.12", note="The omega tactic was removed in v8.14. You're now relying on the lia tactic.")] + Ltac omega := Lia.lia. + End Omega. + End omega. +End Coq. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index d6277b3bb5..2a5eb2db39 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -8,8 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Setoid. -Require Import PeanoNat Le Gt Minus Bool Lt. +Require Import PeanoNat Bool. Set Implicit Arguments. (* Set Universe Polymorphism. *) @@ -264,15 +263,13 @@ Section Facts. forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. Proof. intros l l1 l2; revert l1 l2 l. - intro l1; induction l1 as [ | x1 l1]; intro l2; destruct l2 as [ | x2 l2]; - simpl; auto; intros l H. - absurd (length (x2 :: l2 ++ l) <= length l). - simpl; rewrite app_length; auto with arith. - rewrite <- H; auto with arith. - absurd (length (x1 :: l1 ++ l) <= length l). - simpl; rewrite app_length; auto with arith. - rewrite H; auto with arith. - injection H as [= H H0]; f_equal; eauto. + intro l1; induction l1 as [ | x1 l1]; intro l2; destruct l2 as [ | x2 l2]. + - now intros. + - intros l Hl. apply (f_equal (@length A)) in Hl. + now rewrite ?app_length, Nat.add_cancel_r in Hl. + - intros l Hl. apply (f_equal (@length A)) in Hl. + now rewrite ?app_length, Nat.add_cancel_r in Hl. + - intros l [=H1 H2 %IHl1]. now subst. Qed. Lemma app_inv_tail_iff: @@ -472,7 +469,7 @@ Section Elts. - destruct l; simpl; [ inversion 2 | auto ]. - destruct l; simpl. * inversion 2. - * intros d ie; right; apply hn; auto with arith. + * intros d ie; right; apply hn. now apply Nat.succ_le_mono. Qed. Lemma In_nth l x d : In x l -> @@ -481,9 +478,9 @@ Section Elts. induction l as [|a l IH]. - easy. - intros [H|H]. - * subst; exists 0; simpl; auto with arith. + * subst; exists 0; simpl; auto using Nat.lt_0_succ. * destruct (IH H) as (n & Hn & Hn'). - exists (S n); simpl; auto with arith. + apply Nat.succ_lt_mono in Hn. now exists (S n). Qed. Lemma nth_overflow : forall l n d, length l <= n -> nth n l d = d. @@ -491,7 +488,7 @@ Section Elts. intro l; induction l as [|? ? IHl]; intro n; destruct n; simpl; intros d H; auto. - inversion H. - - apply IHl; auto with arith. + - apply IHl. now apply Nat.succ_le_mono. Qed. Lemma nth_indep : @@ -499,7 +496,8 @@ Section Elts. Proof. intro l; induction l. - inversion 1. - - intros [|n] d d'; simpl; auto with arith. + - intros [|n] d d'; [intros; reflexivity|]. + intros H. apply IHl. now apply Nat.succ_lt_mono. Qed. Lemma app_nth1 : @@ -507,7 +505,8 @@ Section Elts. Proof. intro l; induction l. - inversion 1. - - intros l' d [|n]; simpl; auto with arith. + - intros l' d [|n]; simpl; [intros; reflexivity|]. + intros H. apply IHl. now apply Nat.succ_lt_mono. Qed. Lemma app_nth2 : @@ -515,15 +514,15 @@ Section Elts. Proof. intro l; induction l as [|? ? IHl]; intros l' d [|n]; auto. - inversion 1. - - intros; simpl; rewrite IHl; auto with arith. + - intros; simpl; rewrite IHl; [reflexivity|now apply Nat.succ_le_mono]. Qed. Lemma app_nth2_plus : forall l l' d n, nth (length l + n) (l ++ l') d = nth n l' d. Proof. intros. - rewrite app_nth2, minus_plus; trivial. - auto with arith. + rewrite app_nth2, Nat.add_comm, Nat.add_sub; trivial. + now apply Nat.le_add_r. Qed. Lemma nth_middle : forall l l' a d, @@ -540,7 +539,7 @@ Section Elts. revert l. induction n as [|n IH]; intros [|a l] H; try easy. - exists nil; exists l; now simpl. - - destruct (IH l) as (l1 & l2 & Hl & Hl1); auto with arith. + - destruct (IH l) as (l1 & l2 & Hl & Hl1); [now apply Nat.succ_lt_mono|]. exists (a::l1); exists l2; simpl; split; now f_equal. Qed. @@ -557,7 +556,7 @@ Section Elts. rewrite Hnth; f_equal. + apply IHl with d d'; [ now inversion Hlen | ]. intros n Hlen'; apply (Hnth (S n)). - now simpl; apply lt_n_S. + now apply (Nat.succ_lt_mono n (length l)). + simpl; apply Nat.lt_0_succ. Qed. @@ -575,18 +574,18 @@ Section Elts. induction l as [|a l IH]. - easy. - intros [H|H]. - * subst; exists 0; simpl; auto with arith. + * subst; now exists 0. * destruct (IH H) as (n,Hn). - exists (S n); simpl; auto with arith. + now exists (S n). Qed. Lemma nth_error_None l n : nth_error l n = None <-> length l <= n. Proof. revert n. induction l as [|? ? IHl]; intro n; destruct n; simpl. - split; auto. - - split; auto with arith. - - split; now auto with arith. - - rewrite IHl; split; auto with arith. + - now split; intros; [apply Nat.le_0_l|]. + - now split; [|intros ? %Nat.nle_succ_0]. + - now rewrite IHl, Nat.succ_le_mono. Qed. Lemma nth_error_Some l n : nth_error l n <> None <-> n < length l. @@ -594,8 +593,8 @@ Section Elts. revert n. induction l as [|? ? IHl]; intro n; destruct n; simpl. - split; [now destruct 1 | inversion 1]. - split; [now destruct 1 | inversion 1]. - - split; now auto with arith. - - rewrite IHl; split; auto with arith. + - now split; intros; [apply Nat.lt_0_succ|]. + - now rewrite IHl, Nat.succ_lt_mono. Qed. Lemma nth_error_split l n a : nth_error l n = Some a -> @@ -613,7 +612,7 @@ Section Elts. Proof. revert l. induction n as [|n IHn]; intros [|a l] H; auto; try solve [inversion H]. - simpl in *. apply IHn. auto with arith. + simpl in *. apply IHn. now apply Nat.succ_lt_mono. Qed. Lemma nth_error_app2 l l' n : length l <= n -> @@ -621,7 +620,7 @@ Section Elts. Proof. revert l. induction n as [|n IHn]; intros [|a l] H; auto; try solve [inversion H]. - simpl in *. apply IHn. auto with arith. + simpl in *. apply IHn. now apply Nat.succ_le_mono. Qed. (** Results directly relating [nth] and [nth_error] *) @@ -841,8 +840,9 @@ Section Elts. Theorem count_occ_In l x : In x l <-> count_occ l x > 0. Proof. induction l as [|y l IHl]; simpl. - - split; [destruct 1 | apply gt_irrefl]. + - split; [destruct 1 | apply Nat.nlt_0_r]. - destruct eq_dec as [->|Hneq]; rewrite IHl; intuition. + now apply Nat.lt_0_succ. Qed. Theorem count_occ_not_In l x : ~ In x l <-> count_occ l x = 0. @@ -877,6 +877,36 @@ Section Elts. intros H. simpl. now destruct (eq_dec x y). Qed. + Lemma count_occ_app l1 l2 x : + count_occ (l1 ++ l2) x = count_occ l1 x + count_occ l2 x. + Proof. + induction l1 as [ | h l1 IHl1]; cbn; auto. + now destruct (eq_dec h x); [ rewrite IHl1 | ]. + Qed. + + Lemma count_occ_elt_eq l1 l2 x y : x = y -> + count_occ (l1 ++ x :: l2) y = S (count_occ (l1 ++ l2) y). + Proof. + intros ->. + rewrite ? count_occ_app; cbn. + destruct (eq_dec y y) as [Heq | Hneq]; + [ apply Nat.add_succ_r | now contradiction Hneq ]. + Qed. + + Lemma count_occ_elt_neq l1 l2 x y : x <> y -> + count_occ (l1 ++ x :: l2) y = count_occ (l1 ++ l2) y. + Proof. + intros Hxy. + rewrite ? count_occ_app; cbn. + now destruct (eq_dec x y) as [Heq | Hneq]; [ contradiction Hxy | ]. + Qed. + + Lemma count_occ_bound x l : count_occ l x <= length l. + Proof. + induction l as [|h l]; cbn; auto. + destruct (eq_dec h x); [ apply (proj1 (Nat.succ_le_mono _ _)) | ]; intuition. + Qed. + End Elts. (*******************************) @@ -960,26 +990,22 @@ Section ListOps. elim (length l); simpl; auto. Qed. - Lemma rev_nth : forall l d n, n < length l -> + Lemma rev_nth : forall l d n, n < length l -> nth n (rev l) d = nth (length l - S n) l d. Proof. intro l; induction l as [|a l IHl]. - intros d n H; inversion H. - intros ? n H. - simpl in H. - simpl (rev (a :: l)). - simpl (length (a :: l) - S n). - inversion H. - rewrite <- minus_n_n; simpl. - rewrite <- rev_length. - rewrite app_nth2; auto. - rewrite <- minus_n_n; auto. - rewrite app_nth1; auto. - rewrite (minus_plus_simpl_l_reverse (length l) n 1). - replace (1 + length l) with (S (length l)); auto with arith. - rewrite <- minus_Sn_m; auto with arith. - apply IHl ; auto with arith. - rewrite rev_length; auto. + - intros d n H; inversion H. + - intros ? n H. simpl in H. + inversion H. + + rewrite Nat.sub_diag; simpl. + rewrite <- rev_length. + rewrite app_nth2; auto. + now rewrite Nat.sub_diag. + + simpl. rewrite app_nth1; [|now rewrite rev_length]. + rewrite IHl; [|eassumption]. + destruct (length l); [exfalso; now apply (Nat.nlt_0_r n)|]. + rewrite (Nat.sub_succ_l n); [reflexivity|]. + now apply Nat.succ_le_mono. Qed. @@ -1138,10 +1164,18 @@ Section Map. intro l; induction l; simpl map; intros d n; destruct n; firstorder. Qed. + Lemma nth_error_map : forall n l, + nth_error (map l) n = option_map f (nth_error l n). + Proof. + intro n. induction n as [|n IHn]; intro l. + - now destruct l. + - destruct l as [|? l]; [reflexivity|exact (IHn l)]. + Qed. + Lemma map_nth_error : forall n l d, nth_error l n = Some d -> nth_error (map l) n = Some (f d). Proof. - intro n; induction n; intros [ | ] ? Heq; simpl in *; inversion Heq; auto. + intros n l d H. now rewrite nth_error_map, H. Qed. Lemma map_app : forall l l', @@ -1322,7 +1356,7 @@ Proof. + inversion Hlen. + now rewrite nth_overflow; destruct n. - destruct n; simpl; [ reflexivity | apply IHln ]. - destruct Hlen; [ left; apply lt_S_n | right ]; assumption. + destruct Hlen; [ left; apply Nat.succ_lt_mono | right ]; assumption. Qed. @@ -1358,8 +1392,7 @@ Proof. intros A l. enough (H : forall n, fold_left (fun x _ => S x) l n = n + length l) by exact (H 0). induction l as [|? ? IHl]; simpl; auto. - intros; rewrite IHl. - simpl; auto with arith. + now intros; rewrite IHl, Nat.add_succ_r. Qed. (************************************) @@ -1464,7 +1497,7 @@ End Fold_Right_Recursor. simpl; intros n ? ? H0. destruct (orb_false_elim _ _ H0); clear H0; auto. destruct n ; auto. - rewrite IHl; auto with arith. + rewrite IHl; auto. now apply Nat.succ_lt_mono. Qed. Lemma existsb_app : forall l1 l2, @@ -1900,37 +1933,35 @@ Section length_order. Lemma lel_refl : lel l l. Proof. - unfold lel; auto with arith. + now apply Nat.le_refl. Qed. Lemma lel_trans : lel l m -> lel m n -> lel l n. Proof. unfold lel; intros. now_show (length l <= length n). - apply le_trans with (length m); auto with arith. + now apply Nat.le_trans with (length m). Qed. Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m). Proof. - unfold lel; simpl; auto with arith. + now intros ? %Nat.succ_le_mono. Qed. Lemma lel_cons : lel l m -> lel l (b :: m). Proof. - unfold lel; simpl; auto with arith. + intros. now apply Nat.le_le_succ_r. Qed. Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m. Proof. - unfold lel; simpl; auto with arith. + intros. now apply Nat.succ_le_mono. Qed. Lemma lel_nil : forall l':list A, lel l' nil -> nil = l'. Proof. - intro l'; elim l'; auto with arith. - intros a' y H H0. - now_show (nil = a' :: y). - absurd (S (length y) <= 0); auto with arith. + intro l'; elim l'; [now intros|]. + now intros a' y H H0 %Nat.nle_succ_0. Qed. End length_order. @@ -2105,7 +2136,7 @@ Section Cutting. rewrite (length_zero_iff_nil l) in H1. subst. now simpl. - intro l; destruct l as [|x xs]; simpl. * now reflexivity. - * simpl. intro H. apply Peano.le_S_n in H. f_equal. apply iHk, H. + * simpl. intro H. f_equal. apply iHk. now apply Nat.succ_le_mono. Qed. Lemma firstn_O l: firstn 0 l = []. @@ -2114,17 +2145,17 @@ Section Cutting. Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n. Proof. induction n as [|k iHk]; simpl; [auto | intro l; destruct l as [|x xs]; simpl]. - - auto with arith. - - apply Peano.le_n_S, iHk. + - now apply Nat.le_0_l. + - now rewrite <- Nat.succ_le_mono. Qed. Lemma firstn_length_le: forall l:list A, forall n:nat, n <= length l -> length (firstn n l) = n. Proof. intro l; induction l as [|x xs Hrec]. - - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl. + - simpl. intros n H. apply Nat.le_0_r in H. now subst. - intro n; destruct n as [|n]. * now simpl. - * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H). + * simpl. intro H. f_equal. apply Hrec. now apply Nat.succ_le_mono. Qed. Lemma firstn_app n: @@ -2133,7 +2164,7 @@ Section Cutting. Proof. induction n as [|k iHk]; intros l1 l2. - now simpl. - destruct l1 as [|x xs]. - * unfold firstn at 2, length. now rewrite 2!app_nil_l, <- minus_n_O. + * reflexivity. * rewrite <- app_comm_cons. simpl. f_equal. apply iHk. Qed. @@ -2142,13 +2173,13 @@ Section Cutting. firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2. Proof. induction n as [| k iHk];intros l1 l2. - unfold firstn at 2. rewrite <- plus_n_O, app_nil_r. - rewrite firstn_app. rewrite <- minus_diag_reverse. + rewrite firstn_app. rewrite Nat.sub_diag. unfold firstn at 2. rewrite app_nil_r. apply firstn_all. - destruct l2 as [|x xs]. - * simpl. rewrite app_nil_r. apply firstn_all2. auto with arith. + * simpl. rewrite app_nil_r. apply firstn_all2. now apply Nat.le_add_r. * rewrite firstn_app. assert (H0 : (length l1 + S k - length l1) = S k). - auto with arith. - rewrite H0, firstn_all2; [reflexivity | auto with arith]. + now rewrite Nat.add_comm, Nat.add_sub. + rewrite H0, firstn_all2; [reflexivity | now apply Nat.le_add_r]. Qed. Lemma firstn_firstn: @@ -2249,11 +2280,7 @@ Section Cutting. destruct (Nat.le_ge_cases (length (rev l)) x) as [L | L]. - rewrite skipn_all2; [apply Nat.sub_0_le in L | trivial]. now rewrite L, Nat.sub_0_r, skipn_all. - - replace (length (rev l) - (length (rev l) - x)) - with (length (rev l) + x - length (rev l)). - rewrite minus_plus. reflexivity. - rewrite <- (Nat.sub_add _ _ L) at 2. - now rewrite <-!(Nat.add_comm x), <-minus_plus_simpl_l_reverse. + - f_equal. now apply Nat.eq_sym, Nat.add_sub_eq_l, Nat.sub_add. Qed. Lemma removelast_firstn : forall n l, n < length l -> @@ -2268,7 +2295,7 @@ Section Cutting. change (firstn (S (S n)) (a::l)) with ((a::nil)++firstn (S n) l). change (firstn (S n) (a::l)) with (a::firstn n l). rewrite removelast_app. - rewrite IHn; auto with arith. + rewrite IHn; [reflexivity|now apply Nat.succ_le_mono]. clear IHn; destruct l; simpl in *; try discriminate. inversion_clear H as [|? H1]. @@ -2293,7 +2320,7 @@ Section Cutting. simpl in H. change (removelast (a :: l)) with (removelast ((a::nil)++l)). rewrite removelast_app. - simpl; f_equal; auto with arith. + simpl; f_equal. apply IHn. now apply Nat.succ_lt_mono. intro H0; rewrite H0 in H; inversion_clear H as [|? H1]; inversion_clear H1. Qed. @@ -2385,7 +2412,7 @@ Section Add. Lemma Add_length a l l' : Add a l l' -> length l' = S (length l). Proof. - induction 1; simpl; auto with arith. + induction 1; simpl; now auto. Qed. Lemma Add_inv a l : In a l -> exists l', Add a l' l. @@ -2564,13 +2591,13 @@ Section ReDun. - destruct i, j; simpl in *; auto. * elim Hal. eapply nth_error_In; eauto. * elim Hal. eapply nth_error_In; eauto. - * f_equal. apply IH; auto with arith. } + * f_equal. now apply IH;[apply Nat.succ_lt_mono|]. } { induction l as [|a l IHl]; intros H; constructor. * intro Ha. apply In_nth_error in Ha. destruct Ha as (n,Hn). assert (n < length l) by (now rewrite <- nth_error_Some, Hn). - specialize (H 0 (S n)). simpl in H. discriminate H; auto with arith. + specialize (H 0 (S n)). simpl in H. now discriminate H; [apply Nat.lt_0_succ|]. * apply IHl. - intros i j Hi E. apply eq_add_S, H; simpl; auto with arith. } + intros i j Hi %Nat.succ_lt_mono E. now apply eq_add_S, H. } Qed. Lemma NoDup_nth l d : @@ -2582,14 +2609,17 @@ Section ReDun. { intros H; induction H as [|a l Hal Hl IH]; intros i j Hi Hj E. - inversion Hi. - destruct i, j; simpl in *; auto. - * elim Hal. subst a. apply nth_In; auto with arith. - * elim Hal. subst a. apply nth_In; auto with arith. - * f_equal. apply IH; auto with arith. } + * elim Hal. subst a. now apply nth_In, Nat.succ_lt_mono. + * elim Hal. subst a. now apply nth_In, Nat.succ_lt_mono. + * f_equal. apply IH; [| |assumption]; now apply Nat.succ_lt_mono. } { induction l as [|a l IHl]; intros H; constructor. * intro Ha. eapply In_nth in Ha. destruct Ha as (n & Hn & Hn'). - specialize (H 0 (S n)). simpl in H. discriminate H; eauto with arith. + specialize (H 0 (S n)). simpl in H. + apply Nat.succ_lt_mono in Hn. + discriminate H; eauto using Nat.lt_0_succ. * apply IHl. - intros i j Hi Hj E. apply eq_add_S, H; simpl; auto with arith. } + intros i j Hi %Nat.succ_lt_mono Hj %Nat.succ_lt_mono E. + now apply eq_add_S, H. } Qed. (** Having [NoDup] hypotheses bring more precise facts about [incl]. *) @@ -2598,7 +2628,7 @@ Section ReDun. NoDup l -> incl l l' -> length l <= length l'. Proof. intros N. revert l'. induction N as [|a l Hal N IH]; simpl. - - auto with arith. + - intros. now apply Nat.le_0_l. - intros l' H. destruct (Add_inv a l') as (l'', AD). { apply H; simpl; auto. } rewrite (Add_length AD). apply le_n_S. apply IH. @@ -2615,7 +2645,7 @@ Section ReDun. rewrite (Add_in AD) in Hx. simpl in Hx. destruct Hx as [Hx|Hx]; [left; trivial|right]. revert x Hx. apply (IH l''); trivial. - * apply le_S_n. now rewrite <- (Add_length AD). + * apply Nat.succ_le_mono. now rewrite <- (Add_length AD). * now apply incl_Add_inv with a l'. Qed. @@ -2690,9 +2720,8 @@ Section NatSeq. intro len; induction len as [|len IHlen]; intros start n d H. inversion H. simpl seq. - destruct n; simpl. - auto with arith. - rewrite IHlen;simpl; auto with arith. + destruct n; simpl. now rewrite Nat.add_0_r. + now rewrite IHlen; [rewrite Nat.add_succ_r|apply Nat.succ_lt_mono]. Qed. Lemma seq_shift : forall len start, @@ -2700,25 +2729,29 @@ Section NatSeq. Proof. intro len; induction len as [|len IHlen]; simpl; auto. intros. - rewrite IHlen. - auto with arith. + now rewrite IHlen. Qed. Lemma in_seq len start n : In n (seq start len) <-> start <= n < start+len. Proof. - revert start. induction len as [|len IHlen]; simpl; intros. - - rewrite <- plus_n_O. split;[easy|]. - intros (H,H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')). - - rewrite IHlen, <- plus_n_Sm; simpl; split. - + intros [H|H]; subst; intuition auto with arith. - + intros (H,H'). destruct (Lt.le_lt_or_eq _ _ H); intuition. + revert start. induction len as [|len IHlen]; simpl; intros start. + - rewrite <- plus_n_O. split;[easy|]. + intros (H,H'). apply (Nat.lt_irrefl start). + eapply Nat.le_lt_trans; eassumption. + - rewrite IHlen, <- plus_n_Sm; simpl; split. + + intros [H|H]; subst; intuition. + * apply -> Nat.succ_le_mono. apply Nat.le_add_r. + * now apply Nat.lt_le_incl. + + intros (H,H'). inversion H. + * now left. + * right. subst. now split; [apply -> Nat.succ_le_mono|]. Qed. Lemma seq_NoDup len start : NoDup (seq start len). Proof. revert start; induction len; simpl; constructor; trivial. - rewrite in_seq. intros (H,_). apply (Lt.lt_irrefl _ H). + rewrite in_seq. intros (H,_). now apply (Nat.lt_irrefl start). Qed. Lemma seq_app : forall len1 len2 start, @@ -3021,6 +3054,53 @@ Hint Constructors Exists : core. #[global] Hint Constructors Forall : core. +Lemma Exists_map A B (f : A -> B) P l : + Exists P (map f l) <-> Exists (fun x => P (f x)) l. +Proof. + induction l as [|a l IHl]. + - cbn. now rewrite Exists_nil. + - cbn. now rewrite ?Exists_cons, IHl. +Qed. + +Lemma Exists_concat A P (ls : list (list A)) : + Exists P (concat ls) <-> Exists (Exists P) ls. +Proof. + induction ls as [|l ls IHls]. + - cbn. now rewrite Exists_nil. + - cbn. now rewrite Exists_app, Exists_cons, IHls. +Qed. + +Lemma Exists_flat_map A B P ls (f : A -> list B) : + Exists P (flat_map f ls) <-> Exists (fun d => Exists P (f d)) ls. +Proof. + now rewrite flat_map_concat_map, Exists_concat, Exists_map. +Qed. + +Lemma Forall_map A B (f : A -> B) P l : + Forall P (map f l) <-> Forall (fun x => P (f x)) l. +Proof. + induction l as [|a l IHl]. + - constructor; intros; now constructor. + - constructor; intro H; + (constructor; [exact (Forall_inv H) | apply IHl; exact (Forall_inv_tail H)]). +Qed. + +Lemma Forall_concat A P (ls : list (list A)) : + Forall P (concat ls) <-> Forall (Forall P) ls. +Proof. + induction ls as [|l ls IHls]. + - constructor; intros; now constructor. + - cbn. rewrite Forall_app. constructor; intro H. + + constructor; [exact (proj1 H) | apply IHls; exact (proj2 H)]. + + constructor; [exact (Forall_inv H) | apply IHls; exact (Forall_inv_tail H)]. +Qed. + +Lemma Forall_flat_map A B P ls (f : A -> list B) : + Forall P (flat_map f ls) <-> Forall (fun d => Forall P (f d)) ls. +Proof. + now rewrite flat_map_concat_map, Forall_concat, Forall_map. +Qed. + Lemma exists_Forall A B : forall (P : A -> B -> Prop) l, (exists k, Forall (P k) l) -> Forall (fun x => exists k, P k x) l. Proof. @@ -3242,6 +3322,70 @@ Section Repeat. now rewrite (IHl HF') at 1. Qed. + Hypothesis decA : forall x y : A, {x = y}+{x <> y}. + + Lemma count_occ_repeat_eq x y n : x = y -> count_occ decA (repeat y n) x = n. + Proof. + intros ->. + induction n; cbn; auto. + destruct (decA y y); auto. + exfalso; intuition. + Qed. + + Lemma count_occ_repeat_neq x y n : x <> y -> count_occ decA (repeat y n) x = 0. + Proof. + intros Hneq. + induction n; cbn; auto. + destruct (decA y x); auto. + exfalso; intuition. + Qed. + + Lemma count_occ_unique x l : count_occ decA l x = length l -> l = repeat x (length l). + Proof. + induction l as [|h l]; cbn; intros Hocc; auto. + destruct (decA h x). + - f_equal; intuition. + - assert (Hb := count_occ_bound decA x l). + rewrite Hocc in Hb. + exfalso; apply (Nat.nle_succ_diag_l _ Hb). + Qed. + + Lemma count_occ_repeat_excl x l : + (forall y, y <> x -> count_occ decA l y = 0) -> l = repeat x (length l). + Proof. + intros Hocc. + apply Forall_eq_repeat, Forall_forall; intros z Hin. + destruct (decA z x) as [Heq|Hneq]; auto. + apply Hocc, count_occ_not_In in Hneq; intuition. + Qed. + + Lemma count_occ_sgt l x : l = x :: nil <-> + count_occ decA l x = 1 /\ forall y, y <> x -> count_occ decA l y = 0. + Proof. + split. + - intros ->; cbn; split; intros; destruct decA; subst; intuition. + - intros [Heq Hneq]. + apply count_occ_repeat_excl in Hneq. + rewrite Hneq, count_occ_repeat_eq in Heq; trivial. + now rewrite Heq in Hneq. + Qed. + + Lemma nth_repeat a m n : + nth n (repeat a m) a = a. + Proof. + revert n. induction m as [|m IHm]. + - now intros [|n]. + - intros [|n]; [reflexivity|exact (IHm n)]. + Qed. + + Lemma nth_error_repeat a m n : + n < m -> nth_error (repeat a m) n = Some a. + Proof. + intro Hnm. rewrite (nth_error_nth' _ a). + - now rewrite nth_repeat. + - now rewrite repeat_length. + Qed. + End Repeat. Lemma repeat_to_concat A n (a:A) : @@ -3279,11 +3423,12 @@ Qed. Lemma list_max_le : forall l n, list_max l <= n <-> Forall (fun k => k <= n) l. Proof. -intro l; induction l as [|a l IHl]; simpl; intros n; split; intros H; intuition. -- apply Nat.max_lub_iff in H. - now constructor; [ | apply IHl ]. -- inversion_clear H as [ | ? ? Hle HF ]. - apply IHl in HF; apply Nat.max_lub; assumption. + intro l; induction l as [|a l IHl]; simpl; intros n; split. + - now intros. + - intros. now apply Nat.le_0_l. + - intros [? ?] %Nat.max_lub_iff. now constructor; [|apply IHl]. + - intros H. apply Nat.max_lub_iff. + constructor; [exact (Forall_inv H)|apply IHl; exact (Forall_inv_tail H)]. Qed. Lemma list_max_lt : forall l n, l <> nil -> diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 826815410a..69b158a87e 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -71,7 +71,7 @@ Hint Constructors NoDupA : core. Lemma NoDupA_altdef : forall l, NoDupA l <-> ForallOrdPairs (complement eqA) l. Proof. - split; induction 1; constructor; auto. + split; induction 1 as [|a l H rest]; constructor; auto. rewrite Forall_forall. intros b Hb. intro Eq; elim H. rewrite InA_alt. exists b; auto. rewrite InA_alt; intros (a' & Haa' & Ha'). @@ -85,7 +85,7 @@ Definition inclA l l' := forall x, InA x l -> InA x l'. Definition equivlistA l l' := forall x, InA x l <-> InA x l'. Lemma incl_nil l : inclA nil l. -Proof. intro. intros. inversion H. Qed. +Proof. intros a H. inversion H. Qed. #[local] Hint Resolve incl_nil : list. @@ -128,7 +128,7 @@ Qed. Global Instance eqlistA_equiv : Equivalence eqlistA. Proof. constructor; red. - induction x; auto. + intros x; induction x; auto. induction 1; auto. intros x y z H; revert z; induction H; auto. inversion 1; subst; auto. invlist eqlistA; eauto with *. @@ -138,9 +138,9 @@ Qed. Global Instance eqlistA_equivlistA : subrelation eqlistA equivlistA. Proof. - intros x x' H. induction H. + intros x x' H. induction H as [|? ? ? ? H ? IHeqlistA]. intuition. - red; intros. + red; intros x0. rewrite 2 InA_cons. rewrite (IHeqlistA x0), H; intuition. Qed. @@ -165,7 +165,7 @@ Hint Immediate InA_eqA : core. Lemma In_InA : forall l x, In x l -> InA x l. Proof. - simple induction l; simpl; intuition. + intros l; induction l; simpl; intuition. subst; auto. Qed. #[local] @@ -174,8 +174,9 @@ Hint Resolve In_InA : core. Lemma InA_split : forall l x, InA x l -> exists l1 y l2, eqA x y /\ l = l1++y::l2. Proof. -induction l; intros; inv. +intros l; induction l as [|a l IHl]; intros x H; inv. exists (@nil A); exists a; exists l; auto. +match goal with H' : InA x l |- _ => rename H' into H0 end. destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))). exists (a::l1); exists y; exists l2; auto. split; simpl; f_equal; auto. @@ -184,9 +185,10 @@ Qed. Lemma InA_app : forall l1 l2 x, InA x (l1 ++ l2) -> InA x l1 \/ InA x l2. Proof. - induction l1; simpl in *; intuition. + intros l1; induction l1 as [|a l1 IHl1]; simpl in *; intuition. inv; auto. - elim (IHl1 l2 x H0); auto. + match goal with H0' : InA _ (l1 ++ _) |- _ => rename H0' into H0 end. + elim (IHl1 _ _ H0); auto. Qed. Lemma InA_app_iff : forall l1 l2 x, @@ -194,7 +196,7 @@ Lemma InA_app_iff : forall l1 l2 x, Proof. split. apply InA_app. - destruct 1; generalize H; do 2 rewrite InA_alt. + destruct 1 as [H|H]; generalize H; do 2 rewrite InA_alt. destruct 1 as (y,(H1,H2)); exists y; split; auto. apply in_or_app; auto. destruct 1 as (y,(H1,H2)); exists y; split; auto. @@ -240,11 +242,12 @@ Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' -> (forall x, InA x l -> InA x l' -> False) -> NoDupA (l++l'). Proof. -induction l; simpl; auto; intros. +intros l; induction l as [|a l IHl]; simpl; auto; intros l' H H0 H1. inv. constructor. rewrite InA_alt; intros (y,(H4,H5)). destruct (in_app_or _ _ _ H5). +match goal with H2' : ~ InA a l |- _ => rename H2' into H2 end. elim H2. rewrite InA_alt. exists y; auto. @@ -253,13 +256,13 @@ auto. rewrite InA_alt. exists y; auto. apply IHl; auto. -intros. +intros x ? ?. apply (H1 x); auto. Qed. Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l). Proof. -induction l. +intros l; induction l. simpl; auto. simpl; intros. inv. @@ -270,17 +273,17 @@ intros x. rewrite InA_alt. intros (x1,(H2,H3)). intro; inv. -destruct H0. -rewrite <- H4, H2. +match goal with H0 : ~ InA _ _ |- _ => destruct H0 end. +match goal with H4 : eqA x ?x' |- InA ?x' _ => rewrite <- H4, H2 end. apply In_InA. rewrite In_rev; auto. Qed. Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l'). Proof. - induction l; simpl in *; intros; inv; auto. + intros l; induction l; simpl in *; intros; inv; auto. constructor; eauto. - contradict H0. + match goal with H0 : ~ InA _ _ |- _ => contradict H0 end. rewrite InA_app_iff in *. rewrite InA_cons. intuition. @@ -288,17 +291,17 @@ Qed. Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l'). Proof. - induction l; simpl in *; intros; inv; auto. + intros l; induction l as [|a l IHl]; simpl in *; intros l' x H; inv; auto. constructor; eauto. - assert (H2:=IHl _ _ H1). + match goal with H1 : NoDupA (l ++ x :: l') |- _ => assert (H2:=IHl _ _ H1) end. inv. rewrite InA_cons. red; destruct 1. - apply H0. + match goal with H0 : ~ InA a (l ++ x :: l') |- _ => apply H0 end. rewrite InA_app_iff in *; rewrite InA_cons; auto. - apply H; auto. + auto. constructor. - contradict H0. + match goal with H0 : ~ InA a (l ++ x :: l') |- _ => contradict H0 end. rewrite InA_app_iff in *; rewrite InA_cons; intuition. eapply NoDupA_split; eauto. Qed. @@ -356,19 +359,21 @@ Lemma equivlistA_NoDupA_split l l1 l2 x y : eqA x y -> NoDupA (x::l) -> NoDupA (l1++y::l2) -> equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2). Proof. - intros; intro a. + intros H H0 H1 H2; intro a. generalize (H2 a). rewrite !InA_app_iff, !InA_cons. inv. assert (SW:=NoDupA_swap H1). inv. - rewrite InA_app_iff in H0. + rewrite InA_app_iff in *. split; intros. - assert (~eqA a x) by (contradict H3; rewrite <- H3; auto). + match goal with H3 : ~ InA x l |- _ => + assert (~eqA a x) by (contradict H3; rewrite <- H3; auto) + end. assert (~eqA a y) by (rewrite <- H; auto). tauto. - assert (OR : eqA a x \/ InA a l) by intuition. clear H6. + assert (OR : eqA a x \/ InA a l) by intuition. destruct OR as [EQN|INA]; auto. - elim H0. + match goal with H0 : ~ (InA y l1 \/ InA y l2) |- _ => elim H0 end. rewrite <-H,<-EQN; auto. Qed. @@ -448,7 +453,7 @@ Qed. Lemma ForallOrdPairs_inclA : forall l l', NoDupA l' -> inclA l' l -> ForallOrdPairs R l -> ForallOrdPairs R l'. Proof. -induction l' as [|x l' IH]. +intros l l'. induction l' as [|x l' IH]. constructor. intros ND Incl FOP. apply FOP_cons; inv; unfold inclA in *; auto. rewrite Forall_forall; intros y Hy. @@ -476,7 +481,7 @@ Lemma fold_right_commutes_restr : forall s1 s2 x, ForallOrdPairs R (s1++x::s2) -> eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))). Proof. -induction s1; simpl; auto; intros. +intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x H. reflexivity. transitivity (f a (f x (fold_right f i (s1++s2)))). apply Comp; auto. @@ -484,7 +489,9 @@ apply IHs1. invlist ForallOrdPairs; auto. apply TraR. invlist ForallOrdPairs; auto. -rewrite Forall_forall in H0; apply H0. +match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- R a x => + rewrite Forall_forall in H0; apply H0 +end. apply in_or_app; simpl; auto. Qed. @@ -492,14 +499,14 @@ Lemma fold_right_equivlistA_restr : forall s s', NoDupA s -> NoDupA s' -> ForallOrdPairs R s -> equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s'). Proof. - simple induction s. - destruct s'; simpl. + intros s; induction s as [|x l Hrec]. + intros s'; destruct s' as [|a s']; simpl. intros; reflexivity. - unfold equivlistA; intros. + unfold equivlistA; intros H H0 H1 H2. destruct (H2 a). assert (InA a nil) by auto; inv. - intros x l Hrec s' N N' F E; simpl in *. - assert (InA x s') by (rewrite <- (E x); auto). + intros s' N N' F E; simpl in *. + assert (InA x s') as H by (rewrite <- (E x); auto). destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). subst s'. transitivity (f x (fold_right f i (s1++s2))). @@ -520,7 +527,7 @@ Lemma fold_right_add_restr : forall s' s x, NoDupA s -> NoDupA s' -> ForallOrdPairs R s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)). Proof. - intros; apply (@fold_right_equivlistA_restr s' (x::s)); auto. + intros s' s x **; apply (@fold_right_equivlistA_restr s' (x::s)); auto. Qed. End Fold_With_Restriction. @@ -532,7 +539,7 @@ Variable Tra :transpose f. Lemma fold_right_commutes : forall s1 s2 x, eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))). Proof. -induction s1; simpl; auto; intros. +intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x. reflexivity. transitivity (f a (f x (fold_right f i (s1++s2)))); auto. apply Comp; auto. @@ -542,7 +549,7 @@ Lemma fold_right_equivlistA : forall s s', NoDupA s -> NoDupA s' -> equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s'). Proof. -intros; apply fold_right_equivlistA_restr with (R:=fun _ _ => True); +intros; apply (fold_right_equivlistA_restr (R:=fun _ _ => True)); repeat red; auto. apply ForallPairs_ForallOrdPairs; try red; auto. Qed. @@ -551,7 +558,7 @@ Lemma fold_right_add : forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)). Proof. - intros; apply (@fold_right_equivlistA s' (x::s)); auto. + intros s' s x **; apply (@fold_right_equivlistA s' (x::s)); auto. Qed. End Fold. @@ -571,7 +578,7 @@ Lemma fold_right_eqlistA2 : eqB (fold_right f i s) (fold_right f j s'). Proof. intros s. - induction s;intros. + induction s as [|a s IHs];intros s' i j heqij heqss'. - inversion heqss'. subst. simpl. @@ -604,7 +611,7 @@ Lemma fold_right_commutes_restr2 : forall s1 s2 x (i j:B) (heqij: eqB i j), ForallOrdPairs R (s1++x::s2) -> eqB (fold_right f i (s1++x::s2)) (f x (fold_right f j (s1++s2))). Proof. -induction s1; simpl; auto; intros. +intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x i j heqij ?. - apply Comp. + destruct eqA_equiv. apply Equivalence_Reflexive. + eapply fold_right_eqlistA2. @@ -617,7 +624,9 @@ induction s1; simpl; auto; intros. invlist ForallOrdPairs; auto. apply TraR. invlist ForallOrdPairs; auto. - rewrite Forall_forall in H0; apply H0. + match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- _ => + rewrite Forall_forall in H0; apply H0 + end. apply in_or_app; simpl; auto. reflexivity. Qed. @@ -628,14 +637,14 @@ Lemma fold_right_equivlistA_restr2 : equivlistA s s' -> eqB i j -> eqB (fold_right f i s) (fold_right f j s'). Proof. - simple induction s. - destruct s'; simpl. + intros s; induction s as [|x l Hrec]. + intros s'; destruct s' as [|a s']; simpl. intros. assumption. - unfold equivlistA; intros. + unfold equivlistA; intros ? ? H H0 H1 H2 **. destruct (H2 a). assert (InA a nil) by auto; inv. - intros x l Hrec s' i j N N' F E eqij; simpl in *. - assert (InA x s') by (rewrite <- (E x); auto). + intros s' i j N N' F E eqij; simpl in *. + assert (InA x s') as H by (rewrite <- (E x); auto). destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). subst s'. transitivity (f x (fold_right f j (s1++s2))). @@ -663,7 +672,7 @@ Lemma fold_right_add_restr2 : forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)). Proof. - intros; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto. + intros s' s i j x **; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto. Qed. End Fold2_With_Restriction. @@ -674,7 +683,7 @@ Lemma fold_right_commutes2 : forall s1 s2 i x x', eqA x x' -> eqB (fold_right f i (s1++x::s2)) (f x' (fold_right f i (s1++s2))). Proof. - induction s1;simpl;intros. + intros s1; induction s1 as [|a s1 IHs1];simpl;intros s2 i x x' H. - apply Comp;auto. reflexivity. - transitivity (f a (f x' (fold_right f i (s1++s2)))); auto. @@ -688,7 +697,7 @@ Lemma fold_right_equivlistA2 : equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s'). Proof. red in Tra. -intros; apply fold_right_equivlistA_restr2 with (R:=fun _ _ => True); +intros; apply (fold_right_equivlistA_restr2 (R:=fun _ _ => True)); repeat red; auto. apply ForallPairs_ForallOrdPairs; try red; auto. Qed. @@ -697,9 +706,9 @@ Lemma fold_right_add2 : forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)). Proof. - intros. + intros s' s i j x **. replace (f x (fold_right f j s)) with (fold_right f j (x::s)) by auto. - eapply fold_right_equivlistA2;auto. + eapply fold_right_equivlistA2;auto. Qed. End Fold2. @@ -710,7 +719,7 @@ Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }. Proof. -induction l. +intros x l; induction l as [|a l IHl]. right; auto. intro; inv. destruct (eqA_dec x a). @@ -729,28 +738,30 @@ Fixpoint removeA (x : A) (l : list A) : list A := Lemma removeA_filter : forall x l, removeA x l = filter (fun y => if eqA_dec x y then false else true) l. Proof. -induction l; simpl; auto. +intros x l; induction l as [|a l IHl]; simpl; auto. destruct (eqA_dec x a); auto. rewrite IHl; auto. Qed. Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y. Proof. -induction l; simpl; auto. -split. +intros l; induction l as [|a l IHl]; simpl; auto. +intros x y; split. intro; inv. destruct 1; inv. -intros. +intros x y. destruct (eqA_dec x a) as [Heq|Hnot]; simpl; auto. rewrite IHl; split; destruct 1; split; auto. inv; auto. -destruct H0; transitivity a; auto. +match goal with H0 : ~ eqA x y |- _ => destruct H0 end; transitivity a; auto. split. intro; inv. split; auto. contradict Hnot. transitivity y; auto. -rewrite (IHl x y) in H0; destruct H0; auto. +match goal with H0 : InA y (removeA x l) |- _ => + rewrite (IHl x y) in H0; destruct H0; auto +end. destruct 1; inv; auto. right; rewrite IHl; auto. Qed. @@ -758,7 +769,7 @@ Qed. Lemma removeA_NoDupA : forall s x, NoDupA s -> NoDupA (removeA x s). Proof. -simple induction s; simpl; intros. +intros s; induction s as [|a s IHs]; simpl; intros x ?. auto. inv. destruct (eqA_dec x a); simpl; auto. @@ -770,16 +781,16 @@ Qed. Lemma removeA_equivlistA : forall l l' x, ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l'). Proof. -unfold equivlistA; intros. +unfold equivlistA; intros l l' x H H0 x0. rewrite removeA_InA. -split; intros. +split; intros H1. rewrite <- H0; split; auto. contradict H. apply InA_eqA with x0; auto. rewrite <- (H0 x0) in H1. destruct H1. inv; auto. -elim H2; auto. +match goal with H2 : ~ eqA x x0 |- _ => elim H2; auto end. Qed. End Remove. @@ -806,7 +817,7 @@ Hint Constructors lelistA sort : core. Lemma InfA_ltA : forall l x y, ltA x y -> InfA y l -> InfA x l. Proof. - destruct l; constructor. inv; eauto. + intros l; destruct l; constructor. inv; eauto. Qed. Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA. @@ -815,8 +826,8 @@ Proof using eqA_equiv ltA_compat. (* and not ltA_strorder *) inversion_clear Hll'. intuition. split; intro; inv; constructor. - rewrite <- Hxx', <- H; auto. - rewrite Hxx', H; auto. + match goal with H : eqA _ _ |- _ => rewrite <- Hxx', <- H; auto end. + match goal with H : eqA _ _ |- _ => rewrite Hxx', H; auto end. Qed. (** For compatibility, can be deduced from [InfA_compat] *) @@ -830,9 +841,9 @@ Hint Immediate InfA_ltA InfA_eqA : core. Lemma SortA_InfA_InA : forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x. Proof. - simple induction l. - intros. inv. - intros. inv. + intros l; induction l as [|a l IHl]. + intros x a **. inv. + intros x a0 **. inv. setoid_replace x with a; auto. eauto. Qed. @@ -840,13 +851,13 @@ Qed. Lemma In_InfA : forall l x, (forall y, In y l -> ltA x y) -> InfA x l. Proof. - simple induction l; simpl; intros; constructor; auto. + intros l; induction l; simpl; intros; constructor; auto. Qed. Lemma InA_InfA : forall l x, (forall y, InA y l -> ltA x y) -> InfA x l. Proof. - simple induction l; simpl; intros; constructor; auto. + intros l; induction l; simpl; intros; constructor; auto. Qed. (* In fact, this may be used as an alternative definition for InfA: *) @@ -861,7 +872,7 @@ Qed. Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2). Proof. - induction l1; simpl; auto. + intros l1; induction l1; simpl; auto. intros; inv; auto. Qed. @@ -870,7 +881,7 @@ Lemma SortA_app : (forall x y, InA x l1 -> InA y l2 -> ltA x y) -> SortA (l1 ++ l2). Proof. - induction l1; simpl in *; intuition. + intros l1; induction l1; intros l2; simpl in *; intuition. inv. constructor; auto. apply InfA_app; auto. @@ -879,8 +890,8 @@ Qed. Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l. Proof. - simple induction l; auto. - intros x l' H H0. + intros l; induction l as [|x l' H]; auto. + intros H0. inv. constructor; auto. intro. @@ -922,7 +933,7 @@ Qed. Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A). Proof. -repeat red. intros. +repeat red. intros x y ?. rewrite <- (app_nil_r (rev x)), <- (app_nil_r (rev y)). apply eqlistA_rev_app; auto. Qed. @@ -936,15 +947,15 @@ Qed. Lemma SortA_equivlistA_eqlistA : forall l l', SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'. Proof. -induction l; destruct l'; simpl; intros; auto. -destruct (H1 a); assert (InA a nil) by auto; inv. +intros l; induction l as [|a l IHl]; intros l'; destruct l' as [|a0 l']; simpl; intros H H0 H1; auto. +destruct (H1 a0); assert (InA a0 nil) by auto; inv. destruct (H1 a); assert (InA a nil) by auto; inv. inv. assert (forall y, InA y l -> ltA a y). -intros; eapply SortA_InfA_InA with (l:=l); eauto. +intros; eapply (SortA_InfA_InA (l:=l)); eauto. assert (forall y, InA y l' -> ltA a0 y). -intros; eapply SortA_InfA_InA with (l:=l'); eauto. -clear H3 H4. +intros; eapply (SortA_InfA_InA (l:=l')); eauto. +do 2 match goal with H : InfA _ _ |- _ => clear H end. assert (eqA a a0). destruct (H1 a). destruct (H1 a0). @@ -953,13 +964,19 @@ assert (eqA a a0). elim (StrictOrder_Irreflexive a); eauto. constructor; auto. apply IHl; auto. -split; intros. +intros x; split; intros. destruct (H1 x). assert (InA x (a0::l')) by auto. inv; auto. -rewrite H9,<-H3 in H4. elim (StrictOrder_Irreflexive a); eauto. +match goal with H3 : eqA a a0, H4 : InA x l, H9 : eqA x a0 |- InA x l' => + rewrite H9,<-H3 in H4 +end. +elim (StrictOrder_Irreflexive a); eauto. destruct (H1 x). assert (InA x (a::l)) by auto. inv; auto. -rewrite H9,H3 in H4. elim (StrictOrder_Irreflexive a0); eauto. +match goal with H3 : eqA a a0, H4 : InA x l', H9 : eqA x a |- InA x l => + rewrite H9,H3 in H4 +end. +elim (StrictOrder_Irreflexive a0); eauto. Qed. End EqlistA. @@ -970,12 +987,12 @@ Section Filter. Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l). Proof. -induction l; simpl; auto. +intros f l; induction l as [|a l IHl]; simpl; auto. intros; inv; auto. destruct (f a); auto. constructor; auto. apply In_InfA; auto. -intros. +intros y H. rewrite filter_In in H; destruct H. eapply SortA_InfA_InA; eauto. Qed. @@ -984,12 +1001,14 @@ Arguments eq {A} x _. Lemma filter_InA : forall f, Proper (eqA==>eq) f -> forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true. Proof. +(* Unset Mangle Names. *) clear sotrans ltA ltA_strorder ltA_compat. -intros; do 2 rewrite InA_alt; intuition. -destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. -destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition. +intros f H l x; do 2 rewrite InA_alt; intuition; + match goal with Hex' : exists _, _ |- _ => rename Hex' into Hex end. +destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. +destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; intuition. rewrite (H _ _ H0); auto. -destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition. +destruct Hex as (y,(H0,H1)); exists y; rewrite filter_In; intuition. rewrite <- (H _ _ H0); auto. Qed. @@ -997,19 +1016,20 @@ Lemma filter_split : forall f, (forall x y, f x = true -> f y = false -> ltA x y) -> forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l. Proof. -induction l; simpl; intros; auto. +intros f H l; induction l as [|a l IHl]; simpl; intros H0; auto. inv. +match goal with H1' : SortA l, H2' : InfA a l |- _ => rename H1' into H1, H2' into H2 end. rewrite IHl at 1; auto. case_eq (f a); simpl; intros; auto. -assert (forall e, In e l -> f e = false). - intros. +assert (forall e, In e l -> f e = false) as H3. + intros e H3. assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)). case_eq (f e); simpl; intros; auto. elim (StrictOrder_Irreflexive e). transitivity a; auto. replace (List.filter f l) with (@nil A); auto. -generalize H3; clear; induction l; simpl; auto. -case_eq (f a); auto; intros. +generalize H3; clear; induction l as [|a l IHl]; simpl; auto. +case_eq (f a); auto; intros H H3. rewrite H3 in H; auto; try discriminate. Qed. @@ -1043,23 +1063,24 @@ Lemma findA_NoDupA : Proof. set (eqk := fun p p' : A*B => eqA (fst p) (fst p')). set (eqke := fun p p' : A*B => eqA (fst p) (fst p') /\ snd p = snd p'). -induction l; intros; simpl. -split; intros; try discriminate. +intros l; induction l as [|a l IHl]; intros a0 b H; simpl. +split; intros H0; try discriminate. invlist InA. destruct a as (a',b'); rename a0 into a. invlist NoDupA. split; intros. invlist InA. -compute in H2; destruct H2. subst b'. +match goal with H2 : eqke (a, b) (a', b') |- _ => compute in H2; destruct H2 end. +subst b'. destruct (eqA_dec a a'); intuition. destruct (eqA_dec a a') as [HeqA|]; simpl. -contradict H0. -revert HeqA H2; clear - eqA_equiv. +match goal with H0 : ~ InA eqk (a', b') l |- _ => contradict H0 end. +match goal with H2 : InA eqke (a, b) l |- _ => revert HeqA H2; clear - eqA_equiv end. induction l. intros; invlist InA. intros; invlist InA; auto. -destruct a0. -compute in H; destruct H. +match goal with |- InA eqk _ (?p :: _) => destruct p as [a0 b0] end. +match goal with H : eqke (a, b) (a0, b0) |- _ => compute in H; destruct H end. subst b. left; auto. compute. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 3dac62c476..23bc396fd7 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -676,7 +676,7 @@ Qed. We show instead that functional relation reification and the functional form of the axiom of choice are equivalent on decidable - relation with [nat] as codomain + relations with [nat] as codomain. *) Require Import Wf_nat. diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v index 4735d6c9ca..a151cca3af 100644 --- a/theories/Logic/ExtensionalityFacts.v +++ b/theories/Logic/ExtensionalityFacts.v @@ -43,7 +43,7 @@ Definition is_inverse A B f g := (forall a:A, g (f a) = a) /\ (forall b:B, f (g #[universes(template)] Record Delta A := { pi1:A; pi2:A; eq:pi1=pi2 }. -Definition delta {A} (a:A) := {|pi1 := a; pi2 := a; eq := eq_refl a |}. +Definition delta {A} (a:A) := {| pi1 := a; pi2 := a; eq := eq_refl a |}. Arguments pi1 {A} _. Arguments pi2 {A} _. diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v index 131668154e..7560ea96b5 100644 --- a/theories/Logic/ProofIrrelevanceFacts.v +++ b/theories/Logic/ProofIrrelevanceFacts.v @@ -27,7 +27,7 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance). forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. Proof. - intros; rewrite M.proof_irrelevance with (p1:=h) (p2:=eq_refl p). + intros U p Q x h; rewrite (M.proof_irrelevance _ h (eq_refl p)). reflexivity. Qed. End Eq_rect_eq. @@ -45,8 +45,8 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance). forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y), x = y -> exist P x p = exist P y q. Proof. - intros. - rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H). + intros U P x y p q H. + rewrite (M.proof_irrelevance _ q (eq_rect x P p y H)). elim H using eq_indd. reflexivity. Qed. @@ -55,8 +55,8 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance). forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y), x = y -> existT P x p = existT P y q. Proof. - intros. - rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H). + intros U P x y p q H. + rewrite (M.proof_irrelevance _ q (eq_rect x P p y H)). elim H using eq_indd. reflexivity. Qed. diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 37d20bffad..c1928fef8d 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -30,6 +30,7 @@ *) Require Import FunInd Orders OrdersFacts MSetInterface PeanoNat. +Require Arith. (* contains deprecated dependencies *) Local Open Scope list_scope. Local Open Scope lazy_bool_scope. diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v index 2a26b6b12a..4bf971668d 100644 --- a/theories/Numbers/Cyclic/Int63/Cyclic63.v +++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v @@ -218,7 +218,6 @@ Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y. apply Zdiv_lt_upper_bound;auto with zarith. apply Z.lt_le_trans with y;auto with zarith. rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith. - assert (0 < 2^p);auto with zarith. replace (2^p) with 0. destruct x;change (0<y);auto with zarith. destruct p;trivial;discriminate. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index a3ebe67325..d3fac82d09 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -1428,7 +1428,7 @@ Proof. assert (Hp3: (0 < Φ (WW ih il))). {simpl zn2z_to_Z;apply Z.lt_le_trans with (φ ih * wB)%Z; auto with zarith. apply Zmult_lt_0_compat; auto with zarith. - refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. } + } cbv zeta. case_eq (ih <? j)%int63;intros Heq. rewrite -> ltb_spec in Heq. @@ -1465,7 +1465,6 @@ Proof. apply Hrec; rewrite H; clear u H. assert (Hf1: 0 <= Φ (WW ih il) / φ j) by (apply Z_div_pos; auto with zarith). case (Zle_lt_or_eq 1 (φ j)); auto with zarith; intros Hf2. - 2: contradict Heq0; apply Zle_not_lt; rewrite <- Hf2, Zdiv_1_r; auto with zarith. split. replace (φ j + Φ (WW ih il) / φ j)%Z with (1 * 2 + ((φ j - 2) + Φ (WW ih il) / φ j)) by lia. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 9788ad50dc..9540bc1075 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -68,10 +68,11 @@ Ltac pi := repeat f_equal ; apply proof_irrelevance. Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> `n = `m. Proof. + intros A P n m. destruct n as (x,p). destruct m as (x',p'). simpl. - split ; intros ; subst. + split ; intros H ; subst. - inversion H. reflexivity. @@ -92,7 +93,7 @@ Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B) (y : {y:A | y = x}), match_eq A B x fn = fn y. Proof. - intros. + intros A B x fn y. unfold match_eq. f_equal. destruct y. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 45fb48ad5d..2bf54baef3 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -535,6 +535,32 @@ Proof. now apply Permutation_cons_inv with x. Qed. +Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. + +Lemma Permutation_count_occ l1 l2 : + Permutation l1 l2 <-> forall x, count_occ eq_dec l1 x = count_occ eq_dec l2 x. +Proof. + split. + - induction 1 as [ | y l1 l2 HP IHP | y z l | l1 l2 l3 HP1 IHP1 HP2 IHP2 ]; + cbn; intros a; auto. + + now rewrite IHP. + + destruct (eq_dec y a); destruct (eq_dec z a); auto. + + now rewrite IHP1, IHP2. + - revert l2; induction l1 as [|y l1 IHl1]; cbn; intros l2 Hocc. + + replace l2 with (@nil A); auto. + symmetry; apply (count_occ_inv_nil eq_dec); intuition. + + assert (exists l2' l2'', l2 = l2' ++ y :: l2'') as [l2' [l2'' ->]]. + { specialize (Hocc y). + destruct (eq_dec y y); intuition. + apply in_split, (count_occ_In eq_dec). + rewrite <- Hocc; apply Nat.lt_0_succ. } + apply Permutation_cons_app, IHl1. + intros z; specialize (Hocc z); destruct (eq_dec y z) as [Heq | Hneq]. + * rewrite (count_occ_elt_eq _ _ _ Heq) in Hocc. + now injection Hocc. + * now rewrite (count_occ_elt_neq _ _ _ Hneq) in Hocc. + Qed. + End Permutation_properties. Section Permutation_map. diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 206eb606d2..422316d879 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -71,6 +71,7 @@ Section defs. (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) -> forall l:list A, Sorted l -> P l. Proof. + intros P ? ? l. induction l. firstorder using Sorted_inv. firstorder using Sorted_inv. Qed. @@ -78,7 +79,8 @@ Section defs. Proof. split; [induction 1 as [|a l [|]]| induction 1]; auto using Sorted, LocallySorted, HdRel. - inversion H1; subst; auto using LocallySorted. + match goal with H1 : HdRel a (_ :: _) |- _ => inversion H1 end. + subst; auto using LocallySorted. Qed. (** Strongly sorted: elements of the list are pairwise ordered *) @@ -90,7 +92,7 @@ Section defs. Lemma StronglySorted_inv : forall a l, StronglySorted (a :: l) -> StronglySorted l /\ Forall (R a) l. Proof. - intros; inversion H; auto. + intros a l H; inversion H; auto. Defined. Lemma StronglySorted_rect : @@ -99,7 +101,7 @@ Section defs. (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) -> forall l, StronglySorted l -> P l. Proof. - induction l; firstorder using StronglySorted_inv. + intros P ? ? l; induction l; firstorder using StronglySorted_inv. Defined. Lemma StronglySorted_rec : @@ -120,7 +122,8 @@ Section defs. Lemma Sorted_extends : Transitive R -> forall a l, Sorted (a::l) -> Forall (R a) l. Proof. - intros. change match a :: l with [] => True | a :: l => Forall (R a) l end. + intros H a l H0. + change match a :: l with [] => True | a :: l => Forall (R a) l end. induction H0 as [|? ? ? ? H1]; [trivial|]. destruct H1; constructor; trivial. eapply Forall_impl; [|eassumption]. diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index c923b503a7..a49e21fa92 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -93,7 +93,7 @@ Module KeyDecidableType(D:DecidableType). Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. Proof. - intros; apply InA_eqA with p; auto using eqk_equiv. + intros p q m **; apply InA_eqA with p; auto using eqk_equiv. Qed. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). @@ -106,18 +106,18 @@ Module KeyDecidableType(D:DecidableType). Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. Proof. - firstorder. - exists x; auto. - induction H. - destruct y. - exists e; auto. - destruct IHInA as [e H0]. + intros k l; split; intros [y H]. + exists y; auto. + induction H as [a l eq|a l H IH]. + destruct a as [k' y']. + exists y'; auto. + destruct IH as [e H0]. exists e; auto. Qed. Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. Proof. - intros; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv. + intros l x y e **; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. @@ -127,21 +127,21 @@ Module KeyDecidableType(D:DecidableType). Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. Proof. - inversion 1. - inversion_clear H0; eauto. + inversion 1 as [? H0]. + inversion_clear H0 as [? ? H1|]; eauto. destruct H1; simpl in *; intuition. Qed. Lemma In_inv_2 : forall k k' e e' l, InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. Proof. - inversion_clear 1; compute in H0; intuition. + inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition. Qed. Lemma In_inv_3 : forall x x' l, InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. Proof. - inversion_clear 1; compute in H0; intuition. + inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition. Qed. End Elt. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index dc7a48cd6b..7bc9f97e2b 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -65,7 +65,7 @@ Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType. Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. Proof with auto with ordered_type. - intros; elim (compare x y); intro H; [ right | left | right ]... + intros x y; elim (compare x y); intro H; [ right | left | right ]... assert (~ eq y x)... Defined. @@ -83,7 +83,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_antirefl : forall x, ~ lt x x. Proof. - intros; intro; absurd (eq x x); auto with ordered_type. + intros x; intro; absurd (eq x x); auto with ordered_type. Qed. Instance lt_strorder : StrictOrder lt. @@ -91,14 +91,14 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. Proof with auto with ordered_type. - intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. + intros x y z H ?; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. elim (lt_not_eq H); apply eq_trans with z... elim (lt_not_eq (lt_trans Hlt H))... Qed. Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. Proof with auto with ordered_type. - intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. + intros x y z H H0; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. elim (lt_not_eq H0); apply eq_trans with x... elim (lt_not_eq (lt_trans H0 Hlt))... Qed. @@ -111,7 +111,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Qed. Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x. - Proof. intros; destruct (compare x y); auto. Qed. + Proof. intros x y; destruct (compare x y); auto. Qed. Module TO. Definition t := t. @@ -157,7 +157,7 @@ Module OrderedTypeFacts (Import O: OrderedType). forall x y : t, eq x y -> exists H : eq x y, compare x y = EQ H. Proof. - intros; case (compare x y); intros H'; try (exfalso; order). + intros x y H; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. Qed. @@ -165,7 +165,7 @@ Module OrderedTypeFacts (Import O: OrderedType). forall x y : t, lt x y -> exists H : lt x y, compare x y = LT H. Proof. - intros; case (compare x y); intros H'; try (exfalso; order). + intros x y H; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. Qed. @@ -173,7 +173,7 @@ Module OrderedTypeFacts (Import O: OrderedType). forall x y : t, lt y x -> exists H : lt y x, compare x y = GT H. Proof. - intros; case (compare x y); intros H'; try (exfalso; order). + intros x y H; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. Qed. @@ -203,7 +203,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}. Proof. - intros; elim (compare x y); [ left | right | right ]; auto with ordered_type. + intros x y; elim (compare x y); [ left | right | right ]; auto with ordered_type. Defined. Definition eqb x y : bool := if eq_dec x y then true else false. @@ -211,7 +211,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma eqb_alt : forall x y, eqb x y = match compare x y with EQ _ => true | _ => false end. Proof. - unfold eqb; intros; destruct (eq_dec x y); elim_comp; auto. + unfold eqb; intros x y; destruct (eq_dec x y); elim_comp; auto. Qed. (* Specialization of results about lists modulo. *) @@ -327,7 +327,7 @@ Module KeyOrderedType(O:OrderedType). Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. Proof. unfold eqke, ltk; intuition; simpl in *; subst. - exact (lt_not_eq H H1). + match goal with H : lt _ _, H1 : eq _ _ |- _ => exact (lt_not_eq H H1) end. Qed. #[local] @@ -398,18 +398,18 @@ Module KeyOrderedType(O:OrderedType). Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. Proof with auto with ordered_type. - firstorder. - exists x... - induction H. - destruct y. - exists e... - destruct IHInA as [e H0]. + intros k l; split; intros [y H]. + exists y... + induction H as [a l eq|a l H IH]. + destruct a as [k' y']. + exists y'... + destruct IH as [e H0]. exists e... Qed. Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. Proof. - intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. + intros l x y e **; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. @@ -437,7 +437,7 @@ Module KeyOrderedType(O:OrderedType). Lemma Sort_Inf_NotIn : forall l k e, Sort l -> Inf (k,e) l -> ~In k l. Proof. - intros; red; intros. + intros l k e H H0; red; intros H1. destruct H1 as [e' H2]. elim (@ltk_not_eqk (k,e) (k,e')). eapply Sort_Inf_In; eauto with ordered_type. @@ -457,34 +457,34 @@ Module KeyOrderedType(O:OrderedType). Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> ltk e e' \/ eqk e e'. Proof. - inversion_clear 2; auto with ordered_type. + intros l; inversion_clear 2; auto with ordered_type. left; apply Sort_In_cons_1 with l; auto. Qed. Lemma Sort_In_cons_3 : forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k. Proof. - inversion_clear 1; red; intros. + inversion_clear 1 as [|? ? H0 H1]; red; intros H H2. destruct (Sort_Inf_NotIn H0 H1 (In_eq H2 H)). Qed. Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. Proof. - inversion 1. - inversion_clear H0; eauto with ordered_type. + inversion 1 as [? H0]. + inversion_clear H0 as [? ? H1|]; eauto with ordered_type. destruct H1; simpl in *; intuition. Qed. Lemma In_inv_2 : forall k k' e e' l, InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. Proof. - inversion_clear 1; compute in H0; intuition. + inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition. Qed. Lemma In_inv_3 : forall x x' l, InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. Proof. - inversion_clear 1; compute in H0; intuition. + inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition. Qed. End Elt. diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 10545332bb..227ac00e79 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -14,9 +14,9 @@ Institution: PPS, INRIA 12/2010 *) -Require Fin. +Require Fin List. Require Import VectorDef PeanoNat Eqdep_dec. -Import VectorNotations. +Import VectorNotations EqNotations. Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n} (eq : a1 :: v1 = a2 :: v2) : a1 = a2 /\ v1 = v2 := @@ -233,15 +233,6 @@ assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h). + simpl. intros; now rewrite<- (IHv). Qed. -(** ** Properties of [to_list] *) - -Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l. -Proof. -induction l. -- reflexivity. -- unfold to_list; simpl. now f_equal. -Qed. - (** ** Properties of [take] *) Lemma take_O : forall {A} {n} le (v:t A n), take 0 le v = []. @@ -387,3 +378,147 @@ intros P n v1 v2; split; induction n as [|n IHn]. (proj1 (Nat.succ_lt_mono _ _) Hi2). now rewrite <- (nth_order_tl _ _ _ _ Hi1), <- (nth_order_tl _ _ _ _ Hi2) in HP. Qed. + +(** ** Properties of [to_list] *) + +Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l. +Proof. +induction l. +- reflexivity. +- unfold to_list; simpl. now f_equal. +Qed. + +Lemma length_to_list A n (v : t A n): length (to_list v) = n. +Proof. induction v; cbn; auto. Qed. + +Lemma of_list_to_list_opp A n (v: t A n): + rew length_to_list _ _ _ in of_list (to_list v) = v. +Proof. +induction v as [ | h n v IHv ]. +- now apply case0 with (P := fun v => v = nil A). +- replace (length_to_list _ _ (cons _ h _ v)) with (f_equal S (length_to_list _ _ v)) + by apply (UIP_dec Nat.eq_dec). + cbn; rewrite map_subst_map. + f_equal. + now etransitivity; [ | apply IHv]. +Qed. + +Lemma to_list_nil A : to_list (nil A) = List.nil. +Proof. reflexivity. Qed. + +Lemma to_list_cons A h n (v : t A n): + to_list (cons A h n v) = List.cons h (to_list v). +Proof. reflexivity. Qed. + +Lemma to_list_hd A n (v : t A (S n)) d: + hd v = List.hd d (to_list v). +Proof. now rewrite (eta v). Qed. + +Lemma to_list_last A n (v : t A (S n)) d: + last v = List.last (to_list v) d. +Proof. +apply rectS with (v:=v); trivial. +intros a k u IH. +rewrite to_list_cons. +simpl List.last. +now rewrite <- IH, (eta u). +Qed. + +Lemma to_list_const A (a : A) n: + to_list (const a n) = List.repeat a n. +Proof. +induction n as [ | n IHn ]; trivial. +now cbn; rewrite <- IHn. +Qed. + +Lemma to_list_nth_order A n (v : t A n) p (H : p < n) d: + nth_order v H = List.nth p (to_list v) d. +Proof. +revert n v H; induction p as [ | p IHp ]; intros n v H; + (destruct n; [ inversion H | rewrite (eta v) ]); trivial. +now rewrite <- nth_order_tl with (H:=Lt.lt_S_n _ _ H), IHp. +Qed. + +Lemma to_list_tl A n (v : t A (S n)): + to_list (tl v) = List.tl (to_list v). +Proof. now rewrite (eta v). Qed. + +Lemma to_list_append A n m (v1 : t A n) (v2 : t A m): + to_list (append v1 v2) = List.app (to_list v1) (to_list v2). +Proof. +induction v1; simpl; trivial. +now rewrite to_list_cons; f_equal. +Qed. + +Lemma to_list_rev_append_tail A n m (v1 : t A n) (v2 : t A m): + to_list (rev_append_tail v1 v2) = List.rev_append (to_list v1) (to_list v2). +Proof. now revert m v2; induction v1 as [ | ? ? ? IHv1 ]; intros; [ | simpl; rewrite IHv1 ]. Qed. + +Lemma to_list_rev_append A n m (v1 : t A n) (v2 : t A m): + to_list (rev_append v1 v2) = List.rev_append (to_list v1) (to_list v2). +Proof. unfold rev_append; rewrite (Plus.plus_tail_plus n m); apply to_list_rev_append_tail. Qed. + +Lemma to_list_rev A n (v : t A n): + to_list (rev v) = List.rev (to_list v). +Proof. +unfold rev; rewrite (plus_n_O n); unfold eq_rect_r; simpl. +now rewrite to_list_rev_append, List.rev_alt. +Qed. + +Lemma to_list_map A B (f : A -> B) n (v : t A n) : + to_list (map f v) = List.map f (to_list v). +Proof. +induction v; cbn; trivial. +now cbn; f_equal. +Qed. + +Lemma to_list_fold_left A B f (b : B) n (v : t A n): + fold_left f b v = List.fold_left f (to_list v) b. +Proof. now revert b; induction v; cbn. Qed. + +Lemma to_list_fold_right A B f (b : B) n (v : t A n): + fold_right f v b = List.fold_right f b (to_list v). +Proof. now revert b; induction v; cbn; intros; f_equal. Qed. + +Lemma to_list_Forall A P n (v : t A n): + Forall P v <-> List.Forall P (to_list v). +Proof. +split; intros HF. +- induction HF; now constructor. +- remember (to_list v) as l. + revert n v Heql; induction HF; intros n v Heql; + destruct v; inversion Heql; subst; constructor; auto. +Qed. + +Lemma to_list_Exists A P n (v : t A n): + Exists P v <-> List.Exists P (to_list v). +Proof. +split; intros HF. +- induction HF; now constructor. +- remember (to_list v) as l. + revert n v Heql; induction HF; intros n v Heql; + destruct v; inversion Heql; subst; now constructor; auto. +Qed. + +Lemma to_list_In A a n (v : t A n): + In a v <-> List.In a (to_list v). +Proof. +split. +- intros HIn; induction HIn; now constructor. +- induction v; intros HIn; inversion HIn; subst; constructor; auto. +Qed. + +Lemma to_list_Forall2 A B P n (v1 : t A n) (v2 : t B n) : + Forall2 P v1 v2 <-> List.Forall2 P (to_list v1) (to_list v2). +Proof. +split; intros HF. +- induction HF; now constructor. +- remember (to_list v1) as l1. + remember (to_list v2) as l2. + revert n v1 v2 Heql1 Heql2; induction HF; intros n v1 v2 Heql1 Heql2. + + destruct v1; [ | inversion Heql1 ]. + apply case0 with (P0 := fun x => Forall2 P (nil A) x); constructor. + + destruct v1; inversion Heql1; subst. + rewrite (eta v2) in Heql2; inversion Heql2; subst. + rewrite (eta v2); constructor; auto. +Qed. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 47137414dc..ff1a2b5a53 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1775,8 +1775,6 @@ weak_Zmult_plus_distr_r (now Z.mul_add_distr_pos) Definition Zne (x y:Z) := x <> y. (* TODO : to remove someday ? *) -Register Zne as plugins.omega.Zne. - Ltac elim_compare com1 com2 := case (Dcompare (com1 ?= com2)%Z); [ idtac | let x := fresh "H" in diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index ed47539e1e..5490044ac7 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -16,9 +16,11 @@ Require Export ZArith_base. Require Export Zpow_def. -(** Extra modules using [Omega] or [Ring]. *) +(** Extra modules using [Ring]. *) -Require Export Omega. +Require Export OmegaLemmas. +Require Export PreOmega. +Require Export ZArith_hints. Require Export Zcomplements. Require Export Zpower. Require Export Zdiv. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 7f72d42d1f..b7cd849323 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -959,13 +959,6 @@ Definition inj_lt n m := proj1 (Nat2Z.inj_lt n m). Definition inj_ge n m := proj1 (Nat2Z.inj_ge n m). Definition inj_gt n m := proj1 (Nat2Z.inj_gt n m). -Register neq as plugins.omega.neq. -Register inj_eq as plugins.omega.inj_eq. -Register inj_neq as plugins.omega.inj_neq. -Register inj_le as plugins.omega.inj_le. -Register inj_lt as plugins.omega.inj_lt. -Register inj_ge as plugins.omega.inj_ge. -Register inj_gt as plugins.omega.inj_gt. (** For the others, a Notation is fine *) @@ -1033,5 +1026,3 @@ Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z.of_nat (n - m) = 0. Proof. intros. rewrite not_le_minus_0; auto with arith. Qed. - -Register inj_minus2 as plugins.omega.inj_minus2. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 4c533ac458..bef9cede12 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -64,11 +64,6 @@ Proof. apply Z.lt_gt_cases. Qed. -Register dec_Zne as plugins.omega.dec_Zne. -Register dec_Zgt as plugins.omega.dec_Zgt. -Register dec_Zge as plugins.omega.dec_Zge. -Register not_Zeq as plugins.omega.not_Zeq. - (** * Relating strict and large orders *) Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing). @@ -120,12 +115,6 @@ Proof. destruct (Z.eq_decidable n m); [assumption|now elim H]. Qed. -Register Znot_le_gt as plugins.omega.Znot_le_gt. -Register Znot_lt_ge as plugins.omega.Znot_lt_ge. -Register Znot_ge_lt as plugins.omega.Znot_ge_lt. -Register Znot_gt_le as plugins.omega.Znot_gt_le. -Register not_Zne as plugins.omega.not_Zne. - (** * Equivalence and order properties *) (** Reflexivity *) diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 10ea6cc03e..369a0c46ae 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -93,11 +93,3 @@ Proof. apply Z.le_lt_trans with (m*n+p); trivial. now apply Z.add_lt_mono_l. Qed. - -Register Zegal_left as plugins.omega.Zegal_left. -Register Zne_left as plugins.omega.Zne_left. -Register Zlt_left as plugins.omega.Zlt_left. -Register Zgt_left as plugins.omega.Zgt_left. -Register Zle_left as plugins.omega.Zle_left. -Register Zge_left as plugins.omega.Zge_left. -Register Zmult_le_approx as plugins.omega.Zmult_le_approx. diff --git a/theories/dune b/theories/dune index 1cd3d8c119..57b97f080c 100644 --- a/theories/dune +++ b/theories/dune @@ -22,7 +22,6 @@ coq-core.plugins.ring coq-core.plugins.nsatz - coq-core.plugins.omega coq-core.plugins.zify coq-core.plugins.micromega @@ -34,3 +33,6 @@ coq-core.plugins.derive)) (include_subdirs qualified) + +(documentation + (package coq-stdlib)) diff --git a/theories/extraction/ExtrOcamlBigIntConv.v b/theories/extraction/ExtrOcamlBigIntConv.v index 29bd732c78..b4aed4c3f7 100644 --- a/theories/extraction/ExtrOcamlBigIntConv.v +++ b/theories/extraction/ExtrOcamlBigIntConv.v @@ -8,12 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Extraction to Ocaml: conversion from/to [big_int] *) +(** Extraction to OCaml: conversion from/to [Z.t] *) -(** NB: The extracted code should be linked with [nums.cm(x)a] - from ocaml's stdlib and with the wrapper [big.ml] that - simplifies the use of [Big_int] (it can be found in the sources - of Coq). *) +(** NB: The extracted code should be linked with [zarith.cm(x)a] and with + the [big.ml] wrapper. The latter can be found in the sources of Coq. *) Require Coq.extraction.Extraction. diff --git a/theories/extraction/ExtrOcamlNatBigInt.v b/theories/extraction/ExtrOcamlNatBigInt.v index 8a7ba92a94..c854f8fd5d 100644 --- a/theories/extraction/ExtrOcamlNatBigInt.v +++ b/theories/extraction/ExtrOcamlNatBigInt.v @@ -8,17 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Extraction of [nat] into Ocaml's [big_int] *) +(** Extraction of [nat] into Zarith's [Z.t] *) Require Coq.extraction.Extraction. Require Import Arith Even Div2 EqNat Euclid. Require Import ExtrOcamlBasic. -(** NB: The extracted code should be linked with [nums.cm(x)a] - from ocaml's stdlib and with the wrapper [big.ml] that - simplifies the use of [Big_int] (it can be found in the sources - of Coq). *) +(** NB: The extracted code should be linked with [zarith.cm(x)a] and with + the [big.ml] wrapper. The latter can be found in the sources of Coq. *) (** Disclaimer: trying to obtain efficient certified programs by extracting [nat] into [big_int] isn't necessarily a good idea. diff --git a/theories/extraction/ExtrOcamlZBigInt.v b/theories/extraction/ExtrOcamlZBigInt.v index 40a47b36fa..df9153a46d 100644 --- a/theories/extraction/ExtrOcamlZBigInt.v +++ b/theories/extraction/ExtrOcamlZBigInt.v @@ -8,17 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Extraction of [positive], [N] and [Z] into Ocaml's [big_int] *) +(** Extraction of [positive], [N], and [Z], into Zarith's [Z.t] *) Require Coq.extraction.Extraction. Require Import ZArith NArith. Require Import ExtrOcamlBasic. -(** NB: The extracted code should be linked with [nums.cm(x)a] - from ocaml's stdlib and with the wrapper [big.ml] that - simplifies the use of [Big_int] (it can be found in the sources - of Coq). *) +(** NB: The extracted code should be linked with [zarith.cm(x)a] and with + the [big.ml] wrapper. The latter can be found in the sources of Coq. *) (** Disclaimer: trying to obtain efficient certified programs by extracting [Z] into [big_int] isn't necessarily a good idea. diff --git a/theories/index.mld b/theories/index.mld new file mode 100644 index 0000000000..360864342b --- /dev/null +++ b/theories/index.mld @@ -0,0 +1,3 @@ +{0 coq-stdlib } + +The coq-stdlib package only contains Coq theory files for the standard library and no OCaml libraries. diff --git a/theories/micromega/OrderedRing.v b/theories/micromega/OrderedRing.v index 5fa3740ab1..bfbd6fd8d3 100644 --- a/theories/micromega/OrderedRing.v +++ b/theories/micromega/OrderedRing.v @@ -423,7 +423,7 @@ Qed. (* The following theorems are used to build a morphism from Z to R and prove its properties in ZCoeff.v. They are not used in RingMicromega.v. *) -(* Surprisingly, multilication is needed to prove the following theorem *) +(* Surprisingly, multiplication is needed to prove the following theorem *) Theorem Ropp_neg_pos : forall n : R, - n < 0 <-> 0 < n. Proof. @@ -457,4 +457,3 @@ apply Rtimes_pos_pos. assumption. now apply -> Rlt_lt_minus. Qed.*) End STRICT_ORDERED_RING. - diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v index 01cc9ad810..3a50001b1f 100644 --- a/theories/micromega/Zify.v +++ b/theories/micromega/Zify.v @@ -33,5 +33,6 @@ Ltac zify := intros; zify_elim_let ; zify_op ; (zify_iter_specs) ; - zify_saturate ; - zify_to_euclidean_division_equations ; zify_post_hook. + zify_to_euclidean_division_equations ; + zify_post_hook; + zify_saturate. diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index f6ade67c5f..019d11d951 100644 --- a/theories/micromega/ZifyClasses.v +++ b/theories/micromega/ZifyClasses.v @@ -250,8 +250,18 @@ Register rew_iff as ZifyClasses.rew_iff. Register source_prop as ZifyClasses.source_prop. Register injprop_ok as ZifyClasses.injprop_ok. Register iff as ZifyClasses.iff. + +Register InjTyp as ZifyClasses.InjTyp. +Register BinOp as ZifyClasses.BinOp. +Register UnOp as ZifyClasses.UnOp. +Register CstOp as ZifyClasses.CstOp. +Register BinRel as ZifyClasses.BinRel. +Register PropOp as ZifyClasses.PropOp. +Register PropUOp as ZifyClasses.PropUOp. Register BinOpSpec as ZifyClasses.BinOpSpec. Register UnOpSpec as ZifyClasses.UnOpSpec. +Register Saturate as ZifyClasses.Saturate. + (** Propositional logic *) Register and as ZifyClasses.and. @@ -264,3 +274,4 @@ Register impl_morph as ZifyClasses.impl_morph. Register not as ZifyClasses.not. Register not_morph as ZifyClasses.not_morph. Register True as ZifyClasses.True. +Register I as ZifyClasses.I. diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index 9881e73f76..8dee70be45 100644 --- a/theories/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v @@ -307,15 +307,15 @@ Instance Op_N_mul : BinOp N.mul := Add Zify BinOp Op_N_mul. Instance Op_N_sub : BinOp N.sub := - {| TBOp := fun x y => Z.max 0 (x - y) ; TBOpInj := N2Z.inj_sub_max|}. + {| TBOp := fun x y => Z.max 0 (x - y) ; TBOpInj := N2Z.inj_sub_max |}. Add Zify BinOp Op_N_sub. Instance Op_N_div : BinOp N.div := - {| TBOp := Z.div ; TBOpInj := N2Z.inj_div|}. + {| TBOp := Z.div ; TBOpInj := N2Z.inj_div |}. Add Zify BinOp Op_N_div. Instance Op_N_mod : BinOp N.modulo := - {| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem|}. + {| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem |}. Add Zify BinOp Op_N_mod. Instance Op_N_pred : UnOp N.pred := @@ -332,19 +332,19 @@ Add Zify UnOp Op_N_succ. (* zify_Z_rel *) Instance Op_Z_ge : BinRel Z.ge := - {| TR := Z.ge ; TRInj := fun x y => iff_refl (x>= y)|}. + {| TR := Z.ge ; TRInj := fun x y => iff_refl (x>= y) |}. Add Zify BinRel Op_Z_ge. Instance Op_Z_lt : BinRel Z.lt := - {| TR := Z.lt ; TRInj := fun x y => iff_refl (x < y)|}. + {| TR := Z.lt ; TRInj := fun x y => iff_refl (x < y) |}. Add Zify BinRel Op_Z_lt. Instance Op_Z_gt : BinRel Z.gt := - {| TR := Z.gt ;TRInj := fun x y => iff_refl (x > y)|}. + {| TR := Z.gt ;TRInj := fun x y => iff_refl (x > y) |}. Add Zify BinRel Op_Z_gt. Instance Op_Z_le : BinRel Z.le := - {| TR := Z.le ;TRInj := fun x y => iff_refl (x <= y)|}. + {| TR := Z.le ;TRInj := fun x y => iff_refl (x <= y) |}. Add Zify BinRel Op_Z_le. Instance Op_eqZ : BinRel (@eq Z) := @@ -460,7 +460,7 @@ Add Zify UnOp Op_Z_to_nat. (** Specification of derived operators over Z *) Instance ZmaxSpec : BinOpSpec Z.max := - {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec|}. + {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec |}. Add Zify BinOpSpec ZmaxSpec. Instance ZminSpec : BinOpSpec Z.min := @@ -470,49 +470,30 @@ Add Zify BinOpSpec ZminSpec. Instance ZsgnSpec : UnOpSpec Z.sgn := {| UPred := fun n r : Z => 0 < n /\ r = 1 \/ 0 = n /\ r = 0 \/ n < 0 /\ r = - (1) ; - USpec := Z.sgn_spec|}. + USpec := Z.sgn_spec |}. Add Zify UnOpSpec ZsgnSpec. Instance ZabsSpec : UnOpSpec Z.abs := {| UPred := fun n r: Z => 0 <= n /\ r = n \/ n < 0 /\ r = - n ; - USpec := Z.abs_spec|}. + USpec := Z.abs_spec |}. Add Zify UnOpSpec ZabsSpec. (** Saturate positivity constraints *) -Instance SatProd : Saturate Z.mul := - {| - PArg1 := fun x => 0 <= x; - PArg2 := fun y => 0 <= y; - PRes := fun r => 0 <= r; - SatOk := Z.mul_nonneg_nonneg - |}. -Add Zify Saturate SatProd. - -Instance SatProdPos : Saturate Z.mul := +Instance SatPowPos : Saturate Z.pow := {| PArg1 := fun x => 0 < x; - PArg2 := fun y => 0 < y; + PArg2 := fun y => 0 <= y; PRes := fun r => 0 < r; - SatOk := Z.mul_pos_pos + SatOk := Z.pow_pos_nonneg |}. -Add Zify Saturate SatProdPos. - -Lemma pow_pos_strict : - forall a b, - 0 < a -> 0 < b -> 0 < a ^ b. -Proof. - intros. - apply Z.pow_pos_nonneg; auto. - apply Z.lt_le_incl;auto. -Qed. - +Add Zify Saturate SatPowPos. -Instance SatPowPos : Saturate Z.pow := +Instance SatPowNonneg : Saturate Z.pow := {| - PArg1 := fun x => 0 < x; - PArg2 := fun y => 0 < y; - PRes := fun r => 0 < r; - SatOk := pow_pos_strict + PArg1 := fun x => 0 <= x; + PArg2 := fun y => True; + PRes := fun r => 0 <= r; + SatOk := fun a b Ha _ => @Z.pow_nonneg a b Ha |}. -Add Zify Saturate SatPowPos. +Add Zify Saturate SatPowNonneg. diff --git a/theories/omega/Omega.v b/theories/omega/Omega.v deleted file mode 100644 index 5c52284621..0000000000 --- a/theories/omega/Omega.v +++ /dev/null @@ -1,24 +0,0 @@ -(************************************************************************) -(* * 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) *) -(************************************************************************) -(**************************************************************************) -(* *) -(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(* *) -(**************************************************************************) - -(* We import what is necessary for Omega *) -Require Export ZArith_base. -Require Export OmegaLemmas. -Require Export PreOmega. -Require Export ZArith_hints. - -Declare ML Module "omega_plugin". diff --git a/theories/omega/OmegaLemmas.v b/theories/omega/OmegaLemmas.v index 08e9ac345d..8ccd8d76f6 100644 --- a/theories/omega/OmegaLemmas.v +++ b/theories/omega/OmegaLemmas.v @@ -261,47 +261,3 @@ Proof. intros n; exists (Z.of_nat n); split; trivial. rewrite Z.mul_1_r, Z.add_0_r. apply Nat2Z.is_nonneg. Qed. - -Register fast_Zplus_assoc_reverse as plugins.omega.fast_Zplus_assoc_reverse. -Register fast_Zplus_assoc as plugins.omega.fast_Zplus_assoc. -Register fast_Zmult_assoc_reverse as plugins.omega.fast_Zmult_assoc_reverse. -Register fast_Zplus_permute as plugins.omega.fast_Zplus_permute. -Register fast_Zplus_comm as plugins.omega.fast_Zplus_comm. -Register fast_Zmult_comm as plugins.omega.fast_Zmult_comm. - -Register OMEGA1 as plugins.omega.OMEGA1. -Register OMEGA2 as plugins.omega.OMEGA2. -Register OMEGA3 as plugins.omega.OMEGA3. -Register OMEGA4 as plugins.omega.OMEGA4. -Register OMEGA5 as plugins.omega.OMEGA5. -Register OMEGA6 as plugins.omega.OMEGA6. -Register OMEGA7 as plugins.omega.OMEGA7. -Register OMEGA8 as plugins.omega.OMEGA8. -Register OMEGA9 as plugins.omega.OMEGA9. -Register fast_OMEGA10 as plugins.omega.fast_OMEGA10. -Register fast_OMEGA11 as plugins.omega.fast_OMEGA11. -Register fast_OMEGA12 as plugins.omega.fast_OMEGA12. -Register fast_OMEGA13 as plugins.omega.fast_OMEGA13. -Register fast_OMEGA14 as plugins.omega.fast_OMEGA14. -Register fast_OMEGA15 as plugins.omega.fast_OMEGA15. -Register fast_OMEGA16 as plugins.omega.fast_OMEGA16. -Register OMEGA17 as plugins.omega.OMEGA17. -Register OMEGA18 as plugins.omega.OMEGA18. -Register OMEGA19 as plugins.omega.OMEGA19. -Register OMEGA20 as plugins.omega.OMEGA20. - -Register fast_Zred_factor0 as plugins.omega.fast_Zred_factor0. -Register fast_Zred_factor1 as plugins.omega.fast_Zred_factor1. -Register fast_Zred_factor2 as plugins.omega.fast_Zred_factor2. -Register fast_Zred_factor3 as plugins.omega.fast_Zred_factor3. -Register fast_Zred_factor4 as plugins.omega.fast_Zred_factor4. -Register fast_Zred_factor5 as plugins.omega.fast_Zred_factor5. -Register fast_Zred_factor6 as plugins.omega.fast_Zred_factor6. - -Register fast_Zmult_plus_distr_l as plugins.omega.fast_Zmult_plus_distr_l. -Register fast_Zopp_plus_distr as plugins.omega.fast_Zopp_plus_distr. -Register fast_Zopp_mult_distr_r as plugins.omega.fast_Zopp_mult_distr_r. -Register fast_Zopp_eq_mult_neg_1 as plugins.omega.fast_Zopp_eq_mult_neg_1. - -Register new_var as plugins.omega.new_var. -Register intro_Z as plugins.omega.intro_Z. diff --git a/theories/omega/OmegaPlugin.v b/theories/omega/OmegaPlugin.v deleted file mode 100644 index e0cf24f6aa..0000000000 --- a/theories/omega/OmegaPlugin.v +++ /dev/null @@ -1,17 +0,0 @@ -(************************************************************************) -(* * 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) *) -(************************************************************************) - -(* To strictly import the omega tactic *) - -Require ZArith_base. -Require OmegaLemmas. -Require PreOmega. - -Declare ML Module "omega_plugin". diff --git a/theories/omega/OmegaTactic.v b/theories/omega/OmegaTactic.v deleted file mode 100644 index e0cf24f6aa..0000000000 --- a/theories/omega/OmegaTactic.v +++ /dev/null @@ -1,17 +0,0 @@ -(************************************************************************) -(* * 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) *) -(************************************************************************) - -(* To strictly import the omega tactic *) - -Require ZArith_base. -Require OmegaLemmas. -Require PreOmega. - -Declare ML Module "omega_plugin". diff --git a/theories/omega/PreOmega.v b/theories/omega/PreOmega.v index 70f25e7243..bf873785d0 100644 --- a/theories/omega/PreOmega.v +++ b/theories/omega/PreOmega.v @@ -12,9 +12,10 @@ Require Import Arith Max Min BinInt BinNat Znat Nnat. Local Open Scope Z_scope. -(** * [Z.div_mod_to_equations], [Z.quot_rem_to_equations], [Z.to_euclidean_division_equations]: the tactics for preprocessing [Z.div] and [Z.modulo], [Z.quot] and [Z.rem] *) +(** * [Z.div_mod_to_equations], [Z.quot_rem_to_equations], [Z.to_euclidean_division_equations]: + the tactics for preprocessing [Z.div] and [Z.modulo], [Z.quot] and [Z.rem] *) -(** These tactic use the complete specification of [Z.div] and +(** These tactics use the complete specification of [Z.div] and [Z.modulo] ([Z.quot] and [Z.rem], respectively) to remove these functions from the goal without losing information. The [Z.euclidean_division_equations_cleanup] tactic removes needless @@ -127,449 +128,6 @@ Module Z. Ltac to_euclidean_division_equations := div_mod_to_equations'; quot_rem_to_equations'; euclidean_division_equations_cleanup. End Z. -Set Warnings "-deprecated-tactic". - -(** * zify: the Z-ification tactic *) - -(* This tactic searches for nat and N and positive elements in the goal and - translates everything into Z. It is meant as a pre-processor for - (r)omega; for instance a positivity hypothesis is added whenever - - a multiplication is encountered - - an atom is encountered (that is a variable or an unknown construct) - - Recognized relations (can be handled as deeply as allowed by setoid rewrite): - - { eq, le, lt, ge, gt } on { Z, positive, N, nat } - - Recognized operations: - - on Z: Z.min, Z.max, Z.abs, Z.sgn are translated in term of <= < = - - on nat: + * - S O pred min max Pos.to_nat N.to_nat Z.abs_nat - - on positive: Zneg Zpos xI xO xH + * - Pos.succ Pos.pred Pos.min Pos.max Pos.of_succ_nat - - on N: N0 Npos + * - N.pred N.succ N.min N.max N.of_nat Z.abs_N -*) - - - - -(** I) translation of Z.max, Z.min, Z.abs, Z.sgn into recognized equations *) - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_unop_core t thm a := - (* Let's introduce the specification theorem for t *) - pose proof (thm a); - (* Then we replace (t a) everywhere with a fresh variable *) - let z := fresh "z" in set (z:=t a) in *; clearbody z. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_unop_var_or_term t thm a := - (* If a is a variable, no need for aliasing *) - let za := fresh "z" in - (rename a into za; rename za into a; zify_unop_core t thm a) || - (* Otherwise, a is a complex term: we alias it. *) - (remember a as za; zify_unop_core t thm za). - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_unop t thm a := - (* If a is a scalar, we can simply reduce the unop. *) - (* Note that simpl wasn't enough to reduce [Z.max 0 0] (#5439) *) - let isz := isZcst a in - match isz with - | true => - let u := eval compute in (t a) in - change (t a) with u in * - | _ => zify_unop_var_or_term t thm a - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_unop_nored t thm a := - (* in this version, we don't try to reduce the unop (that can be (Z.add x)) *) - let isz := isZcst a in - match isz with - | true => zify_unop_core t thm a - | _ => zify_unop_var_or_term t thm a - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_binop t thm a b:= - (* works as zify_unop, except that we should be careful when - dealing with b, since it can be equal to a *) - let isza := isZcst a in - match isza with - | true => zify_unop (t a) (thm a) b - | _ => - let za := fresh "z" in - (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) || - (remember a as za; match goal with - | H : za = b |- _ => zify_unop_nored (t za) (thm za) za - | _ => zify_unop_nored (t za) (thm za) b - end) - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_op_1 := - match goal with - | x := ?t : Z |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x - | |- context [ Z.max ?a ?b ] => zify_binop Z.max Z.max_spec a b - | H : context [ Z.max ?a ?b ] |- _ => zify_binop Z.max Z.max_spec a b - | |- context [ Z.min ?a ?b ] => zify_binop Z.min Z.min_spec a b - | H : context [ Z.min ?a ?b ] |- _ => zify_binop Z.min Z.min_spec a b - | |- context [ Z.sgn ?a ] => zify_unop Z.sgn Z.sgn_spec a - | H : context [ Z.sgn ?a ] |- _ => zify_unop Z.sgn Z.sgn_spec a - | |- context [ Z.abs ?a ] => zify_unop Z.abs Z.abs_spec a - | H : context [ Z.abs ?a ] |- _ => zify_unop Z.abs Z.abs_spec a - end. - -Ltac zify_op := repeat zify_op_1. - - -(** II) Conversion from nat to Z *) - - -Definition Z_of_nat' := Z.of_nat. - -Ltac hide_Z_of_nat t := - let z := fresh "z" in set (z:=Z.of_nat t) in *; - change Z.of_nat with Z_of_nat' in z; - unfold z in *; clear z. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_nat_rel := - match goal with - (* I: equalities *) - | x := ?t : nat |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x - | |- (@eq nat ?a ?b) => apply (Nat2Z.inj a b) (* shortcut *) - | H : context [ @eq nat ?a ?b ] |- _ => rewrite <- (Nat2Z.inj_iff a b) in H - | |- context [ @eq nat ?a ?b ] => rewrite <- (Nat2Z.inj_iff a b) - (* II: less than *) - | H : context [ lt ?a ?b ] |- _ => rewrite (Nat2Z.inj_lt a b) in H - | |- context [ lt ?a ?b ] => rewrite (Nat2Z.inj_lt a b) - (* III: less or equal *) - | H : context [ le ?a ?b ] |- _ => rewrite (Nat2Z.inj_le a b) in H - | |- context [ le ?a ?b ] => rewrite (Nat2Z.inj_le a b) - (* IV: greater than *) - | H : context [ gt ?a ?b ] |- _ => rewrite (Nat2Z.inj_gt a b) in H - | |- context [ gt ?a ?b ] => rewrite (Nat2Z.inj_gt a b) - (* V: greater or equal *) - | H : context [ ge ?a ?b ] |- _ => rewrite (Nat2Z.inj_ge a b) in H - | |- context [ ge ?a ?b ] => rewrite (Nat2Z.inj_ge a b) - end. - -Ltac zify_nat_op := - match goal with - (* misc type conversions: positive/N/Z to nat *) - | H : context [ Z.of_nat (Pos.to_nat ?a) ] |- _ => rewrite (positive_nat_Z a) in H - | |- context [ Z.of_nat (Pos.to_nat ?a) ] => rewrite (positive_nat_Z a) - | H : context [ Z.of_nat (N.to_nat ?a) ] |- _ => rewrite (N_nat_Z a) in H - | |- context [ Z.of_nat (N.to_nat ?a) ] => rewrite (N_nat_Z a) - | H : context [ Z.of_nat (Z.abs_nat ?a) ] |- _ => rewrite (Zabs2Nat.id_abs a) in H - | |- context [ Z.of_nat (Z.abs_nat ?a) ] => rewrite (Zabs2Nat.id_abs a) - - (* plus -> Z.add *) - | H : context [ Z.of_nat (plus ?a ?b) ] |- _ => rewrite (Nat2Z.inj_add a b) in H - | |- context [ Z.of_nat (plus ?a ?b) ] => rewrite (Nat2Z.inj_add a b) - - (* min -> Z.min *) - | H : context [ Z.of_nat (min ?a ?b) ] |- _ => rewrite (Nat2Z.inj_min a b) in H - | |- context [ Z.of_nat (min ?a ?b) ] => rewrite (Nat2Z.inj_min a b) - - (* max -> Z.max *) - | H : context [ Z.of_nat (max ?a ?b) ] |- _ => rewrite (Nat2Z.inj_max a b) in H - | |- context [ Z.of_nat (max ?a ?b) ] => rewrite (Nat2Z.inj_max a b) - - (* minus -> Z.max (Z.sub ... ...) 0 *) - | H : context [ Z.of_nat (minus ?a ?b) ] |- _ => rewrite (Nat2Z.inj_sub_max a b) in H - | |- context [ Z.of_nat (minus ?a ?b) ] => rewrite (Nat2Z.inj_sub_max a b) - - (* pred -> minus ... -1 -> Z.max (Z.sub ... -1) 0 *) - | H : context [ Z.of_nat (pred ?a) ] |- _ => rewrite (pred_of_minus a) in H - | |- context [ Z.of_nat (pred ?a) ] => rewrite (pred_of_minus a) - - (* mult -> Z.mul and a positivity hypothesis *) - | H : context [ Z.of_nat (mult ?a ?b) ] |- _ => - pose proof (Nat2Z.is_nonneg (mult a b)); - rewrite (Nat2Z.inj_mul a b) in * - | |- context [ Z.of_nat (mult ?a ?b) ] => - pose proof (Nat2Z.is_nonneg (mult a b)); - rewrite (Nat2Z.inj_mul a b) in * - - (* O -> Z0 *) - | H : context [ Z.of_nat O ] |- _ => change (Z.of_nat O) with Z0 in H - | |- context [ Z.of_nat O ] => change (Z.of_nat O) with Z0 - - (* S -> number or Z.succ *) - | H : context [ Z.of_nat (S ?a) ] |- _ => - let isnat := isnatcst a in - match isnat with - | true => - let t := eval compute in (Z.of_nat (S a)) in - change (Z.of_nat (S a)) with t in H - | _ => rewrite (Nat2Z.inj_succ a) in H - | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), - hide [Z.of_nat (S a)] in this one hypothesis *) - change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H - end - | |- context [ Z.of_nat (S ?a) ] => - let isnat := isnatcst a in - match isnat with - | true => - let t := eval compute in (Z.of_nat (S a)) in - change (Z.of_nat (S a)) with t - | _ => rewrite (Nat2Z.inj_succ a) - | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), - hide [Z.of_nat (S a)] in the goal *) - change (Z.of_nat (S a)) with (Z_of_nat' (S a)) - end - - (* atoms of type nat : we add a positivity condition (if not already there) *) - | _ : 0 <= Z.of_nat ?a |- _ => hide_Z_of_nat a - | _ : context [ Z.of_nat ?a ] |- _ => - pose proof (Nat2Z.is_nonneg a); hide_Z_of_nat a - | |- context [ Z.of_nat ?a ] => - pose proof (Nat2Z.is_nonneg a); hide_Z_of_nat a - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_nat := repeat zify_nat_rel; repeat zify_nat_op; unfold Z_of_nat' in *. - -(* III) conversion from positive to Z *) - -Definition Zpos' := Zpos. -Definition Zneg' := Zneg. - -Ltac hide_Zpos t := - let z := fresh "z" in set (z:=Zpos t) in *; - change Zpos with Zpos' in z; - unfold z in *; clear z. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_positive_rel := - match goal with - (* I: equalities *) - | x := ?t : positive |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x - | |- (@eq positive ?a ?b) => apply Pos2Z.inj - | H : context [ @eq positive ?a ?b ] |- _ => rewrite <- (Pos2Z.inj_iff a b) in H - | |- context [ @eq positive ?a ?b ] => rewrite <- (Pos2Z.inj_iff a b) - (* II: less than *) - | H : context [ (?a < ?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H - | |- context [ (?a < ?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b) - (* III: less or equal *) - | H : context [ (?a <= ?b)%positive ] |- _ => change (a<=b)%positive with (Zpos a<=Zpos b) in H - | |- context [ (?a <= ?b)%positive ] => change (a<=b)%positive with (Zpos a<=Zpos b) - (* IV: greater than *) - | H : context [ (?a > ?b)%positive ] |- _ => change (a>b)%positive with (Zpos a>Zpos b) in H - | |- context [ (?a > ?b)%positive ] => change (a>b)%positive with (Zpos a>Zpos b) - (* V: greater or equal *) - | H : context [ (?a >= ?b)%positive ] |- _ => change (a>=b)%positive with (Zpos a>=Zpos b) in H - | |- context [ (?a >= ?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b) - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_positive_op := - match goal with - (* Z.pow_pos -> Z.pow *) - | H : context [ Z.pow_pos ?a ?b ] |- _ => change (Z.pow_pos a b) with (Z.pow a (Z.pos b)) in H - | |- context [ Z.pow_pos ?a ?b ] => change (Z.pow_pos a b) with (Z.pow a (Z.pos b)) - (* Zneg -> -Zpos (except for numbers) *) - | H : context [ Zneg ?a ] |- _ => - let isp := isPcst a in - match isp with - | true => change (Zneg a) with (Zneg' a) in H - | _ => change (Zneg a) with (- Zpos a) in H - end - | |- context [ Zneg ?a ] => - let isp := isPcst a in - match isp with - | true => change (Zneg a) with (Zneg' a) - | _ => change (Zneg a) with (- Zpos a) - end - - (* misc type conversions: nat to positive *) - | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H - | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a) - - (* Z.power_pos *) - | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H - | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a) - - (* Pos.add -> Z.add *) - | H : context [ Zpos (?a + ?b) ] |- _ => change (Zpos (a+b)) with (Zpos a + Zpos b) in H - | |- context [ Zpos (?a + ?b) ] => change (Zpos (a+b)) with (Zpos a + Zpos b) - - (* Pos.min -> Z.min *) - | H : context [ Zpos (Pos.min ?a ?b) ] |- _ => rewrite (Pos2Z.inj_min a b) in H - | |- context [ Zpos (Pos.min ?a ?b) ] => rewrite (Pos2Z.inj_min a b) - - (* Pos.max -> Z.max *) - | H : context [ Zpos (Pos.max ?a ?b) ] |- _ => rewrite (Pos2Z.inj_max a b) in H - | |- context [ Zpos (Pos.max ?a ?b) ] => rewrite (Pos2Z.inj_max a b) - - (* Pos.sub -> Z.max 1 (Z.sub ... ...) *) - | H : context [ Zpos (Pos.sub ?a ?b) ] |- _ => rewrite (Pos2Z.inj_sub_max a b) in H - | |- context [ Zpos (Pos.sub ?a ?b) ] => rewrite (Pos2Z.inj_sub_max a b) - - (* Pos.succ -> Z.succ *) - | H : context [ Zpos (Pos.succ ?a) ] |- _ => rewrite (Pos2Z.inj_succ a) in H - | |- context [ Zpos (Pos.succ ?a) ] => rewrite (Pos2Z.inj_succ a) - - (* Pos.pred -> Pos.sub ... -1 -> Z.max 1 (Z.sub ... - 1) *) - | H : context [ Zpos (Pos.pred ?a) ] |- _ => rewrite <- (Pos.sub_1_r a) in H - | |- context [ Zpos (Pos.pred ?a) ] => rewrite <- (Pos.sub_1_r a) - - (* Pos.mul -> Z.mul and a positivity hypothesis *) - | H : context [ Zpos (?a * ?b) ] |- _ => - pose proof (Pos2Z.is_pos (Pos.mul a b)); - change (Zpos (a*b)) with (Zpos a * Zpos b) in * - | |- context [ Zpos (?a * ?b) ] => - pose proof (Pos2Z.is_pos (Pos.mul a b)); - change (Zpos (a*b)) with (Zpos a * Zpos b) in * - - (* xO *) - | H : context [ Zpos (xO ?a) ] |- _ => - let isp := isPcst a in - match isp with - | true => change (Zpos (xO a)) with (Zpos' (xO a)) in H - | _ => rewrite (Pos2Z.inj_xO a) in H - end - | |- context [ Zpos (xO ?a) ] => - let isp := isPcst a in - match isp with - | true => change (Zpos (xO a)) with (Zpos' (xO a)) - | _ => rewrite (Pos2Z.inj_xO a) - end - (* xI *) - | H : context [ Zpos (xI ?a) ] |- _ => - let isp := isPcst a in - match isp with - | true => change (Zpos (xI a)) with (Zpos' (xI a)) in H - | _ => rewrite (Pos2Z.inj_xI a) in H - end - | |- context [ Zpos (xI ?a) ] => - let isp := isPcst a in - match isp with - | true => change (Zpos (xI a)) with (Zpos' (xI a)) - | _ => rewrite (Pos2Z.inj_xI a) - end - - (* xI : nothing to do, just prevent adding a useless positivity condition *) - | H : context [ Zpos xH ] |- _ => hide_Zpos xH - | |- context [ Zpos xH ] => hide_Zpos xH - - (* atoms of type positive : we add a positivity condition (if not already there) *) - | _ : 0 < Zpos ?a |- _ => hide_Zpos a - | _ : context [ Zpos ?a ] |- _ => pose proof (Pos2Z.is_pos a); hide_Zpos a - | |- context [ Zpos ?a ] => pose proof (Pos2Z.is_pos a); hide_Zpos a - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_positive := - repeat zify_positive_rel; repeat zify_positive_op; unfold Zpos',Zneg' in *. - - - - - -(* IV) conversion from N to Z *) - -Definition Z_of_N' := Z.of_N. - -Ltac hide_Z_of_N t := - let z := fresh "z" in set (z:=Z.of_N t) in *; - change Z.of_N with Z_of_N' in z; - unfold z in *; clear z. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_N_rel := - match goal with - (* I: equalities *) - | x := ?t : N |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x - | |- (@eq N ?a ?b) => apply (N2Z.inj a b) (* shortcut *) - | H : context [ @eq N ?a ?b ] |- _ => rewrite <- (N2Z.inj_iff a b) in H - | |- context [ @eq N ?a ?b ] => rewrite <- (N2Z.inj_iff a b) - (* II: less than *) - | H : context [ (?a < ?b)%N ] |- _ => rewrite (N2Z.inj_lt a b) in H - | |- context [ (?a < ?b)%N ] => rewrite (N2Z.inj_lt a b) - (* III: less or equal *) - | H : context [ (?a <= ?b)%N ] |- _ => rewrite (N2Z.inj_le a b) in H - | |- context [ (?a <= ?b)%N ] => rewrite (N2Z.inj_le a b) - (* IV: greater than *) - | H : context [ (?a > ?b)%N ] |- _ => rewrite (N2Z.inj_gt a b) in H - | |- context [ (?a > ?b)%N ] => rewrite (N2Z.inj_gt a b) - (* V: greater or equal *) - | H : context [ (?a >= ?b)%N ] |- _ => rewrite (N2Z.inj_ge a b) in H - | |- context [ (?a >= ?b)%N ] => rewrite (N2Z.inj_ge a b) - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_N_op := - match goal with - (* misc type conversions: nat to positive *) - | H : context [ Z.of_N (N.of_nat ?a) ] |- _ => rewrite (nat_N_Z a) in H - | |- context [ Z.of_N (N.of_nat ?a) ] => rewrite (nat_N_Z a) - | H : context [ Z.of_N (Z.abs_N ?a) ] |- _ => rewrite (N2Z.inj_abs_N a) in H - | |- context [ Z.of_N (Z.abs_N ?a) ] => rewrite (N2Z.inj_abs_N a) - | H : context [ Z.of_N (Npos ?a) ] |- _ => rewrite (N2Z.inj_pos a) in H - | |- context [ Z.of_N (Npos ?a) ] => rewrite (N2Z.inj_pos a) - | H : context [ Z.of_N N0 ] |- _ => change (Z.of_N N0) with Z0 in H - | |- context [ Z.of_N N0 ] => change (Z.of_N N0) with Z0 - - (* N.add -> Z.add *) - | H : context [ Z.of_N (N.add ?a ?b) ] |- _ => rewrite (N2Z.inj_add a b) in H - | |- context [ Z.of_N (N.add ?a ?b) ] => rewrite (N2Z.inj_add a b) - - (* N.min -> Z.min *) - | H : context [ Z.of_N (N.min ?a ?b) ] |- _ => rewrite (N2Z.inj_min a b) in H - | |- context [ Z.of_N (N.min ?a ?b) ] => rewrite (N2Z.inj_min a b) - - (* N.max -> Z.max *) - | H : context [ Z.of_N (N.max ?a ?b) ] |- _ => rewrite (N2Z.inj_max a b) in H - | |- context [ Z.of_N (N.max ?a ?b) ] => rewrite (N2Z.inj_max a b) - - (* N.sub -> Z.max 0 (Z.sub ... ...) *) - | H : context [ Z.of_N (N.sub ?a ?b) ] |- _ => rewrite (N2Z.inj_sub_max a b) in H - | |- context [ Z.of_N (N.sub ?a ?b) ] => rewrite (N2Z.inj_sub_max a b) - - (* pred -> minus ... -1 -> Z.max (Z.sub ... -1) 0 *) - | H : context [ Z.of_N (N.pred ?a) ] |- _ => rewrite (N.pred_sub a) in H - | |- context [ Z.of_N (N.pred ?a) ] => rewrite (N.pred_sub a) - - (* N.succ -> Z.succ *) - | H : context [ Z.of_N (N.succ ?a) ] |- _ => rewrite (N2Z.inj_succ a) in H - | |- context [ Z.of_N (N.succ ?a) ] => rewrite (N2Z.inj_succ a) - - (* N.mul -> Z.mul and a positivity hypothesis *) - | H : context [ Z.of_N (N.mul ?a ?b) ] |- _ => - pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in * - | |- context [ Z.of_N (N.mul ?a ?b) ] => - pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in * - - (* N.div -> Z.div and a positivity hypothesis *) - | H : context [ Z.of_N (N.div ?a ?b) ] |- _ => - pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in * - | |- context [ Z.of_N (N.div ?a ?b) ] => - pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in * - - (* N.modulo -> Z.rem / Z.modulo and a positivity hypothesis (N.modulo agrees with Z.modulo on everything except 0; so we pose both the non-zero proof for this agreement, but also replace things with [Z.rem]) *) - | H : context [ Z.of_N (N.modulo ?a ?b) ] |- _ => - pose proof (N2Z.is_nonneg (N.modulo a b)); - pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); - pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); - rewrite (N2Z.inj_rem a b) in * - | |- context [ Z.of_N (N.div ?a ?b) ] => - pose proof (N2Z.is_nonneg (N.modulo a b)); - pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); - pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); - rewrite (N2Z.inj_rem a b) in * - - (* atoms of type N : we add a positivity condition (if not already there) *) - | _ : 0 <= Z.of_N ?a |- _ => hide_Z_of_N a - | _ : context [ Z.of_N ?a ] |- _ => pose proof (N2Z.is_nonneg a); hide_Z_of_N a - | |- context [ Z.of_N ?a ] => pose proof (N2Z.is_nonneg a); hide_Z_of_N a - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. - -(** The complete Z-ification tactic *) - Require Import ZifyClasses ZifyInst. Require Zify. |