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 algorithm #4

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

Implement the algorithm #4

wants to merge 32 commits into from

Conversation

jeltsch
Copy link
Owner

@jeltsch jeltsch commented Mar 9, 2021

This will ultimately resolve #3.

jeltsch added 28 commits February 9, 2021 18:32
@jeltsch
Add first bits of core data structure support
11134e2
@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
Improve proof for lowest_common_ancestor
549b333
@jeltsch
Add is_child_of
0eca301
@jeltsch
Replace parent lemma by is_child_of lemmas
d58e4e5
@jeltsch
Make vertex an instance of semilattice_sup
652c99a
@jeltsch
Make totality of sup_vertex explicit
8c1da1c
@jeltsch
Improve names of some is_child_of lemmas
b05bea7
@jeltsch
Remove the domintros option for sup_vertex
c7a0b17 
For a function with an associated termination proof, no `domintros` seem
to be generated anyhow. The generation of `domintros` would also be
superfluous, as the termination proof has access to the local
`termination` rule and generated facts do not refer to `domintros`.
@jeltsch
Add leaves
d390026
@jeltsch
Add support for fresh element generation
560a7eb
@jeltsch
Add support for relabeling states
0583194
@jeltsch
Add support for states
729365a
@jeltsch
Rename Foundations to Data_Structure
8596aaf
@jeltsch
Improve the proof of fresh_element_is_fresh
8eb4438
@jeltsch
Merge branch 'enhancement/data-structure' into enhancement/algorithm
51cd480
@jeltsch
Add first bits of the algorithm implementation
fbc289a
@jeltsch jeltsch self-assigned this Mar 9, 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 algorithm
1 participant
@jeltsch