This pull request is an attempt to address issue #102.
Note: It is not yet ready for merging. But I could use an external eye.
This pull request mainly add two files to the library.
theories/Core/SubKTree.v is parameterized by an embedding of a type i into Type, characterized by:
an embedding F: i -> Type;
a binary operation isum: i -> i -> i mapped (up-to-iso) onto sum
an initial element iI: i mapped (up-to-iso) onto void.
It defines from this two categories whose objects are i: iFun ~ F A -> F B and sktree E ~ F A -> ktree E (F B). They are naturally to be seen as restriction of respectively Fun and ktree.
The file [theories/Core/SubKTreeFacts.v] derives all facts previously established for ktree onto sktree. The file is a bit long to compile at the moment, a slightly too brutal proof should be optimized.
My wished sanity check has been to use finite types as labels in the compiler with the least impact on the proofs as possible.
This attempt can be witnessed first via the file tutorial/Label.v that instantiates the needed type classes with i = Nat, F = Fin.t, iI = 0 and isum = +.
Correspondingly, Asm.v is adapted to represent labels as finite types.
As far as purely equational proofs is concerned, the sanity check is passed: most proofs are exactly identical after adapting the types and replacing mentions of ktree by sktree in the names of the lemmas.
However, things are currently not as nice for the few proofs that proceeded by going back down to the level of ktree and doing case analyses on the input labels.
The first example is app_asm_correct, in AsmCombinators.v. The equational part goes through smoothly, but when it comes to unfolding, we now end up with a lot of explicit mentions to the embedding of the isum into Type, and things get quite messy and fail to reduce as it used to. It's worth mentioning that the definition of app_asm itself is somewhat unsatisfactory. It looks like a case_, but is not really one as it goes from i to asm.
A second symptomatic example is in the Seq case of compile_correct. We have a label r of type Fin.t 1, and need to know that it is F1 in order to reduce. However, type dependencies prevent us from destructing it.
I must say my nose is a bit too stuck into the code, I'm having trouble identifying if I made a design mistake that would simplify this, or if it is indeed inherent to the type dependencies introduced. Any remark or help as to how addressing these issues, as well as to whether this pull request as a whole seem relevant would be very welcome!
This pull request is an attempt to address issue #102. Note: It is not yet ready for merging. But I could use an external eye.
This pull request mainly add two files to the library.
theories/Core/SubKTree.vis parameterized by an embedding of a typeiintoType, characterized by:F: i -> Type;isum: i -> i -> imapped (up-to-iso) ontosumiI: imapped (up-to-iso) ontovoid. It defines from this two categories whose objects arei:iFun ~ F A -> F Bandsktree E ~ F A -> ktree E (F B). They are naturally to be seen as restriction of respectivelyFunandktree.The file [theories/Core/SubKTreeFacts.v] derives all facts previously established for
ktreeontosktree. The file is a bit long to compile at the moment, a slightly too brutal proof should be optimized.My wished sanity check has been to use finite types as labels in the compiler with the least impact on the proofs as possible. This attempt can be witnessed first via the file
tutorial/Label.vthat instantiates the needed type classes withi = Nat,F = Fin.t,iI = 0andisum = +. Correspondingly,Asm.vis adapted to represent labels as finite types. As far as purely equational proofs is concerned, the sanity check is passed: most proofs are exactly identical after adapting the types and replacing mentions ofktreebysktreein the names of the lemmas. However, things are currently not as nice for the few proofs that proceeded by going back down to the level ofktreeand doing case analyses on the input labels.The first example is
app_asm_correct, inAsmCombinators.v. The equational part goes through smoothly, but when it comes to unfolding, we now end up with a lot of explicit mentions to the embedding of theisumintoType, and things get quite messy and fail to reduce as it used to. It's worth mentioning that the definition ofapp_asmitself is somewhat unsatisfactory. It looks like acase_, but is not really one as it goes fromitoasm.A second symptomatic example is in the
Seqcase ofcompile_correct. We have a labelrof typeFin.t 1, and need to know that it isF1in order to reduce. However, type dependencies prevent us from destructing it.I must say my nose is a bit too stuck into the code, I'm having trouble identifying if I made a design mistake that would simplify this, or if it is indeed inherent to the type dependencies introduced. Any remark or help as to how addressing these issues, as well as to whether this pull request as a whole seem relevant would be very welcome!
Best, Yannick