From eb4181e9e965fc04eb5a1b3dd1530ca78d687b07 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 22 Oct 2024 10:38:59 +0200 Subject: [PATCH 1/2] PolyComRing: do not show internal names --- theories/algebra/Poly.ec | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index d04d477f57..196e1e258c 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -495,11 +495,11 @@ proof. by apply/negP => /poly_eqP /(_ 0); rewrite !polyCE /= oner_neq0. qed. clone import Ring.ComRing as PolyComRing with type t <= poly , - op zeror <= poly0, - op oner <= poly1, - op ( + ) <= polyD, - op [ - ] <= polyN, - op ( * ) <= polyM + op zeror = poly0, + op oner = poly1, + op ( + ) = polyD, + op [ - ] = polyN, + op ( * ) = polyM proof addrA by apply ZPoly.addrA proof addrC by apply ZPoly.addrC From 981a63721b3ac1956e5f832d81848a77444c014f Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 6 Dec 2024 14:01:38 +0100 Subject: [PATCH 2/2] wip --- easycrypt.project | 6 +++--- theories/algebra/Poly.ec | 4 ++++ 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/easycrypt.project b/easycrypt.project index f592382998..00c1b0bc84 100644 --- a/easycrypt.project +++ b/easycrypt.project @@ -1,4 +1,4 @@ [general] -provers = Alt-Ergo@2.4 -provers = CVC5@1.0 -provers = Z3@4.12 +provers = Alt-Ergo@2.5 +provers = CVC5@1.1 +provers = Z3@4.8 diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index 196e1e258c..b01ccd393a 100644 --- a/theories/algebra/Poly.ec +++ b/theories/algebra/Poly.ec @@ -517,6 +517,10 @@ clone import Ring.ComRing as PolyComRing with (* -------------------------------------------------------------------- *) lemma mul_lc p q : lc p * lc q = (p * q).[deg p + deg q - 2]. proof. +case: (p = PolyComRing.zeror). + move => ->. + have := mul0r q. +move => ->. case: (p = poly0) => [->|nz_p]; first by rewrite !(mul0r, poly0E). case: (q = poly0) => [->|nz_q]; first by rewrite !(mulr0, poly0E). have ->: deg p + deg q - 2 = (deg p - 1) + (deg q - 1) by ring.