From 200cabd17d20c7d670c9eb1414ac80fa7a413996 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 28 Mar 2024 16:47:46 +0100 Subject: [PATCH 1/4] Better examples about reduction modulo p Bug! --- _CoqProject | 2 + elpi/param.elpi | 2 +- examples/flt3_step.v | 118 +++++++++++++++++++++++++++++++++++++ examples/int_to_Zp.v | 59 ++++++++++--------- theories/Param_prod.v | 2 +- theories/Param_sum.v | 133 ++++++++++++++++++++++++++++++++++++++++++ theories/Trocq.v | 2 +- 7 files changed, 287 insertions(+), 31 deletions(-) create mode 100644 examples/flt3_step.v create mode 100644 theories/Param_sum.v diff --git a/_CoqProject b/_CoqProject index c529cfc..336efb0 100644 --- a/_CoqProject +++ b/_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 diff --git a/elpi/param.elpi b/elpi/param.elpi index 5a035e5..7e35fb1 100644 --- a/elpi/param.elpi +++ b/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, diff --git a/examples/flt3_step.v b/examples/flt3_step.v new file mode 100644 index 0000000..3bf547d --- /dev/null +++ b/examples/flt3_step.v @@ -0,0 +1,118 @@ +(*****************************************************************************) +(* * Trocq *) +(* _______ * Copyright (C) 2023 Inria & MERCE *) +(* |__ __| * (Mitsubishi Electric R&D Centre Europe) *) +(* | |_ __ ___ ___ __ _ * Cyril Cohen *) +(* | | '__/ _ \ / __/ _` | * Enzo Crance *) +(* | | | | (_) | (_| (_| | * Assia Mahboubi *) +(* |_|_| \___/ \___\__, | ************************************************) +(* | | * 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. diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v index a98f461..5e1e017 100644 --- a/examples/int_to_Zp.v +++ b/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. diff --git a/theories/Param_prod.v b/theories/Param_prod.v index ec30dea..3e4716c 100644 --- a/theories/Param_prod.v +++ b/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. \ No newline at end of file diff --git a/theories/Param_sum.v b/theories/Param_sum.v new file mode 100644 index 0000000..4ba5fdd --- /dev/null +++ b/theories/Param_sum.v @@ -0,0 +1,133 @@ +(*****************************************************************************) +(* * Trocq *) +(* _______ * Copyright (C) 2023 Inria & MERCE *) +(* |__ __| * (Mitsubishi Electric R&D Centre Europe) *) +(* | |_ __ ___ ___ __ _ * Cyril Cohen *) +(* | | '__/ _ \ / __/ _` | * Enzo Crance *) +(* | | | | (_) | (_| (_| | * Assia Mahboubi *) +(* |_|_| \___/ \___\__, | ************************************************) +(* | | * 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. diff --git a/theories/Trocq.v b/theories/Trocq.v index 207d601..fd9404c 100644 --- a/theories/Trocq.v +++ b/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. From ef5caf2ade3148503afeb412705df071107645ea Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Thu, 28 Mar 2024 19:25:22 +0100 Subject: [PATCH 2/4] no bug so far --- examples/flt3_step.v | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/examples/flt3_step.v b/examples/flt3_step.v index 3bf547d..712cdf4 100644 --- a/examples/flt3_step.v +++ b/examples/flt3_step.v @@ -49,7 +49,7 @@ 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. @@ -76,15 +76,21 @@ Variable Reqmodp01 : forall (m : int) (x : Zmod9), Rp m x -> Trocq Use Rp Rmul Rzero Rone Radd Rmod3 Param10_paths Reqmodp01. Trocq Use Param01_sum. +Notation not A := (A -> Empty). -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). - +Variable Param01_Empty : Param01.Rel Empty Empty. +Variable Param10_Empty : Param10.Rel Empty Empty. + +Trocq Use Param01_Empty. +Trocq Use 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. Proof. trocq; simpl. -exact: Hyp. -Qed. +Admitted. + (* Print Assumptions IntRedModZp. (* No Univalence *) *) From 670f46f8bf4ee2cf32f4d931bdfa4a4d594a2f4a Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 28 Mar 2024 16:47:46 +0100 Subject: [PATCH 3/4] Better examples about reduction modulo p --- examples/flt3_step.v | 69 +++++++++++++----------------------------- examples/int_to_Zp.v | 19 +++++++++--- theories/Param_Empty.v | 3 ++ theories/Trocq.v | 2 +- 4 files changed, 40 insertions(+), 53 deletions(-) diff --git a/examples/flt3_step.v b/examples/flt3_step.v index 712cdf4..0ee0dcf 100644 --- a/examples/flt3_step.v +++ b/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. diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v index 5e1e017..73eaff2 100644 --- a/examples/int_to_Zp.v +++ b/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. diff --git a/theories/Param_Empty.v b/theories/Param_Empty.v index d2a7f5a..1df4610 100644 --- a/theories/Param_Empty.v +++ b/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. diff --git a/theories/Trocq.v b/theories/Trocq.v index fd9404c..ef93cc1 100644 --- a/theories/Trocq.v +++ b/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. From 2d30ab8e7c39b4dbe014978ec453714d9596cbfa Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 29 Mar 2024 03:30:36 +0100 Subject: [PATCH 4/4] Better examples about reduction modulo p --- elpi/param.elpi | 2 +- examples/flt3_step.v | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/elpi/param.elpi b/elpi/param.elpi index 7e35fb1..5a035e5 100644 --- a/elpi/param.elpi +++ b/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.spy-do! [ +param (app [F|Xs]) B (app [F'|Xs']) (W AppR) :- std.do! [ util.when-debug dbg.steps (coq.say "param/app" F Xs "@" B), annot.typecheck F FTy, fresh-type => param F FTy F' FR, diff --git a/examples/flt3_step.v b/examples/flt3_step.v index 0ee0dcf..b5a41df 100644 --- a/examples/flt3_step.v +++ b/examples/flt3_step.v @@ -63,8 +63,8 @@ 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 ^ 3" := (m * m * m)%int (at level 2) : int_scope. -Notation "m ^ 3" := (m * 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) @@ -91,7 +91,7 @@ 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^3 + n^3)%ℤ ≠ p^3%ℤ. + m * n * p % 3 ≢ 0 -> (m³ + n³)%ℤ ≠ p³%ℤ. Proof. trocq=> /=. Admitted.