Skip to content

Commit

Permalink
Better examples about reduction modulo p
Browse files Browse the repository at this point in the history
Bug!
  • Loading branch information
CohenCyril committed Mar 28, 2024
1 parent b1c881a commit 200cabd
Show file tree
Hide file tree
Showing 7 changed files with 287 additions and 31 deletions.
2 changes: 2 additions & 0 deletions _CoqProject
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion elpi/param.elpi
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
118 changes: 118 additions & 0 deletions examples/flt3_step.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,118 @@
(*****************************************************************************)
(* * Trocq *)
(* _______ * Copyright (C) 2023 Inria & MERCE *)
(* |__ __| * (Mitsubishi Electric R&D Centre Europe) *)
(* | |_ __ ___ ___ __ _ * Cyril Cohen <cyril.cohen@inria.fr> *)
(* | | '__/ _ \ / __/ _` | * Enzo Crance <enzo.crance@inria.fr> *)
(* | | | | (_) | (_| (_| | * Assia Mahboubi <assia.mahboubi@inria.fr> *)
(* |_|_| \___/ \___\__, | ************************************************)
(* | | * 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.
59 changes: 31 additions & 28 deletions examples/int_to_Zp.v
Original file line number Diff line number Diff line change
Expand Up @@ -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') :=
Expand All @@ -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).

Expand All @@ -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.
2 changes: 1 addition & 1 deletion theories/Param_prod.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Loading

0 comments on commit 200cabd

Please sign in to comment.