-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Better examples about reduction modulo p (#36)
* Better examples about reduction modulo p --------- Co-authored-by: Assia Mahboubi <Assia.Mahboubi@inria.fr>
- Loading branch information
1 parent
b1c881a
commit e070818
Showing
7 changed files
with
281 additions
and
32 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,97 @@ | ||
| (*****************************************************************************) | ||
| (* * 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. | ||
| 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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,133 @@ | ||
| (*****************************************************************************) | ||
| (* * 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 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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters