Cycles of a list #
Lists have an equivalence relation of whether they are rotational permutations of one another.
This relation is defined as IsRotated
.
Based on this, we define the quotient of lists by the rotation relation, called Cycle
.
We also define a representation of concrete cycles, available when viewing them in a goal state or
via #eval
, when over representable types. For example, the cycle (2 1 4 3)
will be shown
as c[2, 1, 4, 3]
. Two equal cycles may be printed differently if their internal representation
is different.
Return the z
such that x :: z :: _
appears in xs
, or default
if there is no such z
.
Equations
- List.nextOr [] x x = x
- List.nextOr [head] x x = x
- List.nextOr (y :: z :: xs) x x = if x = y then z else List.nextOr (z :: xs) x x
Instances For
nextOr
does not depend on the default value, if the next value appears.
Given an element x : α
of l : List α
such that x ∈ l
, get the next
element of l
. This works from head to tail, (including a check for last element)
so it will match on first hit, ignoring later duplicates.
For example:
next [1, 2, 3] 2 _ = 3
next [1, 2, 3] 3 _ = 1
next [1, 2, 3, 2, 4] 2 _ = 3
next [1, 2, 3, 2] 2 _ = 3
next [1, 1, 2, 3, 2] 1 _ = 1
Instances For
Given an element x : α
of l : List α
such that x ∈ l
, get the previous
element of l
. This works from head to tail, (including a check for last element)
so it will match on first hit, ignoring later duplicates.
prev [1, 2, 3] 2 _ = 1
prev [1, 2, 3] 1 _ = 3
prev [1, 2, 3, 2, 4] 2 _ = 1
prev [1, 2, 3, 4, 2] 2 _ = 1
prev [1, 1, 2] 1 _ = 2
Equations
Instances For
For consistency with EmptyCollection (List α)
.
An induction principle for Cycle
. Use as induction s using Cycle.induction_on
.
Auxiliary decidability algorithm for lists that contain at least two unique elements.
Equations
Instances For
Given a s : Cycle α
such that Nodup s
, retrieve the next element after x ∈ s
.
Instances For
Given a s : Cycle α
such that Nodup s
, retrieve the previous element before x ∈ s
.
Instances For
We define a representation of concrete cycles, available when viewing them in a goal state or
via #eval
, when over representable types. For example, the cycle (2 1 4 3)
will be shown
as c[2, 1, 4, 3]
. Two equal cycles may be printed differently if their internal representation
is different.
As a function from a relation to a predicate, chain
is monotonic.