Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] morphism option of ring tactic

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] morphism option of ring tactic


Chronological Thread 
  • From: Samuel Gruetter <gruetter AT mit.edu>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] morphism option of ring tactic
  • Date: Tue, 7 Aug 2018 17:17:26 +0000
  • Accept-language: en-US
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gruetter AT mit.edu; spf=Pass smtp.mailfrom=gruetter AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-7.mit.edu
  • Ironport-phdr: 9a23:zpBiSRR1HAOgXYWvWjEPiqh1p9psv+yvbD5Q0YIujvd0So/mwa6yZhaN2/xhgRfzUJnB7Loc0qyK6/6mATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbJ/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zI7VfI6bO/Vxc7jBfdwBX2dNQtpdWzBDD466coABD/ABPeFdr4TlulUBtx6+BRSyC+Pr1zRGh2X23bAk3OQ9DQHJwhYgFM8JvXTbttX1KbkdUfypzKbW1zXOdPZW2Tbh6ITSbB8uvOyMUKt2fMHMx0cvEAbFgU+RqYzjJz6U1/4Cs3Ka7+p8VeKjkWknqxlvrTip3sssi4/Jhp4LxVDA7yl23Zg6KNulQ0B4ed6pCIZcuiKAO4Z0WM8vQmJltDw0x7AHoZK3YTYGxZc9yxPRd/CLaZWE7g75WOufPDt0nG9pdbO7ihqo70StyuLxWtOp3FpQsyZJjMXAu3YQ3BLJ8MeHUOFy/kK51DaPyQ/T7uZELFgpmqreKp8t27swmYASsUTHBS/5hln5gLaNdko44Oeo7eLnbav8ppOFNYJ4kAT+MqUymsClH+s3LxUOU3Ca+eS6yrLj4VX0TKhJg/EskKTVqpHXKMcBqqO3AgJZyoMj5Ay+Dzei3tQYh34HLFdddRKIlYjpJk/BIOzkDfihmVShizJrx/HaPrH7HJrCM2XDnK/7fblh805c1BYzzddH6p1IDbEBOev/VVP1tNzFFRA0KBe0wubiCNVlzIwSQ2OPAqmDMKPTq1CE/OwvI/PfLLMS7Xz2LOFg7Przh1c4n0UcdO+nx9FfPHu/B7FtJ1iTSXvqmNYIV2kQ6FkQVuvv3WaLVCNeYz6dRb8x+i02EsryAp3eS5yxjaap2SanWJBaezYVWRi3DX70etDcCL83YyWIL5o5y21WZf2aU4YkkCqWmkr/wrtjIPDT/3xKsJP/ktV5+r+KzE1gxXlPF82Yllq1YSRshGpZFTo3wOZyrVEvkg7eg5g9uORREJlo390MUgo+MsWFneB/GZX3UwPFZdqCDU2tS9OgDCt0EZQ0wsNIbkpgSY2v

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



Archive powered by MHonArc 2.6.18.

Top of Page