Skip to content
Snippets Groups Projects

add a function to obtain a set with all elements of a finite type

Merged Ralf Jung requested to merge ralf/fin_to_set into master
2 unresolved threads

This lets us use the existing nice gmap/gset infrastructure even for total functions when the domain type is finite.

Edited by Ralf Jung

Merge request reports

Merged by Robbert KrebbersRobbert Krebbers 4 years ago (Oct 28, 2020 7:48pm UTC)

Merge details

  • Changes merged into with dff135cd.
  • Deleted the source branch.

Pipeline #36571 failed

Pipeline failed for dff135cd on master

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Ralf Jung added 1 commit

    added 1 commit

    • fda4dbb9 - add SetUnfoldElemOf instance

    Compare with previous version

  • Ralf Jung resolved all threads

    resolved all threads

  • mentioned in commit dff135cd

  • 873 873 Proof. induction 1; set_solver. Qed.
    874 874 End option_and_list_to_set.
    875 875
    876 (** * Finite types to sets. *)
    877 Definition fin_to_set (A : Type) `{SemiSet A C, Finite A} : C :=
    • I noticed that this should not take SemiSet, which contains the proof, but only the operational type classes, as we commonly do to reduce term sizes.

      So, this should be Singleton A C, Empty C, Union C like list_to_set.

    • Please register or sign in to reply
  • 873 873 Proof. induction 1; set_solver. Qed.
    874 874 End option_and_list_to_set.
    875 875
    876 (** * Finite types to sets. *)
    877 Definition fin_to_set (A : Type) `{SemiSet A C, Finite A} : C :=
    878 list_to_set (enum A).
    879
    880 Section fin_to_set.
    881 Context `{SemiSet A C, Finite A}.
    882 Implicit Types a : A.
    883
    884 Lemma elem_of_fin_to_set a : a fin_to_set A.
    • RE 39713291

      SemiSet does not have a Hint Mode, hence this works without type annotation. If you implement my suggestion above, this should fail, even with newer Coq versions, without type annotation.

      That said, we probably should also give classes like SemiSet a Hint Mode.

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