add basic list functionality with Z-based indexing
This starts the work on #108 by implementing insert
and index
for Z
as well as lengthZ
, takeZ
, dropZ
, and porting much of the associated theory.
I have not ported everything, e.g. the interactions with Forall3
, subseteq
, submseteq
, filter
, mask
are missing. Also there are more operations that would need a Z-based version, such as lookup_total
, alter
, delete
, inserts
, find
, imap
, imap2
, resize
, rotate
, rotate_take
, sublist_lookup
, sublist_alter
. There are also some tactics that will not handle these new operations and so might need adjustments or Z-based tactics: solve_length
, simplify_list_eq
.
Still I think this is a useful start that can serve as a foundation for later extensions. :)
Blocked on !441 (merged).
Merge request reports
Activity
added 1 commit
- 98810075 - add basic list functionality with Z-based indexing
- stdpp/listZ.v 0 → 100644
84 Qed. 85 Lemma lookupZ_lt_is_Some_1 l i : is_Some (l !! i) → 0 ≤ i < lengthZ l. 86 Proof. intros [??]; eauto using lookupZ_lt_Some. Qed. 87 Lemma lookupZ_lt_is_Some_2 l i : 0 ≤ i < lengthZ l → is_Some (l !! i). 88 Proof. 89 intros. rewrite lookupZ_eq, Z.to_onat_nonneg by lia. simpl. 90 apply lookup_lt_is_Some_2. lia. 91 Qed. 92 Lemma lookupZ_lt_is_Some l i : is_Some (l !! i) ↔ 0 ≤ i < lengthZ l. 93 Proof. split; auto using lookupZ_lt_is_Some_1, lookupZ_lt_is_Some_2. Qed. 94 Lemma lookupZ_ge_None l i : l !! i = None ↔ i < 0 ∨ lengthZ l ≤ i. 95 Proof. rewrite eq_None_not_Some, lookupZ_lt_is_Some. lia. Qed. 96 Lemma lookupZ_ge_None_1 l i : l !! i = None → i < 0 ∨ lengthZ l ≤ i. 97 Proof. by rewrite lookupZ_ge_None. Qed. 98 Lemma lookupZ_ge_None_2 l i : i < 0 ∨ lengthZ l ≤ i → l !! i = None. 99 Proof. by rewrite lookupZ_ge_None. Qed. added 2 commits
154 160 - rewrite lookup_seqZ_ge by lia. naive_solver lia. 155 161 - rewrite lookup_seqZ_lt by lia. naive_solver lia. 156 162 Qed. 163 164 Lemma lookupZ_seqZ_Some (m n i : Z) : 0 ≤ i < n → seqZ m n !! i = Some (m + i). 165 Proof. 166 rewrite lookupZ_eq. Z.case_to_onat; simpl. 2:lia. 167 intros. rewrite lookup_seqZ_lt by lia. f_equal. lia. 168 Qed. 169 Lemma lookupZ_seqZ_None (m n i : Z) : i < 0 ∨ n ≤ i → seqZ m n !! i = None. 154 160 - rewrite lookup_seqZ_ge by lia. naive_solver lia. 155 161 - rewrite lookup_seqZ_lt by lia. naive_solver lia. 156 162 Qed. 163 164 Lemma lookupZ_seqZ_Some (m n i : Z) : 0 ≤ i < n → seqZ m n !! i = Some (m + i). 165 Proof. 166 rewrite lookupZ_eq. Z.case_to_onat; simpl. 2:lia. 167 intros. rewrite lookup_seqZ_lt by lia. f_equal. lia. 168 Qed. 169 Lemma lookupZ_seqZ_None (m n i : Z) : i < 0 ∨ n ≤ i → seqZ m n !! i = None. 170 Proof. 171 rewrite lookupZ_eq. Z.case_to_onat; simpl. 2:done. 172 intros. apply lookup_seqZ_ge. lia. 173 Qed. 174 Lemma lookupZ_seqZ (m n i m' : Z) : seqZ m n !! i = Some m' ↔ m' = m + i ∧ 0 ≤ i < n. - Resolved by Robbert Krebbers
mentioned in merge request !440 (merged)
mentioned in merge request !441 (merged)
- stdpp/listZ.v 0 → 100644
36 37 (** * General theorems *) 38 Section general_properties. 39 Context {A : Type}. 40 Implicit Types x y z : A. 41 Implicit Types l : list A. 42 Implicit Types i j : Z. 43 44 Lemma lookupZ_eq l i : 45 l !! i = (Z.to_onat i) ≫= (λ m, l !! m). 46 Proof. done. Qed. 47 Lemma insertZ_eq l i x : 48 <[i:=x]> l = from_option (λ n, insert n x l) l (Z.to_onat i). 49 Proof. done. Qed. 50 51 Lemma lookupZ_of_nat l (n : nat) : l !! (Z.of_nat n) = l !! n. mentioned in merge request iris!883