Previous Up Next

Chapter 20  The setoid_replace tactic

Clément Renard







This chapter presents the setoid_replace tactic.

20.1  Description of setoid_replace

Working on user-defined structures in Coq is not very easy if Leibniz equality does not denote the intended equality. For example using lists to denote finite sets drive to difficulties since two non convertible terms can denote the same set.

We present here a Coq module, setoid_replace, which allows to structure and automate some parts of the work. In particular, if everything has been registered a simple tactic can do replacement just as if the two terms were equal.

20.2  Adding new setoid or morphisms

Under the toplevel load the setoid_replace files with the command:

Coq <   Require Setoid.

A setoid is just a type A and an equivalence relation on A.

The specification of a setoid can be found in the file 
theories/Setoids/Setoid.v
It looks like : 
Section Setoid.

Variable A : Type.
Variable Aeq : A -> A -> Prop.

Record Setoid_Theory : Prop :=
{ Seq_refl : (x:A) (Aeq x x);
  Seq_sym : (x,y:A) (Aeq x y) -> (Aeq y x);
  Seq_trans : (x,y,z:A) (Aeq x y) -> (Aeq y z) -> (Aeq x z)
}.

To define a setoid structure on A, you must provide a relation Aeq on A and prove that Aeq is an equivalence relation. That is, you have to define an object of type (Setoid_Theory A Aeq).

Finally to register a setoid the syntax is:

Add Setoid A Aeq ST
where Aeq is a term of type A->A->Prop and ST is a term of type (Setoid_Theory A Aeq).


Error messages:
  1. Not a valid setoid theory.
    That happens when the typing condition does not hold.
  2. A Setoid Theory is already declared for A.
    That happens when you try to declare a second setoid theory for the same type.
Currently, only one setoid structure may be declared for a given type. This allows automatic detection of the theory used to achieve the replacement.

The table of setoid theories is compatible with the Coq sectioning mechanism. If you declare a setoid inside a section, the declaration will be thrown away when closing the section. And when you load a compiled file, all the Add Setoid commands of this file that are not inside a section will be loaded.


Warning: Only the setoid on Prop is loaded by default with the setoid_replace module. The equivalence relation used is iff i.e. the logical equivalence.

20.3  Adding new morphisms

A morphism is nothing else than a function compatible with the equivalence relation. You can only replace a term by an equivalent in position of argument of a morphism. That's why each morphism has to be declared to the system, which will ask you to prove the accurate compatibility lemma.

The syntax is the following :
Add Morphism f : ident
where f is the name of a term which type is a non dependent product (the term you want to declare as a morphism) and ident is a new identifier which will denote the compatibility lemma.


Error messages:
  1. The term term is already declared as a morphism
  2. The term term is not a product
  3. The term term should not be a dependent product
The compatibility lemma generated depends on the setoids already declared.

20.4  The tactic itself

After having registered all the setoids and morphisms you need, you can use the tactic called setoid_replace. The syntax is
setoid_replace term1 with term2
The effect is similar to the one of replace.

You also have a tactic called setoid_rewrite which is the equivalent of rewrite for setoids. The syntax is
setoid_rewrite term

Variants:
  1. setoid_rewrite -> term
  2. setoid_rewrite <- term
The arrow tells the system in which direction the rewriting has to be done. Moreover, you can use rewrite for setoid rewriting. In that case the system will check if the term you give is an equality or a setoid equivalence and do the appropriate work.

Previous Up Next