Commit 3887c4f7 by Simon Spies

### seqZ: rename, by, cbn -> simpl

parent bfebb1e6
Pipeline #17999 canceled with stage
 ... @@ -396,11 +396,9 @@ Definition positives_unflatten (p : positive) : option (list positive) := ... @@ -396,11 +396,9 @@ Definition positives_unflatten (p : positive) : option (list positive) := (** [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. **) (** [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 := (λ x: nat, Z.add x m) <\$> (seq 0 (Z.to_nat len)). Definition seqZ (m len: Z) : list Z := (λ i: nat, Z.add i m) <\$> (seq 0 (Z.to_nat len)). Arguments seqZ : simpl never. Arguments seqZ : simpl never. (** * Basic tactics on lists *) (** * Basic tactics on lists *) (** The tactic [discriminate_list] discharges a goal if it submseteq (** The tactic [discriminate_list] discharges a goal if it submseteq a list equality involving [(::)] and [(++)] of two lists that have a different a list equality involving [(::)] and [(++)] of two lists that have a different ... @@ -1470,63 +1468,63 @@ Qed. ... @@ -1470,63 +1468,63 @@ Qed. (** ** Properties of the [seqZ] function *) (** ** Properties of the [seqZ] function *) Section seqZ. Section seqZ. Implicit Types (m n : Z) (i j: nat). Implicit Types (m n : Z) (i j: nat). Open Scope Z. Local Open Scope Z. Lemma empty_seqZ m n: n ≤ 0 → seqZ m n = []. Lemma seqZ_nil m n: n ≤ 0 → seqZ m n = []. Proof. intros H; destruct n; cbn; eauto; lia. Qed. Proof. intros H; destruct n; simpl; eauto; lia. Qed. Lemma step_seqZ m n: n > 0 → seqZ m n = m :: seqZ (m + 1) (n - 1). Lemma seqZ_cons m n: n > 0 → seqZ m n = m :: seqZ (m + 1) (n - 1). Proof. Proof. intros H. unfold seqZ. intros H. unfold seqZ. replace (Z.to_nat n) with (S (Z.to_nat (n - 1))) by replace (Z.to_nat n) with (S (Z.to_nat (n - 1))) by (rewrite <-Z2Nat.inj_succ; [f_equal|]; lia). (rewrite <-Z2Nat.inj_succ; [f_equal|]; lia). cbn; f_equal; try lia. simpl; f_equal; try lia. erewrite <-fmap_seq, map_map, map_ext; eauto. erewrite <-fmap_seq, map_map, map_ext; eauto. intros; lia. intros; lia. Qed. Qed. Lemma length_seqZ m n: length (seqZ m n) = Z.to_nat n. Lemma seqZ_length m n: length (seqZ m n) = Z.to_nat n. Proof. Proof. unfold seqZ; now rewrite map_length, seq_length. unfold seqZ; by rewrite map_length, seq_length. Qed. Qed. Lemma fmap_seqZ m m' n: (Z.add m) <\$> seqZ m' n = seqZ (m + m') n. Lemma seqZ_fmap m m' n: Z.add m <\$> seqZ m' n = seqZ (m + m') n. Proof. Proof. assert (0 ≤ n ∨ n < 0) as [H|H] by lia. assert (0 ≤ n ∨ n < 0) as [H|H] by lia. - revert m'. pattern n. eapply natlike_ind; auto; clear n H. - revert m'. pattern n. eapply natlike_ind; auto; clear n H. intros n H1 IH j. rewrite step_seqZ; try lia. intros n H1 IH j. rewrite seqZ_cons; try lia. symmetry. rewrite step_seqZ; try lia. symmetry. rewrite seqZ_cons; try lia. replace (Z.succ n - 1) with n by lia. replace (Z.succ n - 1) with n by lia. cbn; rewrite IH. simpl; rewrite IH. f_equal; try lia; f_equal; lia. f_equal; try lia; f_equal; lia. - rewrite !empty_seqZ; auto; lia. - rewrite !seqZ_nil; auto; lia. Qed. Qed. Lemma lookup_seqZ m n i: i < n → seqZ m n !! i = Some (m + i). Lemma seqZ_lookup m n i: i < n → seqZ m n !! i = Some (m + i). Proof. Proof. assert (0 ≤ n ∨ n < 0) as [H|H] by lia. assert (0 ≤ n ∨ n < 0) as [H|H] by lia. - revert m i. pattern n. eapply natlike_ind; auto; clear n H. - revert m i. pattern n. eapply natlike_ind; auto; clear n H. intros; lia. intros; lia. intros n H1 IH. intros j [|i] ?; rewrite step_seqZ. 2, 4: lia. intros n H1 IH. intros j [|i] ?; rewrite seqZ_cons. 2, 4: lia. cbn; f_equal; lia. replace (Z.succ n - 1) with n by lia. simpl; f_equal; lia. replace (Z.succ n - 1) with n by lia. cbn; rewrite IH; f_equal; lia. simpl; rewrite IH; f_equal; lia. - rewrite !empty_seqZ; auto; lia. - rewrite !seqZ_nil; auto; lia. Qed. Qed. Lemma lookup_seqZ_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. Proof. assert (0 ≤ n ∨ n < 0) as [H|H] by lia. assert (0 ≤ n ∨ n < 0) as [H|H] by lia. - revert m i. pattern n. eapply natlike_ind; auto; clear n H. - revert m i. pattern n. eapply natlike_ind; auto; clear n H. intros n H1 IH. intros j [|i] ?; rewrite step_seqZ. 2, 4: lia. intros n H1 IH. intros j [|i] ?; rewrite seqZ_cons. 2, 4: lia. cbn; f_equal; lia. replace (Z.succ n - 1) with n by lia. simpl; f_equal; lia. replace (Z.succ n - 1) with n by lia. cbn; rewrite IH; f_equal; lia. simpl; rewrite IH; f_equal; lia. - rewrite !empty_seqZ; auto; lia. - rewrite !seqZ_nil; auto; lia. Qed. Qed. Lemma lookup_seqZ_inv m n i m' : seqZ m n !! i = Some m' → m' = m + i ∧ i < n. Lemma seqZ_lookup_inv m n i m' : seqZ m n !! i = Some m' → m' = m + i ∧ i < n. Proof. Proof. destruct (Z_le_gt_dec n i); [by rewrite lookup_seqZ_ge|]. destruct (Z_le_gt_dec n i); [by rewrite seqZ_lookup_ge|]. rewrite lookup_seqZ by lia. intuition; [congruence|lia]. rewrite seqZ_lookup by lia. intuition; [congruence|lia]. Qed. Qed. End seqZ. End seqZ. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!