The Coq mailing list

[Michael Sammler <sammler.michael AT web.de>]

Dear all,

I have a definition ded : form -> Prop and a definition equiv: form -> 
form -> form and I would like to rewrite with terms of the form ded 
(equiv A B) using the ssr rewrite. When I define a setoid for a compound 
definition ded_equiv(A B: form) := ded (equiv A B), I can rewrite with 
terms of the form ded_equiv A B using both ssr rewrite and 
setoid_rewrite, but terms of the form ded (equiv A B) only work with 
setoid_rewrite, but not with ssr rewrite, which gives "not a rewritable 
relation: (ded (equiv A B))".

I have attached an example, which shows the problem (and I have tried it 
with Coq 8.7.2, 8.8.0 and the dev version).

Is there a way to rewrite with ded (equiv A B) using ssr rewrite?

Best regards,

Michael Sammler

From Coq Require Export ssreflect ssrfun ssrbool.
Require Export Coq.Setoids.Setoid.
Require Export Relations.Relation_Definitions.
Require Export Classes.Morphisms.

Parameter form: Type.
Parameter equiv: form -> form -> form.
Parameter ded: form -> Prop.
Definition ded_equiv(A B : form) := ded (equiv A B).
Axiom ded_equiv_refl: reflexive _ ded_equiv.
Axiom ded_equiv_sym: symmetric _ ded_equiv.
Axiom ded_equiv_trans: transitive _ ded_equiv.
Add Parametric Relation : form ded_equiv
         reflexivity proved by (ded_equiv_refl)
         symmetry proved by (ded_equiv_sym)
         transitivity proved by (ded_equiv_trans)
         as ded_equiv_rel.

Goal forall (A B: form),
    ded_equiv A B -> (ded (equiv A B)) -> ded_equiv A B.
Proof.
  move => A B H1 H2.
  (* ssreflect rewrite works, if the use ded_equiv *)
  have ->:= H1.
  (* but not if we unfold the definition *)
  Fail have <-:= H2. (* fails with not a rewritable relation: (ded (equiv A 
B)) in rule _top_assumption_ *)
  (* but setoid_rewrite works with the unfolded definition *)
  setoid_rewrite <-H2.
  reflexivity.
Qed.

(* another try to define the setoid *)
Axiom ded_equiv2_refl: reflexive _ (fun A B => ded (equiv A B)).
Axiom ded_equiv2_sym: symmetric _ (fun A B => ded (equiv A B)).
Axiom ded_equiv2_trans: transitive _ (fun A B => ded (equiv A B)).
Add Parametric Relation : form (fun A B => ded (equiv A B))
         reflexivity proved by (ded_equiv2_refl)
         symmetry proved by (ded_equiv2_sym)
         transitivity proved by (ded_equiv2_trans)
         as ded_equiv2_rel.

Add Parametric Morphism : (ded) with signature
    (fun A B => ded (equiv A B)) ==> (Basics.flip Basics.impl) as ded_mor.
Proof.
Admitted.

Goal forall (A B: form),
    ded (equiv A B) -> (fun A B => ded (equiv A B)) A B -> ded A.
Proof.
  move => A B H1 H2.
  (* here ssreflect rewrite does not work as well *)
  Fail have ->:= H1.
  (* but setoid_rewrite works *)
  setoid_rewrite H1.
  (* not even with this version does ssr rewrite work *)
  Fail have <-:= H2.
  (* but setoid_rewrite works *)
  setoid_rewrite <-H2.
Abort.