The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

Thanks Michael for your explanations, so I'm using the "preprocess"
option now, but it turns out I also need "morphism" and "constants"
for examples like the last one below, so here's what I'm doing now:


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}.

  Ltac is_positive_cst p :=
    match eval hnf in p with
    | xH => constr:(true)
    | xO ?q => is_positive_cst q
    | xI ?q => is_positive_cst q
    | _ => constr:(false)
    end.
    
  Ltac is_Z_cst n :=
    match eval hnf in n with
    | Z0 => constr:(true)
    | Zpos ?p => is_positive_cst p
    | Zneg ?p => is_positive_cst p
    | _ => constr:(false)
    end.

  Ltac mword_cst w :=
    match w with
    | ZToReg ?x => let b := is_Z_cst x in
                  match b with
                  | true => x
                  | _ => constr:(NotConstant)
                  end
    | _ => constr:(NotConstant)
  end.

  Hint Rewrite
    ZToReg_morphism.(morph_add)
    ZToReg_morphism.(morph_sub)
    ZToReg_morphism.(morph_mul)
  : rew_ZToReg_morphism.
  
  Add Ring mword_ring : (@regRing mword MW)
      (preprocess [autorewrite with rew_ZToReg_morphism],
       morphism (@ZToReg_morphism mword MW),
       constants [mword_cst]).
  
  Goal forall (x y: Z),
      add (ZToReg x) (ZToReg y) = ZToReg (x + y).
  Proof.
    intros. ring.
  Qed.
  
  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.
    ring.
  Qed.

  (* this one requires "morphism" and "constants": *)
  Goal forall (P: mword),
      add P (add P P) = mul (ZToReg 3) P.
  Proof.
    intros. ring.
  Qed.

End FlatToRiscv.


On Tue, 2018-08-07 at 09:02 +0000, Soegtrop, Michael wrote:
> P.S.: of cause you can remove the morphism from Add Ring, since it doesn't
> serve any purpose:
> 
>   Add Ring mword_ring :
>     (@regRing mword MW) (
>        preprocess [repeat (rewrite ZToReg_morphism.(morph_add) || rewrite
> ZToReg_morphism.(morph_sub) || rewrite ZToReg_morphism.(morph_mul))]
>     ).
> 
> Best regards,
> 
> Michael
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928