Better examples about reduction modulo p

examples/flt3_step.v

@@ -18,6 +18,7 @@ Set Universe Polymorphism.
 
 Declare Scope int_scope.
 Delimit Scope int_scope with int.
+Delimit Scope int_scope with ℤ.
 Local Open Scope int_scope.
 Declare Scope Zmod9_scope.
 Delimit Scope Zmod9_scope with Zmod9.
@@ -49,20 +50,30 @@ Definition eqmodp (x y : int) := modp x = modp y.
 
 (* for now translations need the support of a global reference: *)
 Definition eq_Zmod9 (x y : Zmod9) := (x = y).
-Arguments eq_Zmod9 /. 
+Arguments eq_Zmod9 /.
 
 Notation "0" := zero : int_scope.
 Notation "0" := zerop : Zmod9_scope.
 Notation "1" := one : int_scope.
 Notation "1" := onep : Zmod9_scope.
-Notation "x == y" := (eqmodp x%int y%int)
-  (format "x  ==  y", at level 70) : int_scope.
 Notation "x + y" := (add x%int y%int) : int_scope.
 Notation "x + y" := (addp x%Zmod9 y%Zmod9) : Zmod9_scope.
 Notation "x * y" := (mul x%int y%int) : int_scope.
 Notation "x * y" := (mulp x%Zmod9 y%Zmod9) : Zmod9_scope.
-
-Module IntToZmod9.
+Notation not A := (A -> Empty). 
+Notation "m ^ 2" := (m * m)%int (at level 2) : int_scope.
+Notation "m ^ 2" := (m * m)%Zmod9 (at level 2) : Zmod9_scope.
+Notation "m ^ 3" := (m * m * m)%int (at level 2) : int_scope.
+Notation "m ^ 3" := (m * m * m)%Zmod9 (at level 2) : Zmod9_scope.
+Notation "m % 3" := (mod3 m)%int (at level 2) : int_scope.
+Notation "m % 3" := (modp3 m)%Zmod9 (at level 2) : Zmod9_scope.
+Notation "x ≡ y" := (eqmodp x%int y%int)
+  (format "x  ≡  y", at level 70) : int_scope.
+Notation "x ≢ y" := (not (eqmodp x%int y%int))
+  (format "x  ≢  y", at level 70) : int_scope.
+Notation "x ≠ y" := (not (x = y)).
+Notation "ℤ/9ℤ" := Zmod9.
+Notation ℤ := int.
 
 Definition Rp := SplitSurj.toParam (SplitSurj.Build reprpK).
 
@@ -74,51 +85,13 @@ Variable Rmul : binop_param Rp Rp Rp mul mulp.
 Variable Reqmodp01 : forall (m : int) (x : Zmod9), Rp m x ->
   forall n y, Rp n y -> Param01.Rel (eqmodp m n) (eq_Zmod9 x y).
 
-Trocq Use Rp Rmul Rzero Rone Radd Rmod3 Param10_paths Reqmodp01.
-Trocq Use Param01_sum.
-Notation not A := (A -> Empty). 
 
-Variable Param01_Empty : Param01.Rel Empty Empty.
-Variable Param10_Empty : Param10.Rel Empty Empty.
 
-Trocq Use Param01_Empty.
-Trocq Use Param10_Empty.
+Trocq Use Rp Rmul Rzero Rone Radd Rmod3 Param10_paths Reqmodp01.
+Trocq Use Param01_sum Param01_Empty Param10_Empty.
 
-Lemma flt3_step : forall (m n p : int),
-   (not (eqmodp (mod3 (m * n * p)%int) 0%int)) ->
-  not ((m * m * m) + (n * n * n) = (p * p * p))%int.
+Lemma flt3_step : forall (m n p : ℤ),
+  m * n * p % 3 ≢ 0 -> (m^3 + n^3)%ℤ  ≠ p^3%ℤ.
 Proof.
-trocq; simpl.
+trocq=> /=.
 Admitted.
-
-
-(* Print Assumptions IntRedModZp. (* No Univalence *) *)
-
-End IntToZmod9.
-
-Module Zmod9ToInt.
-
-Definition Rp := SplitSurj.toParamSym (SplitSurj.Build reprpK).
-
-Axiom Rzero : Rp zerop zero.
-Variable Radd : binop_param Rp Rp Rp addp add.
-Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp.
-
-Trocq Use Rp Param01_paths Param10_paths Radd Rzero.
-
-Goal (forall x y, x + y = y + x)%Zmod9.
-Proof.
-  trocq.
-  exact addC.
-Qed.
-
-Goal (forall x y z, x + y + z = y + x + z)%Zmod9.
-Proof.
-  intros x y z.
-  suff addpC: forall x y, (x + y = y + x)%Zmod9. {
-    by rewrite (addpC x y). }
-  trocq.
-  exact addC.
-Qed.
-
-End Zmod9ToInt.

examples/int_to_Zp.v

@@ -18,6 +18,7 @@ Set Universe Polymorphism.
 
 Declare Scope int_scope.
 Delimit Scope int_scope with int.
+Delimit Scope int_scope with ℤ.
 Local Open Scope int_scope.
 Declare Scope Zmod7_scope.
 Delimit Scope Zmod7_scope with Zmod7.
@@ -55,6 +56,18 @@ Notation "x + y" := (add x%int y%int) : int_scope.
 Notation "x + y" := (addp x%Zmod7 y%Zmod7) : Zmod7_scope.
 Notation "x * y" := (mul x%int y%int) : int_scope.
 Notation "x * y" := (mulp x%Zmod7 y%Zmod7) : Zmod7_scope.
+Notation "m ²" := (m * m)%int (at level 2) : int_scope.
+Notation "m ²" := (m * m)%Zmod7 (at level 2) : Zmod7_scope.
+Notation "m ³" := (m * m * m)%int (at level 2) : int_scope.
+Notation "m ³" := (m * m * m)%Zmod7 (at level 2) : Zmod7_scope.
+Notation "x ≡ y" := (eqmodp x%int y%int)
+  (format "x  ≡  y", at level 70) : int_scope.
+Notation "x ≢ y" := (not (eqmodp x%int y%int))
+  (format "x  ≢  y", at level 70) : int_scope.
+Notation "x ≠ y" := (not (x = y)).
+Notation "ℤ/7ℤ" := Zmod7.
+Notation ℤ := int.
+Notation "P ∨ Q" := (P + Q)%type.
 
 Module IntToZmod7.
 
@@ -69,11 +82,9 @@ Variable Reqmodp01 : forall (m : int) (x : Zmod7), Rp m x ->
 
 Trocq Use Rp Rmul Rzero Rone Param10_paths Reqmodp01.
 Trocq Use Param01_sum.
-Notation "P \/ Q" := (P + Q)%type.
 
-Lemma IntRedModZp :
- forall (m n p : int), (m = n * n)%int ->
-   (m = p * p * p)%int -> (m == 0)%int \/ (m == 1)%int.
+Lemma IntRedModZp : forall (m n p : ℤ),
+  m = n²%ℤ -> m = p³%ℤ  -> m ≡ 0 ∨ m ≡ 1.
 Proof.
 trocq=> /=.
 Admitted.

theories/Param_Empty.v

@@ -55,3 +55,6 @@ Proof.
   - exact R_in_map_Empty.
   - exact R_in_mapK_Empty.
 Defined.
+
+Axiom Param01_Empty : Param01.Rel Empty Empty.
+Axiom Param10_Empty : Param10.Rel Empty Empty.

theories/Trocq.v

@@ -15,4 +15,4 @@ From elpi Require Export elpi.
 From HoTT Require Export HoTT.
 From Trocq Require Export
   HoTT_additions Hierarchy Param_Type Param_forall Param_arrow Database Param
-  Param_paths Vernac Common Param_nat Param_trans Param_bool Param_sum.
+  Param_paths Vernac Common Param_nat Param_trans Param_bool Param_sum Param_Empty.