From 2d30ab8e7c39b4dbe014978ec453714d9596cbfa Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 29 Mar 2024 03:30:36 +0100 Subject: [PATCH] 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.