Better examples about reduction modulo p

_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

examples/flt3_step.v

@@ -0,0 +1,97 @@
+(*****************************************************************************)
+(*                            *                    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.
+Delimit Scope int_scope with ℤ.
+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" := (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.
+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 ³" := (m * m * m)%int (at level 2) : int_scope.
+Notation "m ³" := (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).
+
+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 Param01_Empty Param10_Empty.
+
+Lemma flt3_step : forall (m n p : ℤ),
+  m * n * p % 3 ≢ 0 -> (m³ + n³)%ℤ  ≠ p³%ℤ.
+Proof.
+trocq=> /=.
+Admitted.

examples/int_to_Zp.v

@@ -18,10 +18,11 @@ 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 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 +33,67 @@ 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.
-
-Module IntToZmodp.
+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.
 
 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.
 
-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.
+Lemma IntRedModZp : forall (m n p : ℤ),
+  m = n²%ℤ -> m = p³%ℤ  -> m ≡ 0 ∨ m ≡ 1.
 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 +103,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_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/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/Param_sum.v

@@ -0,0 +1,133 @@
+(*****************************************************************************)
+(*                            *                    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 HoTT Require Import HoTT.
+Require Import Hierarchy.
+
+Set Universe Polymorphism.
+Unset Universe Minimization ToSet.
+
+Print sum.
+
+Inductive sumR
+  A A' (AR : A -> A' -> Type) B B' (BR : B -> B' -> Type) : A + B -> A' + B' -> Type :=
+    | inlR a a' (aR : AR a a') : sumR A A' AR B B' BR (inl a) (inl a')
+    | inrR b b' (bR : BR b b') : sumR A A' AR B B' BR (inr b) (inr b').
+
+(*  *)
+
+Definition sum_map
+  (A A' : Type) (AR : Param10.Rel A A') (B B' : Type) (BR : Param10.Rel B B') :
+    A + B -> A' + B' :=
+      fun p =>
+        match p with
+        | inl a => inl (map AR a)
+        | inr b => inr (map BR b)
+        end.
+
+Definition inl_inj {A B} {a1 a2 : A}  :
+  @inl A B a1 = inl a2 -> a1 = a2 :=
+    fun e => 
+      match e in @paths _ _ (inl a1) return _ = a1 with
+      | @idpath _ _ => @idpath _ a1
+      end.
+
+Definition inr_inj {A B} {b1 b2 : B}  :
+  @inr A B b1 = inr b2 -> b1 = b2 :=
+    fun e => 
+      match e in @paths _ _ (inr b1) return _ = b1 with
+      | @idpath _ _ => @idpath _ b1
+      end.
+
+Definition inl_inr {A B a b} : @inl A B a = inr b -> False.
+Proof. discriminate. Defined.
+
+Definition inr_inl {A B b a} : @inr A B b = inl a -> False.
+Proof. discriminate. Defined.
+
+Definition sum_map_in_R
+  (A A' : Type) (AR : Param2a0.Rel A A') (B B' : Type) (BR : Param2a0.Rel B B') :
+    forall p p', sum_map A A' AR B B' BR p = p' -> sumR A A' AR B B' BR p p'.
+Proof.
+case=> [a|b] [a'|b']; do ?discriminate.
+- by move=> /inl_inj<-; constructor; apply: map_in_R.
+- by move=> /inr_inj<-; constructor; apply: map_in_R.
+Defined.
+
+(*  *)
+
+Definition sum_R_in_map
+  (A A' : Type) (AR : Param2b0.Rel A A') (B B' : Type) (BR : Param2b0.Rel B B') :
+    forall p p', sumR A A' AR B B' BR p p' -> sum_map A A' AR B B' BR p = p'.
+Proof.
+by move=> _ _ [a a' aR|b b' bR]/=; apply: ap; apply: R_in_map.
+Defined.
+
+Definition sum_R_in_mapK
+  (A A' : Type) (AR : Param40.Rel A A') (B B' : Type) (BR : Param40.Rel B B') :
+    forall p p' (r : sumR A A' AR B B' BR p p'),
+      sum_map_in_R A A' AR B B' BR p p' (sum_R_in_map A A' AR B B' BR p p' r) = r.
+Proof.
+  move=> _ _ [a a' aR|b b' bR]/=; rewrite /internal_paths_rew.
+Admitted.
+
+Definition Map0_sum A A' (AR : Param00.Rel A A') B B' (BR : Param00.Rel B B') :
+  Map0.Has (sumR A A' AR B B' BR).
+Proof. constructor. Defined.
+
+Definition Map1_sum A A' (AR : Param10.Rel A A') B B' (BR : Param10.Rel B B') :
+  Map1.Has (sumR A A' AR B B' BR).
+Proof. constructor. exact (sum_map A A' AR B B' BR). Defined.
+
+Definition Map2a_sum A A' (AR : Param2a0.Rel A A') B B' (BR : Param2a0.Rel B B') :
+  Map2a.Has (sumR A A' AR B B' BR).
+Proof.
+  unshelve econstructor.
+  - exact (sum_map A A' AR B B' BR).
+  - exact (sum_map_in_R A A' AR B B' BR).
+Defined.
+
+Definition Map2b_sum A A' (AR : Param2b0.Rel A A') B B' (BR : Param2b0.Rel B B') :
+  Map2b.Has (sumR A A' AR B B' BR).
+Proof.
+  unshelve econstructor.
+  - exact (sum_map A A' AR B B' BR).
+  - exact (sum_R_in_map A A' AR B B' BR).
+Defined.
+
+Definition Map3_sum A A' (AR : Param30.Rel A A') B B' (BR : Param30.Rel B B') :
+  Map3.Has (sumR A A' AR B B' BR).
+Proof.
+  unshelve econstructor.
+  - exact (sum_map A A' AR B B' BR).
+  - exact (sum_map_in_R A A' AR B B' BR).
+  - exact (sum_R_in_map A A' AR B B' BR).
+Defined.
+
+Definition Map4_sum A A' (AR : Param40.Rel A A') B B' (BR : Param40.Rel B B') :
+  Map4.Has (sumR A A' AR B B' BR).
+Proof.
+  unshelve econstructor.
+  - exact (sum_map A A' AR B B' BR).
+  - exact (sum_map_in_R A A' AR B B' BR).
+  - exact (sum_R_in_map A A' AR B B' BR).
+  - exact (sum_R_in_mapK A A' AR B B' BR).
+Defined.
+
+Definition Param01_sum A A' (AR : Param01.Rel A A') B B' (BR : Param01.Rel B B') :
+  Param01.Rel (A + B) (A' + B').
+exists (sumR A A' AR B B' BR).
+- exact: Map0_sum.
+- admit.
+Admitted.

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 Param_Empty.