From e3c9027e1c54a59c9d9e66043541e6e4ef36ddb1 Mon Sep 17 00:00:00 2001 From: Simon Spies Date: Fri, 28 Jun 2019 07:41:32 +0200 Subject: [PATCH] SeqZ Function --- theories/list.v | 57 ++++++++++++++++++++++++++++++++++++++++++++++ theories/numbers.v | 7 ++++++ 2 files changed, 64 insertions(+) diff --git a/theories/list.v b/theories/list.v index c83aa15..0986c85 100644 --- a/theories/list.v +++ b/theories/list.v @@ -394,6 +394,13 @@ used by [positives_flatten]. *) Definition positives_unflatten (p : positive) : option (list positive) := positives_unflatten_go p [] 1. + +(** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1] +over integers, provided [n >= 0]. If n < 0, then the range is empty. **) +Definition seqZ (m len: Z) : list Z := + (λ i: nat, Z.add i m) <\$> (seq 0 (Z.to_nat len)). +Arguments seqZ : simpl never. + (** * Basic tactics on lists *) (** The tactic [discriminate_list] discharges a goal if it submseteq a list equality involving [(::)] and [(++)] of two lists that have a different @@ -1460,6 +1467,7 @@ Proof. rewrite lookup_seq by done. intuition congruence. Qed. + (** ** Properties of the [Permutation] predicate *) Lemma Permutation_nil l : l ≡ₚ [] ↔ l = []. Proof. split. by intro; apply Permutation_nil. by intros ->. Qed. @@ -3345,6 +3353,55 @@ Section mapM. Proof. eauto using mapM_fmap_Forall2_Some_inv, Forall2_true, mapM_length. Qed. End mapM. +(** ** Properties of the [seqZ] function *) +Section seqZ. + Implicit Types (m n: Z) (i j: nat). + Local Open Scope Z. + Lemma seqZ_nil m n: n ≤ 0 → seqZ m n = []. + Proof. by destruct n. Qed. + Lemma seqZ_cons m n: 0 < n → seqZ m n = m :: seqZ (Z.succ m) (Z.pred n). + Proof. + intros H. unfold seqZ. replace n with (Z.succ (Z.pred n)) at 1 by lia. + rewrite Z2Nat.inj_succ by lia. f_equal/=. + rewrite <-fmap_seq, <-list_fmap_compose. + apply map_ext; naive_solver lia. + Qed. + Lemma seqZ_length m n: length (seqZ m n) = Z.to_nat n. + Proof. unfold seqZ; by rewrite fmap_length, seq_length. Qed. + Lemma seqZ_fmap m m' n: Z.add m <\$> seqZ m' n = seqZ (m + m') n. + Proof. + revert m'. induction n as [|n ? IH|] using (Z_succ_pred_induction 0); intros m'. + - by rewrite seqZ_nil. + - rewrite (seqZ_cons m') by lia. rewrite (seqZ_cons (m + m')) by lia. + f_equal/=. rewrite Z.pred_succ, IH; simpl. f_equal; lia. + - by rewrite !seqZ_nil by lia. + Qed. + Lemma seqZ_lookup_lt m n i: i < n → seqZ m n !! i = Some (m + i). + Proof. + revert m i. + induction n as [|n ? IH|] using (Z_succ_pred_induction 0); intros m i Hi; try lia. + rewrite seqZ_cons by lia. destruct i as [|i]; simpl. + - f_equal; lia. + - rewrite Z.pred_succ, IH by lia. f_equal; lia. + Qed. + Lemma seqZ_lookup_ge m n i : n ≤ i → seqZ m n !! i = None. + Proof. + revert m i. + induction n as [|n ? IH|] using (Z_succ_pred_induction 0); intros m i Hi; try lia. + - by rewrite seqZ_nil. + - rewrite seqZ_cons by lia. + destruct i as [|i]; simpl; [lia|]. by rewrite Z.pred_succ, IH by lia. + - by rewrite seqZ_nil by lia. + Qed. + Lemma seqZ_lookup m n i m' : seqZ m n !! i = Some m' ↔ m' = m + i ∧ i < n. + Proof. + destruct (Z_le_gt_dec n i). + { rewrite seqZ_lookup_ge by lia. naive_solver lia. } + rewrite seqZ_lookup_lt by lia. naive_solver lia. + Qed. +End seqZ. + + (** ** Properties of the [permutations] function *) Section permutations. Context {A : Type}. diff --git a/theories/numbers.v b/theories/numbers.v index 5959739..f039f96 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -467,6 +467,13 @@ Proof. apply Nat.mod_bound_pos; lia. } by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod. Qed. +Lemma Z_succ_pred_induction y (P : Z → Prop) : + P y → + (∀ x, y ≤ x → P x → P (Z.succ x)) → + (∀ x, x ≤ y → P x → P (Z.pred x)) → + (∀ x, P x). +Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed. + Close Scope Z_scope. (** * Injectivity of casts *) -- 2.24.1