Merge pull request #16 from math-comp/additive

Add support for additive functions and Z-modules
math-comp · Oct 1, 2021 · 404bfae · 404bfae
2 parents 0bd9a55 + 900245a
commit 404bfae
Show file tree

Hide file tree

Showing 5 changed files with 441 additions and 244 deletions.
diff --git a/examples/ring_examples.v b/examples/ring_examples.v
@@ -19,72 +19,79 @@ Variables (R : comRingType) (a b c : R).
 
 
 (* Using the _%:R embedding from nat to R *)
-Goal 
-    (a + b + c) ^+ 2 =
-    a * a + b ^+ 2 + c * c + 2%:R * a * b + 2%:R * a * c + 2%:R * b * c.
+Goal (a + b + c) ^+ 2 =
+     a * a + b ^+ 2 + c * c + 2%:R * a * b + 2%:R * a * c + 2%:R * b * c.
 Proof. ring. Qed.
 
 (* Using the _%:~R embedding from int to R : 2 is coerced to (Posz 2) : int *)
-Goal 
-    (a + b + c) ^+ 2 =
-    a * a + b ^+ 2 + c * c + 2%:~R * a * b + 2%:~R * a * c + 2%:~R * b * c.
+Goal (a + b + c) ^+ 2 =
+     a * a + b ^+ 2 + c * c + 2%:~R * a * b + 2%:~R * a * c + 2%:~R * b * c.
 Proof. ring. Qed.
 
 (* With an identity hypothesis *)
 (* Using the _%:R embedding from nat to R *)
-Goal 
-    2%:R * a * b = 30%:R -> (a + b) ^+ 2 = a ^+ 2 + b ^+ 2 + 30%:R.
+Goal 2%:R * a * b = 30%:R -> (a + b) ^+ 2 = a ^+ 2 + b ^+ 2 + 30%:R.
 Proof. move=> H; ring: H. Qed.
 
 (* With an identity hypothesis *)
 (* Using the _%:~R embedding from int to R *)
-Goal 
-    2%:~R * a * b = 30%:~R -> (a + b) ^+ 2 = a ^+ 2 + b ^+ 2 + 30%:~R.
+Goal 2%:~R * a * b = 30%:~R -> (a + b) ^+ 2 = a ^+ 2 + b ^+ 2 + 30%:~R.
 Proof. move=> H; ring: H. Qed.
 
-(* With numeral constants *)
-Goal 20%:R * 3%:R = 60%:R :> R.
-Proof. ring. Qed.
+End AbstractCommutativeRing.
 
-Goal 20%:~R * 3%:~R = 60%:~R :> R.
-Proof. ring. Qed.
+Section AbstractRingMorphism.
 
-Goal 200%:~R * 30%:~R = 6000%:~R :> R.
+Variables (R : ringType) (R' : comRingType) (f : {rmorphism R -> R'}) (a b : R).
+
+Goal f ((a + b) ^+ 2) = f a ^+ 2 + f b ^+ 2 + 2%:R * f a * f b.
 Proof. ring. Qed.
 
+End AbstractRingMorphism.
 
-Goal 2%:~R * 10%:~R ^+ 2 * 3%:~R * 10%:~R ^+ 2 = 6%:~R * 10%:~R ^+ 4:> R.
+Section AbstractAdditiveFunction.
+
+Variables (V' V : zmodType) (R : comRingType).
+Variables (g : {additive V' -> V}) (f : {additive V -> R}) (a : V') (b : V).
+
+Goal f (g a + b) ^+ 2 = f (g a) ^+ 2 + f b ^+ 2 + f (g (a *+ 2)) * f b.
 Proof. ring. Qed.
 
-End AbstractCommutativeRing.
+End AbstractAdditiveFunction.
 
-Section RingMorphism.
+Section NumeralExamples.
 
-Variables (R : ringType) (R' : comRingType) (f : {rmorphism R -> R'}) (a b : R).
+Variable (R : comRingType).
 
-Goal f ((a + b) ^+ 2) = f a ^+ 2 + f b ^+ 2 + 2%:R * f a * f b.
+(* With numeral constants *)
+Goal 20%:R * 3%:R = 60%:R :> R.
 Proof. ring. Qed.
 
-End RingMorphism.
+Goal 20%:~R * 3%:~R = 60%:~R :> R.
+Proof. ring. Qed.
 
-Section NumeralExamples.
+Goal 200%:~R * 30%:~R = 6000%:~R :> R.
+Proof. ring. Qed.
+
+Goal 2%:~R * 10%:~R ^+ 2 * 3%:~R * 10%:~R ^+ 2 = 6%:~R * 10%:~R ^+ 4:> R.
+Proof. ring. Qed.
 
-Lemma abstract_constants (R : comRingType): 200%:R * 30%:R = 6000%:R :> R.
+Goal 200%:R * 30%:R = 6000%:R :> R.
 Proof.
 Time ring. (* 0.186 secs *)
 Qed.
 
-Lemma int_constants : 200%:R * 30%:R = 6000%:R :> int.
+Goal 200%:R * 30%:R = 6000%:R :> int.
 Proof.
 Time ring. (* 0.343 secs *)
 Qed.
 
-Lemma rat_constants : 20%:R * 3%:R = 60%:R :> rat.
+Goal 20%:R * 3%:R = 60%:R :> rat.
 Proof.
 Time ring. (* 0.018 secs *)
 Qed.
 
-Lemma rat_constants_larger : 200%:R * 30%:R = 6000%:R :> rat.
+Goal 200%:R * 30%:R = 6000%:R :> rat.
 Proof.
 Time ring. (* 0.208 secs *)
 Qed.
@@ -93,13 +100,12 @@ End NumeralExamples.
 
 Section MoreVariables.
 
-Variables (q w e r t y u i o p a s d f g h j k l 
-: int).
+Variables (q w e r t y u i o p a s d f g h j k l : int).
 
 Lemma test_vars : 
-    q * w * e * r * t * y * u * i * o * p * a * s * d * f * g * h * j * k * l
- =  l * w * e * r * t * y * u * i * o * p * a * s * d * f * g * h * j * k * q.
-  Proof. Time ring. Qed. (* 0.049 secs *)
+  q * w * e * r * t * y * u * i * o * p * a * s * d * f * g * h * j * k * l =
+  l * w * e * r * t * y * u * i * o * p * a * s * d * f * g * h * j * k * q.
+Proof. Time ring. Qed. (* 0.049 secs *)
 
 End MoreVariables.
 

diff --git a/theories/field.elpi b/theories/field.elpi
@@ -20,10 +20,10 @@ quote-arg Ring VarMap (trm Proof)
       (coq.typecheck Proof {{ @eq (GRing.Ring.sort lp:Ring) lp:T1 lp:T2 }})
       "An argument is not a proof of equation of the expected type",
     IdRingMorph = {{ @GRing.idfun_rmorphism lp:Ring }},
-    ring.quote Ring none Ring (x\ x) IdRingMorph T1 RE1 PE1 VarMap,
-    ring.quote Ring none Ring (x\ x) IdRingMorph T2 RE2 PE2 VarMap,
-    RMcorrect1 = {{ @RMEeval_correct lp:Ring lp:Ring lp:IdRingMorph lp:RE1 }},
-    RMcorrect2 = {{ @RMEeval_correct lp:Ring lp:Ring lp:IdRingMorph lp:RE2 }},
+    quote.ring Ring none Ring (x\ x) IdRingMorph T1 RE1 PE1 VarMap,
+    quote.ring Ring none Ring (x\ x) IdRingMorph T2 RE2 PE2 VarMap,
+    RMcorrect1 = {{ @RingEval_correct lp:Ring lp:Ring lp:IdRingMorph lp:RE1 }},
+    RMcorrect2 = {{ @RingEval_correct lp:Ring lp:Ring lp:IdRingMorph lp:RE2 }},
     Proof' = {{ lib:ring.etrans (lib:ring.esym lp:RMcorrect1)
                                 (lib:ring.etrans lp:Proof lp:RMcorrect2) }}
   ].
@@ -37,9 +37,10 @@ pred field-reflection i:term, i:term, i:term, i:term, i:term, i:term, i:term,
                       i:term, i:term, i:goal, o:list sealed-goal.
 field-reflection Ring Field VarMap' Lpe' RE1 RE2 PE1 PE2 LpeProofs' G GS :-
   IdRingMorph = {{ @GRing.idfun_rmorphism lp:Ring }},
-  FMcorrect1 = {{ @FMEeval_correct lp:Ring lp:Field lp:IdRingMorph lp:RE1 }},
-  FMcorrect2 = {{ @FMEeval_correct lp:Ring lp:Field lp:IdRingMorph lp:RE2 }},
-  Fcorrect = {{ @Fcorrect lp:Field 100 lp:VarMap' lp:Lpe' lp:PE1 lp:PE2 lp:LpeProofs' }},
+  FMcorrect1 = {{ @FieldEval_correct lp:Ring lp:Field lp:IdRingMorph lp:RE1 }},
+  FMcorrect2 = {{ @FieldEval_correct lp:Ring lp:Field lp:IdRingMorph lp:RE2 }},
+  Fcorrect =
+    {{ @Fcorrect lp:Field 100 lp:VarMap' lp:Lpe' lp:PE1 lp:PE2 lp:LpeProofs' }},
   coq.ltac.call "field_reflection"
     [ trm FMcorrect1, trm FMcorrect2, trm Fcorrect ] G GS.
 field-reflection _ _ _ _ _ _ _ _ _ _ _ :-
@@ -60,9 +61,9 @@ field (goal _ _ P _ Args as G) GS :- std.do! [
       std.unzip { std.map Args (quote-arg Ring VarMap) } Lpe LpeProofs,
       IdRingMorph = {{ @GRing.idfun_rmorphism lp:Ring }},
       field-mode =>
-        ring.quote Ring (some Field) Ring (x\ x) IdRingMorph T1 RE1 PE1 VarMap,
+        quote.ring Ring (some Field) Ring (x\ x) IdRingMorph T1 RE1 PE1 VarMap,
       field-mode =>
-        ring.quote Ring (some Field) Ring (x\ x) IdRingMorph T2 RE2 PE2 VarMap
+        quote.ring Ring (some Field) Ring (x\ x) IdRingMorph T2 RE2 PE2 VarMap
     ) ReifTime,
     coq.say "Reification:" ReifTime "sec.",
     list-constant Ty VarMap VarMap',