4
$\begingroup$

I've been chatting with folks on Mastodon about this but the perspective there is markedly Agda-focused, so I thought I'd ask here for some broader opinions.

What tools/libraries are there for reasoning about Categories with Families and Language Semantics in a Proof Assistant?

I'm particularly looking for:

  1. Tools that will let me reason in the language of CwFs without committing to a particular category
  2. Tools that will help me automatically rewrite goals using the category and CwF laws without much boilerplate. Many of the CwF equations have a "direction" and can safely be turned into rewrite rules without risking non-termination.

In Agda, (1) and (2) are at odds with each other: there's the REWRITING option, but it doesn't support rewriting in terms of fields of a record. So unless morphism composition and comprehension are given concrete definitions, it can't rewrite.

Are there frameworks in Coq or Lean for this? I know there are tactics there to rewrite by a particular equality, but I have no idea how easy it is to automatically rewrite by all of the CwF laws.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
4
$\begingroup$

I am really sorry to inflict this upon you but could you not use a parametrised module instead of a record together with an abstract block to rigidify the parameters and thus enable REWRITING?

e.g. this seems accepted:

{-# OPTIONS --rewriting #-}

open import Agda.Builtin.Equality

{-# BUILTIN REWRITE _≡_ #-}

module _ {a} (A : Set a) (x y : A) (eq : x ≡ y) where

  abstract
    x' : A
    x' = x
    y' : A
    y' = y
    eq' : x' ≡ y'
    eq' = eq

  {-# REWRITE eq' #-}

  lemma : x' ≡ y'
  lemma = refl

You can then perhaps recover your record-based interface by having wrapper modules re-exporting the results thus obtained?

Improve this answer
$\endgroup$
3
  • $\begingroup$ Hmm, okay, that works better than anything I've tried so far, even if we introduce an operation foo : X -> X and rewrite by eq: foo x ≡ y. It probably shouldn't be too hard to write an elaborator reflection macro that takes a record type and re-declares each of its fields as an abstract... $\endgroup$
    – Joey Eremondi
    Commented Jun 22, 2023 at 19:58
  • $\begingroup$ Hmmm, interesting development, it looks like the problem is that I was using a relation other than the normal builtin equality. If I use e.g. HeterogeneousEquality, the example you give fails to compile. I'll see if there's an existing bug report $\endgroup$
    – Joey Eremondi
    Commented Jun 22, 2023 at 20:18
  • $\begingroup$ Huzzah, it works! I'll leave the question open a bit though, since I am genuinely curious how this would work in Coq or Lean. $\endgroup$
    – Joey Eremondi
    Commented Jun 22, 2023 at 21:26
3
$\begingroup$

Coq has a notion of a hint database which can contain either equalities or proofs of an equivalence relation other than equality, and an "autorewrite" tactic which repeatedly rewrites according to hints in the database according to a normal form is reached. https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#coq:tacn.autorewrite

There is an associated mini-dsl for defining rewrite strategies, specifying the order in which equations should be applied, whether rewriting should go from the top down or bottom up, etc. https://coq.inria.fr/refman/addendum/generalized-rewriting.html#strategies4rewriting

For equivalence relations other than equality, the user must additionally supply proofs that it plays nicely with other things, e.g., $x \sim y \implies f x \sim f y$. This "setoid rewriting" machinery is facilitated by the typeclass system which can automatically find these proofs if they are declared in the appropriate typeclass database. https://coq.inria.fr/refman/addendum/generalized-rewriting.html

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.