The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Hello,

I provide below an other example related to Armaël's question.

By default, ring does not benefit from computations over "constants".
This could be painful (see the proof of "painful_test" in attachment).

But, ring provides a way to overcome this limitation, see:
https://coq.inria.fr/refman/addendum/ring.html#adding-a-ring-structure

In particular, the user can provide a tactic (like dummy_cte in 
attachment) to discriminate between "constants" and other terms.

Is there a standard way to do it ?

In order to have a robust tactic (instead of dummy_cte), we could define 
a tactic that recognizes closed terms in normal formal form (ie built 
from constructors of inductive types). But this might not be sufficient 
in practice (e.g. the rational (4#2) would not be considered as a constant).

Any ideas ?

Sylvain.



Le 08/11/2018 à 11:24, Armaël Guéneau a écrit :
> Dear Coq-club,
>
> I'm writing a reflexive tactic that (roughly speaking) simplifies
> arithmetic expressions. It first reifies the goal into something like:
>
> Inductive expr :=
> | EAdd : expr -> expr -> expr
> | EMul : expr -> expr -> expr
> | ECst : Z -> expr.
>
> ECst is a catch-all case: it may store arbitrary-looking terms, not only
> numerical constants. These should be treated as abstract by the tactic.
>
> Then, I implemented a [simplify : expr -> expr] Coq function, and proved
> that it is meaning-preserving. Finally, my tactic reifies the goal,
> applies the theorem specialized to the reified expression, and reduces
> the result to obtain the simplified goal.
>
> The issue I have is with this last part: I want to evaluate [simplify],
> but I do not want the reduction tactic to reduce the contents of [ECst
> ..], since these can contain arbitrary terms that should be treated as
> abstract.
>
> How do I evaluate my tactic in a robust way? I feel like this is a
> relatively fundamental issue, and for example I wonder how
> [ring_simplifies] works around it? Does anyone know?
>
> For the moment I thought about:
>
> - Listing all the functions transitively used by [simplify] and reduce
> with a whitelist (cbv [the functions...]). However: 1) there is a lot of
> them 2) it's bad from a maintainability perspective 3) it does not quite
> work as the whitelist will include stuff like Nat.eqb that might very
> well be used in a [ECst ..].
>
> - Introducing local definitions for the terms in [ECst foo] (using [set
> (x := foo)]); and blacklisting these local definitions during reduction.
> There is a technical issue: the blacklist is discovered dynamically, so
> I cannot specify it in Ltac using cbv -[foo bar baz]. I guess I could
> write a small plugin to handle dynamically constructing the blacklist,
> if that's what it takes...
>
> Any ideas?
>
> — Armaël
Require Import ZArith.
Require Import QArith.
Require Import Qcanon.

Notation "a # b" := (Q2Qc (a#b)%Q) (at level 55, no associativity) : Qc_scope.

Local Open Scope Z_scope.
Local Open Scope Qc_scope.

Definition Z2Qc z := z#1.
Coercion Z2Qc: Z >-> Qc.

Lemma painful_test (x:Qc): (2*x-2*(x-1))*x+3*x = 5*x.
Proof.
  ring_simplify.  (* ring fails to reduce this to a trivial equality *)
  cutrewrite (2*x + x*3 = x*(2+3)).
  - try ring. (* ring fails *)
    cutrewrite (2+3=5); auto.
  - ring.
Qed.


(* Now, we can import computation on scalar into ring 

   we need a tactic to discriminate "constants" over other terms.

   Here is a simple (non-robust) tactic 

*)
Ltac dummy_cte t :=
  match t with
  | (Q2Qc _) => t
  | (Z2Qc _) => t
  | _ => InitialRing.NotConstant
  end.

Global Add Ring Qcring: Qcrt (decidable Qc_eq_bool_correct, constants [dummy_cte]).

Lemma perfect_test (x:Qc): (2*x-2*(x-1))*x+3*x = 5*x.
Proof.
  ring_simplify. 
  auto.
Qed.

(* An example showing the lack of robustness in dummy_cte *)
Lemma test_failure (x:Z): (2*x-2*(x-1))*x+3*x = 5*x.
Proof.
  ring_simplify. 
  auto.
Qed.