The Coq mailing list

[Cao Qinxiang <caoqinxiang AT gmail.com>]

Dear Abhishek,

If rewrite (modEq0 d), it is to replace "d" in : "(fun d0 => modEq d0 (d0 + a - b) ?1) d", which cannot succeed.

Best,

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

On Tue, Nov 5, 2019 at 11:27 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Thanks. That worked. 

Is it a bug that  `rewrite (modEq0 d) at 2` succeeds but `rewrite (modEq0 d)` doesn't? I thought the "at ..." suffix was used to prevent rewriting at unneeded places, not to make the rewrite succeed.

-- Abhishek

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

On Mon, Nov 4, 2019 at 10:30 PM Cao Qinxiang <caoqinxiang AT gmail.com> wrote:

The following line should work:

rewrite (modEq0 d) at 2.

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

On Tue, Nov 5, 2019 at 1:32 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

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/