Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Implement the data structure #2

Draft
wants to merge 28 commits into
base: master
Choose a base branch
from
Draft

Implement the data structure #2

wants to merge 28 commits into from

Conversation

jeltsch
Copy link
Owner

@jeltsch jeltsch commented Feb 9, 2021

This will ultimately resolve #1.

@jeltsch jeltsch self-assigned this Feb 9, 2021
@jeltsch
Copy link
Owner Author

jeltsch commented Feb 9, 2021 •
edited
Loading

As next steps we should do the following:

  • For element labels:
    • Simplify the proof of non-emptiness of the set of element labeling functions
    • Switch to using the Lifting and the Transfer package, which will enable us to easily use the constraints of the subtype
    • Prove element_of_after_label_of and label_of_after_element_of
  • For supertrees:
    • Instantiate the semilattice_sup class for vertices
    • Change the definition of sup_vertex to always use single steps, which will enable us to use parent
    • Switch to using Isar syntax for the conditions in sup_vertex
    • Prove totality of sup_vertex
    • Prove the following properties about parent:
      • A node of zero height (a leaf) has no children.
      • A node of non-zero height (an inner node) has two certain children.
    • Prove the following properties about index_at_height and labels_under:
      • They are kind of inverses of each other.
      • The label set of a tree of zero height is the singleton set containing the index of the tree’s root.
      • The label set of a tree of non-zero height is the disjoint union of the label sets of its immediate subtrees.
    • Show the connection between index_at_height and parent

jeltsch added 12 commits February 9, 2021 19:25
@jeltsch
Simplify the non-emptiness proof for element_labeling
082ec01 
The key to have a short, largely automatic proof is to explicitly
specify that the witness for the existential statement is `Map.empty`.
@jeltsch
Switch to using the Lifting and the Transfer package
5d8199a 
This enables us to easily use the constraints of the `element_labeling`
subtype in future proofs.
@jeltsch
Prove that element_of and label_of are mutual inverses
d741d76
@jeltsch
Fix index calculation in lowest_common_ancestor
7adae88
@jeltsch
Simplify the definition of lowest_common_ancestor
63c4d68 
The new definition consistently uses `parent`. For this to be possible,
it uses small steps also in the first two clauses.
@jeltsch
Switch to consistent use of Isar syntax
4cefdbd 
Previously, the conditions in the definition of `lowest_common_ancestor`
were specified using Pure implications.
@jeltsch
Move index to a better position
958c0f9
@jeltsch
Fix the naming of labels in the definition of index
d43377f
@jeltsch
Rename index index_at_height
444a16b
@jeltsch
Introduce vertex type
e8d7c99 
We do not want to make `nat × nat` an instance of `semilattice_sup`,
since there are lattice structures for this type that are more standard
than our structure.
@jeltsch
Fix parent_graph_is_acyclic
2e39598 
The previous version did not outrule cycles as such but only outruled
that all vertices have cycles of a certain common size.
@jeltsch
Fix mix-up of i₁ with h₂ in lowest_common_ancestor
92744fd
@jeltsch jeltsch marked this pull request as draft February 12, 2021 21:49
jeltsch added 12 commits February 14, 2021 23:07
@jeltsch jeltsch changed the title Add support for core data structures Implement the data structure Mar 8, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@jeltsch jeltsch

Labels
type: enhancement
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Implement the data structure
1 participant
@jeltsch