The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

Dear Coq-club,

I'm trying to figure out how to use the "morphism" option of of the 
"Add Ring" command.
I have the following:


Require Import Coq.ZArith.ZArith.

Open Scope Z_scope.

Class Reg(t: Set) := mkReg {
  add: t -> t -> t;
  sub: t -> t -> t;
  mul: t -> t -> t;

  ZToReg: Z -> t;

  regRing: @ring_theory t (ZToReg 0) (ZToReg 1) add mul sub
                        (fun x => sub (ZToReg 0) x) (@eq t);
  ZToReg_morphism:
    @ring_morph t (ZToReg 0) (ZToReg 1) add mul sub
                (fun x => sub (ZToReg 0) x) (@eq t)
                Z 0 1  Z.add Z.mul Z.sub Z.opp Z.eqb
                ZToReg;
}.

Section FlatToRiscv.

  Context {mword: Set}.
  Context {MW: Reg mword}.

  Add Ring mword_ring :
    (@regRing mword MW) (morphism (@ZToReg_morphism mword MW)).

  (* I'd like to solve the following goal automatically using "ring": *)
  Goal forall (x y: Z),
      add (ZToReg x) (ZToReg y) = ZToReg (x + y).
  Proof.
    intros.
    (* but it fails! *)
    Fail ring.
    (* however, the morphism I provided to "Add Ring" does contain a 
       lemma which can solve this goal: *)
    rewrite (ZToReg_morphism.(morph_add)).
    reflexivity.
  Qed.
  (* So, am I expecting too much of "ring"? Or am I not using it properly? *)
  
  (* And for reference, here's a more realistic example of what kind of
     goal I'd like to solve with "ring": *)
  Goal forall (P : mword) (L : Z),
      add (add P (mul (ZToReg 4) (ZToReg L))) (ZToReg 4) =
      add P (mul (ZToReg 4) (ZToReg (L + 1))).
  Proof.
    intros.
    rewrite (ZToReg_morphism.(morph_add)).
    ring.
  Qed.

  (* My question is:
     Can I get rid of the "rewrite (ZToReg_morphism.(morph_add))"? *)

End FlatToRiscv.


Thanks!

Sam