todo.org

Limitations

Invariants hidden in external lemmas

An example of such a case would be when we’re dealing with a proof style that first reifies an OCaml computation with a Gallina model, and uses their equivalence as an invariant. Then once evaluating the lemma, the proof calls out to an external lemma to reduce the proof.

Tasks

remove proof validator

Prove goals using new tactics

[1] seq to array

[2] make rev list

[3] array exists

[4] array findi

[5] array find map

[6] array is sorted

[7] array of rev list

[8] array partition

[9] array foldi

[10] sll of array

[11] sll partition

[12] stack reverse

[13] stack filter

[14] tree to array

Check the proofs go through with the latest changes

[1] seq to array

[2] make rev list

[3] array exists

[4] array findi

[5] array find map

[6] array is sorted

[7] array of rev list

[8] array partition

[9] array foldi

[10] sll of array

[11] sll partition

[12] stack reverse

[13] stack filter

[14] tree to array