search

coq-community / hydra-battles

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
https://coq-community.org/hydra-battles/doc/hydras.pdf
MIT License
67 stars 12 forks source link

Changes to the Ackermann sub-library #31

Open Casteran opened 3 years ago

Casteran commented 3 years ago

In the files inherited from Goedel (now in theories/Ackermann), the predicates isPR and isPRrel are of sort Set, but all the proofs of primitive recursivity were opaque (endind by Qed), which forbids us from analysing the implementation of a proven primitive recursive function (code size, for instance).

It happens that changing all Qed into Defined is the proofs of primitive recursivity breaks the compilation of the goedel library (a repeated ltac tactic at line 1552 of codeSysPrf.v loops).

The branch transparent-IsPR restricts this change opaque->transparent to a few modules of Ackermann, so as to prevent the compilation of goedel to fail. If it's OK, I propose to merge it into master.

Zimmi48 commented 3 years ago

Sounds reasonable. Another solution would be to adapt Goedel to work with these changes.

Casteran commented 3 years ago

Yes, I will try to understand which lemma should remain or made opaque (or simply not being unfolded) in Goedel. Meanwhile, I will maintain two branches in hydra-battles.