SeqZ Function

This MR adds a simple range function on integers to stdpp. Calling range m n results in the range m, m + 1, ..., n - 1 and is empty, if m >= n.

How is this different from seq m (n-m)?

Oh I see, this is on Z and not on nat.

Hm, seems a bit annoying to have one be start len and the other start end.

I'll change it to the length, truncating if m - n < 0.

So, I guess we basically want is seqZ?

If we go that way, could you make sure that we have exactly the same lemmas as we have for seq?

As a general comment, please use unicode characters everywhere (e.g. → and ∀), and use <$> instead of map. Thanks :)

added 1 commit

• 42f9dbef - range -> seqZ function

Compare with previous version

I changed it to seqZ and updated the lemmas to match the seq ones.

added 1 commit

• 3d6ed210 - section with implicit types for seqZ

Compare with previous version

added 1 commit

• bfebb1e6 - Notation in seqZ definition

Compare with previous version

@robbertkrebbers what do you think?

resolved all discussions

added 1 commit

• 3887c4f7 - seqZ: rename, by, cbn -> simpl

Compare with previous version

@simonspies you can just mark discussions as resolved that you have dealt with. No need to trigger 15 notification emails with the same text. :)

added 1 commit

• 2b8d69bc - seqZ: move definition and use different length lemma

Compare with previous version

added 1 commit

• a370c21f - seqZ: rewrite by, seqZ_lookup_inv iff, case brackets

Compare with previous version

I was a bit annoyed by the clumsiness of the proofs using natlike_ind, and the fact that it doesn't work nicely with Coq's induction tactic. The following alternative induction principle appears to be quite nice:

Lemma Z_induction (P : Z → Prop) :
  P 0%Z →
  (∀ 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.

Using that, the proofs can be done using the induction tactic and without having to do case analyses before the induction:

Lemma seqZ_cons m n : 0 ≤ n → seqZ m (Z.succ n) = m :: seqZ (Z.succ m) n.
Proof.
  intros H. unfold seqZ. rewrite Z2Nat.inj_succ by done.
  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_induction; intros m'.
  - by rewrite seqZ_nil.
  - rewrite !seqZ_cons by lia. f_equal/=. rewrite IH. 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_induction; intros m i Hi; try lia.
  rewrite seqZ_cons by lia. destruct i as [|i]; simpl.
  - f_equal; lia.
  - rewrite 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_induction; intros m i Hi; try lia.
  - by rewrite seqZ_nil.
  - rewrite seqZ_cons by lia.
    destruct i as [|i]; simpl; [lia|]. by rewrite 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.

What do you think? If you like this, I think we should move Z_induction to numbers.v and give it a reasonable name.

On a related note, I don't quite like that we end up doing replace (Z.succ n - 1) with n all the time. So I rewrote seqZ_cons a bit.

The Z induction lemma is very nice. How about Z_from_zero_ind for the name?

As it generates goals containing Z.succ, your version of the seqZ_cons lemma works well if the Z_induction lemma is used. In the original version, it tried to find a formulation such that rewrite seqZ_cons is always possible instead of first replacing the argument with Z.succ ... and then rewriting. I don't have enough experience with Z to say anything about how often one encounters Z.succ. What do you think?

added 2 commits

• e23cc0c7 - seqZ comment, 80 char line width
• 7393911a - compact proofs using new induction lemma on Z

Compare with previous version

added 1 commit

• 89217996 - simplify proof of seqZ_cons

Compare with previous version

resolved all discussions

What do you think?

I think your version is better.

Z_from_zero_ind

Now that I think of it, the induction principle can actually be generalized to:

Lemma Z_from_zero_ind 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.

Contrary to Coq's Z.order_induction' (which has the Proper premise), this induction principle should be usable with the induction tactic.

So, Z_from_zero_ind is not the best name anymore :)

added 1 commit

• 162d4f32 - lt vs gt

Compare with previous version

added 1 commit

• 19950ecc - more general induction lemma

Compare with previous version

resolved all discussions