Scholarlink

<p>In dependently typed proof assistants, users can declare axioms to extend the ambient logic locally with new principles and propositional equalities governing them. Additionally, rewrite rules have recently been proposed to allow users to extend the logic with new definitional equalities, enabling them to handle new principles with a computational behaviour. While axioms can only break consistency, the addition of arbitrary rewrite rules can break other important metatheoretical properties such as preservation of typing. In this paper, we present an implementation of rewrite rules on top of <Emphasis FontCategory="SansSerif">the Rocq Prover</Emphasis>, together with two modular criteria to ensure that the added rewrite rules preserve confluence and typing. These criteria, based on the triangle property for the former and bidirectional type checking for the latter, are formally expressed for PCUIC—the type theory of Rocq recently developed in the MetaRocq project.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

The Rewster: Type Preserving Rewrite Rules for the Rocq Prover

  • 期刊论文

  • 发表日期：

    2026年4月11日

查看全文
  • Yann Leray,
  • Gaëtan Gilbert,
  • Nicolas Tabareau,
  • Théo Winterhalter

摘要

In dependently typed proof assistants, users can declare axioms to extend the ambient logic locally with new principles and propositional equalities governing them. Additionally, rewrite rules have recently been proposed to allow users to extend the logic with new definitional equalities, enabling them to handle new principles with a computational behaviour. While axioms can only break consistency, the addition of arbitrary rewrite rules can break other important metatheoretical properties such as preservation of typing. In this paper, we present an implementation of rewrite rules on top of the Rocq Prover, together with two modular criteria to ensure that the added rewrite rules preserve confluence and typing. These criteria, based on the triangle property for the former and bidirectional type checking for the latter, are formally expressed for PCUIC—the type theory of Rocq recently developed in the MetaRocq project.