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

Merge branch 'set-seq-lemmas' into 'master'

Add lemmas regarding set_seq

See merge request !105
parents e4aefeed 5998dbf4
No related branches found
No related tags found
1 merge request!105Add lemmas regarding set_seq
Pipeline #21134 passed
......@@ -1082,6 +1082,27 @@ Section set_seq.
SetUnfoldElemOf x (set_seq (C:=C) start len) (start x < start + len).
Proof. constructor; apply elem_of_set_seq. Qed.
Lemma set_seq_len_pos n start len : n set_seq (C:=C) start len 0 < len.
Proof. rewrite elem_of_set_seq. lia. Qed.
Lemma set_seq_subseteq start1 len1 start2 len2 :
0 < len1
set_seq (C:=C) start1 len1 set_seq (C:=C) start2 len2
start2 start1 start1 + len1 start2 + len2.
Proof.
intros Hlen. set_unfold. split.
- intros Hx. pose proof (Hx start1). pose proof (Hx (start1 + len1 - 1)). lia.
- intros Heq x. lia.
Qed.
Lemma set_seq_subseteq_len_gt start1 len1 start2 len2 :
set_seq (C:=C) start1 len1 set_seq (C:=C) start2 len2 len1 len2.
Proof.
destruct len1 as [|len1].
- set_unfold. lia.
- rewrite set_seq_subseteq; lia.
Qed.
Lemma set_seq_plus_disjoint start len1 len2 :
set_seq (C:=C) start len1 ## set_seq (start + len1) len2.
Proof. set_solver by lia. Qed.
......
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