From e0708188ab0541b7f3df82a2bb13ba8620f95480 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 22 Apr 2024 14:56:48 +0200 Subject: [PATCH] Better examples about reduction modulo p (#36) * Better examples about reduction modulo p --------- Co-authored-by: Assia Mahboubi --- _CoqProject | 2 + examples/flt3_step.v | 97 ++++++++++++++++++++++++++++++ examples/int_to_Zp.v | 74 +++++++++++++---------- theories/Param_Empty.v | 3 + theories/Param_prod.v | 2 +- theories/Param_sum.v | 133 +++++++++++++++++++++++++++++++++++++++++ theories/Trocq.v | 2 +- 7 files changed, 281 insertions(+), 32 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/examples/flt3_step.v b/examples/flt3_step.v new file mode 100644 index 0000000..b5a41df --- /dev/null +++ b/examples/flt3_step.v @@ -0,0 +1,97 @@ +(*****************************************************************************) +(* * 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. +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. diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v index a98f461..73eaff2 100644 --- a/examples/int_to_Zp.v +++ b/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. 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/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..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_paths Vernac Common Param_nat Param_trans Param_bool Param_sum Param_Empty.