The Coq mailing list

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

I tried to set up rewriting up to mod equivalence (see modEq below).

`rewrite` does not seem to work in the last lemma below even though I can prove it manually using only the declared instances.

Require Import ZArith.
Open Scope Z_scope.
Require Import Morphisms.
Definition modEq (d:Z) := fun (a b :Z)=> a mod d = b mod d.

Global Instance modProperAdd (d:Z) :
  Proper ((modEq d) ==> (modEq d) ==>(modEq d)) Z.add.
Proof using.
  intros a b Hx e f Hy.
  unfold modEq in *.
  rewrite Zplus_mod.
  symmetry.
  rewrite Zplus_mod.
  f_equal.
  congruence.
Qed.

Global Instance modProperSub (d:Z) :
  Proper ((modEq d) ==> (modEq d) ==>(modEq d)) Z.sub.
Proof using.
  intros a b Hx e f Hy.
  unfold modEq in *.
  rewrite Zminus_mod.
  symmetry.
  rewrite Zminus_mod.
  f_equal.
  congruence.
Qed.

Lemma modEqRw (d a b:Z) :
  modEq d a b -> a mod d = b mod d.
Proof using.
  tauto.
Qed.

Global Instance modEqR (d:Z): Reflexive (modEq d).
Proof using.
  hnf. intros. unfold modEq in *. congruence.
Qed.
Global Instance modEqS (d:Z): Symmetric (modEq d).
Proof using.
  hnf. intros. unfold modEq in *. congruence.
Qed.
Global Instance modEqT (d:Z): Transitive (modEq d).
Proof using.
  hnf. intros. unfold modEq in *. congruence.
Qed.

Lemma modEq0 (d:Z): modEq d d 0.
Proof using.
  hnf. rewrite Z_mod_same_full.
  reflexivity.
Qed.

Global Instance modProperOpp (d:Z) :
  Proper ((modEq d) ==> (modEq d)) Z.opp.
Admitted.

Lemma rwTest (d a b:Z):
  (d+a-b) mod d  = (a-b) mod d.
Proof using.
  erewrite modEqRw.
  2:{
    Fail rewrite modEq0. (* help! why does this fail? *)
    apply modProperAdd;[ | reflexivity].
    apply modProperAdd;[ | reflexivity].
    apply modEq0.
  }
  reflexivity.
Qed.    

Thanks.

-- Abhishek

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