Removing transfer from core

Stream: general

[Gabriel Ebner]

@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]

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

[Gabriel Ebner]

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]

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]

dlist is not the problem. Only three examples for dlist use transfer.

[Gabriel Ebner]

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]

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]

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]

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

https://github.com/leanprover/lean/commit/1f45995c169fb518177dfad5060b5a748e8a3b1f#diff-3e35acfba743354acb6f107e860bdb79

[Simon Hudon]

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

[Reid Barton]

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

[Simon Hudon]

Actually @Johannes Hölzl and I would really like to move transfer to mathlib so that we can keep developing it

[Johannes Hölzl]

well, transfer is not so important (we can copy it under another name). I guess ⇒ is more important for some people

[Mario Carneiro]

I can rewrite the proofs for int if required; do the previous proofs work?

[Gabriel Ebner]

Probably.

[Gabriel Ebner]

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