The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Hi,

In our development, we want to use the following relation instead of iff :

Definition t_iff : Type -> Type -> Type :=

  fun A B : Type => prod (A -> B)  (B -> A).

We want to rewrite using this relation at appropriate places

(t_iff is a equivalence relation and a congruence w.r.t many type constructors like prod, sum, function)

For example, if we have the following hypothesis:

H1: forall a, t_iff (P a) (Q a) 

H2: prod (P a) (R a)

we want to "rewrite" H1 in H2 to get 

H2: prod (Q a) (R a)

(prod is the cousin of /\ for types)

We have a tactic which does something like that in the attached file (trewrite tactics).

( build_tiff_term ) is it's key part.

The trouble is that trewrite expects a fully instantiated t_iff relation.

(see the generalize in some trewrite versions)

In this case, we first have to instantiate H1 with (a) and then 

use the trewrite tactic on the result. 

When we were using the "<->" relation(on Props), rewrite used to smoothly handle such cases.

It looks like the setoid mechanism wont work for the t_iff relation because it is a relation that lives in Type.

Is there some trick to easily rewrite with t_iff? 

-- Abhishek

http://www.cs.cornell.edu/~aa755/

Attachment: eq_rel.v
Description: Binary data