## Stream: maths

### Topic: Hi I'm int2, here's my recursor

#### Kevin Buzzard (Aug 09 2020 at 17:44):

If I want access to all the API of int for my brand spanking new type int2, a ring which I can prove is an initial object in the category of rings but which is not defeq to int, how can I get it? Is the idea that we should write automation like for to-additive? Somehow to-additive is the solution for X -> X -> X and I'm asking for a solution for the initial object? Should automation be porting all the constructions so that they apply to an arbitrary type with the right constructor and eliminator? Does one have to write different code for each constant in mathlib? When an inductive type is made, the recursor is given as an axiom and then some computer program makes about ten more functions using it, with names like mk_inj or whatever. Should other algorithms be run later on. Hey there should be a linter for checking to see that properties and definitions are canonical, in the sense that we might be explaining them for the irreducible real but the results remain true for any object with the right recursor (the reals are uniquely defined up to unique isomorphism by some purely topological/ring-theoretic properties).If I have real2 and a proof that it has the right recursor, can use Lean's theory of real manifolds with my reals?

#### Mario Carneiro (Aug 09 2020 at 17:47):

This is transfer

#### Sebastien Gouezel (Aug 09 2020 at 17:57):

Lean can definitely use its theory of manifolds for your type, because everything is set up for general (normed) fields :-)

#### Kevin Buzzard (Aug 09 2020 at 18:09):

oh did I mention that my real2 has a real2-valued norm?

#### Kevin Buzzard (Aug 09 2020 at 18:17):

so when do I get transfer in Lean? I'm now beginning to see the point of it. What are the obstructions for getting it working in Lean 3? Will Lean 4 be any different? How much of a problem is the g ^ n v n \bub g order issue?

#### Mario Carneiro (Aug 09 2020 at 18:18):

We need a bunch of lemmas to be marked in the library

#### Mario Carneiro (Aug 09 2020 at 18:18):

I think the tactic itself works fine, although it is a bit raw

#### Kevin Buzzard (Aug 09 2020 at 18:19):

for example how could i get a proof of B\'ezout's theorem for int2?

#### Kevin Buzzard (Aug 09 2020 at 18:19):

(NB searching for Bezout without the accent gives no results in mathlib -- is this expected behaviour?)

#### Mario Carneiro (Aug 09 2020 at 18:20):

we need better docs on the theorem, I guess

#### Mario Carneiro (Aug 09 2020 at 18:20):

I think it has the very natural and obvious name of gcd_eq_gcd_ab

#### Mario Carneiro (Aug 09 2020 at 18:21):

I think the best demo of transfer in mathlib right now is the derivation of lemmas about num using the isomorphism to nat

#### Mario Carneiro (Aug 09 2020 at 18:22):

actually that's not really true, it uses transfer in the abstract but it's a homegrown version

#### Mario Carneiro (Aug 09 2020 at 18:23):

I recall there being a proof of int properties using transfer in core but I think it has since been replaced by an elementary proof

#### Mario Carneiro (Aug 09 2020 at 18:53):

Here's a proof of bezout's theorem for int2 written in a way that makes the boilerplate parts obvious:

import data.int.gcd tactic.transfer

-- this should be in the library already
attribute [class] relator.bi_unique

def equiv.rel {α β} (e : α ≃ β) (a : α) (b : β) := e a = b

instance equiv.rel.bi_total {α β} (e : α ≃ β) : relator.bi_total e.rel :=
⟨λ a, ⟨_, rfl⟩, λ b, ⟨_, e.apply_symm_apply _⟩⟩

instance equiv.rel.bi_unique {α β} (e : α ≃ β) : relator.bi_unique e.rel :=
⟨λ a b c h1 h2, e.injective (h1.trans h2.symm), λ a b c h1 h2, h1.symm.trans h2⟩

-- int2 is a type, suppose we have proven an equivalence to int
constant int2 : Type
constant int2.equiv : int2 ≃ ℤ

-- and we know it is a ring and the equivalence respects the ring ops
-- (the ring structure may or may not be directly induced by int2.equiv, but we are proving here
-- that it may as well be)
@[instance] constant int2.ring : ring int2
axiom int2.equiv_zero : int2.equiv 0 = 0
axiom int2.equiv_one : int2.equiv 1 = 1
axiom int2.equiv_add (a b) : int2.equiv (a + b) = a.equiv + b.equiv
axiom int2.equiv_mul (a b) : int2.equiv (a * b) = a.equiv * b.equiv

-- we also need a gcd function in order to state bezout
constant int2.gcd : int2 → int2 → int2
axiom int2.equiv_gcd (a b) : int2.equiv (int2.gcd a b) = (int2.equiv a).gcd (int2.equiv b)

-- surprisingly not a one liner from mathlib, but let's suppose this is somewhere
theorem int.bezout (x y : ℤ) : ∃ a b, (int.gcd x y : ℤ) = x * a + y * b := sorry

-- Here we begin the setup for transfer. The core concept is a relation between the types we
-- want to transfer. One natural source of transfer relations is equivs, but they can also
-- come from general injective / surjective functions. But equivs have the nicest properties
def int2.rel : int2 → ℤ → Prop := equiv.rel int2.equiv
instance int2.rel.bi_total : relator.bi_total int2.rel := equiv.rel.bi_total _
instance int2.rel.bi_unique : relator.bi_unique int2.rel := equiv.rel.bi_unique _

-- Now to each equiv lemma we associate the corresponding relational lemma
theorem int2.rel.zero : int2.rel 0 0 := int2.equiv_zero
theorem int2.rel.one : int2.rel 1 1 := int2.equiv_one

theorem int2.rel.add {{x x'}} (hx : int2.rel x x') {{y y'}} (hy : int2.rel y y') :
int2.rel (x + y) (x' + y') :=
by cases hx; cases hy; apply int2.equiv_add

theorem int2.rel.mul {{x x'}} (hx : int2.rel x x') {{y y'}} (hy : int2.rel y y') :
int2.rel (x * y) (x' * y') :=
by cases hx; cases hy; apply int2.equiv_mul

theorem int2.rel.gcd {{x x'}} (hx : int2.rel x x') {{y y'}} (hy : int2.rel y y') :
int2.rel (int2.gcd x y) (int.gcd x' y' : ℤ) :=
by cases hx; cases hy; apply int2.equiv_gcd

-- Finally, the proof of int2.bezout itself is performed by structural recursion on the term
-- (this is what the transfer tactic should be able to automate)
theorem int2.bezout : ∀ x y : int2, ∃ a b, int2.gcd x y = x * a + y * b :=
begin
refine iff.mpr _ int.bezout,
refine relator.rel_forall_of_total int2.rel (λ x x' hx, _), -- ∀ x,
refine relator.rel_forall_of_total int2.rel (λ y y' hy, _), -- ∀ y,
refine relator.rel_exists_of_total int2.rel (λ a a' ha, _), -- ∃ a,
refine relator.rel_exists_of_total int2.rel (λ b b' hb, _), -- ∃ b,
apply relator.rel_eq int2.rel.bi_unique, -- eq
{ exact int2.rel.gcd hx hy }, -- gcd x y
{ exact int2.rel.mul hx ha }, -- x * a
{ exact int2.rel.mul hy hb } }, -- y * b
end


#### Kevin Buzzard (Aug 09 2020 at 19:18):

Is this related to tactic#equiv_rw ?

#### Kevin Buzzard (Aug 09 2020 at 19:19):

This takes me to a link with messed up style in duck duck go browser on Android

#### Kevin Buzzard (Aug 09 2020 at 19:24):

So all the constants in the statement of the theorem, you need analogous constants in your rel machine

#### Mario Carneiro (Aug 09 2020 at 19:25):

definitions too, although those (like gcd) can be proven using the same process recursively

#### Mario Carneiro (Aug 09 2020 at 19:25):

In fact this also has a great deal of similarity to (my understanding of) Cyril's parametricity tactic

#### Kevin Buzzard (Aug 09 2020 at 19:26):

Here's a harder one. Int has functions called things like gcd_a and gcd_b. We can use nat if you like, I don't know what's easier. But then there's a theorem that Bezout is realised by these two functions. Can we pull back these functions whilst maintaining computability and prove the corresponding theorem about int2?

#### Mario Carneiro (Aug 09 2020 at 19:27):

Are you okay with the implementation e o gcd_a o e^-1 for int2.gcd_a? That will be computable if e is

#### Mario Carneiro (Aug 09 2020 at 19:28):

Most of the time this is not actually the definition we want, so the framework lets the user supply a separate definition for things like int2.gcd_a

#### Mario Carneiro (Aug 09 2020 at 19:28):

but any definition will be equal to that one

#### Mario Carneiro (Aug 09 2020 at 19:29):

the procedure for pulling back gcd_eq_gcd_ab directly instead of the existential one follows exactly the same recipe, in fact it's a bit easier since there are fewer quantifiers to deal with

#### Mario Carneiro (Aug 09 2020 at 19:30):

for a purely universal formula, you can often do it by a simp set (this is what the poor-mans transfer in data.num.lemmas is doing)

#### Mario Carneiro (Aug 09 2020 at 19:31):

the real power of relations shows up when you are pulling full first order formulas like bezout here

#### Mario Carneiro (Aug 09 2020 at 19:32):

in fact you can even quantify over higher order things as long as you have a system of relations that covers all the types you want to talk about

#### Mario Carneiro (Aug 09 2020 at 19:32):

The funny arrow notation you see in the relator file (for example

lemma rel_and : ((↔) ⇒ (↔) ⇒ (↔)) (∧) (∧) :=


) is that system of relations

#### Mario Carneiro (Aug 09 2020 at 19:34):

In this case ((↔) ⇒ (↔) ⇒ (↔)) is a relation that relates elements of Prop -> Prop -> Prop to itself

#### Mario Carneiro (Aug 09 2020 at 19:35):

I could have written int2.rel.add et al using this relator notation but it's pretty impenetrable when you see it for the first time

#### Mario Carneiro (Aug 09 2020 at 19:36):

theorem int2.rel.add : (int2.rel ⇒ int2.rel ⇒ int2.rel) (+) (+) :=
by cases hx; cases hy; apply int2.equiv_add


#### Kevin Buzzard (Aug 09 2020 at 19:39):

So there should be some tag which triggers an auto generation of a proof/definition which takes as input any initial object in the category of rings and spits out a theorem/definition in this int_recursor namespace?

#### Mario Carneiro (Aug 09 2020 at 19:41):

It depends on the goal. I should look into what isabelle's transfer front end does

#### Mario Carneiro (Aug 09 2020 at 19:41):

For this proof, you want int2.rel theorems about all the constants in your theorems, but that's not general enough for int3

#### Mario Carneiro (Aug 09 2020 at 19:42):

the library needs to be marked up for all the transfers it is meant to support

#### Mario Carneiro (Aug 09 2020 at 19:44):

in this case, one reasonable transfer would be to go from int to any ring, and maybe the other way around under some is_int typeclass

#### Kevin Buzzard (Aug 09 2020 at 22:12):

I see, there could be a typeclass for "I'm an initial object in rings" and an automated method to prove generalisations of int theorems for any object with the is_int typeclass

right

#### Adam Topaz (Aug 09 2020 at 23:09):

How would you phrase this typeclass without universe issues?

#### Mario Carneiro (Aug 09 2020 at 23:09):

there is no universe issue

#### Mario Carneiro (Aug 09 2020 at 23:09):

it can be as simple as the assertion of a ring equiv to int

Oh ok.

#### Mario Carneiro (Aug 09 2020 at 23:10):

Well, if you take Kevin's approach there might be an issue with stating "I'm an initial object" if you want to do that by stating a universal property

#### Adam Topaz (Aug 09 2020 at 23:11):

I guess if it's initial with respect to universe level 0 rings, then it's initial with respect to any universe level, but that requires proof

#### Mario Carneiro (Aug 09 2020 at 23:11):

more to the point, that requires the existence of an actual initial object in the universe in question

Right

#### Mario Carneiro (Aug 09 2020 at 23:12):

luckily lean supplies such objects using the inductive schema

#### Mario Carneiro (Aug 09 2020 at 23:12):

so basically you can't get away from using a concrete implementation like int

#### Kevin Buzzard (Aug 10 2020 at 18:47):

I am annoyed that I can't make int without using nat. Is there a way of making int an inductive type directly? Oh -- I can make it into a quotient of an inductive type, like zero : int | succ : int -> int | pred : int -> int modulo succ pred = id = pred succ. Is it somehow a theorem that it cannot be an inductive type? Oh wait, I can just define it as nat can't I :-/ and then put an exotic zero and 1 and add on it.

#### Mario Carneiro (Aug 10 2020 at 21:20):

Yes, that construction will work

#### Mario Carneiro (Aug 10 2020 at 21:21):

The problem is that int is not naturally presented as an inductive type, unlike nat

#### Mario Carneiro (Aug 10 2020 at 21:23):

But quotients of free algebras give you quite a lot of structures. Especially if you want to show it is initial in the category of rings

#### Reid Barton (Aug 10 2020 at 21:25):

it's a higher inductive type :octopus:

#### Reid Barton (Aug 10 2020 at 21:27):

well, I guess I had in mind the quotient of int \x int which is a two-step construction

#### Reid Barton (Aug 10 2020 at 21:27):

but you can also naturally express it as a single higher (or quotient) inductive type

#### Adam Topaz (Aug 10 2020 at 22:03):

Here is some sketchy cubical agda

data Int {ℓ} : Type ℓ where
zero : Int
one : Int
add : Int {ℓ} → Int {ℓ} → Int
mul : Int {ℓ} → Int {ℓ} → Int
neg : Int {ℓ} → Int
mul_assoc : ∀ {a b c} → mul a (mul b c) ≡ mul a (mul b c)
one_mul : ∀ {a} → mul one a ≡ a
mul_one : ∀ {a} → mul a one ≡ a
left_distrib : ∀ {a b c} → mul a (add b c) ≡ add (mul a b) (mul a c)
right_distrib : ∀ {a b c} → mul (add a b) c ≡ add (mul a c) (mul b c)
add_compat : ∀ {a b c} → a ≡ b → add a c ≡ add b c
mul_compat_left : ∀ {a b c} → a ≡ b → mul a c ≡ mul b c
mul_compat_right : ∀ {a b c} → a ≡ b → mul c a ≡ mul c b
neg_compat : ∀ {a b} → a ≡ b → neg a ≡ neg b
is_set : isSet Int


#### Adam Topaz (Aug 10 2020 at 22:05):

But it's "obviously" the initial ring :)

#### Alex J. Best (Aug 10 2020 at 22:06):

I quite enjoyed this LICS talk on the topic https://www.youtube.com/watch?v=Fov95A2bGDI

#### Adam Topaz (Aug 10 2020 at 22:08):

Haven't seen that lecture, thanks!

Last updated: May 19 2021 at 02:10 UTC