Skip to main content
7 votes

Policies on introducing free variables when rewriting?

If I understand correctly, what you are talking about is treated using existential variables in Coq. These are variables but on the "meta" level, meaning that they stand for a term yet-to-be-...
Meven Lennon-Bertrand's user avatar
4 votes

Reasoning about CwFs in a proof assistant

I am really sorry to inflict this upon you but could you not use a parametrised module instead of a record together with an ...
gallais's user avatar
  • 1,256
3 votes

Policies on introducing free variables when rewriting?

In Metamath, the MMJ2 proof assistant introduces work variables, which names are constructed with a & prefix, a letter giving the type code of the variable, ...
Thierry Arnoux's user avatar
3 votes
Accepted

How do I enable this kind of rewriting?

In order to add a Morphism, your function needs a name. It can't just be an anonymous function. Below is a minimal working example. ...
djao's user avatar
  • 464
3 votes

Reasoning about CwFs in a proof assistant

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 ...
Patrick Nicodemus's user avatar
2 votes
Accepted

Rewriting/Applying unidirectional morphisms in Coq

Morphisms only affect rewrite, not apply. The following does work, and makes use of the ...
djao's user avatar
  • 464
2 votes
Accepted

Rewriting inside quantified propositions in Coq?

Yes, the tactic setoid_rewrite lets you rewrite under binders. Here is the reference manual link. For your example this gives: ...
Villetaneuse's user avatar
1 vote
Accepted

Rewrite with definitional equality and dependent types

Maybe I should have thought of this more before asking, but I thought of a solution that's at least better than everything I've thought of so far: ...
sudgy's user avatar
  • 193
1 vote

Rewrite with definitional equality and dependent types

If you have ssreflect: ...
djao's user avatar
  • 464
1 vote

Rewrite with definitional equality and dependent types

This works: Theorem test : forall (S : nat -> Prop) (H : S O), ex_intro S O H = ex_intro S a H. Proof. intros S H. change a with O. Abort. Is this what you ...
Trebor's user avatar
  • 4,015

Only top scored, non community-wiki answers of a minimum length are eligible