Martin Escardo, 21th April 2023
Based on Section 8.1 of the paper https://doi.org/10.2168/LMCS-4(3:3)2008

Updated 25th May 2023 to (i) give an alternative construction of our
formula for a putative root, and (ii) prove its correctness.

We provide a formula for a putative root of any boolean function
f : πβΏ β π, using only f and β, and show its correctness.

In more detail:

Let π be the two-point set with elements β and β, referred to as the
type of booleans.

Consider a given boolean function f : πβΏ β π.

Definition. A *root* of f is some xs in πβΏ such that f xs = β.

Definition. A *putative root* of f is any xs in πβΏ such that if f has
some root, then xs is a root.

Example. If f doesn't have any root, then any xs in πβΏ is putative root.

Example. If xs is a root, then xs is a putative root.

Theorem. For any n, there is a formula that mentions only f and β such
that for any given function f : πβΏ β π, the formula gives a putative
root of f.

We will need to be more precise regarding the formal details of the
statement of this theorem, where we will need to distinguish between
(abstract syntax for) formulas for putative roots and actual putative
roots, but, for the moment, the above imprecise formulation of the
theorem should be good enough.

Example. For n = 3, we have the putative root x := (xβ,xβ,xβ) where

y  := f(0,0,f(0,0,0))
xβ := f(0,y,f(0,y,0))
xβ := f(xβ,0,f(xβ,0,0))
xβ := f(xβ,xβ,0)

The purpose of this Agda file is to construct such a formula for any
given n, and prove that it indeed gives a putative root.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Various.RootsOfBooleanFunctions where

open import MLTT.Spartan hiding (_^_)
open import MLTT.Two-Properties
open import UF.Base

\end{code}

For any f : π β π, we can check whether it is constantly β by checking
whether f (f β) is β, which is easily proved by case analysis on the
value of f β:

\begin{code}

motivating-fact : (f : π β π) β f (f β) οΌ β β (b : π) β f b οΌ β
motivating-fact f = Ξ³ (f β) refl
where
Ξ³ : (bβ : π) β f β οΌ bβ β f bβ οΌ β β (b : π) β f b οΌ β
Ξ³ β p q β = q
Ξ³ β p q β = π-elim
(zero-is-not-one
β   β))
Ξ³ β p q β = p
Ξ³ β p q β = q

\end{code}

Motivated by this, we define:

\begin{code}

Ξ΅π : (π β π) β π
Ξ΅π f = f β

Aπ : (π β π) β π
Aπ f = f (Ξ΅π f)

\end{code}

The desired property of Aπ is the following, which follows from the
motivating fact, in one direction, and directly in the other
direction:

\begin{code}

Aπ-propertyβ : (f : π β π) β Aπ f οΌ β β (b : π) β f b οΌ β
Aπ-propertyβ = motivating-fact

Aπ-propertyβ : (f : π β π) β ((b : π) β f b οΌ β) β Aπ f οΌ β
Aπ-propertyβ f Ξ± = Ξ± (Ξ΅π f)

\end{code}

From this it follows directly that for any f : π β π we can find a
boolean bβ such that if f bβ οΌ β then f n οΌ β for every boolean b:

\begin{code}

Οπ : (f : π β π) β Ξ£ bβ κ π , (f bβ οΌ β β (b : π) β f b οΌ β)
Οπ f = Ξ΅π f , Aπ-propertyβ f

\end{code}

The functional Ξ΅π computes the putative root Ξ΅ f for any f : π β π:

\begin{code}

is-root : {X : π€ Μ } β X β (X β π) β π€β Μ
is-root xβ f = f xβ οΌ β

has-root : {X : π€ Μ } β (X β π) β π€ Μ
has-root {π€} {X} f = Ξ£ x κ X , is-root x f

is-putative-root : {X : π€ Μ } β X β (X β π) β π€ Μ
is-putative-root xβ f = has-root f β is-root xβ f

Ξ΅π-gives-putative-root : {n : β} (f : π β π)
β is-putative-root (Ξ΅π f) f
Ξ΅π-gives-putative-root f (b , r) =
different-from-β-equal-β
(Ξ» (p : Aπ f οΌ β) β zero-is-not-one
f b οΌβ¨ Aπ-propertyβ f p b β©
β   β))
\end{code}

We define the type X ^ n of n-tuples of elements of a type X by
induction as follows.

\begin{code}

data _^_ (X : π€ Μ ) : β β π€ Μ where
_,_ : {n : β} β X β X ^ n β X ^ (succ n)

\end{code}

(This is just another notation for the type of so-called vectors.)

We will often use the "prepend" function (x ,_), for any given x,
written "cons x", defined by cons x xs = (x , xs), or, equivalently:

\begin{code}

cons : {X : π€ Μ } {n : β} β X β X ^ n β X ^ (succ n)
cons x = (x ,_)

\end{code}

We are now ready to compute putative roots of boolean functions. We
will later adapt this argument to give a *formula* for the putative
root.

We define two functions A and Ξ΅ by simultateous induction on n as
follows:

\begin{code}

A : {n : β} β (π ^ n β π) β π
Ξ΅ : {n : β} β (π ^ n β π) β π ^ n

A f = f (Ξ΅ f)

Ξ΅ {succ n} f = cons bβ (Ξ΅ (f β cons bβ) )
where
bβ : π
bβ = Ξ΅π (b β¦ A (f β cons b))

\end{code}

It is of course possible to first define Ξ΅, by induction on n, and
then A directly from Ξ΅ as follows. If we also expand the definition of
Ξ΅π, we get:

\begin{code}

private

Ξ΅' : {n : β} β (π ^ n β π) β π ^ n
Ξ΅' {succ n} f = cons bβ (Ξ΅' (f β cons bβ))
where
bβ : π
bβ = (f β cons β) (Ξ΅' (f β cons β))

A' : {n : β} β (π ^ n β π) β π
A' f = f (Ξ΅' f)

\end{code}

However, we want to highlight the role of A in our definition of Ξ΅.

We have that A f οΌ β if and only if f xs οΌ β for all xs in π ^ n:

\begin{code}

A-propertyβ : {n : β} (f : π ^ n β π)
β ((xs : π ^ n) β f xs οΌ β)
β A f οΌ β
A-propertyβ f Ξ± = Ξ± (Ξ΅ f)

A-propertyβ : {n : β}
(f : π ^ n β π)
β A f οΌ β
β (xs : π ^ n) β f xs οΌ β
f (Ξ΅ {0} f) οΌβ¨ p β©
β           β
A-propertyβ {succ n} f p (x , xs) = II
where
IH : (b : π) β A (f β cons b) οΌ β β (xs : π ^ n) β f (cons b xs) οΌ β
IH b = A-propertyβ {n} (f β cons b)

bβ : π
bβ = Ξ΅π (b β¦ A (f β cons b))

I : A (f β cons bβ) οΌ β β (b : π) β A (f β cons b) οΌ β
I = Aπ-propertyβ (b β¦ A (f β cons b))

II : f (x , xs) οΌ β
II = IH x (I p x) xs

Ο : {n : β} (f : π ^ n β π)
β Ξ£ xβ κ π ^ n , (f xβ οΌ β β (x : π ^ n) β f x οΌ β)
Ο f = Ξ΅ f , A-propertyβ f

\end{code}

From this it follows that Ξ΅ f computes a putative root of f.

\begin{code}

Ξ΅-gives-putative-root : {n : β}  (f : π ^ n β π)
β is-putative-root (Ξ΅ f) f
Ξ΅-gives-putative-root {n} f (x , p) =
different-from-β-equal-β
(Ξ» (q : A f οΌ β) β zero-is-not-one
f x οΌβ¨ A-propertyβ f q x β©
β   β))

\end{code}

Hence we can check whether f has a root by checking whether f (Ξ΅ f) οΌ β.

\begin{code}

root-existence-criterion : {n : β}  (f : π ^ n β π)
β has-root f β is-root (Ξ΅ f) f
root-existence-criterion {n} f = (I , II)
where
I : has-root f β f (Ξ΅ f) οΌ β
I = Ξ΅-gives-putative-root f

II : f (Ξ΅ f) οΌ β β has-root f
II p = Ξ΅ f , p

\end{code}

The above computes a putative root, but what we want to do in this
file is to give a *formula* for computing putative roots using only β
and f, as discussed above. In a way, this is already achieved
above. Here are some examples:

\begin{code}

exampleβ : (f : π ^ 2 β π)
β Ξ΅ f οΌ (f (β , f (β , β , β¨β©) , β¨β©) ,
f (f (β , f (β , β , β¨β©) , β¨β©) , β , β¨β©) ,
exampleβ f = refl

exampleβ : (f : π ^ 3 β π) β
let
y  = f (β , β , f (β , β , β , β¨β©) , β¨β©)
xβ = f (β , y , f (β , y , β , β¨β©) , β¨β©)
xβ = f (xβ , β , f (xβ , β , β , β¨β©) , β¨β©)
xβ = f (xβ , xβ , β , β¨β©)
in
Ξ΅ f οΌ (xβ , xβ , xβ , β¨β©)
exampleβ f = refl

\end{code}

But we want to make this explicit. For that purpose, we introduce a
type E of symbolic expressions, or formulas, using only the symbol O
(standing for β) and the symbol π (standing for any given function
f : π ^ n β π), defined by induction as follows, with n as a fixed
parameter:

\begin{code}

data E (n : β) : π€β Μ where
O : E n
π : E n ^ n β E n

\end{code}

Given a function f : π ^ n β π, any expression e of type E n can be
evaluated to a boolean by replacing the symbol O by the boolean β and
the symbol π by the function f, by induction on formulas, where we use
the variable e to range over expressions, and the variable es to range
over tuples of expressions.

\begin{code}

module _ {n : β} (f : π ^ n β π) where

eval  : E n β π
evals : {k : β} β E n ^ k β π ^ k

eval O      = β
eval (π es) = f (evals es)

evals (e , es) = eval e , evals es

\end{code}

We use the following auxilary constructions to define a formula for a
putative root of any n-ary boolean function:

\begin{code}

ππ ππ€  : {n : β}   β E (succ n) β E n     β E (succ n)
ππ ππ€s : {n k : β} β E (succ n) β E n ^ k β E (succ n) ^ k

ππ ππ€ eβ O      = O
ππ ππ€ eβ (π es) = (π β cons eβ) (ππ ππ€s eβ es)

ππ ππ€s eβ (e , es) = ππ ππ€ eβ e , ππ ππ€s eβ es

\end{code}

Their intended behaviour is as follows:

\begin{code}

ππ ππ€-behaviour : {n : β}
(f : π ^ succ n β π)
(eβ : E (succ n))
(e  : E n)
β eval f (ππ ππ€ eβ e) οΌ eval (f β cons (eval f eβ)) e

ππ ππ€s-behaviour : {n k : β}
(f : π ^ succ n β π)
(eβ : E (succ n))
(es : E n ^ k)
β evals f (ππ ππ€s eβ es) οΌ evals (f β cons (eval f eβ)) es

ππ ππ€-behaviour f eβ O      = refl
ππ ππ€-behaviour f eβ (π es) = ap (f β cons (eval f eβ)) (ππ ππ€s-behaviour f eβ es)

ππ ππ€s-behaviour f eβ β¨β©       = refl
ππ ππ€s-behaviour f eβ (e , es) = apβ _,_
(ππ ππ€-behaviour  f eβ e )
(ππ ππ€s-behaviour f eβ es)
\end{code}

With this, we can give a formula to compute Ξ΅:

\begin{code}

Ξ΅-formula : (n : β) β E n ^ n
Ξ΅-formula (succ n) = cons cβ (ππ ππ€s cβ (Ξ΅-formula n))
where
cβ : E (succ n)
cβ = (π β cons O) (ππ ππ€s O (Ξ΅-formula n))

\end{code}

Notice the similarity with the definition of Ξ΅, in particular with its
incarnation Ξ΅'.

Here is an example that illustrates this concretely:

\begin{code}

exampleβ-formula :
let
y  = π (O , O , π (O , O , O , β¨β©) , β¨β©)
xβ = π (O , y , π (O , y , O , β¨β©) , β¨β©)
xβ = π (xβ , O , π (xβ , O , O , β¨β©) , β¨β©)
xβ = π (xβ , xβ , O , β¨β©)
in
Ξ΅-formula 3 οΌ (xβ , xβ , xβ , β¨β©)
exampleβ-formula = refl

\end{code}

The desired property of the formula is that evaluating it with any
concrete f gives the putative root Ξ΅ f of f:

\begin{code}

Ξ΅-formula-lemma : (n : β) (f : π ^ n β π)
β evals f (Ξ΅-formula n) οΌ Ξ΅ f
Ξ΅-formula-lemma 0        f = refl
Ξ΅-formula-lemma (succ n) f = Ξ³
where
es : E n ^ n
es = Ξ΅-formula n

bβ : π
bβ = (f β cons β) (Ξ΅ (f β cons β))

cβ : E (succ n)
cβ = (π β cons O) (ππ ππ€s O es)

IH : (b : π) β evals (f β cons b) es οΌ Ξ΅ (f β cons b)
IH b = Ξ΅-formula-lemma n (f β cons b)

cβ-property : eval f cβ οΌ bβ
cβ-property =
eval f cβ                            οΌβ¨ refl β©
(f β cons β) (evals f (ππ ππ€s O es))  οΌβ¨ I β©
(f β cons β) (evals (f β cons β) es) οΌβ¨ II β©
(f β cons β) (Ξ΅ (f β cons β))        οΌβ¨ refl β©
bβ                                   β
where
I  = ap (f β cons β) (ππ ππ€s-behaviour f O es)
II = ap (f β cons β) (IH β)

Ξ³ : evals f (Ξ΅-formula (succ n)) οΌ Ξ΅ f
Ξ³ = evals f (Ξ΅-formula (succ n))               οΌβ¨ refl β©
cons (eval f cβ) (evals f (ππ ππ€s cβ es))   οΌβ¨ I β©
cons bβ (evals f (ππ ππ€s cβ es))            οΌβ¨ II β©
cons bβ (evals (f β cons (eval f cβ)) es)  οΌβ¨ III β©
cons bβ (evals (f β cons bβ) es)           οΌβ¨ IV β©
cons bβ (Ξ΅ (f β cons bβ))                  οΌβ¨ refl β©
Ξ΅ f                                        β
where
I   = ap (Ξ» - β cons - (evals f (ππ ππ€s cβ es))) cβ-property
II  = ap (cons bβ) (ππ ππ€s-behaviour f cβ es)
III = ap (Ξ» - β cons bβ (evals (f β cons -) es)) cβ-property
IV  = ap (cons bβ) (IH bβ)

\end{code}

From this, together with "Ξ΅-gives-putative-root" proved above, it
follows immediately that "Ξ΅-formula n" gives a formula for a putative
root of any n-ary boolean function:

\begin{code}

Ξ΅-formula-theorem : (n : β) (f : π ^ n β π)
β is-putative-root (evals f (Ξ΅-formula n)) f
Ξ΅-formula-theorem n f = Ξ³
where
Ξ΄ : is-putative-root (Ξ΅ f) f
β is-putative-root (evals f (Ξ΅-formula n)) f
Ξ΄ i Ο = f (evals f (Ξ΅-formula n)) οΌβ¨ ap f (Ξ΅-formula-lemma n f) β©
f (Ξ΅ f)                   οΌβ¨ i Ο β©
β                         β

Ξ³ : is-putative-root (evals f (Ξ΅-formula n)) f
Ξ³ = Ξ΄ (Ξ΅-gives-putative-root f)

\end{code}

Which has our desired theorem as a corollary, namely that, for every n,
there is a formula for a putative root of any n-ary boolean function:

\begin{code}

putative-root-formula-theorem
: (n : β) β Ξ£ es κ E n ^ n , ((f : π ^ n β π) β is-putative-root (evals f es) f)
putative-root-formula-theorem n = Ξ΅-formula n , Ξ΅-formula-theorem n

\end{code}

Our original definition of the formula for the putative root was the following:

\begin{code}

Ξ΅α΅ : {n k : β} β (E k ^ n β E k) β E k ^ n
Ξ΅α΅ {0}      {k} f = β¨β©
Ξ΅α΅ {succ n} {k} f = cons cβ (Ξ΅α΅ (f β cons cβ))
where
cβ : E k
cβ = (f β cons O) (Ξ΅α΅ (f β cons O))

Ξ΅-formula' : (n : β) β E n ^ n
Ξ΅-formula' n = Ξ΅α΅ π

exampleβ-formula' :
let
y  = π (O , O , π (O , O , O , β¨β©) , β¨β©)
xβ = π (O , y , π (O , y , O , β¨β©) , β¨β©)
xβ = π (xβ , O , π (xβ , O , O , β¨β©) , β¨β©)
xβ = π (xβ , xβ , O , β¨β©)
in
Ξ΅-formula' 3 οΌ (xβ , xβ , xβ , β¨β©)
exampleβ-formula' = refl

formulas-agreementβ : Ξ΅-formula' 3 οΌ Ξ΅-formula 3
formulas-agreementβ = refl

formulas-agreementβ : Ξ΅-formula' 4 οΌ Ξ΅-formula 4
formulas-agreementβ = refl

\end{code}

TODO. The above formula grows doubly exponentially in size. However,
using variables for common subexpressions, they grow
exponentially. Define a type of expression accomodating variables for
common subexpressions and produce a version Ξ΅-formula that produced
such reduced-size expressions.

The advantage of this definition is that it is almost literally the
same as that of Ξ΅'.

The disadvantage is that it is difficult to find a suitable induction
hypothesis to prove the correctness of Ξ΅-formula' directly. We did
find such a proof, but it is long and messy, and we decided not to
include it here for that reason.

We proposed the following challenges in social media, which were
solved by Alice Laroche.

Challenges.

(1) Find an elegant proof that the function Ξ΅-formula' gives a
formulate for putative roots.

(2) Moreover, show that Ξ΅-formula' = Ξ΅-formula.

(3) Show that Ξ΅ gives the infimum of the (possibly empty) set of roots
in the lexicographic order.

It is easier to prove (2) and then deduce (1), using the idea of proof
of Ξ΅-formula-theorem, rather than prove (1) directly.

Added by Alice Laroche, 1st June 2023.

We show that both definitions are equivalent, and from that deduce the
correctness of Ξ΅-formula'.

We first define another pair of auxiliary constructions that will be

\begin{code}

πππ‘ : {n m : β} (f : E m ^ n β E m ^ m) β E n β E m
πππ‘s : {n m k : β} (f : E m ^ n β E m ^ m) β E n ^ k β E m ^ k

πππ‘ f O = O
πππ‘ f (π es) = π (f (πππ‘s f es))

πππ‘s f (e , es) = πππ‘ f e , πππ‘s f es

\end{code}

Notice that ππ ππ€ and ππ ππ€ are more refined versions of πππ‘ and πππ‘s

\begin{code}

πππ‘-cons-ππ ππ€ : {n k : β}
(eβ : E (succ n))
(e : E n)
β πππ‘ (cons eβ ) e οΌ ππ ππ€ eβ e
πππ‘s-cons-ππ ππ€s : {n k : β}
β (eβ : E (succ n))
β (es : E n ^ k)
β πππ‘s (cons eβ ) es οΌ ππ ππ€s eβ es

πππ‘-cons-ππ ππ€ {n} {k} eβ O = refl
πππ‘-cons-ππ ππ€ {n} {k} eβ (π es) = ap (π β cons eβ) (πππ‘s-cons-ππ ππ€s eβ es)

πππ‘s-cons-ππ ππ€s {n} {k} eβ β¨β© = refl
πππ‘s-cons-ππ ππ€s {n} {k} eβ (e , es) = apβ _,_
(πππ‘-cons-ππ ππ€ {k = k} eβ e)
(πππ‘s-cons-ππ ππ€s eβ es)

πππ‘-πππ‘  : {n m : β}
(f : E m ^ (succ n) β E m ^ m)
(eβ : E (succ n)) β (e : E n)
β πππ‘ f (πππ‘ (cons eβ) e) οΌ πππ‘ (f β cons (πππ‘ f eβ)) e

πππ‘-πππ‘s : {n m k : β}
(f : E m ^ (succ n) β E m ^ m)
(eβ : E (succ n)) β (es : E n ^ k)
β πππ‘s f (πππ‘s (cons eβ) es) οΌ πππ‘s (f β cons (πππ‘ f eβ)) es

πππ‘-πππ‘ f eβ O      = refl
πππ‘-πππ‘ f eβ (π es) = ap (π β f β cons (πππ‘ f eβ)) (πππ‘-πππ‘s f eβ es)

πππ‘-πππ‘s f eβ β¨β©       = refl
πππ‘-πππ‘s f eβ (e , es) = apβ _,_ (πππ‘-πππ‘ f eβ e) (πππ‘-πππ‘s f eβ es)

\end{code}

Using the additional flexibility given by those functions we can show
how to unroll the compositions that happen in Ξ΅α΅.

\begin{code}

unroll-Ξ΅α΅-lemma : {n k : β}
(f : E k ^ n β E k ^ k)
β Ξ΅α΅ (π β f) οΌ πππ‘s f (Ξ΅α΅ π)
unroll-Ξ΅α΅-lemma {0}      {k} f = refl
unroll-Ξ΅α΅-lemma {succ n} {k} f = Ξ³
where
cβ : E k
cβ = (π β f β cons O) (Ξ΅α΅ (π β f β cons O))

cβ : E (succ n)
cβ = (π β cons O) (Ξ΅α΅ (π β cons O))

cβ-property : cβ οΌ πππ‘ f cβ
cβ-property = (π β f β cons O) (Ξ΅α΅ (π β f β cons O))        οΌβ¨ I β©
(π β f β cons O) (πππ‘s (f β cons O) (Ξ΅α΅ π))   οΌβ¨ refl β©
πππ‘ (f β cons O) (π (Ξ΅α΅ π))                   οΌβ¨ II β©
πππ‘ f (πππ‘ (cons O) (π (Ξ΅α΅ π)))               οΌβ¨ refl β©
πππ‘ f ((π β cons O) ((πππ‘s (cons O) (Ξ΅α΅ π)))) οΌβ¨ III β©
πππ‘ f ((π β cons O) (Ξ΅α΅ (π β cons O)))        οΌβ¨ refl β©
πππ‘ f cβ                                      β
where
I = ap (π β f β cons O) (unroll-Ξ΅α΅-lemma (f β cons O))
II = πππ‘-πππ‘ f O (π (Ξ΅α΅ π)) β»ΒΉ
III = ap (πππ‘ f β (π β cons O)) (unroll-Ξ΅α΅-lemma (cons O) β»ΒΉ)

Ξ³ :  Ξ΅α΅ (π β f) οΌ πππ‘s f (Ξ΅α΅ π)
Ξ³ = Ξ΅α΅ (π β f) οΌβ¨ refl β©
cβ , (Ξ΅α΅ (π β f β cons cβ))                  οΌβ¨ I β©
πππ‘ f cβ , (Ξ΅α΅ (π β f β cons (πππ‘ f cβ)))    οΌβ¨ II β©
πππ‘ f cβ , πππ‘s (f β cons (πππ‘ f cβ)) (Ξ΅α΅ π) οΌβ¨ III β©
πππ‘ f cβ , πππ‘s f (πππ‘s (cons cβ) (Ξ΅α΅ π))    οΌβ¨ IV β©
πππ‘ f cβ , πππ‘s f (Ξ΅α΅ (π β cons cβ))         οΌβ¨ refl β©
πππ‘s f (cβ , (Ξ΅α΅ (π β cons cβ)))             οΌβ¨ refl β©
πππ‘s f (Ξ΅α΅ π)                                β
where
I   = ap (Ξ» x β x , (Ξ΅α΅ (π β f β cons x))) cβ-property
II  = ap (πππ‘ f cβ ,_) (unroll-Ξ΅α΅-lemma (f β cons (πππ‘ f cβ)))
III = ap (πππ‘ f cβ ,_) (πππ‘-πππ‘s f cβ (Ξ΅α΅ π) β»ΒΉ)
IV  = ap (Ξ» x β πππ‘ f cβ , πππ‘s f x) (unroll-Ξ΅α΅-lemma (cons cβ) β»ΒΉ)

unroll-Ξ΅α΅ : {n : β}
(eβ : E (succ n))
β Ξ΅α΅ (π β (cons eβ)) οΌ ππ ππ€s eβ (Ξ΅α΅ π)
unroll-Ξ΅α΅ eβ = unroll-Ξ΅α΅-lemma (cons eβ) β πππ‘s-cons-ππ ππ€s eβ (Ξ΅α΅ π)

\end{code}

From this we can show that Ξ΅-formula' n and Ξ΅-formula n are indeed
equal.

\begin{code}

formulas-are-equal : (n : β) β Ξ΅-formula' n οΌ Ξ΅-formula n
formulas-are-equal 0 = refl
formulas-are-equal (succ n) = Ξ³
where
cβ : E (succ n)
cβ = (π β cons O) (Ξ΅α΅ (π β cons O))

cβ : E (succ n)
cβ = (π β cons O) (ππ ππ€s O (Ξ΅-formula n))

cβ-property : cβ οΌ cβ
cβ-property = (π β cons O) (Ξ΅α΅ (π β cons O))       οΌβ¨ I β©
(π β cons O) (ππ ππ€s O (Ξ΅α΅ π))        οΌβ¨ II β©
(π β cons O) (ππ ππ€s O (Ξ΅-formula n)) β
where
I = ap (π β cons O) (unroll-Ξ΅α΅ O)
II = ap (π β cons O β ππ ππ€s O) (formulas-are-equal n)

Ξ³ : Ξ΅-formula' (succ n) οΌ Ξ΅-formula (succ n)
Ξ³ = Ξ΅-formula' (succ n)            οΌβ¨ refl β©
cβ , Ξ΅α΅ (π β cons cβ)          οΌβ¨ I β©
cβ , (ππ ππ€s cβ (Ξ΅-formula' n)) οΌβ¨ refl β©
cβ , (ππ ππ€s cβ (Ξ΅α΅ π))         οΌβ¨ II β©
cβ , (ππ ππ€s cβ (Ξ΅-formula n))  οΌβ¨ III β©
cβ , (ππ ππ€s cβ (Ξ΅-formula n))  οΌβ¨ refl β©
Ξ΅-formula (succ n) β
where
I   = ap (cβ ,_) (unroll-Ξ΅α΅ cβ)
II  = ap (Ξ» x β cβ , (ππ ππ€s cβ x)) (formulas-are-equal n)
III = ap (Ξ» x β x , (ππ ππ€s x (Ξ΅-formula n))) cβ-property
\end{code}

It then follows immediately by transport that Ξ΅-formula' is correct.

\begin{code}

Ξ΅-formula'-theorem : (n : β) (f : π ^ n β π)
β is-putative-root (evals f (Ξ΅-formula' n)) f
Ξ΅-formula'-theorem n f = transport (Ξ» x β is-putative-root (evals f x) f)
(formulas-are-equal n β»ΒΉ)
(Ξ΅-formula-theorem n f)

\end{code}

Added by Alice Laroche, 5th june 2023.

We prove that Ξ΅ f indeed computes the infimum of the set of roots
ordered by the lexicographical order.

\begin{code}

open import Notation.Order

lex-order : {X : π€ Μ } {n : β} β (X β X β  π₯ Μ ) β (X ^ n β X ^ n β π€ β π₯ Μ )
lex-order {n = 0}      _β€_ _        _        = π
lex-order {n = succ n} _β€_ (x , xs) (y , ys) = (x β€ y)
Γ ((x οΌ y) β lex-order _β€_ xs ys)

_β€ββββ_ : {n : β} (xs ys : π ^ n) β π€β Μ
_β€ββββ_ = lex-order _β€β_

open import TypeTopology.InfProperty

Ξ΅-is-roots-lower-bound : {n : β}
(f : π ^ n β π)
β is-roots-lower-bound _β€ββββ_ f (Ξ΅ f)
Ξ΅-is-roots-lower-bound {0}      f _        p = β
Ξ΅-is-roots-lower-bound {succ n} f (x , xs) p = Ξ³ (x , xs) p
where
bβ : π
bβ = Ξ΅π (b β¦ A (f β cons b))

bβ-property : (xs : π ^ n) β f (β , xs) οΌ β β bβ οΌ β
bβ-property xs p = Ξ΅-gives-putative-root (f β cons β) (xs , p)

Ξ΄ : (b : π) (xs : π ^ n) β f (b , xs) οΌ β β bβ οΌ b β Ξ΅ (f β cons bβ) β€ββββ xs
Ξ΄ b xs p refl = Ξ΅-is-roots-lower-bound (f β cons bβ) xs p

Ξ³ : (xs : π ^ (succ n)) β f xs οΌ β β Ξ΅ f β€ββββ  xs
Ξ³ (β , xs) p = β-minimal-converse (bβ-property xs p) , Ξ΄ β xs p
Ξ³ (β , xs) p = β-top , Ξ΄ β xs p

lower-bound-property : {n : β}
(f : π ^ (succ n) β π)
(b : π)
(xs : π ^ n)
β is-roots-lower-bound _β€ββββ_ f (b , xs)
β is-roots-lower-bound _β€ββββ_ (f β cons b) xs
lower-bound-property f b xs lower-bound ys p = prβ (lower-bound (b , ys) p) refl

Ξ΅-is-upper-bound-of-roots-lower-bounds : {n : β}
(f : π ^ n β π)
β is-upper-bound-of-lower-bounds _β€ββββ_ f (Ξ΅ f)
Ξ΅-is-upper-bound-of-roots-lower-bounds {0}      f xs lower-bound = β
Ξ΅-is-upper-bound-of-roots-lower-bounds {succ n} f xs lower-bound = Ξ³ xs lower-bound
where

bβ : π
bβ = Ξ΅π (b β¦ A (f β cons b))

bβ-property : (xs : π ^ n)
β is-roots-lower-bound _β€ββββ_ f (β , xs)
β (b : π) β b οΌ bβ β β β€ bβ
bβ-property xs lower-bound β eq = transport (β β€_) eq
(prβ (lower-bound (β , Ξ΅ (f β cons β))
(eq β»ΒΉ)))
bβ-property xs lower-bound β eq = transport (β β€_) eq β

Ξ΄ : (b : π) (xs : π ^ n)
β is-roots-lower-bound _β€ββββ_ f (b , xs)
β b οΌ bβ
β xs β€ββββ Ξ΅ (f β cons bβ)
Ξ΄ b xs lower-bound refl = Ξ΅-is-upper-bound-of-roots-lower-bounds
(f β cons bβ) xs
(lower-bound-property f bβ xs lower-bound)

Ξ³ : (xs : π ^ (succ n)) β is-roots-lower-bound _β€ββββ_ f xs β xs β€ββββ Ξ΅ f
Ξ³ (β , xs) lower-bound = β ,
Ξ΄ β xs lower-bound
Ξ³ (β , xs) lower-bound = bβ-property xs lower-bound bβ refl ,
Ξ΄ β xs lower-bound

Ξ΅-is-roots-infimum : {n : β} (f : π ^ n β π) β is-roots-infimum _β€ββββ_ f (Ξ΅ f)
Ξ΅-is-roots-infimum f = Ξ΅-is-roots-lower-bound f ,
Ξ΅-is-upper-bound-of-roots-lower-bounds f

π^n-has-inf : {n : β} β has-inf {X = π ^ n} _β€ββββ_
π^n-has-inf f =  Ξ΅ f ,
Ξ΅-gives-putative-root f ,
Ξ΅-is-roots-infimum f

\end{code}

End of Alice's contribution.