Coq as a Metatheory for Nuprl with Bar Induction
by Vincent Rahli, Mark Bickford
- Presented at Continuity, Computability, Constructivity â€“ From Logic to Algorithms (CCC 2015), Kochel am See, Germany, September 14, 2015.
- Unofficial PDF
These past few years, we have been experimenting in Nuprl with versions of Brouwerâ€™s Bar Induction principle. Until recently we had no formal proof that these rules are valid Nuprl reasoning principles. Thanks to our formalization of Nuprlâ€™s metatheory in Coq, we can now rigorously check whether these principles are consistent with Nuprl. In this paper we present a proof, using our Coq framework, of the validity of Brouwerâ€™s Bar Induction principle on sequences of natural numbers. To prove this result we added all Coq functions from natural numbers to natural numbers to Nuprlâ€™s computation system.