Chapter 6

[derik713]

This PR implements the material covered in Chapter 6. It includes the equivalence theorems from Sections 6.1 and 6.2, the implementation of the TimeM monad, and the functions introduced in Sections 6.3 and 6.4.

Implementation details

• Section 6.3: Introduced the ValidSizeTree idea so that the .height field (which has O(1) cost) can be used correctly.
• Some of the more involved complexity proofs in Section 6.2 are still missing, as well as the proofs for Sections 6.3 and 6.4.
• I could not find a satisfactory solution for qsort₁/qsort and select₀/select in Section 6.2.
• Some functions remain only partially implemented because I was unable to prove their termination.

[arademaker]

O arquivo API é desnecessário, o projeto já importa a CSLib, basta você usar como https://github.com/arademaker/fad/blob/main/Fad/Chapter2.lean#L4

[derik713]

De fato, acabei não percebendo e usando igual pessoal do cap 10. Acabei de passar para o formato da CSLib.

[arademaker]

I will accept it since it's a genuine improvement over main. Hope you can now remove the remaining partial definitions.