Skip to content
Snippets Groups Projects

Added some lemmas about [sublist]

Open Jonas Kastberg requested to merge jihgfee/stdpp:sublist_lemmas into master
2 unresolved threads

Added some generally useful lemmas about the [sublist] function

Merge request reports

Members who can merge are allowed to add commits.

Merge request pipeline #71677 passed

Merge request pipeline passed for 4575401f

Ready to merge by members who can write to the target branch.
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • 987 987 intros; eapply elem_of_list_lookup_2.
    988 988 destruct (nth_lookup_or_length l i d); [done | by lia].
    989 989 Qed.
    990 Lemma elem_of_list_delete x i l :
    991 x delete i l x l.
    992 Proof.
  • Robbert Krebbers
  • Robbert Krebbers
    • Sorry for the very belated response.

      I think the results in this MR make sense. I think we're still missing many of these results for the other relations (suffix, prefix, submseteq, ⊆), and ideally we make sure 1.) they are all there and consistent 2.) they are proved for the version lowest in the hierarchy and then derive the other ones. But I think even if we do not do that know, this MR provides an improvement.

    • Author Contributor

      I finally got around to fixing the review feedback.

      We should make sure to come up with a list as you suggest. Maybe as a separate issue that one can then hack away at in increments.

    • Please register or sign in to reply
  • Jonas Kastberg resolved all threads

    resolved all threads

  • Jonas Kastberg added 1 commit

    added 1 commit

    • e8b54df1 - Resolved some review feedback

    Compare with previous version

  • Jonas Kastberg added 115 commits

    added 115 commits

    Compare with previous version

  • Jonas Kastberg added 1 commit

    added 1 commit

    Compare with previous version

  • Status: Robbert still needs to figure out naming and also lemma statements to make sure they are sufficiently complete and consistent.

  • Please register or sign in to reply
    Loading