The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hello Abhishek,


On Wed, 2022-06-22 at 02:09 +0000, Abhishek Anand wrote:
> How difficult would it be to generalize the Saturate class to capture
> relationships between the function result and the function arguments?
> Such functionality is often needed to write properties of nonlinear
> functions that lia doesn't understand:
> 
> Zmod_le : ∀ a b : Z, 0 < b → 0 <= a → a mod b <= a
> mod_pos_bound : ∀ a b : Z, 0 < b → 0 <= a mod b < b

For mod and div, there ad'hoc support via the flag
Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::=
constr:(true)

> 
> Here is the existing definition of Saturate:
> Class Saturate {T: Type} (Op : T -> T -> T) :=
>   mksat {
>       (** Given [Op x y],
>           - [PArg1] is the pre-condition of x
>           - [PArg2] is the pre-condition of y
>           - [PRes]  is the pos-condition of (Op x y) *)
>       PArg1 : T -> Prop;
>       PArg2 : T -> Prop;
>       PRes  : T -> Prop;
>       (** [SatOk] states the correctness of the reasoning *)
>       SatOk : forall x y, PArg1 x -> PArg2 y -> PRes (Op x y)
>     }.
> 
> Clearly, for Zmod_le, the conclusion mentions not just the result (a
> mod b) but also `a`. One way to solve this to generalize PRes to be
> ternary. Then we wont even need PArg1 and PArg2:

The motivation was to exploit positivity constraints. If we have in the
context, 
0 <= Z.of_nat x and 0 <= Z.of_nat y, we would like to to have 
0 <= Z.of_nat x * Z.of_nat y.
For this purpose, PArg1 and PArg2 would be matched from the context (if
possible) and only the conclusion is added. 
Note that it is wise to avoid generating a lot of formulae of the form 
A -> B -> C as it may be very costly for `lia`.

> 
> 
> Class Saturate {T: Type} (Op : T -> T -> T) :=
>   mksat {
>       PRes  : T ->T ->T -> Prop;
>       (** [SatOk] states the correctness of the reasoning *)
>       SatOk : forall x y, PRes x y (Op x y)
>     }.
> 
> Would it be more difficult to implement saturation for instances of
> the above version?

The implementation would probably be simpler.
For efficiency, the current implementation is in Ocaml.
It seems possible to do it in pure Ltac with the following:
- perform a traversal of terms
- when you encounter a binary operator, perform typeclass resolution to
get a Saturate instance.
- Generalize SatOK with the arguments
- Optimize to not generate the same term twice


What would fit the existing Saturate better would be: 

Class Saturate {T: Type} (Op : T -> T -> T) :=
   mksat {
       PArg1 : T -> Prop;
       PArg2 : T -> Prop;
       PRes  : T -> T -> T -> Prop;
       SatOk : forall x y, PArg1 x -> PArg2 y -> PRes x y (Op x y)
    }.

There is probably almost nothing to change in the plugin code to make
it work.


Best,
--
Frédéric