The Coq mailing list

[Abhishek Anand <aa755 AT pm.me>]

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

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:

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?

--

Abhishek Anand