Formalizing Elligator (ECC)

Stream: general

[Chris Anto Fröschl]

Greetings everyone.

This is the first time I'm about to ask a question here. I hope this channel is the most appropriate regarding this subject.

I have played through the Natural Number Game and I am still working through MIL. Therefore, forgive me if I'm missing some obvious solutions.

I intend to formalize Elligator as introduced in https://eprint.iacr.org/2013/325.pdf (Chapter 3 and 5). I hope people interested can aid me as a beginner hitting dead ends.

Currently I'm only trying to formalize all the statements of Chapter 3, i.e. Elligator 1, postponing the actual proofs for later.

I've already got Theorem 1 somewhat formalized (definitely not perfect or beautiful, but I wanted to remain as close to the original as possible given my current Lean abilities).

Regarding Definition 2, the decoding function, I'm inexperienced at how to handle such function definitions with more complex return types, i.e. a point on a complete Edwards Curve. I've seen some function declarations in MIL Chapter 4, but in my case I need to get the Theorem 1 x and y into this definition, while providing an appropriate signature types. For the latter I suppose a beforehand prepared equivalent Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass configuration is the way to go?

Any better/more accessible options? I thought about totally ignoring the notion of an Elliptic curve and just returning a tuple of G(p) points.

Any recommendations?

There are also several more questions which I've tried to elaborate in my code comments. Although these are mostly issues which will hurt any time later or might just be bad architecture decisions on my part. Therefore, recommendations are welcome!

Here is my current attempt:

import Mathlib.FieldTheory.Finite.GaloisField
-- import Mathlib.NumberTheory.LegendreSymbol.Basic

-- TODO noncomputable => consequences in usage?
-- TODO define necessary theorems for proof as stated in paper
noncomputable def χ
  [Fact (Nat.Prime q)]
  (a : GaloisField q 1)
  : GaloisField q 1 := a^((q-1)/2)

-- TODO Could also factor all the helper variables out in lemmas
theorem elligator1_map_theorem1
  (q n : Nat)
  (q_mod_4_congruent_3 : q % 4 = 3)
  -- TODO Fact wanted like this? More inexplicit variant? Otherwise I can't build GaloisField
  -- TODO How to make q itself a prime power (like in the paper) instead of just a prime?
  -- Perhaps just define another prime which is taken ^ in an assertion to define the actual q
  -- Staying with normal prime for now to see how proof is affected...
  -- => Staying with power of 1 for now so that legendre symbol fits proofs
  -- TODO if proof easily extendable from G(p) to G(p^n), we actually showed
  -- more than the paper explicitly typesetted
  [Fact (Nat.Prime q)]
  (s c d r u v X Y x y : GaloisField q 1)
  (s_h1 : s ≠ 0)
  (s_h2 : (s^2 - 2) * (s^2 + 2) ≠ 0)
  (c_h : c = 2 / s^2 )
  (r_h : r = c + 1 / c)
  (d_h : d = -(c + 1)^2 / (c - 1)^2)
  :
  (c * (c - 1) * (c + 1) ≠ 0)
  ∧ (r ≠ 0)
  -- TODO more elegant way to express a number being a square?
  -- (or in this case a non-square)
  ∧ (¬ (∃ (w : GaloisField q 1), w^2 = d))
  ∧ (
    -- TODO how to exclude +- 1 since this is a type, not a set
    -- -> declaring t above and an extra h could perhaps do... better more general way?
    -- -> actually no... forall would mean all t's from the type, ignoring the h
    ∀ (t : GaloisField q 1), (t ≠ 1 ∧ t ≠ -1) →
      u = (1 - t) / (1 + t)
      ∧ v = u^5 + (r^2 - 2) * u^3 + u
      ∧ X = χ v * u
      ∧ Y = (χ v * v)^((q+1)/4) * χ v * χ (u^2 + 1 / c^2)
      ∧ x = (c - 1) * s * X * (1 + X) / Y
      ∧ y = (r * X - (1 + X)^2) / (r * X + (1 + X)^2)
      ∧ x^2 + y^2 = 1 + d * x^2 * y^2
      ∧ u * v * X * Y * x * (y + 1) ≠ 0
      ∧ Y^2 = X^5 + (r^2 - 2) * X^3 + X
  )
  := by
  sorry

-- TODO how to use the variables introduced by above theorem (need x and y)
-- TODO (x, y) type = E(GaloisField q 1) possible (complete Edwards curve)
def elligator1_map
  [Fact (Nat.Prime q)]
  (t : GaloisField q 1)
  -- TODO below is just a filler
  : (GaloisField q 1) :=
  t

[Chris Anto Fröschl]

Regarding my χ Definition which is just a Legendre Symbol (which I can't use because of it's limitation to integers, i.e. not G(q) elements), can someone explain what limitations I'm going to face regarding the required "noncomputation" flag?

I inserted it, because the used GaloisField apperantly restricts the Definition:

failed to compile definition, compiler IR check failed at 'χ'. Error: depends on declaration 'instFieldGaloisField', which has no executable code; consider marking definition as 'noncomputable'

I just intend to use χ as a matter of proof. But regarding an actual Elligator definition as an executable function, this might bring restrictions from what I understand?

Are there any alternatives I could try?
As a computer scientist, I of course immediately thought about type casting/coercing my existing G(q) element to an integer, to in the end be able to use Mathlib.NumberTheory.LegendreSymbol . But I failed to get something to compile that way.

[Kenny Lau]

@Chris Froeschl if you're a mathematician, then i would say "noncomputable has no consequences, and you can use it freely"

if you're a computer scientist, then i would say "noncomputable has no consequences, and you can use it freely"

[Kenny Lau]

(i don't think we've really developed a lot on the computability of finite fields, so they're all non-computable as of now)

[Chris Anto Fröschl]

@Kenny Lau that's more than enough for me. Thank you.

[Jz Pan]

Isn't GaloisField q 1 ZMod q ?

[Chris Anto Fröschl]

Jz Pan said:

Isn't GaloisField q 1 ZMod q ?

Indeed, although I intend to extend the proof for prime powers later. I'm just using GaloisField q 1 with an explicit 1 currently, since the paper does so in the out written proof (while claiming that the validity extends to prime powers)

[Jz Pan]

Then maybe I think you should use {F : Type*} [Field F] [Fintype F] (or [Finite F]) instead, as not all finite fields are equal to some GaloisField, but just isomorphic to...

[Quang Dao]

I think we badly need a verified library for elliptic curve cryptography (where everything is executable), and those of us working on SNARK formalization would be very interested: https://github.com/Verified-zkEVM/ArkLib

[Quang Dao]

What is your goal in formalizing Elligator? Do you want to be more involved in setting up a general ECC library?

[Kevin Buzzard]

Do you need finite fields beyond $\Z/p\Z$ with $p$ prime (e.g. finite fields of size $2^{255}$)? If so then figuring out how to model them computationally efficiently would be something which you can think about before launching into elliptic curves.

[Chris Anto Fröschl]

Jz Pan said:

Then maybe I think you should use {F : Type*} [Field F] [Fintype F] (or [Finite F]) instead, as not all finite fields are equal to some GaloisField, but just isomorphic to...

I've seen this notation already. But admittedly I'm somewhat overwhelmed and confused at what exactly is happening and where my q comes into play. The documentation didn't help me either. Would you mind to elaborate a bit more?

Perhaps Zmod q is the correct choice after all (?). Regarding my previous response, I misread that ZMod is somehow restricted to primes (which it is not). However, I'm still unsure if a concrete FiniteField type of some sort would be more appropriate regarding the usage in later ECC definitions.

[Chris Anto Fröschl]

Quang Dao said:

What is your goal in formalizing Elligator? Do you want to be more involved in setting up a general ECC library?

Nothing in particular. It's part of a university thesis I'm writing about Elligator while getting more comfortable with Lean itself.

Working towards a more general ECC library is perhaps too much of a leap for a beginner like me. Although I'm currently searching for follow-up research topics, where formalization of general cryptographic protocols (especially zero-knowledge proofs) would definitely be of interest.

[Kenny Lau]

@Chris Froeschl the crucial problem here is that, (i haven't read the paper) it seems that your project is dependent on the theory of finite fields

[Kenny Lau]

and we don't have a computability theory for finite fields

[Kenny Lau]

i understand that you only want to formalise a certain part of computability theory, but one very important point of Lean is that it is built from the ground up, nobody can skip any steps

[Kevin Buzzard]

Just to be clear: there are finite fields of prime order $p$ for all primes, and they are implemented in a way which presumably computes, or could easily be made computable, with ZMod p. And then there are prime powers $q$ such as 4, and for each prime power $q$ there's a finite field of size $q$, and it is not ZMod q (this is not a field if $q$ isn't prime), and it is a mildly nontrivial, but solved, problem to figure out how to make computationally efficient models of these finite fields, but this has not been implemented in Lean yet.

[Kevin Buzzard]

For example the finite field of size 4 is not $\{0,1,2,3\}$ (which satisfies $2^2=0$, this can't happen in a field) but is of the form $\{0,1,\alpha,\alpha+1\}$ where $\alpha^2=\alpha+1.$ For more general prime powers one wants a generalization of this construction so one needs an analogue of $X^2=X+1$ and then some way of implementing finite fields involving having a specific basis, maybe fast look-up for multiplication and so on.

[Kenny Lau]

image.png

From the paper linked, it seems like q is an arbitrary prime power, not just prime

[Chris Anto Fröschl]

@Kevin Buzzard thank you for the elaboration. Isn't a Galois Field therefore a good choice in my case of using a prime power?
I could of course also just restrict myself to p^1 while using ZMod p and see how far I can get. The theorem proof is only extendable to a prime power, but a plain prime is also more than enough to give a valid proof.

@Kenny Lau
Regarding computability: If I understood the comments before correctly, this shouldn't hinder me regarding the classical reasoning for the proof, right? If so, I'm for now totally happy with that. Of course, I can understand, that there is a longing to have a computability theory for such things. But that's another topic for another day.

Regarding prime powers: yes and no. The actual map is provably valid for prime powers, but the Elligator interface only cares about primes.

ell1.PNG

ell2.PNG

[Chris Anto Fröschl]

I will try to get my Lean statements more well defined until evening, to offer a new discussion playground.

A pointer on how to reuse the main theorem and it's variables inside a def would perhaps be helpful to finish the map definition without any Elliptic Curve. I at least haven't seen an explicit reuse of theorem results inside a real def without accompanying proof. I just want access to the x and y, which were proven correct beforehand.

Thanks for the comments so far!

[Kenny Lau]

Chris Froeschl said:

Isn't a Galois Field therefore a good choice in my case of using a prime power?

I don't know if it's better than the other alternative proposed, namely {F : Type*} [Field F] [Fintype F], which you didn't seem to have understood.

this shouldn't hinder me regarding the classical reasoning for the proof, right?

yes, if you're happy to do everything clasically and forgo using #eval, that is completely fine.

[Kenny Lau]

A pointer on how to reuse the main theorem and it's variables inside a def would perhaps be helpful to finish the map definition without any Elliptic Curve. I at least haven't seen an explicit reuse of theorem results inside a real def without accompanying proof. I just want access to the x and y, which were proven correct beforehand.

your example is a bit complicated so i'm not sure if i can give the best advice; but people might make accompanying definitions

[Kenny Lau]

i.e. you can make a def x : Zmod p := ...

[Kenny Lau]

then you can reuse the x later

[Kenny Lau]

the goal is to basically make each theorem as short as possible by using as many accompanying definitions as possible

[Kenny Lau]

big theorems aren't very useful

[Chris Anto Fröschl]

Kenny Lau said:

big theorems aren't very useful

Indeed, I don't think the structure is any beautiful either, but I wanted to start out as close as possible to the paper at the beginning.

Thanks for the seperate def hint. I already expected some solution like that.

[Kenny Lau]

Chris Froeschl said:

Indeed, I don't think the structure is any beautiful either, but I wanted to start out as close as possible to the paper at the beginning.

to re-use an analogy i've used elsewhere, if you're programming a calculator, and you wrote an a algorithm to compute the logarithm of an arbitrary float, then congratulations, your work is done; but in Lean, you also have to provide the theorems to make whatever you wrote usable. in this case i would expect a theorem Real.log (Real.exp x) = x

[Kenny Lau]

image.png

[Kenny Lau]

and if you're following the paper, I see the word "define" in the paper, so I would define those 6 functions

[Kenny Lau]

(please do them inside namespace Elligator, we don't need x appearing in the root namespace :melt: )

[Kenny Lau]

to give you some even more explicit instructions, right after they defined χ in the paper, they actually stated some properties of that function (without proof). if you're following the paper, then you should also prove those properties first :upside_down:

[Chris Anto Fröschl]

I'm currently stuck with an error I can't seem to solve. I'm refactored everything to use GaloisField q n, while providing the necessary properties for χ :

import Mathlib

namespace Elligator1

variable (q : ℕ) [Fact (Nat.Prime q)] (q_mod_4_congruent_3 : q % 4 = 3)
variable (n : ℕ)

noncomputable def χ (a : GaloisField q n) : GaloisField q n := a^((q-1)/2)

lemma χ_a_zero_eq_zero
  (a : GaloisField q n)
  (a_eq_zero : a = 0)
  :
  χ a = 0 := sorry

This results in following error for every χ call:

Application type mismatch: In the application
  @χ a
the argument
  a
has type
  GaloisField q n : Type
but is expected to have type
  ℕ : Type

I'm fairly certain, that my input type for the function is not a Nat, but most of the the time the computer knows better. Any opinions/thoughts?

PS: The previous ZMod q version only worked if I used {q : Nat} instead of (q : Nat), otherwise resulting in the same error. I thought that curly braces are meant for implicit arguments, therefore being not really appropriate in a variable declaration. Am I using something wrong?

[Chris Anto Fröschl]

Kenny Lau said:

Chris Froeschl said:

Isn't a Galois Field therefore a good choice in my case of using a prime power?

I don't know if it's better than the other alternative proposed, namely {F : Type*} [Field F] [Fintype F], which you didn't seem to have understood.

I'm just not able to understand from the documentation or given explanation, how the so defined Finite Field is using a custom q which I can provide. Otherwise, I would of course use the most truthfully related to my paper. I overall find the lack of accessible examples in documentation to be a bit of a hindrance in usage. But that is perhaps just due to lack of experience on my part.

[Kenny Lau]

@Chris Froeschl the issue here is about canonical models, i.e. whether we want to talk about a specific model of GF(p^n) that we constructed, or whether we want to reason about finite fields in general. (this is a matter that mathematicians don't tend to think about a lot) in your case, (why don't you just ask? both times this was brought up, you just said "i can't understand" instead of just asking :melt:), the q would be recoverable as Fintype.card F.

[Kenny Lau]

@Chris Froeschl also, your defined χ is mathematically wrong. please read the paper carefully. you seem to be mixing up hypotheses where q is a prime power and where q is a simple prime.

[Kenny Lau]

@Chris Froeschl now to address the error you received: if you hover over χ, you can see:

image.png

which means that χ is expecting firstly the q and n you implicitly used in its definition

[Chris Anto Fröschl]

Ah stupid me. I'm sorry for asking something that trivial. I got all confused by refactoring.

[Chris Anto Fröschl]

I just expected that the global context variables of this file would be directly know, without me adding some explicit parameter, be it round or curly braces . Therefore, not looking at the extra tool tip

[Chris Anto Fröschl]

Sorry for being absent for a while. I've got a hopefully better structure for the proof regarding some aspects, although I'm still having some concerns regarding the exact translation of the paper statements.
Here is my current draft:

import Mathlib

namespace Elligator1

variable (q : ℕ)
variable (q_prime : Nat.Prime q)
variable [Fact (Nat.Prime q)]
variable (q_mod_4_congruent_3 : q % 4 = 3)
include q_prime q_mod_4_congruent_3

-- Using explict G(p^1) since χ is defined so, therefore the rest of the proof
-- has to also follow this convention
-- Chapter 3.1 Definition of quadratic character
noncomputable def χ
  (a : GaloisField q 1)
  :
  GaloisField q 1 := a^((q-1)/2)

lemma χ_a_zero_eq_zero
  (a : GaloisField q 1)
  (a_eq_zero : a = 0)
  :
  χ q a = 0 := by
    change a^((q-1)/2) = 0
    rw [a_eq_zero]
    apply zero_pow
    intro h
    have h0 : q > 1 := by
      apply Nat.Prime.one_lt
      apply q_prime
    sorry

lemma χ_a_square_eq_square
  (a : GaloisField q 1)
  (a_eq_nonzero : a ≠ 0)
  (a_square : ∃ (w : GaloisField q 1), w^2 = a)
  :
  χ q a = 1 := by
    change a^((q-1)/2) = 1
    sorry

lemma χ_a_nonsquare_eq_nonsquare
  (a : GaloisField q 1)
  (a_eq_nonzero : a ≠ 0)
  (a_square : ¬ (∃ (w : GaloisField q 1), w^2 = a))
  :
  χ q a = -1 := sorry

lemma χ_neg_one_eq_nonsquare :
  χ q (-1 : GaloisField q 1) = -1 := sorry

lemma χ_χ_a_eq_χ_a
  (a : GaloisField q 1)
  :
  χ q (χ q a) = χ q a := sorry

lemma χ_ab_eq_χ_a_mul_χ_b
  (a b : GaloisField q 1)
  :
  χ q (a * b) = χ q a * χ q b := sorry

lemma χ_1_over_a_eq_χ_a
  (a : GaloisField q 1)
  (a_non_zero : a ≠ 0)
  :
  χ q (1 / a) = χ q a := sorry

lemma χ_1_over_a_eq_1_over_χ_a
  (a : GaloisField q 1)
  (a_non_zero : a ≠ 0)
  :
  χ q (1 / a) = 1 / χ q a := sorry

variable (s : GaloisField q 1)
variable (s_h1 : s ≠ 0)
variable (s_h2 : (s^2 - 2) * (s^2 + 2) ≠ 0)
include s_h1 s_h2

noncomputable def c : GaloisField q 1 := 2 / s^2
noncomputable def r : GaloisField q 1 := c q s + 1 / c q s
noncomputable def d : GaloisField q 1 := -(c q s + 1)^2 / (c q s - 1)^2
noncomputable def u (t : GaloisField q 1) : GaloisField q 1 := (1 - t) / (1 + t)
noncomputable def v
  (t : GaloisField q 1)
  : GaloisField q 1 := (u q t)^5 + ((r q s)^2 - 2) * (u q t)^3 + u q t
noncomputable def X (t : GaloisField q 1) : GaloisField q 1 := χ q (v q s t) * u q t
noncomputable def Y (t : GaloisField q 1) : GaloisField q 1 :=
  (χ q (v q s t) * (v q s t))^((q + 1) / 4) * χ q (v q s t) * χ q ((u q t)^2 + 1 / (c q s)^2)
noncomputable def x (t : GaloisField q 1) : GaloisField q 1 :=
  (c q s - 1) * s * (X q s t) * (1 + (X q s t)) / Y q s t
noncomputable def y (t : GaloisField q 1) : GaloisField q 1 :=
  (r q s * (X q s t) - (1 + (X q s t))^2) / ((r q s) * (X q s t) + (1 + (X q s t))^2)

theorem c_h : c q s * (c q s - 1) * (c q s + 1) ≠ 0 := by
  change (2 / s^2) * ((2 / s^2) - 1) * ((2 / s^2) + 1) ≠ 0
  --intro h
  have h1 : (2 / s^2) ≠ 0 := by sorry
  have h2 : s^2 ≠ 2 := by sorry
  have h3 : s^2 ≠ -2 := by sorry
  have h4 : (2 / s^2) ≠ 1 := by sorry
  have h5 : (2 / s^2) ≠ -1 := by sorry
  apply mul_ne_zero
  · apply mul_ne_zero
    · exact h1
--    · apply sub_ne_zero
    · sorry
  -- · apply add_ne_zero
  · sorry

theorem r_ne_zero : r q s ≠ 0 := sorry

theorem d_nonsquare : ¬ (∃ (w : GaloisField q 1), w^2 = d q s) := sorry

theorem u_h :
  -- TODO better way to say the function is well defined for those t's?
  ∀ {t : GaloisField q 1}, (t ≠ 1 ∧ t ≠ -1)
  → ∃ (w : GaloisField q 1), w = u q t := sorry

-- TODO such 'well defined' theorems for v, X, Y, x and y as soon as idiomatic
-- structure is found.

-- Chapter 3.2 Theorem 1
theorem map_fulfills_curve_equation :
  ∀ {t : GaloisField q 1}, (t ≠ 1 ∧ t ≠ -1)
  → (x q s t)^2 + (y q s t)^2 = 1 + (d q s) * (x q s t)^2 * (y q s t)^2 := sorry

-- Chapter 3.2 Theorem 1
theorem map_variables_mul_neq_zero :
  ∀ {t : GaloisField q 1}, (t ≠ 1 ∧ t ≠ -1)
  → u q t * v q s t * X q s t  * Y q s t * x q s t * (y q s t + 1) ≠ 0 := by
    --apply mul_ne_zerow (
    sorry

-- Chapter 3.2 Theorem 1
theorem map_fulfills_specific_equation :
  ∀ {t : GaloisField q 1}, (t ≠ 1 ∧ t ≠ -1)
  → (Y q s t) ^2 = (X q s t)^5 + ((r q s)^2 - 2) * (X q s t)^3 + X q s t := sorry

-- Chapter 3.2 Definition 2
noncomputable def ϕ
  (t : GaloisField q 1)
  : (GaloisField q 1) × (GaloisField q 1) :=
  (x q s t, y q s t)
  --if t == 1 then (0, 1) else (x q s t, y q s t)
  --if (t == 1 ∨ t == -1) then (0, 1) else (x q s t, y q s t)
--  match t with
  -- TODO throws error
  -- | 1 => (0, 1)
  --| -1 => (0, 1)
 -- | _ => (x q s t, y q s t)

-- Chapter 3.3 Theorem 3.1
theorem ϕ_inv_only_two_specific_preimages
  (t : GaloisField q 1)
  :
  ϕ q s t = ϕ q s (-t)
  ↔ ¬ (∃ (w : GaloisField q 1) (h: w ≠ -t), ϕ q s w = ϕ q s t) := by
  sorry

def ϕ_over_F_prop1 (t : GaloisField q 1) := (ϕ q s t).snd + 1 ≠ 0

noncomputable def η
  (t : GaloisField q 1) :
  GaloisField q 1
  := ((ϕ q s t).snd - 1) / (2 * ((ϕ q s t).snd + 1))

def ϕ_over_F_prop2 (t : GaloisField q 1)
  := ∃ (w : GaloisField q 1), w^2 = (1 + η q s t * r q s)^2 - 1

def ϕ_over_F_prop3 (t : GaloisField q 1)
  := (η q s t) * (r q s) = -2 → (ϕ q s t).fst = 2 * s * (c q s - 1) * χ q (c q s) / r q s

-- Chapter 3.3 Theorem 3.2
-- TODO extra theorem as indicated in paper? I.e:
-- (x,y) ∈ ϕ(F_q) → (x,y) ∈ E(F_q) ϕ_prop1 /\ ϕ_prop2 /\ ϕ_prop3
-- Isn't this by definition?
noncomputable def ϕ_over_F
  (t : GaloisField q 1) :
  Set ((GaloisField q 1) × (GaloisField q 1)) :=
  {
    n | n = ϕ q s t
    ∧ ϕ_over_F_prop1 q s t
    ∧ ϕ_over_F_prop2 q s t
    ∧ ϕ_over_F_prop3 q s t
  }

noncomputable def X2 (t : GaloisField q 1) : GaloisField q 1
  := -(1 + (η q s t) * (r q s)) + ((1 + (η q s t) * (r q s))^2 - 1)^((q + 1) / 4)

noncomputable def z (t : GaloisField q 1) : GaloisField q 1
  := χ q
    (
      ((c q s) - 1)
      * s
      * (X2 q s t)
      * (1 + (X2 q s t))
      * (x q s t)
      * (((X2 q s t) + 1 / (c q s)^2)^2)
    )

noncomputable def u2 (t : GaloisField q 1) : GaloisField q 1
  := (z q s t) * (X2 q s t)

noncomputable def t2 (t : GaloisField q 1) : GaloisField q 1
  := (1 - (u2 q s t)) / (1 + (u2 q s t))

-- Chapter 3.3 Theorem 3.3
theorem invmap_representative
  (t : GaloisField q 1)
  -- TODO how to say all are well defined?
  :
  (x q s t, y q s t) ∈ (ϕ_over_F q s t)
  -- TODO exact effect as paper statement?
  → (ϕ q s (t2 q s t)) = (x q s t, y q s t) :=
  sorry

I will try to fill in some sorries as I go along. I don't think, most of the proofs should be too hard, although I'm not that trained in finding the appropriate theorems.

In the meantime, I hope someone could give me directions regarding following problems:

def ϕ

noncomputable def ϕ
  (t : GaloisField q 1)
  : (GaloisField q 1) × (GaloisField q 1) :=
  (x q s t, y q s t)
  if (t == 1 ∨ t == -1) then (0, 1) else (x q s t, y q s t)
--  match t with
  -- TODO throws error
  -- | 1 => (0, 1)
  --| -1 => (0, 1)
 -- | _ => (x q s t, y q s t)

I have to distinguish if the input t is 1, -1 or something else. I tried to do achieve this using a simple if else or pattern matching (see comments in code above). Both resulted in errors which I don't seem to be able to resolve.

Using the if else approach I get:

failed to synthesize
  BEq (GaloisField q 1)

Are GaloisField elements perhaps not viable for such operation?

Using pattern matching:

Dependent elimination failed: Type mismatch when solving this alternative: it has type
  motive
    (Quot.mk
      (⇑(QuotientAddGroup.con (Submodule.toAddSubgroup (RingHom.ker (MvPolynomial.aeval id).toRingHom))).toSetoid)
      (-1)) : Sort ?u.97165
but is expected to have type
  motive t✝ : Sort ?u.97165

I don't care, as long as one of the methods works. Currently, I can't see any working alternatives. Any thoughts?

Following Elements of ... are defined for each

I'm currently trying to map the logic of elements being defined for specific t's by a structure like this (as stated in Theorem 1 of the paper for example):

theorem u_h :
  ∀ {t : GaloisField q 1}, (t ≠ 1 ∧ t ≠ -1)
  → ∃ (w : GaloisField q 1), w = u q t := sorry

I'm not sure if this is idiomatic or any joy regarding provability, i.e. saying that there must be some result if the preconditions are met.

Any alternatives?

I hope my overall structure got a bit more modular. I decided to avoid the notion of an elliptic curve by just talking about tuples of G(q) points, fulfilling some equations (which are definitions of Twisted Edwards Curve equations) by theorem.

Any comments and general naming/structure recommendations are, as always, welcome.

[Kenny Lau]

@Chris Froeschl you're asking 10 questions at the same time, slow down; the correct thing to use for if is = not ==.

[Chris Anto Fröschl]

Oh, I thought == would immediately convert to Boolean, which is somewhat what I want in this case. Either way, the error just switched from being an error regarding BEq synthesize to Decidable synthesize:

failed to synthesize
  Decidable (t = 1)

[Chris Anto Fröschl]

And excuse me for perhaps throwing to many questions into a single message... I feel like some of the problems could be interlinked with the current general structure of the program.

[Aaron Liu]

You want to use the classical decidability instance, to do this you can put open scoped Classical in before the if

[Chris Anto Fröschl]

Perfect, that works. If you know, you know I suppose.

[Chris Anto Fröschl]

I'm currently trying to formalize the statement of Theorem 4:

2025-06-23-131524_493x237_scrot.png

I'm encountering issues regarding the definition of S. My current attempt of translation:

import Mathlib

variable (q : ℕ)
variable (q_prime : Nat.Prime q)
variable [Fact (Nat.Prime q)]
variable (q_mod_4_congruent_3 : q % 4 = 3)
include q_prime q_mod_4_congruent_3

-- ... rest as quoted above

noncomputable def b : ℕ := Int.toNat ⌊ Real.log q ⌋

def S (b : ℕ) : Set (List Bin) := {n | n.length = b}

noncomputable def σ
  (τ : List Bin)
  (τ_in_S : τ ∈ S (b q))
  : GaloisField q 1 :=
  ∑ i ∈ (Finset.range (b q - 1)), τ[i]! * 2^i

noncomputable def ι
  (τ : List Bin)
  (τ_in_S : τ ∈ S (b q)) : (GaloisField q 1 × GaloisField q 1)
  := ϕ q s (σ q τ τ_in_S)

-- TODO does not work because of type inference error
theorem S_cardinality : Set.ncard (S (b q)) = (q + 1) / 2 := by sorry

I'm not even sure if Bin is a proper binary type of any sort. At least I was not able to find any documentation.
The last theorem provides an error, which indicates, that Bin is perhaps not the type I think it is:

▶ 279:36-279:43: error:
don't know how to synthesize implicit argument 'Bin'
  @S ?m.201855 (b q)
context:
q : ℕ
q_prime : Nat.Prime q
inst✝ : Fact (Nat.Prime q)
q_mod_4_congruent_3 : q % 4 = 3
s : GaloisField q 1
s_h1 : s ≠ 0
s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0
⊢ Type ?u.201854

Note: All holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be

If Bin is indeed a valid type, then I'm not able to use it during calculations in regards to type coercion. Error at τ[i]! in σ:

▶ 272:35-272:40: error:
failed to synthesize
  Inhabited Bin

Otherwise, usage of Bool might fit the bill, although requiring another level of indirection.

Either way, I was hoping to use Lists, so that my S definition, aswell as argument access is manageable in followup theorems and definitions.

Any more obvious translations, regarding the paper statement?

[Kenny Lau]

@Chris Froeschl i would use Fin 2; and also pay attention to the base of your log. Also I don't think your S is correct.

[Chris Anto Fröschl]

Fin 2 is a great idea. Thanks!

[Chris Anto Fröschl]

Is there a way to configure the base of Real.log? I can't seem to find an answer consulting the documentation at https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Log/Basic.html#Real.log

Or are there alternative logarithm definitions I'm not aware of? (even finding this one wasn't trivial)

[Kenny Lau]

try docs#Nat.log

[Chris Anto Fröschl]

Kenny Lau said:

Also I don't think your S is correct.

I was trying to translate the notion of {0, 1}^b, which should be all preimages of σ, i.e. all permutations of b-bit strings. Shouldn't the list description be somewhat equivalent? Or am I missing something?

[Sébastien Gouëzel]

docs#Real.logb

[Edward van de Meent]

Chris Froeschl said:

Kenny Lau said:

Also I don't think your S is correct.

I was trying to translate the notion of {0, 1}^b, which should be all preimages of σ, i.e. all permutations of b-bit strings. Shouldn't the list description be somewhat equivalent? Or am I missing something?

mathlib does have List.Vector (the type of lists of a given length), but the alternative is to use Fin b -> Fin 2 here. The nice bit about using functions is that applying permutations (which are of type Equiv.Perm (Fin b)) will be as simple as composing the maps. AFAIK there is not really api for doing this to List.Vector

[Chris Anto Fröschl]

Edward van de Meent said:

mathlib does have List.Vector (the type of lists of a given length), but the alternative is to use Fin b -> Fin 2 here. The nice bit about using functions is that applying permutations (which are of type Equiv.Perm (Fin b)) will be as simple as composing the maps. AFAIK there is not really api for doing this to List.Vector

Would you mind elaborating a bit more on the Fin b -> Fin 2 part? I'm not able to see where a function from Nats smaller than b to {0, 1} would fit the definition here. But that is perhaps just because I didn't work too much with functions as a concept in Lean (besides in MIL), let alone permutations of such kind. An example might help a beginner like me.

[Chris Anto Fröschl]

Another issue I'm currently encountering during proofs, is how to handle cases
where I'm not able to use typical theorem shortcuts, because I'm bound to
GaloisFields (as of my current type decisions).

A concrete example is the following: (runnable example)

import Mathlib

namespace Elligator1

variable (q : ℕ)
variable (q_prime : Nat.Prime q)
variable [Fact (Nat.Prime q)]
variable (q_mod_4_congruent_3 : q % 4 = 3)
include q_prime q_mod_4_congruent_3

variable (s : GaloisField q 1)
variable (s_h1 : s ≠ 0)
variable (s_h2 : (s^2 - 2) * (s^2 + 2) ≠ 0)
include s_h1 s_h2

noncomputable def c : GaloisField q 1 := 2 / s^2

lemma q_ne_two : q ≠ 2 := by
  intro h
  have mod_two : 2 % 4 = 2 := by norm_num
  nth_rw 1 [← h] at mod_two
  rw [q_mod_4_congruent_3] at mod_two
  norm_num at mod_two

lemma c_ne_zero : c q s ≠ 0 := by
  change 2 / s^2 ≠ 0
  apply div_ne_zero
  · intro h
    sorry
  · rw [pow_two]
    apply mul_ne_zero s_h1 s_h1

Typical *_ne_zero theorems do not work, since (2 : GaloisField q 1).

I know the characteristic of GaloisField q 1 is q, and since q ≠ 2,
2 cannot be zero in this field.
But I'm just not able to find something that could help me from
Mathlib.FieldTheory.Finite.GaloisField to finish the last sorry of.

I also tried to use a *_ne_zero theorem from
Mathlib.Algebra.GroupWithZero.Units.Basic (like Units.ne_zero), since div_ne_zero
came from there, but I didn't manage to unify it properly, probably due to to
coercion issues (?).

lemma c_ne_zero : c q s ≠ 0 := by
  change 2 / s^2 ≠ 0
  apply div_ne_zero
  -- does not work
  · apply Units.ne_zero (2 : GaloisField q 1)
  · rw [pow_two]
    apply mul_ne_zero s_h1 s_h1

or using divisibilty arguments: (I know, that a GaloisField isn't a proper MonoidWithZero)

lemma c_ne_zero : c q s ≠ 0 := by
  change 2 / s^2 ≠ 0
  apply div_ne_zero
  · intro h
    have h1 : (2 : GaloisField q 1) = 0 ↔ q ∣ 2 := by
      --apply Ideal.Quotient.eq_zero_iff_dvd
      sorry
    rw [h1] at h
    --apply prime_two_or_dvd_of_dvd_two_mul_pow_self_two q_prime h
    sorry

[Kevin Buzzard]

docs#GaloisField

[Kevin Buzzard]

I don't think you should be developing any API for GaloisField. You won't be able to use it in applications where you just have a random finite field, because such a finite field will not be equal to a GaloisField and Lean takes equality much more seriously than paper mathematics.

[Kevin Buzzard]

Why not just set up the theory for an arbitrary [Field F] and assume results about its characteristic rather than its order? That's all you need here. The art of formalisation is proving things in the right generality, which is often not the generality of the source you're following.

[Chris Anto Fröschl]

@Kevin Buzzard like I mentioned earlier, I would prefer to use the most general form of a finite field. I only hesitated, because the documentation I was able to find, is/was non obvious to me. GaloisField just felt more intuitive for a beginner, because you can explicitly provide your q.

Either way, I'm currently trying to refactor everything to use {F : Type*} [Field F] [Fintype F]. Is my attempt of stating that q is the amount of elements in F idiomatic in the following example?

import Mathlib

namespace Elligator1

variable {F : Type*} [Field F] [Fintype F]

variable (q : ℕ)
variable (q_prime : Nat.Prime q) [Fact (Nat.Prime q)]
variable (q_mod_4_congruent_3 : q % 4 = 3)
variable (field_cardinality : Fintype.card F = q)

-- Chapter 3.1 Definition of quadratic character
noncomputable def χ
  (a : F)
  (q : ℕ)
  (field_cardinality : Fintype.card F = q)
  (q_prime : Nat.Prime q)
  (q_mod_4_congruent_3 : q % 4 = 3)
  : F := a^((Fintype.card F - 1) / 2)
-- ...

[Chris Anto Fröschl]

I'm also unsure, if my usage of explicit round brace arguments is correct. Am I missing some idiomatic way to not repeat this for every theorem and statement by using my variables or other globals better?
The current definition will result in calling χ a q field_cardinality q_prime q_mod_4_congruent_3 multiple times across the code.

I'm aware of subtypes, which might shorten my input parameters. But I'm not sure, if this will work out any better in the long run, since I have to build subtypes with multiple requirements like (q : {q : ℕ // (Fintype.card F = q ∧ Nat.Prime q ∧ q % 4 = 3)}), resulting in harder access to individual q properties during proofs.

[Kevin Buzzard]

@Chris Froeschl the most general form of a finite field is (F : Type*) [Field F] [Finite F]. That's the point I'm trying to make.

A theorem proved for (F : Type*) [Field F] [Finite F] will apply to GaloisField, but a theorem proved for GaloisField will not apply to (F : Type*) [Field F] [Finite F].

[Kevin Buzzard]

Yes I would say that just saying card F = q is fine, although my instinct would be to use Nat.card F and Finite F because in my work I don't want to get bogged down in issues with constructivism. But in your situation Fintype might be more appropriate, I am not clear on this point.

[Kevin Buzzard]

Going back to your original question about showing that 2 isn't 0, my instinct would be to prove (or hopefully find in the library) that if F is a field of size q and q is prime then q is the characteristic of F. Then because q doesn't divide 2 you'll be able to deduce that 2 isn't 0.

[metakuntyyy]

Kevin Buzzard said:

Just to be clear: there are finite fields of prime order $p$ for all primes, and they are implemented in a way which presumably computes, or could easily be made computable, with ZMod p. And then there are prime powers $q$ such as 4, and for each prime power $q$ there's a finite field of size $q$, and it is not ZMod q (this is not a field if $q$ isn't prime), and it is a mildly nontrivial, but solved, problem to figure out how to make computationally efficient models of these finite fields, but this has not been implemented in Lean yet.

Would it make sense to have a computational model for prime powers?

[Kevin Buzzard]

Yes definitely, but this would probably not be either of GaloisField q or [Field F] [Finite F], unless there is some @[csimp] wizardry which one can do here.

[Kevin Buzzard]

I believe that Magma (the CAS) has hard-coded addition and multiplication tables for all finite fields of order <= 1000 (or even more) which makes it super-fast for arithmetic in finite fields.

[Kenny Lau]

metakuntyyy said:

Would it make sense to have a computational model for prime powers?

You're very welcome to write one :slight_smile:
(clarification: this means, it might be a bit hard to write, i'm not familiar with any algorithm at all, i don't want to just factorise x^q-x by "hand", what's the current record complexity of finding an irreducible polynomial?)

[Mario Carneiro]

This looks relevant: https://users.mai.liu.se/nilqu94/publications/nhq_master_thesis.pdf

[Mario Carneiro]

oh, it's only about $2^n$

[Kevin Buzzard]

As I say, magma is just literally storing a (perhaps well-chosen) irred poly of degree n over $\Z/p\Z$ for all $(p,n)$ with $p^n\leq 1000$ or so, rather than computing them.

[metakuntyyy]

This seems interesting as I am currently trying to prove a theorem that would allow me to write a tactic to show that a polynomial in $\mathbb{Z}_p$ is irreducible. I'm unaware as of now if there are any algorithms that prove that a polynomial is irreducible over a finite field. I don't think anyone would use the splitting field $X^q-X$, much rather find an irreducible and do the adjoin root construction.

@Kevin Buzzard Wouldn't we have then the problem that we would have to prove that a polynomial is irreducible. I assume that may be the hard part, unless I'm missing some knowledge. The best algorithm I know to show that a polynomial over finite fields is irreducible is to show that it doesn't divide a factor of half of its degree.

[Chris Anto Fröschl]

I'm having a perhaps trivial issue with my new finite field type definition again.

import Mathlib

namespace Elligator1

variable {F : Type*} [Field F] [Finite F]

variable (q : ℕ)
variable (q_prime : Nat.Prime q) [Fact (Nat.Prime q)]
variable (q_mod_4_congruent_3 : q % 4 = 3)
variable (field_cardinality : Nat.card F = q)

variable (s : F)
variable (s_h1 : s ≠ 0)
variable (s_h2 : (s^2 - 2) * (s^2 + 2) ≠ 0)

/-- c(s) is a constant defined in the paper.

Paper definition at chapter 3.2 theorem 1.
-/
noncomputable def c
  (s : F)
  (s_h1 : s ≠ 0)
  (s_h2 : (s^2 - 2) * (s^2 + 2) ≠ 0)
  (q : ℕ)
  (field_cardinality : Nat.card F = q)
  (q_prime : Nat.Prime q)
  (q_mod_4_congruent_3 : q % 4 = 3)
  : F := 2 / s^2

lemma s_pow_two_ne_neg_two
  (s : F)
  (s_h1 : s ≠ 0)
  (s_h2 : (s^2 - 2) * (s^2 + 2) ≠ 0)
  (q : ℕ)
  (field_cardinality : Nat.card F = q)
  (q_prime : Nat.Prime q)
  (q_mod_4_congruent_3 : q % 4 = 3)
  : s^2 ≠ -2 := by
  have h1 : s^2 + 2 ≠ 0 := by
    intro h
    rw [h] at s_h2
    norm_num at s_h2
  intro h
  rw [h] at h1
  norm_num at h1

lemma c_ne_neg_one
  (s : F)
  (s_h1 : s ≠ 0)
  (s_h2 : (s^2 - 2) * (s^2 + 2) ≠ 0)
  (q : ℕ)
  (field_cardinality : Nat.card F = q)
  (q_prime : Nat.Prime q)
  (q_mod_4_congruent_3 : q % 4 = 3)
  :
  let c_of_s := c s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3
  c_of_s ≠ -1 := by
  change 2 / s^2 ≠ -1
  intro h
  have h1 : s^2 = -2 := by
    calc
      s^2 = 2 / (-1 : F) := by
        rw [← h]
        ring_nf
        rw [inv_inv]
        rw [mul_assoc]
        rw [inv_mul_cancel (2 : F)]
          -- here
      _ = -2 := by norm_num
  apply s_pow_two_ne_neg_two s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3 at h1
  exact h1

Regarding this runnable example, the lemma c_ne_neg_one uses some
theorems from Mathlib.Algebra.Group.Defs. This works all fine and good with
the current definition of F, until mul_inv_cancel throws following error:

F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
s : F
s_h1 : s ≠ 0
s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0
q : ℕ
field_cardinality : Nat.card F = q
q_prime : Nat.Prime q
q_mod_4_congruent_3 : q % 4 = 3
h : 2 / s ^ 2 = -1
⊢ s ^ 2 = s ^ 2 * (2⁻¹ * 2)

▶ 70:13-70:35: error:
failed to synthesize
  Group F

I tried to add a [Group F] at my F restrictions, but this didn't resolve the
issue. Any thoughts on why a finite field is not transformable into a group or how to resolve?

[Kevin Buzzard]

Group in Lean means "group under multiplication". So Lean is right, a field is not a group (because it contains a zero). This also means that you cannot use inv_mul_cancel on F because inv_mul_cancel is a theorem about groups. Indeed inv_mul_cancel is not true for a field because $0^{-1}\times 0=0\times 0\not=1$. Use inv_mul_cancel₀ instead.

I tried to add a [Group F]

That means "now put a new group structure on F, completely unrelated to the field structure". So that's definitely not a good idea.

[Chris Anto Fröschl]

Kevin Buzzard said:

That means "now put a new group structure on F, completely unrelated to the field structure". So that's definitely not a good idea

Indeed... I was only grabbing for something to understand the problem better.

[Chris Anto Fröschl]

Kevin Buzzard said:

Use inv_mul_cancel₀ instead.

Argh I didn't see that one. Thank's for the explanation!

[Kevin Buzzard]

yeah that's a theorem which works for "groups with zero", which is a mathlibism for "the disjoint union of a group (under multiplication) and a 0" which is exactly what a field is.

[Chris Anto Fröschl]

I've worked myself through theorem 1 during the last week.

I've also created a repo with a primitive unconfigured blueprint for anyone interested:

https://github.com/chrisathmedu/elligator
https://chrisathmedu.github.io/elligator/docs/Elligator/Elligator1.html

I hope to get through theorem 3 and 4 the upcoming weeks, followed by a hopefully more straightforward Elligator 2 implementation (due to me having more experience with Lean now).

Discussions and recommendations regarding the current state and structure are, as always, welcome.

[Chris Anto Fröschl]

I'm currently searching for a good way to express that a variable is defined for all inputs, i.e. does not have an unexpected zero divisor or something comparable. Context:

2025-07-28-110648_425x178_scrot.png

I'm currently doing something along those lines:

variable {F : Type*} [Field F] [Fintype F]

noncomputable def u
  (t : {n : F // n ≠ 1 ∧ n ≠ -1})
  (q : ℕ)
  (field_cardinality : Fintype.card F = q)
  (q_prime : Nat.Prime q)
  (q_mod_4_congruent_3 : q % 4 = 3)
  : F :=
  (1 - t.val) / (1 + t.val)

theorem u_defined
  (q : ℕ)
  (field_cardinality : Fintype.card F = q)
  (q_prime : Nat.Prime q)
  (q_mod_4_congruent_3 : q % 4 = 3) :
  ∀ t : {n : F // n ≠ 1 ∧ n ≠ -1}, ∃ (w : F), w = (u t q field_cardinality q_prime q_mod_4_congruent_3) := by
  intro t
  use u t q field_cardinality q_prime q_mod_4_congruent_3

This however does not show anything, besides fulfilling the type requirements.

An alternative would be, to do something like this:

theorem u_defined :
  ∀ t : {n : F // n ≠ 1 ∧ n ≠ -1}, (1 + t.val) ≠ 0 := by ...

This actually describes what we would do on paper. But I'm still wondering if there is any Lean method beyond that?

[Kenny Lau]

@Chris Anto Fröschl i haven't read everything you said, but in lean the philosophy is to have junk values and then only prove correctness in terms of theorems, so for example in a field, the inverse of 0 is axiomatically 0, and the x * x^-1 = 1 axiom is instead replaced with x \ne 0 -> x * x^-1 = 1.

[Chris Anto Fröschl]

Excuse the long absence. I was busy writing my thesis.

I'm currently up for theorem 3 of Elligator 1 after having done some refactoring of theorem 1. @Kenny Lau thanks again for the last hint. I was mostly curious if there is some "automatic" way of finding problem cases of hidden critical divisors or the like. I ended up just proofing that the divisors are non-zero.

I'm currently having an issue with if_neg during the unfold of a function using an if else at https://github.com/chrisathmedu/elligator/blob/79bec26d86edba054013d90af48347dbb88abeb7/Elligator/Elligator1.lean#L1366 . The relevant pieces:

noncomputable def ϕ
  (t : F)
  (s : F)
  (s_h1 : s ≠ 0)
  (s_h2 : (s^2 - 2) * (s^2 + 2) ≠ 0)
  (q : ℕ)
  (field_cardinality : Fintype.card F = q)
  (q_prime_power : IsPrimePow q)
  (q_mod_4_congruent_3 : q % 4 = 3)
  : (F) × (F) :=
  open scoped Classical in if h : t ≠ 1 ∧ t ≠ -1
  then
  (
    x ⟨t, h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3,
    y ⟨t, h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3
  )
  else (0, 1)

-- Chapter 3.3 Theorem 3.1
theorem ϕ_inv_only_two_specific_preimages
  (t : F)
  (s : F)
  (s_h1 : s ≠ 0)
  (s_h2 : (s^2 - 2) * (s^2 + 2) ≠ 0)
  (q : ℕ)
  (field_cardinality : Fintype.card F = q)
  (q_prime_power : IsPrimePow q)
  (q_mod_4_congruent_3 : q % 4 = 3)
  :
  let ϕ_of_t := ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3
  let ϕ_of_neg_t := ϕ (-t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3
  ϕ_of_t = ϕ_of_neg_t
  ↔ ¬ (∃ (w : { n : F // n ≠ t ∧ n ≠ -t}), ϕ w.val s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = ϕ_of_t) := by
    intro ϕ_of_t ϕ_of_neg_t
    constructor
    · intro h1
      sorry
    · intro h1
      by_cases h2 : t = 1 ∨ t = -1
      · rcases h2 with h2_1 | h2_1
        · change ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = ϕ (-t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3
          rw [h2_1]
          unfold ϕ
          have h2_1_1 : ¬(1 ≠ 1 ∧ 1 ≠ -1) := by sorry
          have h2_1_2 : ¬(-1 ≠ 1 ∧ -1 ≠ -1) := by sorry
          rw [if_neg h2_1_1, if_neg h2_1_2]
          sorry
        · sorry
      · sorry

I currently receive the error that the pattern of the condition is not found:

case pos.inl
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
t s : F
s_h1 : s ≠ 0
s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0
q : ℕ
field_cardinality : Fintype.card F = q
q_prime_power : IsPrimePow q
q_mod_4_congruent_3 : q % 4 = 3
ϕ_of_t : F × F := ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3
ϕ_of_neg_t : F × F := ϕ (-t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3
h1 : ¬∃ w, ϕ (↑w) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = ϕ_of_t
h2_1 : t = 1
h2_1_1 : ¬(1 ≠ 1 ∧ 1 ≠ -1)
h2_1_2 : ¬(-1 ≠ 1 ∧ -1 ≠ -1)
⊢ (if h : 1 ≠ 1 ∧ 1 ≠ -1 then
    (x ⟨1, h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3,
      y ⟨1, h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3)
  else (0, 1)) =
  if h : -1 ≠ 1 ∧ -1 ≠ -1 then
    (x ⟨-1, h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3,
      y ⟨-1, h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3)
  else (0, 1)

▼ expected type (1366:22-1366:28)
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
t s : F
s_h1 : s ≠ 0
s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0
q : ℕ
field_cardinality : Fintype.card F = q
q_prime_power : IsPrimePow q
q_mod_4_congruent_3 : q % 4 = 3
ϕ_of_t : F × F := ⋯
ϕ_of_neg_t : F × F := ⋯
h1 : ¬∃ w, ϕ (↑w) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = ϕ_of_t
h2_1 : t = 1
h2_1_1 : ¬(1 ≠ 1 ∧ 1 ≠ -1)
h2_1_2 : ¬(-1 ≠ 1 ∧ -1 ≠ -1)
⊢ ¬(1 ≠ 1 ∧ 1 ≠ -1)

▼ 1366:15-1366:28: error:
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  if 1 ≠ 1 ∧ 1 ≠ -1 then ?m.128798 else ?m.128799
case pos.inl
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
t s : F
s_h1 : s ≠ 0
s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0
q : ℕ
field_cardinality : Fintype.card F = q
q_prime_power : IsPrimePow q
q_mod_4_congruent_3 : q % 4 = 3
ϕ_of_t : F × F := ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3
ϕ_of_neg_t : F × F := ϕ (-t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3
h1 : ¬∃ w, ϕ (↑w) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = ϕ_of_t
h2_1 : t = 1
h2_1_1 : ¬(1 ≠ 1 ∧ 1 ≠ -1)
h2_1_2 : ¬(-1 ≠ 1 ∧ -1 ≠ -1)
⊢ (if h : 1 ≠ 1 ∧ 1 ≠ -1 then
    (x ⟨1, h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3,
      y ⟨1, h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3)
  else (0, 1)) =
  if h : -1 ≠ 1 ∧ -1 ≠ -1 then
    (x ⟨-1, h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3,
      y ⟨-1, h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3)
  else (0, 1)

Is this perhaps somehow related to the Classical keyword used with the if? Or just some issue related to proper encapsulation? I was not able to find similar examples and only know if_neg/if_pos from the MIL book. Any ideas?

[Aaron Liu]

docs#dif_neg

[Chris Anto Fröschl]

I already tried dif_neg. Same error.

[Aaron Liu]

that shouldn't happen, maybe try simp?

[Chris Anto Fröschl]

Oh... simp solved the goal. I use simp way to seldom. Thanks!

[Aaron Liu]

Have you checked the types of 1 and -1 in h2_1_1 and h2_1_2? I think they might be not the same as the types in your condition.

[Kevin Buzzard]

(note the difficulty that people have in answering your question because you didn't post a #mwe )

[Aaron Liu]

If you have ¬((1 : Nat) ≠ 1 ∧ (1 : Int) ≠ -1) it's not gonna match with ¬((1 : F) ≠ 1 ∧ (1 : F) ≠ -1)

[Chris Anto Fröschl]

Argh indeed. I forgot to set the type explicitly.

[Chris Anto Fröschl]

Kevin Buzzard said:

(note the difficulty that people have in answering your question because you didn't post a #mwe )

Excuse. I would have to construct a totally new example since there is so much interlink between the actual definitions and theorems where I'm currently at.

I will try my best to provide better MWE in the future!

[Aaron Liu]

this would be so much easier with a #mwe since I wouldn't have to wait for your feedback I could just try it myself

[Aaron Liu]

none of the definitions or theorems ended up mattering here and sometimes while constructing a #mwe I end up accidentally solving my problem