Draft: Predicate `list.Sorted.sorted` recursively-defined.
I believe that predicate list.Sorted.sorted
remains an inductive definition for historical reasons.
Since we can attach variant
to logical symbols, such predicate can be easily defined recursively, as follows:
let rec ghost predicate sorted (l: list t)
variant { l }
= match l with
| Nil | Cons _ Nil -> true
| Cons x (Cons y l) ->
le x y && sorted (Cons y l)
end
A quick grep
shows that list.Sorted
is used in seven different examples:
- coincidence_count_list
- insertion_sort_list
- mergesort_list
- sorted_list
- tower_of_hanoi
- verifythis_2019_cartesian_trees
- verifythis_2019_ghc_sort
With this new definition of sorted
, the only proofs that remain to be ported are verifythis_2019_cartesian_trees
and _cartesian_trees
(both authored by @qgarcher ). However, I do not do believe such proofs are stuck due to the new definition of sorted
. The first one seems to be an issue with detached nodes of interactive proof; the second one seems to be some trick invariants and a postcondition with an existential quantifier.