Skip to content
Snippets Groups Projects
Commit 6ac98356 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'kimaya/add-seq-lemmas' into 'master'

add lemmas about seq

See merge request !588
parents 0dbb3948 a9167769
No related branches found
No related tags found
1 merge request!588add lemmas about seq
Pipeline #117329 passed
......@@ -12,7 +12,8 @@ API-breaking change is listed.
- Rename `map_filter_empty_iff` to `map_empty_filter` and add
`map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler)
- Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`:
`length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
`length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
- Add `elem_of_seq` and `seq_nil`. (by Kimaya Bedarkar)
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
......
......@@ -98,6 +98,12 @@ Section seq.
k seq j n j k < j + n.
Proof. rewrite elem_of_list_In, in_seq. done. Qed.
Lemma seq_nil n m : seq n m = [] m = 0.
Proof. by destruct m. Qed.
Lemma seq_subseteq_mono m n1 n2 : n1 n2 seq m n1 seq m n2.
Proof. by intros Hle i Hi%elem_of_seq; apply elem_of_seq; lia. Qed.
Lemma Forall_seq (P : nat Prop) i n :
Forall P (seq i n) j, i j < i + n P j.
Proof. rewrite Forall_forall. setoid_rewrite elem_of_seq. auto with lia. Qed.
......@@ -118,6 +124,7 @@ Section seq.
- rewrite take_nil. replace (m `min` 0) with 0 by lia. done.
- destruct m; simpl; auto with f_equal.
Qed.
End seq.
(** ** Properties of the [seqZ] function *)
......
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