Skip to content
Snippets Groups Projects

add basic list functionality with Z-based indexing

Open Ralf Jung requested to merge ralf/listZ into master

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).

Edited by Ralf Jung

Merge request reports

Merge request pipeline #79542 passed

Merge request pipeline passed for 5e0eed6a

Approval is optional
Merge blocked: 2 checks failed
Unresolved discussions must be resolved.
Merge conflicts must be resolved.

Merge details

  • The source branch is 505 commits behind the target branch.
  • 12 commits and 1 merge commit will be added to master.
  • Source branch will be deleted.

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
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.
  • Comment on lines +94 to +99
    Author Owner

    These names are picked for consistency with the nat lemmas, but they don't make a ton of sense here. I don't understand why the ge is in the name at all, why are these not called lookup_None...?

  • Please register or sign in to reply
  • Ralf Jung added 2 commits

    added 2 commits

    • 5037bea2 - add basic list functionality with Z-based indexing
    • 6affda89 - add some seqZ lemmas

    Compare with previous version

  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
  • 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.
    • Author Owner

      Here I decided to change the names compared to the old lemmas. The new lemma names would also make sense for the old lemmas, but that would be a breaking change.

    • Please register or sign in to reply
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
  • 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.
    • Author Owner

      FWIW by today's standards I would expect a lemma of this name to look like seqZ m n !! i = if decide (0 ≤ i < n) then Some (m+i) else None. This lemma here is still just about the some case, and might be called lookupZ_seqZ_Some_iff?

    • Please register or sign in to reply
  • Ralf Jung changed the description

    changed the description

  • Ralf Jung added 4 commits

    added 4 commits

    • 70e42e01 - list: add some missing lemmas, and small fixes
    • 7201564e - add basic list functionality with Z-based indexing
    • 0b1115b8 - add some seqZ lemmas
    • 2c66c717 - add replicateZ and associated theory

    Compare with previous version

  • Ralf Jung
  • Ralf Jung mentioned in merge request !440 (merged)

    mentioned in merge request !440 (merged)

  • Ralf Jung added 3 commits

    added 3 commits

    • f88de74d - add basic list functionality with Z-based indexing
    • fc695004 - add some seqZ lemmas
    • 3cb4cff5 - add replicateZ and associated theory

    Compare with previous version

  • Ralf Jung added 3 commits

    added 3 commits

    • baf3ff3b - add basic list functionality with Z-based indexing
    • 79de48cd - add some seqZ lemmas
    • 6ae7c195 - add replicateZ and associated theory

    Compare with previous version

  • Ralf Jung added 1 commit

    added 1 commit

    Compare with previous version

  • Ralf Jung changed the description

    changed the description

  • Ralf Jung mentioned in merge request !441 (merged)

    mentioned in merge request !441 (merged)

  • Ralf Jung changed the description

    changed the description

  • Ralf Jung added 3 commits

    added 3 commits

    Compare with previous version

  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
  • 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.
    • Author Owner

      Another way to state this would be lookup_lookupZ : l !! n = l !! (Z.of_nat n) (i.e., also flipping the direction). In different contexts, one or the other direction makes more sense.

    • Please register or sign in to reply
  • Ralf Jung added 4 commits

    added 4 commits

    • d68c3d11 - add basic list functionality with Z-based indexing
    • 0e10ed64 - add some seqZ lemmas
    • 1b2e8f40 - add replicateZ and associated theory
    • c03ca765 - add Forall2

    Compare with previous version

  • Ralf Jung added 3 commits

    added 3 commits

    Compare with previous version

  • Ralf Jung mentioned in merge request iris!883

    mentioned in merge request iris!883

  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Please register or sign in to reply
    Loading