Skip to content
Snippets Groups Projects
Commit 40135869 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'ci/robbert/seq_S' into 'master'

Rename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlib

See merge request !212
parents 523920d1 d7732dcb
No related branches found
No related tags found
No related merge requests found
...@@ -40,7 +40,8 @@ Coq 8.8 and 8.9 are no longer supported. ...@@ -40,7 +40,8 @@ Coq 8.8 and 8.9 are no longer supported.
returns `"0"` for `N`, `Z`, and `nat`. returns `"0"` for `N`, `Z`, and `nat`.
- Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename - Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename
`map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake. `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.
- Rename `seq_S_end_app` to `seq_S_snoc`. - Rename `seq_S_end_app` to `seq_S`. (The lemma `seq_S` is also in Coq's stdlib
since Coq 8.12.)
The following `sed` script should perform most of the renaming The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`): (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
...@@ -57,7 +58,7 @@ s/\bQp_mult_plus_distr_l\b/Qp_mul_add_distr_r/g ...@@ -57,7 +58,7 @@ s/\bQp_mult_plus_distr_l\b/Qp_mul_add_distr_r/g
s/\bQp_mult_plus_distr_r\b/Qp_mul_add_distr_l/g s/\bQp_mult_plus_distr_r\b/Qp_mul_add_distr_l/g
s/\bmap_fmap_empty\b/fmap_empty/g s/\bmap_fmap_empty\b/fmap_empty/g
s/\bmap_fmap_empty_inv\b/fmap_empty_inv/g s/\bmap_fmap_empty_inv\b/fmap_empty_inv/g
s/\bseq_S_end_app\b/seq_S_snoc/g s/\bseq_S_end_app\b/seq_S/g
' $(find theories -name "*.v") ' $(find theories -name "*.v")
``` ```
......
...@@ -67,9 +67,10 @@ Section seq. ...@@ -67,9 +67,10 @@ Section seq.
Qed. Qed.
Lemma NoDup_seq j n : NoDup (seq j n). Lemma NoDup_seq j n : NoDup (seq j n).
Proof. apply NoDup_ListNoDup, seq_NoDup. Qed. Proof. apply NoDup_ListNoDup, seq_NoDup. Qed.
Lemma seq_S_snoc j n : seq j (S n) = seq j n ++ [j + n]. (* FIXME: This lemma is in the stdlib since Coq 8.12 *)
Lemma seq_S n j : seq j (S n) = seq j n ++ [j + n].
Proof. Proof.
revert j. induction n as [|n IH]; intros j; simpl in *; f_equal; [done |]. revert j. induction n as [|n IH]; intros j; f_equal/=; [done |].
by rewrite IH, Nat.add_succ_r. by rewrite IH, Nat.add_succ_r.
Qed. Qed.
...@@ -147,7 +148,8 @@ Section seqZ. ...@@ -147,7 +148,8 @@ Section seqZ.
Proof. Proof.
intros. unfold seqZ. rewrite Z2Nat.inj_add, seq_app, fmap_app by done. intros. unfold seqZ. rewrite Z2Nat.inj_add, seq_app, fmap_app by done.
f_equal. rewrite Nat.add_comm, <-!fmap_add_seq, <-list_fmap_compose. f_equal. rewrite Nat.add_comm, <-!fmap_add_seq, <-list_fmap_compose.
apply list_fmap_ext; naive_solver auto with lia. apply list_fmap_ext; [|done]; intros j; simpl.
rewrite Nat2Z.inj_add, Z2Nat.id by done. lia.
Qed. Qed.
Lemma seqZ_S m i : seqZ m (S i) = seqZ m i ++ [m + i]. Lemma seqZ_S m i : seqZ m (S i) = seqZ m i ++ [m + i].
...@@ -161,7 +163,7 @@ Section seqZ. ...@@ -161,7 +163,7 @@ Section seqZ.
Proof. Proof.
rewrite elem_of_list_lookup. rewrite elem_of_list_lookup.
setoid_rewrite lookup_seqZ. split; [naive_solver lia|]. setoid_rewrite lookup_seqZ. split; [naive_solver lia|].
exists (Z.to_nat (k - m)). lia. exists (Z.to_nat (k - m)). rewrite Z2Nat.id by lia. lia.
Qed. Qed.
Lemma Forall_seqZ (P : Z Prop) m n : Lemma Forall_seqZ (P : Z Prop) m n :
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment