[Coq-Club] morphism option of ring tactic

[Samuel Gruetter]

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.


T

[Soegtrop, Michael]

Dear Samuel,

in general the purpose of ring is to solve goals by using the associativity and commutativity laws of one ring. The ring is selected by the type parameter of the equality. In your case you need additional lemmas to solve the goal, which have nothing to do with associativity or commutativity.

The Coq manual states, that the purpose of providing a ring morphism is to extend a generally non computational ring with a computational constant type, so that constant folding can be done. I would think this only works when the provided morphism is computational and not an axiom. It might also be that the ring tactic only tries to use the morphism if the respective terms are free of variables, which is not the case in your example. Add Ring has a "cnstants" option to provide a tactic to judge what a constant is, but I don't see how this would help you. So your usage of morphism seems to be a stretch.

But there is a way to do it: use the "preprocess" option to Add Ring to apply rewrites to convert all Z operators to mword operators like this:

Add Ring mword_ring :
(@regRing mword MW) (
morphism (@ZToReg_morphism 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: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenche

[Soegtrop, Michael]

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: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muen

[Samuel Gruetter]

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.

Post by Soegtrop, Michael
P.S.: of cause you can remove the morphism from Add Ring, since it doesn't
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: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich

[Soegtrop, Michael]

Dear Samuel,

I am happy that I could help :-)

Two more notes:

1.) There is an (undocumented) tactic called "is_constructor". This might simplify your checks. There is also a tactic to check for ground terms in the pipeline. Search for "is_" in https://github.com/coq/coq/blob/master/plugins/ltac/extratactics.ml4 for other undocumented term classification tactics (I have it on my to do list to write the documentation).

2.) In case you are working on large terms, it might be worthwhile to do a performance comparison of autorewrite vs. repeat rewrite vs. rewrite_strat vs. match context + rewrite. A usage of rewrite_strat for your case would look as below, but there are quite a few options one can try:

[rewrite_strat (bottomup terms ZToReg_morphism.(morph_add) ZToReg_morphism.(morph_sub) ZToReg_morphism.(morph_mul))]

In case you look into this, I would be interested in the results. I did test this in the past, but I had only rater modest term sizes where it did not make much of a difference and didn't bother to create large artificial terms. For large term sizes, timing might be substantially different.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munic

[Samuel Gruetter]

Post by Soegtrop, Michael
1.) There is an (undocumented) tactic called "is_constructor". This might
simplify your checks. There is also a tactic to check for ground terms in
the pipeline. Search for "is_" in
https://github.com/coq/coq/blob/master/plugins/ltac/extratactics.ml4 for
other undocumented term classification tactics (I have it on my to do list
to write the documentation).

Turns out the library already has an Ltac isZcst:

https://github.com/coq/coq/blob/629fbc743f8b5e7623a6834f19885b2e379cb782/plugins/setoid_ring/InitialRing.v#L883

Post by Soegtrop, Michael
2.) In case you are working on large terms, it might be worthwhile to do a
performance comparison of autorewrite vs. repeat rewrite vs. rewrite_strat
vs. match context + rewrite. A usage of rewrite_strat for your case would
[rewrite_strat (bottomup terms ZToReg_morphism.(morph_add)
ZToReg_morphism.(morph_sub) ZToReg_morphism.(morph_mul))]
In case you look into this, I would be interested in the results. I did
test this in the past, but I had only rater modest term sizes where it did
not make much of a difference and didn't bother to create large artificial
terms. For large term sizes, timing might be substantially different.

For ring preprocessing, I didn't have any large terms so far, but I did for
expressions involving Z.testbit. There, switching from "repeat rewrite" to
rewrite_strat yielded a ~10x speedup:
https://github.com/mit-plv/riscv-coq/commit/4d83bc1