(type theory) - feedback on first exercise using definitions

Stream: new members

[rzeta0]

To get a better insight into how proof assistants like Lean work, I've been working through Nederpelt's Type Theory & Formal proof, doing all the exercises. I'm now on Chapter 8 which introduces definitions.

The very first exercise at the end of the chapter is supposed to be easy, but the introduction to definitions was a little rapid so I'm unsure if the ideas really settled.

I'd welcome your feedback on my solution below.

I've intentionally been verbose with my thinking to expose any flaws in my understanding.

---

Exercise 8.1

In Section 8.7, we gave the name $p(m,n,u)$ to a proof of the proposition

$$∃x,y : \mathbb{Z}. (mx+ny = 1)$$

in the context $Γ ≡ m : \mathbb{N}^+, n : \mathbb{N}^+, u : coprime(m,n)$.

Assume that we have constructed, in context $m : \mathbb{N}^+, n : \mathbb{N}^+$, a proof (i.e. an inhabitant) $q(m,n)$ of the proposition

$$coprime(m,n) ⇒coprime(n,m)$$

Find an inhabitant of

$$∃x,y : \mathbb{Z}. (nx+my = 1)$$

in context $Γ$.

---

My Solution

We start with $p$ which is the name given to the proof of the proposition

$$\exists x,y : \mathbb{Z}. (mx+ny = 1) \tag{i}$$

The name $p$ also carries with it the ordered list of arguments $(m,n,u)$. The first two arguments are the positive natural numbers $n$ and $m$ expected by the proof. The third argument is a proof that the first two arguments, $m$ and $n$ (in that order), are co-prime.

That is

$$\Gamma \;  \triangleright \;  p(m,n,u) := \textbf{formalproof} \; : \; \exists x,y:\mathbb{Z}.(mx + ny = 1)$$

Note that we don't need to know the details of $\textbf{formalproof}$, we can assume it exists, and refer to it by its name $p$.

We want to prove the proposition

$$\exists x,y : \mathbb{Z}. (nx+my = 1) \tag{ii}$$

The order of $n$ and $m$ is different to (i), and this means $p(m,n,u)$ is not a proof of (ii). Is this correct?

We are given a proof $q(m,n)$ of the proposition $coprime(m,n) \implies coprime(n,m)$, that is

$$q(m,n) := \textbf{anotherproof} \; : \; coprime(m,n) \implies coprime(n,m)$$

So the proof $q(m,n)$ applied to $u$, the proof $coprime(m,n)$, gives us a proof $coprime(n,m)$.

$$q(m,n)u \; : \; coprime(n,m)$$

We also need to check that the context of $q$ allows it to be used in the context in which we apply it to $u$, that is, $\Gamma$. The context of $q$ us a subset of $\Gamma$ so can be used, and it can be used with $u$ because $u$ is defined in $\Gamma$. Is this right?

If we are to use $p$ as a proof of $∃x,y : \mathbb{Z}. (nx+my = 1)$, the order of the variables $n$ and $m$ require the proof to be of the form $p(n,m,?)$ and not $p(m,n,?)$. The $?$ a proof that $n$ and $m$ (in that order) are co-prime. We have that from above.

And so $p(n,m,q(m,n)u)$ is a proof of the proposition (ii). That is

$$\Gamma \;  \triangleright \;  p(n,m,q(m,n)u) \; : \; \exists x,y:\mathbb{Z}.(nx + my = 1)$$

And we can choose to give this proof a name $r(m,n,u)$, but that is optional.

$$\Gamma \;  \triangleright \; r(m,n,u) \; := \;  p(n,m,q(m,n)u) \; : \; \exists x,y:\mathbb{Z}.(nx + my = 1)$$

---

Variable Order and Renaming

Assuming the above is ok, one question I am not happy about is why we can't just ignore the order of variables $m$ and $n$ and just use the fact that they have the correct type to be the first and second arguments of $p(m,n,u)$. That is,

$$\begin{align*}\Gamma \;  \triangleright \;  p(m,n,u) \; & : \; \exists x,y:\mathbb{Z}.(mx + ny = 1) \\ \\ & \equiv \exists x,y:\mathbb{Z}.(nx + my = 1) \text{ by variable rewriting}\end{align*}$$

[Aaron Liu]

you can try your idea out in Lean and see what happens

import Mathlib

-- we give this proof a name
theorem p (m n : ℕ+) (u : Nat.Coprime m n) : ∃ x y : ℤ, m * x + n * y = 1 :=
  -- don't worry about the contents of the proof
  ⟨Nat.gcdA m n, Nat.gcdB m n,
    (Nat.gcd_eq_gcd_ab m n).symm.trans (congrArg Nat.cast (Nat.Coprime.gcd_eq_one u))⟩

-- we also give this other proof a name
theorem q (m n : ℕ+) : Nat.Coprime m n → Nat.Coprime n m :=
  -- don't worry about the contents
  Nat.Coprime.symm

-- in this context, inhabit this type
example (m n : ℕ+) (u : Nat.Coprime m n) : ∃ x y : ℤ, n * x + m * y = 1 :=
  sorry

[Aaron Liu]

rzeta0 said:

Variable Order and Renaming

Assuming the above is ok, one question I am not happy about is why we can't just ignore the order of variables $m$ and $n$ and just use the fact that they have the correct type to be the first and second arguments of $p(m,n,u)$. That is,

$$\begin{align*}\Gamma \;  \triangleright \;  p(m,n,u) \; & : \; \exists x,y:\mathbb{Z}.(mx + ny = 1) \\ \\ & \equiv \exists x,y:\mathbb{Z}.(nx + my = 1) \text{ by variable rewriting}\end{align*}$$

I am confused, what do you mean "by variable rewriting"? You can't just identify all the variables that have the same type.

[rzeta0]

At school, in pen and paper maths (no lean, no type theory), if I were asked to prove the statement

$$\exists x,y:\mathbb{Z}.(nx + my=1) \tag{1}$$

using a given proof $p(m,n)$ of

$$\exists x,y:\mathbb{Z}.(mx + ny=1) \tag{2}$$

I would say $p(n,m)$ is sufficient, and is a proof of (1) because only the names of the variables have changed.

I think this is where my question comes from.

---

Thanks for the code. I tried it.

I tried p m n u and it gave the following which challenges my intuition about "renaming"

Type mismatch
  p m n u
has type
  ∃ x y, ↑↑m * x + ↑↑n * y = 1
but is expected to have type
  ∃ x y, ↑↑n * x + ↑↑m * y = 1

the correct answer is of course

example (m n : ℕ+) (u : Nat.Coprime m n) : ∃ x y : ℤ, n * x + m * y = 1 :=
  p n m (q m n u)

[Aaron Liu]

but it's not just $p(n,m)$

[Aaron Liu]

the $p$ takes three arguments

[Aaron Liu]

do you mean renaming like this?

import Mathlib

-- we give this proof a name
theorem p (m n : ℕ+) (u : Nat.Coprime m n) : ∃ x y : ℤ, m * x + n * y = 1 :=
  -- don't worry about the contents of the proof
  ⟨Nat.gcdA m n, Nat.gcdB m n,
    (Nat.gcd_eq_gcd_ab m n).symm.trans (congrArg Nat.cast (Nat.Coprime.gcd_eq_one u))⟩

-- we also give this other proof a name
theorem q (m n : ℕ+) : Nat.Coprime m n → Nat.Coprime n m :=
  -- don't worry about the contents
  Nat.Coprime.symm

-- in this context, inhabit this type
example (m n : ℕ+) (u : Nat.Coprime m n) : ∃ x y : ℤ, n * x + m * y = 1 := by
  -- we have p(m,n,u)
  have pmnu := p m n u
  -- swap some names around
  rename' m => n, n => m
  -- so now the goal is `∃ x y : ℤ, m * x + n * y = 1`
  -- but of course renaming didn't just affect the goal
  -- we've also renamed occurrences of `m` and `n` in the types of `u` and `pmnu`
  -- so it didn't really help (it's just kind of shuffling names around)
  sorry

[rzeta0]

Aaron Liu said:

but it's not just $p(n,m)$

I did mean $p(m,n)$ with two arguments. I was trying to simplify the scenario to see if I could explain my thinking about variable renaming.

Let me think of a different school exercise example.

Imagine there is a proof (a theorem) that the product of two odd numbers $a, b$ is odd. That is $ab$ is odd. Let's call this proof $P$. It takes two arguments $a$ and $b$.

Now imagine we're asked to prove that for two odd numbers $b$ and $a$, the product $ba$ is odd. Then I can use $P(x,y)$ with $x=b, y=a$.

So I don't understand why we need to develop a new proof $P(b,a)$ that uses the idea of commutativity of products, when we have $P(a,b)$.

Apologies if I'm being stupid. Doing for "formal" maths has exposed things that I have only weakly understood previously.

[Vlad Tsyrklevich]

Your idea works when $p(m, n)$ is a proof of universally quantified statement over $m, n$ that are both of the same type. The reason it doesn't work in your original example is that it's not a a priori clear that $coprime(a, b) \iff coprime(b, a)$. Of course we know that coprime is a symmetric relation on two numbers, but in formal math you have to actually prove that. Indeed, in the exercise they tell you that coprime is symmetric and that you can use that fact. You can't just "re-write variables" though, if $p(m, n, u)$ takes two numbers $m, n$ and a proof that $m > n$ and returns a proof that $m \ge n$ then you cannot just rewrite it to $n \ge m$--the relation is no longer symmetric and the statement is false.

[rzeta0]

Thanks Aaron and Vlad, you have both given me something to think about.

Your example of $\ge$ not being symmetric is helpful.

Again I apologise for the lack of precision in my question.

I think doing the rest of the exercises will help this issue resolve itself in my brain.

[Vlad Tsyrklevich]

No need for apology, on the contrary I think you stated your context and idea with enough precision to make it immediately clear what the counterexample is.