Allow parametrized rings for FStar.Tactics.CanonCommSemiring

[TWal]

The CanonCommSemiring currently doesn't allow semirings to be parametrized with implicit parameters. Allowing this would be very useful, for example to define a ring of integers "modulo m", where m would be an implicit parameter.

Before the pull request, the following minimal test was failing:

open FStar.Tactics
open FStar.Tactics.CanonCommSemiring
open FStar.Algebra.CommMonoid
open FStar.Mul

type int_ring (k:nat) = int

let ( +% ) (#k:nat) (x y:int_ring k): int_ring k = x+y
let ( *% ) (#k:nat) (x y:int_ring k) : int_ring k = x*y
let ( ~% ) (#k:nat) (a:int_ring k) : int_ring k = -a
let ( -% ) (#k:nat) (a b:int_ring k) : int_ring k = (a +% ~% b)

[@@canon_attr]
let int_plus_cm (#k:nat): cm (int_ring k) =
  CM 0 ( +% ) (fun x -> ()) (fun x y z -> ()) (fun x y -> ())

[@@canon_attr]
let int_multiply_cm (#k:nat): cm (int_ring k) =
  CM 1 ( *% ) (fun x -> ()) (fun x y z -> ()) (fun x y -> ())

[@@canon_attr]
let int_cr (#k:nat): cr (int_ring k) =
  CR int_plus_cm int_multiply_cm ( ~% ) (fun x -> ()) (fun x y z -> ()) (fun x -> ())

let int_semiring (#k:nat) () : Tac unit =
  canon_semiring (int_cr #k)

let test (#k:nat) (a:int_ring k) =
  assert (a +% (~% a) +% 2 *% a +% (~% a) == (~% a) +% 2 *% a) by (int_semiring #k (); trefl(); qed())

With this pull request, it is now working as expected.

I adapted the ring_cr of examples/semiring/CanonCommSemiring.Test.fst to parametrize it and make it fully general, and added it to ulib/FStar.Tactics.CanonCommSemiring.fst, however I'm not sure it's the right place for it or not.

[ghost]

All CLA requirements met.

[TWal]

I tested more thoroughly the parametrized ring_mod on my project, and noticed some times where the tactic is failing, for example:

let test_ring_cr3 (#m:nat{2 < m}) (a:mod_ring m) =
  assert (a +% a == (2 *% a)) by (canon_semiring (ring_cr #m); trefl (); qed ())

But, this (more harder?) assertion succeeds:

let test_ring_cr2 (#m:nat{2 < m}) (a:mod_ring m) =
  assert (a +% a == (0 *% a) +% (2 *% a)) by (canon_semiring (ring_cr #m); trefl (); qed ())

However, both examples are working fine with the unparametrized version of ring_cr in examples/semiring/CanonCommSemiring.Test.fst

[TWal]

The problem is that the tactic assume the ring is concrete so we can compute the result of operations between constants.

The function canonical_sum_simplify generates conditions such as if c == 0 then ... or if c == 1 then ... and assumes that the normalizer will be able to deduce if the condition will be true or false.

I'm thinking one solution for this would be for the tactic to generate goals like c == ?u and then use the result for the if c == 0 then ... condition. Before giving the goal c == ?u to the user, we could try to solve it with the normalizer for example.

[TWal]

One other solution would be to rewrite the semiring_reflect lemma: instead of the goal interp_cs r vm (polynomial_simplify r e1) == interp_cs r vm (polynomial_simplify r e2))), we could write a function that test the equality between two canonical_sum. This function would detect constants that need to be equal to 0 or 1, and generate goals for these equalities.

[TWal]

I don't intend to finish this pull request in the future, closing it.