From 7393911a03edca2281013fd2f6c2e75d4b04f6ae Mon Sep 17 00:00:00 2001 From: Simon Spies Date: Thu, 27 Jun 2019 14:19:24 +0200 Subject: [PATCH] compact proofs using new induction lemma on Z --- theories/list.v | 66 ++++++++++++++++++---------------------------- theories/numbers.v | 7 +++++ 2 files changed, 32 insertions(+), 41 deletions(-) diff --git a/theories/list.v b/theories/list.v index 3055653..dd78fd2 100644 --- a/theories/list.v +++ b/theories/list.v @@ -3345,13 +3345,11 @@ End mapM. (** ** Properties of the [seqZ] function *) Section seqZ. - Implicit Types (m n : Z) (i j: nat). + Implicit Types (m n: Z) (i j: nat). Local Open Scope Z. - Lemma seqZ_nil m n: n ≤ 0 → seqZ m n = []. - Proof. intros H; destruct n; simpl; eauto; lia. Qed. - - Lemma seqZ_cons m n: n > 0 → seqZ m n = m :: seqZ (m + 1) (n - 1). + Proof. by destruct n. Qed. + Lemma seqZ_cons m n: n > 0 → seqZ m n = m :: seqZ (Z.succ m) (Z.pred n). Proof. intros H. unfold seqZ. replace (Z.to_nat n) with (S (Z.to_nat (n - 1))) by @@ -3360,52 +3358,38 @@ Section seqZ. erewrite <-fmap_seq, map_map, map_ext; eauto. intros; 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. - + 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. - assert (0 ≤ n ∨ n < 0) as [H|H] by lia. - - revert m'. pattern n. eapply natlike_ind; auto; clear n H. - intros n H1 IH j. rewrite seqZ_cons by lia. - symmetry. rewrite seqZ_cons by lia. - replace (Z.succ n - 1) with n by lia. - simpl; rewrite IH. - f_equal; try lia; f_equal; lia. - - rewrite !seqZ_nil; auto; lia. + revert m'. induction n as [|n ? IH|] using Z_from_zero_ind; 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 m n i: i < n → seqZ m n !! i = Some (m + i). + Lemma seqZ_lookup_lt m n i: i < n → seqZ m n !! i = Some (m + i). Proof. - assert (0 ≤ n ∨ n < 0) as [H|H] by lia. - - revert m i. pattern n. eapply natlike_ind; auto; clear n H. - { intros; lia. } - intros n H1 IH. intros j [|i] ?; rewrite seqZ_cons by lia. - { simpl; f_equal; lia. } - replace (Z.succ n - 1) with n by lia. - simpl; rewrite IH by lia; f_equal; lia. - - rewrite !seqZ_nil; auto; lia. + revert m i. + induction n as [|n ? IH|] using Z_from_zero_ind; 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. + Lemma seqZ_lookup_ge m n i : n ≤ i → seqZ m n !! i = None. Proof. - assert (0 ≤ n ∨ n < 0) as [H|H] by lia. - - revert m i. pattern n. eapply natlike_ind; auto; clear n H. - intros n H1 IH. intros j [|i] ?; rewrite seqZ_cons by lia. - { simpl; f_equal; lia. } - replace (Z.succ n - 1) with n by lia. - simpl; rewrite IH; f_equal; lia. - - rewrite !seqZ_nil; auto; lia. + revert m i. + induction n as [|n ? IH|] using Z_from_zero_ind; 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_inv m n i m' : seqZ m n !! i = Some m' ↔ m' = m + i ∧ i < n. + 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. split; [discriminate|lia]. } - rewrite seqZ_lookup by lia. intuition; [congruence|lia|congruence]. + { rewrite seqZ_lookup_ge by lia. naive_solver lia. } + rewrite seqZ_lookup_lt by lia. naive_solver lia. Qed. End seqZ. diff --git a/theories/numbers.v b/theories/numbers.v index 5959739..54e6ae0 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_from_zero_ind (P : Z → Prop) : + P 0 → + (∀ x, 0 ≤ x → P x → P (Z.succ x)) → + (∀ x, x ≤ 0 → P x → P (Z.pred x)) → + (∀ x, P x). +Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ 0). Qed. + Close Scope Z_scope. (** * Injectivity of casts *) -- 2.26.2