From ef5caf2ade3148503afeb412705df071107645ea Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Thu, 28 Mar 2024 19:25:22 +0100 Subject: [PATCH] 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 *) *)