(* Copyright (c) 2012-2013, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects some trivial facts on the Coq types [nat] and [N] for natural numbers, and the type [Z] for integers. It also declares some useful notations. *) Require Export PArith NArith ZArith. Require Import Qcanon. Require Export base decidable. Open Scope nat_scope. Coercion Z.of_nat : nat >-> Z. (** * Notations and properties of [nat] *) Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level). Reserved Notation "x ≤ y < z" (at level 70, y at next level). Reserved Notation "x < y < z" (at level 70, y at next level). Reserved Notation "x < y ≤ z" (at level 70, y at next level). Infix "≤" := le : nat_scope. Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%nat : nat_scope. Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%nat : nat_scope. Notation "x < y < z" := (x < y ∧ y < z)%nat : nat_scope. Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%nat : nat_scope. Notation "(≤)" := le (only parsing) : nat_scope. Notation "(<)" := lt (only parsing) : nat_scope. Infix "`div`" := NPeano.div (at level 35) : nat_scope. Infix "`mod`" := NPeano.modulo (at level 35) : nat_scope. Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec. Instance nat_le_dec: ∀ x y : nat, Decision (x ≤ y) := le_dec. Instance nat_lt_dec: ∀ x y : nat, Decision (x < y) := lt_dec. Instance nat_inhabited: Inhabited nat := populate 0%nat. Lemma lt_n_SS n : n < S (S n). Proof. auto with arith. Qed. Lemma lt_n_SSS n : n < S (S (S n)). Proof. auto with arith. Qed. Definition sum_list_with {A} (f : A → nat) : list A → nat := fix go l := match l with | [] => 0 | x :: l => f x + go l end. Notation sum_list := (sum_list_with id). (** * Notations and properties of [positive] *) Open Scope positive_scope. Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec. Instance positive_inhabited: Inhabited positive := populate 1. Notation "(~0)" := xO (only parsing) : positive_scope. Notation "(~1)" := xI (only parsing) : positive_scope. Instance: Injective (=) (=) (~0). Proof. by injection 1. Qed. Instance: Injective (=) (=) (~1). Proof. by injection 1. Qed. (** Since [positive] represents lists of bits, we define list operations on it. These operations are in reverse, as positives are treated as snoc lists instead of cons lists. *) Fixpoint Papp (p1 p2 : positive) : positive := match p2 with | 1 => p1 | p2~0 => (Papp p1 p2)~0 | p2~1 => (Papp p1 p2)~1 end. Infix "++" := Papp : positive_scope. Notation "(++)" := Papp (only parsing) : positive_scope. Notation "( p ++)" := (Papp p) (only parsing) : positive_scope. Notation "(++ q )" := (λ p, Papp p q) (only parsing) : positive_scope. Fixpoint Preverse_go (p1 p2 : positive) : positive := match p2 with | 1 => p1 | p2~0 => Preverse_go (p1~0) p2 | p2~1 => Preverse_go (p1~1) p2 end. Definition Preverse : positive → positive := Preverse_go 1. Global Instance: LeftId (=) 1 (++). Proof. intros p. induction p; simpl; intros; f_equal; auto. Qed. Global Instance: RightId (=) 1 (++). Proof. done. Qed. Global Instance: Associative (=) (++). Proof. intros ?? p. induction p; simpl; intros; f_equal; auto. Qed. Global Instance: ∀ p : positive, Injective (=) (=) (++ p). Proof. intros p ???. induction p; simplify_equality; auto. Qed. Lemma Preverse_go_app_cont p1 p2 p3 : Preverse_go (p2 ++ p1) p3 = p2 ++ Preverse_go p1 p3. Proof. revert p1. induction p3; simpl; intros. * apply (IHp3 (_~1)). * apply (IHp3 (_~0)). * done. Qed. Lemma Preverse_go_app p1 p2 p3 : Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2. Proof. revert p1. induction p3; intros p1; simpl; auto. by rewrite <-Preverse_go_app_cont. Qed. Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1. Proof. unfold Preverse. by rewrite Preverse_go_app. Qed. Lemma Preverse_xO p : Preverse (p~0) = (1~0) ++ Preverse p. Proof Preverse_app p (1~0). Lemma Preverse_xI p : Preverse (p~1) = (1~1) ++ Preverse p. Proof Preverse_app p (1~1). Fixpoint Plength (p : positive) : nat := match p with | 1 => 0%nat | p~0 | p~1 => S (Plength p) end. Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat. Proof. induction p2; simpl; f_equal; auto. Qed. Close Scope positive_scope. (** * Notations and properties of [N] *) Infix "≤" := N.le : N_scope. Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%N : N_scope. Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%N : N_scope. Notation "x < y < z" := (x < y ∧ y < z)%N : N_scope. Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%N : N_scope. Notation "(≤)" := N.le (only parsing) : N_scope. Notation "(<)" := N.lt (only parsing) : N_scope. Infix "`div`" := N.div (at level 35) : N_scope. Infix "`mod`" := N.modulo (at level 35) : N_scope. Instance: Injective (=) (=) Npos. Proof. by injection 1. Qed. Instance N_eq_dec: ∀ x y : N, Decision (x = y) := N.eq_dec. Program Instance N_le_dec (x y : N) : Decision (x ≤ y)%N := match Ncompare x y with | Gt => right _ | _ => left _ end. Next Obligation. congruence. Qed. Program Instance N_lt_dec (x y : N) : Decision (x < y)%N := match Ncompare x y with | Lt => left _ | _ => right _ end. Next Obligation. congruence. Qed. Instance N_inhabited: Inhabited N := populate 1%N. (** * Notations and properties of [Z] *) Infix "≤" := Z.le : Z_scope. Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%Z : Z_scope. Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%Z : Z_scope. Notation "x < y < z" := (x < y ∧ y < z)%Z : Z_scope. Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%Z : Z_scope. Notation "(≤)" := Z.le (only parsing) : Z_scope. Notation "(<)" := Z.lt (only parsing) : Z_scope. Infix "`div`" := Z.div (at level 35) : Z_scope. Infix "`mod`" := Z.modulo (at level 35) : Z_scope. Infix "`quot`" := Z.quot (at level 35) : Z_scope. Infix "`rem`" := Z.rem (at level 35) : Z_scope. Instance Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec. Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y)%Z := Z_le_dec. Instance Z_lt_dec: ∀ x y : Z, Decision (x < y)%Z := Z_lt_dec. Instance Z_inhabited: Inhabited Z := populate 1%Z. (* Note that we cannot disable simpl for [Z.of_nat] as that would break [omega] and [lia]. *) Arguments Z.to_nat _ : simpl never. Arguments Z.mul _ _ : simpl never. Arguments Z.add _ _ : simpl never. Arguments Z.opp _ : simpl never. Arguments Z.pow _ _ : simpl never. Arguments Z.div _ _ : simpl never. Arguments Z.modulo _ _ : simpl never. Arguments Z.quot _ _ : simpl never. Arguments Z.rem _ _ : simpl never. (** * Notations and properties of [Qc] *) Notation "2" := (1+1)%Qc : Qc_scope. Infix "≤" := Qcle : Qc_scope. Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%Qc : Qc_scope. Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%Qc : Qc_scope. Notation "x < y < z" := (x < y ∧ y < z)%Qc : Qc_scope. Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%Qc : Qc_scope. Notation "(≤)" := Qcle (only parsing) : Qc_scope. Notation "(<)" := Qclt (only parsing) : Qc_scope. Instance Qc_eq_dec: ∀ x y : Qc, Decision (x = y) := Qc_eq_dec. Program Instance Qc_le_dec (x y : Qc) : Decision (x ≤ y)%Qc := if Qclt_le_dec y x then right _ else left _. Next Obligation. by apply Qclt_not_le. Qed. Program Instance Qc_lt_dec (x y : Qc) : Decision (x < y)%Qc := if Qclt_le_dec x y then left _ else right _. Next Obligation. by apply Qcle_not_lt. Qed. Instance: Reflexive Qcle. Proof. red. apply Qcle_refl. Qed. Instance: Transitive Qcle. Proof. red. apply Qcle_trans. Qed. Lemma Qcle_ngt (x y : Qc) : (x ≤ y ↔ ¬y < x)%Qc. Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed. Lemma Qclt_nge (x y : Qc) : (x < y ↔ ¬y ≤ x)%Qc. Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed. Lemma Qcplus_le_mono_l (x y z : Qc) : (x ≤ y ↔ z + x ≤ z + y)%Qc. Proof. split; intros. * by apply Qcplus_le_compat. * replace x with ((0 - z) + (z + x))%Qc by ring. replace y with ((0 - z) + (z + y))%Qc by ring. by apply Qcplus_le_compat. Qed. Lemma Qcplus_le_mono_r (x y z : Qc) : (x ≤ y ↔ x + z ≤ y + z)%Qc. Proof. rewrite !(Qcplus_comm _ z). apply Qcplus_le_mono_l. Qed. Lemma Qcplus_lt_mono_l (x y z : Qc) : (x < y ↔ z + x < z + y)%Qc. Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed. Lemma Qcplus_lt_mono_r (x y z : Qc) : (x < y ↔ x + z < y + z)%Qc. Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed. (** * Conversions *) (** The function [Z_to_option_N] converts an integer [x] into a natural number by giving [None] in case [x] is negative. *) Definition Z_to_option_N (x : Z) : option N := match x with | Z0 => Some N0 | Zpos p => Some (Npos p) | Zneg _ => None end. Definition Z_to_option_nat (x : Z) : option nat := match x with | Z0 => Some 0 | Zpos p => Some (Pos.to_nat p) | Zneg _ => None end. Lemma Z_to_option_N_Some x y : Z_to_option_N x = Some y ↔ (0 ≤ x)%Z ∧ y = Z.to_N x. Proof. split. * intros. by destruct x; simpl in *; simplify_equality; auto using Zle_0_pos. * intros [??]. subst. destruct x; simpl; auto; lia. Qed. Lemma Z_to_option_N_Some_alt x y : Z_to_option_N x = Some y ↔ (0 ≤ x)%Z ∧ x = Z.of_N y. Proof. rewrite Z_to_option_N_Some. split; intros [??]; subst; auto using N2Z.id, Z2N.id, eq_sym. Qed. Lemma Z_to_option_nat_Some x y : Z_to_option_nat x = Some y ↔ (0 ≤ x)%Z ∧ y = Z.to_nat x. Proof. split. * intros. by destruct x; simpl in *; simplify_equality; auto using Zle_0_pos. * intros [??]. subst. destruct x; simpl; auto; lia. Qed. Lemma Z_to_option_nat_Some_alt x y : Z_to_option_nat x = Some y ↔ (0 ≤ x)%Z ∧ x = Z.of_nat y. Proof. rewrite Z_to_option_nat_Some. split; intros [??]; subst; auto using Nat2Z.id, Z2Nat.id, eq_sym. Qed. Lemma Z_to_option_of_nat x : Z_to_option_nat (Z.of_nat x) = Some x. Proof. apply Z_to_option_nat_Some_alt. auto using Nat2Z.is_nonneg. Qed. (** The function [Z_of_sumbool] converts a sumbool [P] into an integer by yielding one if [P] and zero if [Q]. *) Definition Z_of_sumbool {P Q : Prop} (p : {P} + {Q}) : Z := (if p then 1 else 0)%Z. (** Some correspondence lemmas between [nat] and [N] that are not part of the standard library. We declare a hint database [natify] to rewrite a goal involving [N] into a corresponding variant involving [nat]. *) Lemma N_to_nat_lt x y : N.to_nat x < N.to_nat y ↔ (x < y)%N. Proof. by rewrite <-N.compare_lt_iff, nat_compare_lt, N2Nat.inj_compare. Qed. Lemma N_to_nat_le x y : N.to_nat x ≤ N.to_nat y ↔ (x ≤ y)%N. Proof. by rewrite <-N.compare_le_iff, nat_compare_le, N2Nat.inj_compare. Qed. Lemma N_to_nat_0 : N.to_nat 0 = 0. Proof. done. Qed. Lemma N_to_nat_1 : N.to_nat 1 = 1. Proof. done. Qed. Lemma N_to_nat_div x y : N.to_nat (x `div` y) = N.to_nat x `div` N.to_nat y. Proof. destruct (decide (y = 0%N)). { subst. by destruct x. } apply NPeano.Nat.div_unique with (N.to_nat (x `mod` y)). { by apply N_to_nat_lt, N.mod_lt. } rewrite (N.div_unique_exact (x * y) y x), N.div_mul by lia. by rewrite <-N2Nat.inj_mul, <-N2Nat.inj_add, <-N.div_mod. Qed. (* We have [x `mod` 0 = 0] on [nat], and [x `mod` 0 = x] on [N]. *) Lemma N_to_nat_mod x y : y ≠ 0%N → N.to_nat (x `mod` y) = N.to_nat x `mod` N.to_nat y. Proof. intros. apply NPeano.Nat.mod_unique with (N.to_nat (x `div` y)). { by apply N_to_nat_lt, N.mod_lt. } rewrite (N.div_unique_exact (x * y) y x), N.div_mul by lia. by rewrite <-N2Nat.inj_mul, <-N2Nat.inj_add, <-N.div_mod. Qed. Hint Rewrite <-N2Nat.inj_iff : natify. Hint Rewrite <-N_to_nat_lt : natify. Hint Rewrite <-N_to_nat_le : natify. Hint Rewrite Nat2N.id : natify. Hint Rewrite N2Nat.inj_add : natify. Hint Rewrite N2Nat.inj_mul : natify. Hint Rewrite N2Nat.inj_sub : natify. Hint Rewrite N2Nat.inj_succ : natify. Hint Rewrite N2Nat.inj_pred : natify. Hint Rewrite N_to_nat_div : natify. Hint Rewrite N_to_nat_0 : natify. Hint Rewrite N_to_nat_1 : natify. Ltac natify := repeat autorewrite with natify in *. Hint Extern 100 (Nlt _ _) => natify : natify. Hint Extern 100 (Nle _ _) => natify : natify. Hint Extern 100 (@eq N _ _) => natify : natify. Hint Extern 100 (lt _ _) => natify : natify. Hint Extern 100 (le _ _) => natify : natify. Hint Extern 100 (@eq nat _ _) => natify : natify. Instance: ∀ x, PropHolds (0 < x)%N → PropHolds (0 < N.to_nat x). Proof. unfold PropHolds. intros. by natify. Qed. Instance: ∀ x, PropHolds (0 ≤ x)%N → PropHolds (0 ≤ N.to_nat x). Proof. unfold PropHolds. intros. by natify. Qed.