Hi I'm `int2`, here's my recursor

Stream: maths

[Kevin Buzzard]

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]

This is transfer

[Sebastien Gouezel]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

we need better docs on the theorem, I guess

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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
  { apply int2.rel.add, -- +
    { exact int2.rel.mul hx ha }, -- x * a
    { exact int2.rel.mul hy hb } }, -- y * b
end

[Kevin Buzzard]

Is this related to tactic#equiv_rw ?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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]

but any definition will be equal to that one

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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

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

) is that system of relations

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

right

[Adam Topaz]

How would you phrase this typeclass without universe issues?

[Mario Carneiro]

there is no universe issue

[Mario Carneiro]

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

[Adam Topaz]

Oh ok.

[Mario Carneiro]

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]

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]

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

[Adam Topaz]

Right

[Mario Carneiro]

luckily lean supplies such objects using the inductive schema

[Mario Carneiro]

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

[Kevin Buzzard]

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]

Yes, that construction will work

[Mario Carneiro]

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

[Mario Carneiro]

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]

it's a higher inductive type :octopus:

[Reid Barton]

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

[Reid Barton]

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

[Adam Topaz]

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
  add_assoc : ∀ {a b c} → add a (add b c) ≡ add (add a b) c
  add_comm : ∀ {a b} → add a b ≡ add b a
  zero_add : ∀ {a} → add zero a ≡ a
  add_neg_left : ∀ {a} → add (neg a) a ≡ zero
  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]

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

[Alex J. Best]

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

[Adam Topaz]

Haven't seen that lecture, thanks!