Merge pull request #86 from math-comp/semirings

Fix the support for semirings
math-comp · Sep 29, 2023 · 97a2ceb · 97a2ceb
2 parents b8a2149 + 6c4785a
commit 97a2ceb
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 11 deletions.
diff --git a/examples/ring_examples.v b/examples/ring_examples.v
@@ -2,7 +2,7 @@
 (* `ring_examples_no_check.v`. To edit this file, uncomment `Require Import`s *)
 (* below: *)
 (* From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat. *)
-(* From mathcomp Require Import ring. *)
+(* From mathcomp Require Import ring ssrZ. *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -12,6 +12,18 @@ Import GRing.Theory.
 
 Local Open Scope ring_scope.
 
+Goal forall a b : nat, (a + b) ^+ 2 = a ^+ 2 + b ^+ 2 + 2%N * a * b.
+Proof. move=> a b; ring. Qed.
+
+Goal forall a b : int, (a + b) ^+ 2 = a ^+ 2 + b ^+ 2 + 2 * a * b.
+Proof. move=> a b; ring. Qed.
+
+Goal forall a b : rat, (a + b) ^+ 2 = a ^+ 2 + b ^+ 2 + 2%:R * a * b.
+Proof. move=> a b; ring. Qed.
+
+Goal forall a b : int * rat, (a + b) ^+ 2 = a ^+ 2 + b ^+ 2 + 2%:R * a * b.
+Proof. move=> a b; ring. Qed.
+
 Section AbstractCommutativeRing.
 
 Variables (R : comRingType) (a b c : R) (n : nat).

diff --git a/examples/ring_examples_check.v b/examples/ring_examples_check.v
@@ -1,4 +1,4 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
-From mathcomp Require Import ring.
+From mathcomp Require Import ring ssrZ.
 
 Load "ring_examples.v".
diff --git a/examples/ring_examples_no_check.v b/examples/ring_examples_no_check.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
-From mathcomp Require Import ring.
+From mathcomp Require Import ring ssrZ.
 
 Ltac ring_reflection ::= ring_reflection_no_check.
 

diff --git a/theories/ring.v b/theories/ring.v
@@ -359,6 +359,7 @@ apply: Pcond_simpl_complete;
 Qed.
 
 Ltac reflexivity_no_check :=
+  move=> *;
   match goal with
     | |- @eq ?T ?LHS ?RHS => exact_no_check (@Logic.eq_refl T LHS)
   end.
@@ -403,29 +404,26 @@ End Internals.
 (* Auxiliary Ltac code which will be invoked from Elpi *)
 
 Ltac ring_reflection_check Lem R VarMap Lpe RE1 RE2 PE1 PE2 LpeProofs :=
-  refine (Lem R 100%N VarMap Lpe RE1 RE2 PE1 PE2 LpeProofs
-              (fun _ _ _ _ _ _ _ _ => erefl) _);
-  [ vm_compute; reflexivity ].
+  exact (Lem R 100%N VarMap Lpe RE1 RE2 PE1 PE2 LpeProofs
+             ltac:(reflexivity) ltac:(vm_compute; reflexivity)).
 
 Ltac ring_reflection_no_check Lem R VarMap Lpe RE1 RE2 PE1 PE2 LpeProofs :=
   exact_no_check (Lem
     R 100%N VarMap Lpe RE1 RE2 PE1 PE2 LpeProofs
-    (fun _ _ _ _ _ _ _ _ => ltac:(reflexivity_no_check))
-    ltac:(vm_compute; reflexivity)).
+    ltac:(reflexivity_no_check) ltac:(vm_compute; reflexivity)).
 
 Ltac ring_reflection := ring_reflection_check.
 
 Ltac field_reflection_check Lem F VarMap Lpe RE1 RE2 PE1 PE2 LpeProofs :=
   refine (Lem F 100%N VarMap Lpe RE1 RE2 PE1 PE2 LpeProofs
-              (fun _ _ _ _ _ _ _ _ _ _ => erefl) _);
-  field_normalization.
+              ltac:(reflexivity) ltac:(field_normalization)).
 
 Ltac field_reflection_no_check Lem F VarMap Lpe RE1 RE2 PE1 PE2 LpeProofs :=
   let obligation := fresh in
   eassert (obligation : _);
   [ | exact_no_check (Lem
         F 100%N VarMap Lpe RE1 RE2 PE1 PE2 LpeProofs
-        (fun _ _ _ _ _ _ _ _ _ _ => ltac:(reflexivity_no_check))
+        ltac:(reflexivity_no_check)
         ltac:(field_normalization; exact obligation)) ].
 
 Ltac field_reflection := field_reflection_check.