Questions tagged [rewriting]

In a rewriting system, one specifies a set of rules that describe valid replacements of subformulae by other ones. (from nLab).

Filter by
Sorted by
Tagged with
1 vote
1 answer
84 views

Rewriting inside quantified propositions in Coq?

Is there a simple way to use rewrites inside quantified Props? As an example, consider the following: ...
Agnishom Chattopadhyay's user avatar
4 votes
2 answers
299 views

Reasoning about CwFs in a proof assistant

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 ...
Joey Eremondi's user avatar
2 votes
1 answer
77 views

Debug autorewrite in Coq

I often meet proofs using autorewrite which Coq takes a while to process for some reason. (Setoid rewriting) I then manually figure out which rewrite rules were ...
8bc3 457f's user avatar
  • 224
1 vote
0 answers
61 views

Can you help me lay out the different variations of CoC and their generalizations?

I am learning the typed lambda-calculus and looking into the Calculus of Constructions. It was going well until I was slapped in the face with variations, and now I'm confused about the layout of all ...
Alex Byard's user avatar
4 votes
3 answers
261 views

Rewrite with definitional equality and dependent types

In Coq, there are some terms that are equal by definition, but there's not an easy way to replace one value with the other inside a proof. The two ways that I know that work in general are to use the ...
sudgy's user avatar
  • 193
6 votes
2 answers
158 views

Policies on introducing free variables when rewriting?

When using a fact like x = y <=> x + z = y + z as a rewrite rule, it can be desirable to introduce an unused free variable into the result of the rewrite ...
Cris P's user avatar
  • 305