From 2fe0aaf1145e0c3d92a0de8d59cb4295f36472d8 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Thu, 17 Oct 2024 11:52:08 +0200
Subject: [PATCH] flt3_step: closed under the global context

---
 examples/flt3_step.v   | 24 ++++++++++++++----------
 theories/Param_Empty.v | 17 +++++++++++++++--
 2 files changed, 29 insertions(+), 12 deletions(-)

diff --git a/examples/flt3_step.v b/examples/flt3_step.v
index 7af7378..7cac6a8 100644
--- a/examples/flt3_step.v
+++ b/examples/flt3_step.v
@@ -41,9 +41,9 @@ Definition binop_param {X X'} RX {Y Y'} RY {Z Z'} RZ
 
 (* Arithmetic on Z_9*)
 Definition Zmod9 := 'Z_9.
-Definition zerop : Zmod9 := Zp0. 
+Definition zerop : Zmod9 := Zp0.
 Definition addp : Zmod9 -> Zmod9 -> Zmod9 := @Zp_add 8.
-Definition mulp : Zmod9 -> Zmod9 -> Zmod9 := @Zp_mul 8. 
+Definition mulp : Zmod9 -> Zmod9 -> Zmod9 := @Zp_mul 8.
 Definition onep : Zmod9 := Zp1.
 
 (* Quotient *)
@@ -94,7 +94,7 @@ Notation "x ≢ y" := (not (eqmodp x%int y%int))
   (format "x  ≢  y", at level 70) : int_scope.
 Notation "x ≠ y" := (not (x = y)) (at level 70).
 Notation "ℤ/9ℤ" := Zmod9.
-Notation ℤ := int. 
+Notation ℤ := int.
 
 Definition Rp := SplitSurj.toParam (SplitSurj.Build reprpK).
 
@@ -116,12 +116,12 @@ rewrite /Rp /= /graph /= => x1 y1 <- x2 y2 <-.
 by rewrite /modp rmorphM.
 Qed.
 
-(* This lemma says that mod-ing by 3 is the same as first mod-ing by 9 and then 
+(* This lemma says that mod-ing by 3 is the same as first mod-ing by 9 and then
    mod-ing by 3. Can probably be streamlined... *)
 Lemma Rmod3 : unop_param Rp Rp mod3 modp3.
 Proof.
 rewrite /Rp /= /graph /= => x y <- {y}.
-rewrite /modp /mod3 /modp3. 
+rewrite /modp /mod3 /modp3.
 apply: val_inj=> /=.
 wlog : x / exists n, x = Posz n.
   move=> hwlog.
@@ -144,7 +144,7 @@ case=> n -> {x}.
 set u : 'I_9 := _%:~R; set v := (X in (X %% 3)%N).
 have {v} -> : v = (n %% 9)%N by exact: val_Zp_nat.
 rewrite modn_dvdm //.
-have -> : nat_of_ord u = ((n %% 3)%N %% 9)%N. 
+have -> : nat_of_ord u = ((n %% 3)%N %% 9)%N.
   by rewrite {}/u modz_nat /= (@val_Zp_nat 9).
 rewrite modn_small //; apply: (@ltn_trans 3) => //; exact: ltn_pmod.
 Qed.
@@ -164,8 +164,12 @@ Trocq Use Param01_Empty.
 Trocq Use Param10_Empty.
 
 Lemma flt3_step : forall (m n p : ℤ),
-  (m * n * p % 3)%Z ≢ 0 -> (m³ + n³)%ℤ  ≠ p³%ℤ.
+  ((m * n * p)%Z % 3)%Z ≢ 0 -> (m³ + n³)%ℤ  ≠ p³%ℤ.
 Proof.
-(* automated proof of the reduction of the problem to ℤ/9ℤ *)
-trocq => /=.
-Admitted.
+trocq=> /=.
+
+(* the following should be a call to troq to compute *)
+move=> + + + /eqP + /eqP.
+by do 3![case; do 9?[case=> //=] => ?].
+Qed.
+Print Assumptions flt3_step.
diff --git a/theories/Param_Empty.v b/theories/Param_Empty.v
index 9fd8327..426897f 100644
--- a/theories/Param_Empty.v
+++ b/theories/Param_Empty.v
@@ -57,5 +57,18 @@ Proof.
   - exact R_in_mapK_Empty.
 Defined.
 
-Axiom Param01_Empty : Param01.Rel Empty Empty.
-Axiom Param10_Empty : Param10.Rel Empty Empty.
+Definition Param01_Empty : Param01.Rel Empty Empty.
+Proof.
+unshelve econstructor; first exact: EmptyR.
+- done.
+- constructor; exact map_Empty.
+Defined.
+
+
+Definition Param10_Empty : Param10.Rel Empty Empty.
+Proof.
+unshelve econstructor; first exact: EmptyR.
+- constructor; exact map_Empty.
+- done.
+Defined.
+