Better examples about reduction modulo p

Bug!

_CoqProject

@@ -21,6 +21,7 @@ theories/Param_nat.v
 theories/Param_paths.v
 theories/Param_sigma.v
 theories/Param_prod.v
+theories/Param_sum.v
 theories/Param_option.v
 theories/Param_vector.v
 theories/Param_Empty.v
@@ -29,6 +30,7 @@ theories/Param_list.v
 examples/artifact_paper_example.v
 examples/N.v
 examples/int_to_Zp.v
+examples/flt3_step.v
 examples/peano_bin_nat.v
 examples/setoid_rewrite.v
 examples/summable.v

elpi/param.elpi

@@ -196,7 +196,7 @@ param
     ).
 
 % TrocqConv for F (argument B in param.args) + TrocqApp
-param (app [F|Xs]) B (app [F'|Xs']) (W AppR) :- std.do! [
+param (app [F|Xs]) B (app [F'|Xs']) (W AppR) :- std.spy-do! [
   util.when-debug dbg.steps (coq.say "param/app" F Xs "@" B),
   annot.typecheck F FTy,
   fresh-type => param F FTy F' FR,

examples/flt3_step.v

@@ -0,0 +1,118 @@
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *       Copyright (C) 2023 Inria & MERCE       *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <[email protected]>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <[email protected]>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <[email protected]>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
+
+From Coq Require Import ssreflect.
+From Trocq Require Import Trocq.
+
+Set Universe Polymorphism.
+
+Declare Scope int_scope.
+Delimit Scope int_scope with int.
+Local Open Scope int_scope.
+Declare Scope Zmod9_scope.
+Delimit Scope Zmod9_scope with Zmod9.
+Local Open Scope Zmod9_scope.
+
+Definition unop_param {X X'} RX {Y Y'} RY
+   (f : X -> Y) (g : X' -> Y') :=
+  forall x x', RX x x' -> RY (f x) (g x').
+
+Definition binop_param {X X'} RX {Y Y'} RY {Z Z'} RZ
+   (f : X -> Y -> Z) (g : X' -> Y' -> Z') :=
+  forall x x', RX x x' -> forall y y', RY y y' -> RZ (f x y) (g x' y').
+
+(***
+We setup an axiomatic context in order not to develop
+arithmetic modulo in Coq/HoTT.
+**)
+Axiom (int@{i} : Type@{i}) (zero : int) (add : int -> int -> int)
+      (mul : int -> int -> int) (one : int)
+      (mod3 : int -> int).
+Axiom (addC : forall m n, add m n = add n m).
+Axiom (Zmod9 : Type) (zerop : Zmod9) (addp : Zmod9 -> Zmod9 -> Zmod9)
+      (mulp : Zmod9 -> Zmod9 -> Zmod9) (onep : Zmod9).
+Axiom (modp : int -> Zmod9) (reprp : Zmod9 -> int)
+      (reprpK : forall x, modp (reprp x) = x)
+      (modp3 : Zmod9 -> Zmod9).
+
+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 /.
+
+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.
+
+Definition Rp := SplitSurj.toParam (SplitSurj.Build reprpK).
+
+Axiom Rzero : Rp zero zerop.
+Axiom Rone : Rp one onep.
+Variable Rmod3 : unop_param Rp Rp mod3 modp3.
+Variable Radd : binop_param Rp Rp Rp add addp.
+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.
+
+Lemma flt3_step (m n p : int) :
+   ((m * m * m) + (n * n * n) = (p * p * p))%int ->
+   (eqmodp (mod3 (m * n * p)%int) 0%int).
+
+Proof.
+trocq; simpl.
+exact: Hyp.
+Qed.
+
+(* 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

@@ -19,9 +19,9 @@ Set Universe Polymorphism.
 Declare Scope int_scope.
 Delimit Scope int_scope with int.
 Local Open Scope int_scope.
-Declare Scope Zmodp_scope.
-Delimit Scope Zmodp_scope with Zmodp.
-Local Open Scope Zmodp_scope.
+Declare Scope Zmod7_scope.
+Delimit Scope Zmod7_scope with Zmod7.
+Local Open Scope Zmod7_scope.
 
 Definition binop_param {X X'} RX {Y Y'} RY {Z Z'} RZ
    (f : X -> Y -> Z) (g : X' -> Y' -> Z') :=
@@ -32,54 +32,57 @@ We setup an axiomatic context in order not to develop
 arithmetic modulo in Coq/HoTT.
 **)
 Axiom (int@{i} : Type@{i}) (zero : int) (add : int -> int -> int)
-      (mul : int -> int -> int).
+      (mul : int -> int -> int) (one : int).
 Axiom (addC : forall m n, add m n = add n m).
-Axiom (Zmodp : Type) (zerop : Zmodp) (addp : Zmodp -> Zmodp -> Zmodp)
-      (mulp : Zmodp -> Zmodp -> Zmodp).
-Axiom (modp : int -> Zmodp) (reprp : Zmodp -> int)
+Axiom (Zmod7 : Type) (zerop : Zmod7) (addp : Zmod7 -> Zmod7 -> Zmod7)
+      (mulp : Zmod7 -> Zmod7 -> Zmod7) (onep : Zmod7).
+Axiom (modp : int -> Zmod7) (reprp : Zmod7 -> int)
       (reprpK : forall x, modp (reprp x) = x).
 
 Definition eqmodp (x y : int) := modp x = modp y.
 
 (* for now translations need the support of a global reference: *)
-Definition eq_Zmodp (x y : Zmodp) := (x = y).
-Arguments eq_Zmodp /.
+Definition eq_Zmod7 (x y : Zmod7) := (x = y).
+Arguments eq_Zmod7 /.
 
 Notation "0" := zero : int_scope.
-Notation "0" := zerop : Zmodp_scope.
+Notation "0" := zerop : Zmod7_scope.
+Notation "1" := one : int_scope.
+Notation "1" := onep : Zmod7_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%Zmodp y%Zmodp) : Zmodp_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%Zmodp y%Zmodp) : Zmodp_scope.
+Notation "x * y" := (mulp x%Zmod7 y%Zmod7) : Zmod7_scope.
 
-Module IntToZmodp.
+Module IntToZmod7.
 
 Definition Rp := SplitSurj.toParam (SplitSurj.Build reprpK).
 
 Axiom Rzero : Rp zero zerop.
+Axiom Rone : Rp one onep.
 Variable Radd : binop_param Rp Rp Rp add addp.
 Variable Rmul : binop_param Rp Rp Rp mul mulp.
-Variable Reqmodp01 : forall (m : int) (x : Zmodp), Rp m x ->
-  forall n y, Rp n y -> Param01.Rel (eqmodp m n) (eq_Zmodp x y).
+Variable Reqmodp01 : forall (m : int) (x : Zmod7), Rp m x ->
+  forall n y, Rp n y -> Param01.Rel (eqmodp m n) (eq_Zmod7 x y).
 
-Trocq Use Rp Rmul Rzero Param10_paths Reqmodp01.
+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 : Zmodp), (m = n * n)%Zmodp -> m = 0) ->
- forall (m n p : int), (m = n * n)%int -> (m == 0)%int.
+ forall (m n p : int), (m = n * n)%int ->
+   (m = p * p * p)%int -> (m == 0)%int \/ (m == 1)%int.
 Proof.
-move=> Hyp.
-trocq; simpl.
-exact: Hyp.
-Qed.
+trocq=> /=.
+Admitted.
 
 (* Print Assumptions IntRedModZp. (* No Univalence *) *)
 
-End IntToZmodp.
+End IntToZmod7.
 
-Module ZmodpToInt.
+Module Zmod7ToInt.
 
 Definition Rp := SplitSurj.toParamSym (SplitSurj.Build reprpK).
 
@@ -89,19 +92,19 @@ 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)%Zmodp.
+Goal (forall x y, x + y = y + x)%Zmod7.
 Proof.
   trocq.
   exact addC.
 Qed.
 
-Goal (forall x y z, x + y + z = y + x + z)%Zmodp.
+Goal (forall x y z, x + y + z = y + x + z)%Zmod7.
 Proof.
   intros x y z.
-  suff addpC: forall x y, (x + y = y + x)%Zmodp. {
+  suff addpC: forall x y, (x + y = y + x)%Zmod7. {
     by rewrite (addpC x y). }
   trocq.
   exact addC.
 Qed.
 
-End ZmodpToInt.
+End Zmod7ToInt.

theories/Param_prod.v

@@ -156,4 +156,4 @@ Proof.
   - exact (prod_map_in_R A A' AR B B' BR).
   - exact (prod_R_in_map A A' AR B B' BR).
   - exact (prod_R_in_mapK A A' AR B B' BR).
-Defined.
+Defined.

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_paths Vernac Common Param_nat Param_trans Param_bool Param_sum.