Skip to main content

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
2 votes
1 answer

Rewriting/Applying unidirectional morphisms in Coq

Link to Code Gist I have the following definition ...
Agnishom Chattopadhyay's user avatar
1 vote
1 answer

How do I enable this kind of rewriting?

Link to Code Gist Given two extensionally equal sets, s1 ≡ s2, I want to be able to obtain a ∈ s2 from ...
Agnishom Chattopadhyay's user avatar
1 vote
1 answer

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

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

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

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

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

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
  • 345