# Zulip Chat Archive

## Stream: general

### Topic: Removing transfer from core

#### Gabriel Ebner (Jan 10 2019 at 11:19):

@Johannes Hölzl suggested removing transfer from core and move it into mathlib. Maybe the biggest positive effect is that we could then use the ⇒ symbol in mathlib.

I tried just removing the file, but some theorems about integers and dlist are proving using transfer. Any ideas? Does anyone want to rewrite the proofs by hand? Should we just remove the ⇒ notation for 3.4.2?

#### Kevin Buzzard (Jan 10 2019 at 11:36):

Can one move those theorems about integers out of core as well?

#### Gabriel Ebner (Jan 10 2019 at 12:37):

Probably not:

instance : comm_ring int := { add := int.add, add_assoc := by int.transfer, zero := int.zero, zero_add := by int.transfer, add_zero := by int.transfer, neg := int.neg, add_left_neg := by int.transfer, add_comm := by int.transfer, mul := int.mul, mul_assoc := by int.transfer tt, one := int.one, one_mul := by int.transfer, mul_one := by int.transfer, left_distrib := by int.transfer tt, right_distrib := by int.transfer tt, mul_comm := by int.transfer}

#### Simon Hudon (Jan 10 2019 at 16:47):

Can a more specific script handle them? E.g. search and replace mul with add and other lemmas similarly? Also Can we take dlist out of core?

#### Gabriel Ebner (Jan 10 2019 at 16:49):

`dlist`

is not the problem. Only three examples for `dlist`

use `transfer`

.

#### Gabriel Ebner (Jan 10 2019 at 16:50):

It's the integers that are problematic. We prove that the integers form a commutative ring using transfer, I'm not sure we should remove that instance from core.

#### Gabriel Ebner (Jan 10 2019 at 16:53):

Maybe I should clarify: `transfer`

here switches between two isomorphic representations of the integers. The definition of `int`

is an inductive type with two constructors 1) non-negative natural number 2) negative number. The `transfer`

tactic then switches to the much nicer definition using pairs of natural numbers.

#### Andrew Ashworth (Jan 10 2019 at 16:58):

The proofs for `int`

should be in the git history, iirc. They were not always proved via transfer, but maybe I am thinking of Lean 2.

#### Gabriel Ebner (Jan 10 2019 at 17:05):

Doesn't even look so bad. I thought it was more horrible:

protected lemma distrib_left (a b c : ℤ) : a * (b + c) = a * b + a * c := begin cases (int.left_total_rel_int_nat_nat a) with a' ha, cases (int.left_total_rel_int_nat_nat b) with b' hb, cases (int.left_total_rel_int_nat_nat c) with c' hc, apply (int.rel_eq (int.rel_mul ha (int.rel_add hb hc)) (int.rel_add (int.rel_mul ha hb) (int.rel_mul ha hc)))^.mpr, simp [mul_add, add_mul] end

#### Simon Hudon (Jan 10 2019 at 17:18):

How are integers used in core? I thought only natural numbers were really needed there

#### Reid Barton (Jan 10 2019 at 17:22):

What about, in 3.4.2, simply freeing up the character ⇒ somehow, while leaving transfer and the instances in place?

#### Simon Hudon (Jan 10 2019 at 17:26):

Actually @Johannes Hölzl and I would really like to move `transfer`

to mathlib so that we can keep developing it

#### Johannes Hölzl (Jan 10 2019 at 18:30):

well, `transfer`

is not so important (we can copy it under another name). I guess `⇒`

is more important for some people

#### Mario Carneiro (Jan 10 2019 at 20:32):

I can rewrite the proofs for `int`

if required; do the previous proofs work?

#### Gabriel Ebner (Jan 10 2019 at 20:33):

Probably.

#### Gabriel Ebner (Jan 11 2019 at 17:25):

See https://github.com/leanprover/lean/pull/1989

Last updated: May 08 2021 at 10:12 UTC