Zulip Chat Archive

Stream: general

Topic: Removing transfer from core


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 10 2019 at 11:36):

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

view this post on Zulip 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}

view this post on Zulip 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?

view this post on Zulip Gabriel Ebner (Jan 10 2019 at 16:49):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

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

view this post on Zulip Simon Hudon (Jan 10 2019 at 17:18):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 10 2019 at 20:32):

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

view this post on Zulip Gabriel Ebner (Jan 10 2019 at 20:33):

Probably.

view this post on Zulip 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