## Stream: general

### Topic: how to use transfer

#### Mario Carneiro (Oct 06 2018 at 05:21):

Okay, here is a mockup use of transfer:

import tactic.interactive

inductive xnat : Type
| zero : xnat
| succ : xnat → xnat

instance : has_zero xnat := ⟨xnat.zero⟩
instance : has_one xnat := ⟨xnat.succ 0⟩

def to_xnat : ℕ → xnat
| 0 := 0
| (nat.succ n) := (to_xnat n).succ

def of_xnat : xnat → ℕ
| 0 := 0
| (xnat.succ n) := (of_xnat n).succ

theorem to_of_xnat : ∀ n, (to_xnat (of_xnat n)) = n
| 0 := rfl
| (xnat.succ n) := congr_arg xnat.succ (to_of_xnat n)

theorem of_to_xnat : ∀ n, (of_xnat (to_xnat n)) = n
| 0 := rfl
| (nat.succ n) := congr_arg nat.succ (of_to_xnat n)

def rel (x : xnat) (n : ℕ) : Prop := to_xnat n = x

lemma rel_zero : rel 0 0 := eq.refl _
lemma rel_succ : (rel ⇒ rel) xnat.succ nat.succ :=
by rintro m _ ⟨⟩; exact rfl
lemma rel_one : rel 1 1 := eq.refl _

⟨λ m n, by induction n; [exact m, exact n_ih.succ]⟩

theorem to_xnat_add (m) : ∀ n, to_xnat (m + n) = to_xnat m + to_xnat n
| 0 := rfl
| (nat.succ n) := congr_arg xnat.succ (to_xnat_add n)

lemma rel_add : (rel ⇒ rel ⇒ rel) (+) (+) :=
by rintro m _ ⟨⟩ n _ ⟨⟩; apply to_xnat_add

lemma rel_eq : (rel ⇒ rel ⇒ iff) (=) (=) :=
by rintro m _ ⟨⟩ n _ ⟨⟩; exact
⟨λ e, by simpa [of_to_xnat] using congr_arg of_xnat e, congr_arg _⟩

instance : relator.bi_total rel :=
⟨λ a, ⟨_, to_of_xnat _⟩, λ a, ⟨_, rfl⟩⟩

example : ∀ x y : xnat, x + y = y + x :=
begin
transfer.transfer [relator.rel_forall_of_total, rel_eq, rel_add],
end


#### Scott Olson (Oct 06 2018 at 05:26):

Coincidentally I was playing with some proofs recently where I wished I had automatic transport. I'm playing with (regular) languages, and I've manually proven language equivalences like L₁ ≃ L₃ → L₂ ≃ L₄ → L₁ ∪ L₂ ≃ L₃ ∪ L₄ which feel a lot like the A ≃ B → P A ≃ P B univalent transport

#### Johan Commelin (Oct 06 2018 at 05:27):

@Mario Carneiro Thanks a lot for this mock-up! Do you mind if I post my thoughts about it?

#### Mario Carneiro (Oct 06 2018 at 05:28):

of course, that's the idea

#### Scott Olson (Oct 06 2018 at 05:28):

I wonder if transfer would apply here? It might run intro trouble because these is an equivalence of functions, and funext-as-a-theorem would still be something cubical types have and Lean doesn't, but I haven't thought this through

#### Johan Commelin (Oct 06 2018 at 05:28):

Should we take it to a different thread?

#### Johan Commelin (Oct 06 2018 at 05:29):

@Mario Carneiro wrote a mockup use of transfer:

import tactic.interactive

inductive xnat : Type
| zero : xnat
| succ : xnat → xnat

instance : has_zero xnat := ⟨xnat.zero⟩
instance : has_one xnat := ⟨xnat.succ 0⟩

def to_xnat : ℕ → xnat
| 0 := 0
| (nat.succ n) := (to_xnat n).succ

def of_xnat : xnat → ℕ
| 0 := 0
| (xnat.succ n) := (of_xnat n).succ

theorem to_of_xnat : ∀ n, (to_xnat (of_xnat n)) = n
| 0 := rfl
| (xnat.succ n) := congr_arg xnat.succ (to_of_xnat n)

theorem of_to_xnat : ∀ n, (of_xnat (to_xnat n)) = n
| 0 := rfl
| (nat.succ n) := congr_arg nat.succ (of_to_xnat n)

def rel (x : xnat) (n : ℕ) : Prop := to_xnat n = x

lemma rel_zero : rel 0 0 := eq.refl _
lemma rel_succ : (rel ⇒ rel) xnat.succ nat.succ :=
by rintro m _ ⟨⟩; exact rfl
lemma rel_one : rel 1 1 := eq.refl _

⟨λ m n, by induction n; [exact m, exact n_ih.succ]⟩

theorem to_xnat_add (m) : ∀ n, to_xnat (m + n) = to_xnat m + to_xnat n
| 0 := rfl
| (nat.succ n) := congr_arg xnat.succ (to_xnat_add n)

lemma rel_add : (rel ⇒ rel ⇒ rel) (+) (+) :=
by rintro m _ ⟨⟩ n _ ⟨⟩; apply to_xnat_add

lemma rel_eq : (rel ⇒ rel ⇒ iff) (=) (=) :=
by rintro m _ ⟨⟩ n _ ⟨⟩; exact
⟨λ e, by simpa [of_to_xnat] using congr_arg of_xnat e, congr_arg _⟩

instance : relator.bi_total rel :=
⟨λ a, ⟨_, to_of_xnat _⟩, λ a, ⟨_, rfl⟩⟩

example : ∀ x y : xnat, x + y = y + x :=
begin
transfer.transfer [relator.rel_forall_of_total, rel_eq, rel_add],
end


#### Johan Commelin (Oct 06 2018 at 05:30):

First of all: I think for general applicability I think we need a quick way to construct rel from an equiv.

#### Johan Commelin (Oct 06 2018 at 05:32):

And then I have several conflicting thoughts...

#### Johan Commelin (Oct 06 2018 at 05:33):

One is, given nat and the definition of xnat I would like to just immediately transfer comm_semiring to xnat.

#### Johan Commelin (Oct 06 2018 at 05:33):

All the structure and proofs should be transferable using automation.

#### Johan Commelin (Oct 06 2018 at 05:34):

On the other hand, one might find oneself in the situation where both sides are already equipped with some structure. In this case both already have a 0 and a +.

#### Mario Carneiro (Oct 06 2018 at 05:34):

It is easy to define equiv.rel : A ~= B -> A -> B -> Prop

#### Johan Commelin (Oct 06 2018 at 05:35):

Right, I'm collecting things that you find easy to define (-;

#### Mario Carneiro (Oct 06 2018 at 05:35):

immediately transferring structures is both more difficult and not necessarily what we want

#### Johan Commelin (Oct 06 2018 at 05:35):

So, suppose that both have a 0 and + like in your example.

#### Mario Carneiro (Oct 06 2018 at 05:36):

I would prefer an expedited method for showing that pre-existing structures are compatible with an equiv

#### Mario Carneiro (Oct 06 2018 at 05:36):

..oh wait, that's group_iso etc

Exactly

#### Mario Carneiro (Oct 06 2018 at 05:36):

so problem solved?

#### Johan Commelin (Oct 06 2018 at 05:36):

So we show that to_xnat is an add_monoid iso. And then?

#### Johan Commelin (Oct 06 2018 at 05:37):

Then there should be an easy way to extract those rel-lemmas

#### Mario Carneiro (Oct 06 2018 at 05:37):

oh yes, that's a one liner

#### Johan Commelin (Oct 06 2018 at 05:37):

After that, proving that xnat is a comm_monoid should be by transfer.

#### Johan Commelin (Oct 06 2018 at 05:37):

Or something like that.

#### Mario Carneiro (Oct 06 2018 at 05:38):

we could put that in the theorems for group_iso

#### Mario Carneiro (Oct 06 2018 at 05:38):

But I am wary about constructing structure using transfer

#### Mario Carneiro (Oct 06 2018 at 05:38):

you might use transfer to prove that the addition is commutative, like I showed, but the definitions themselves should stand on their own

#### Johan Commelin (Oct 06 2018 at 05:39):

lemma rel_zero : rel 0 0 := eq.refl _
lemma rel_succ : (rel ⇒ rel) xnat.succ nat.succ :=
by rintro m _ ⟨⟩; exact rfl
lemma rel_one : rel 1 1 := eq.refl _
lemma rel_add : (rel ⇒ rel ⇒ rel) (+) (+) :=
by rintro m _ ⟨⟩ n _ ⟨⟩; apply to_xnat_add

lemma rel_eq : (rel ⇒ rel ⇒ iff) (=) (=) :=
by rintro m _ ⟨⟩ n _ ⟨⟩; exact
⟨λ e, by simpa [of_to_xnat] using congr_arg of_xnat e, congr_arg _⟩

instance : relator.bi_total rel :=
⟨λ a, ⟨_, to_of_xnat _⟩, λ a, ⟨_, rfl⟩⟩

example : ∀ x y : xnat, x + y = y + x :=
begin
transfer.transfer [relator.rel_forall_of_total, rel_eq, rel_add],
end


I would wish that this could all be compressed into 2 or 3 lines.

#### Mario Carneiro (Oct 06 2018 at 05:40):

I don't think it needs to, it can be done in generality

#### Mario Carneiro (Oct 06 2018 at 05:40):

the stuff about applying transfer.transfer is not nice though, it should be easier than that

#### Johan Commelin (Oct 06 2018 at 05:41):

@Mario Carneiro Why are you cautious about transfering structure?

#### Mario Carneiro (Oct 06 2018 at 05:41):

there are very few cases when it is the right thing to do

#### Johan Commelin (Oct 06 2018 at 05:43):

Hmmm, maybe I'm sad about that. I would have to see how it turns out in practice...

#### Johan Commelin (Oct 06 2018 at 05:44):

I would wish that if someone inadvertently defined xnat, then we could just say: "Aaah, that's equiv to nat. Bam!!! from now one it is a comm_semiring and you can use all theorems about nat for your xnat."

#### Johan Commelin (Oct 06 2018 at 05:45):

Hmm, I want to use more.

#### Johan Commelin (Oct 06 2018 at 05:46):

I want to use that it is not just some random equiv. I want to use that they are structurally equivalent. Is that a thing?

#### Johan Commelin (Oct 06 2018 at 05:46):

They are the same inductive type.

#### Johan Commelin (Oct 06 2018 at 05:46):

But I'm getting distracted, I think.

#### Scott Olson (Oct 06 2018 at 05:47):

So you're interested in duplicated definitions, not e.g. nat vs. binnat?

#### Johan Commelin (Oct 06 2018 at 05:48):

Well, not really. Like I said, I was getting distracted.

#### Johan Commelin (Oct 06 2018 at 05:49):

@Mario Carneiro Ok, I think I know what I want. I want you to remove every mention of rel in your example.

#### Mario Carneiro (Oct 06 2018 at 05:49):

That's the key part that makes transfer work

#### Johan Commelin (Oct 06 2018 at 05:49):

In the proof that addition is commutative, I want to invoke big_transfer

#### Mario Carneiro (Oct 06 2018 at 05:49):

you could remove everything else

#### Johan Commelin (Oct 06 2018 at 05:49):

And it will ask me for a rel

#### Johan Commelin (Oct 06 2018 at 05:50):

And I will answer: use this equiv

#### Mario Carneiro (Oct 06 2018 at 05:50):

but it is a logical relations proof, not a rewrite proof

#### Mario Carneiro (Oct 06 2018 at 05:50):

That's fine, I think

#### Johan Commelin (Oct 06 2018 at 05:50):

And then it says: Good. But then you need to prove these goals: rel_zero, rel_add.

#### Mario Carneiro (Oct 06 2018 at 05:50):

the user layer can handle that

#### Johan Commelin (Oct 06 2018 at 05:50):

And it generates those two goals. And I prove them with tidy.

#### Mario Carneiro (Oct 06 2018 at 05:51):

But the user layer here really needs work

#### Mario Carneiro (Oct 06 2018 at 05:51):

there is nothing, it's not even an interactive tactic

#### Johan Commelin (Oct 06 2018 at 05:51):

And there you have a 4 line tactic proof of commutativity. And all the other stuff above is gone.

Aaah...!

#### Johan Commelin (Oct 06 2018 at 05:51):

When I asked whether there was a tactic for transfer, you said "Yes". And I immediately assumed it was interactive.

Lol

#### Johan Commelin (Oct 06 2018 at 05:52):

For me tactic implies interactive. Silly me.

#### Mario Carneiro (Oct 06 2018 at 05:52):

In the int.basic example, there is a local redefinition of transfer to get the big list of relevant rel theorems for this particular relation

#### Mario Carneiro (Oct 06 2018 at 05:52):

because it is often the case that you will want to use the same relation, or pair of structures, in multiple nearby proofs

#### Mario Carneiro (Oct 06 2018 at 05:53):

in int.basic it is of course used for each of the axioms of the ring structure

#### Johan Commelin (Oct 06 2018 at 05:53):

But, can a tactic automatically infer what it needs to know about a relation, given a certain goal?

#### Mario Carneiro (Oct 06 2018 at 05:53):

no, it doesn't even know the target

#### Mario Carneiro (Oct 06 2018 at 05:54):

For example in my mockup I have a goal on xnat and I said transfer with no info

#### Mario Carneiro (Oct 06 2018 at 05:54):

how would it know that I am transferring to nat instead of something else? and why that relation instead of something else?

#### Johan Commelin (Oct 06 2018 at 05:55):

begin
interactive.transfer my_equiv.to_rel,
{ -- prove rel_zero },
end


#### Johan Commelin (Oct 06 2018 at 05:55):

Would that be possible?

#### Mario Carneiro (Oct 06 2018 at 05:55):

I think we will need to rewrite transfer anyway, I very much doubt the one in core works well enough for our purposes

#### Mario Carneiro (Oct 06 2018 at 05:56):

(at least we should copy it to mathlib and give it a nice front end)

#### Mario Carneiro (Oct 06 2018 at 05:56):

That would be possible, but like I said you want more reuse than that

Cool

#### Mario Carneiro (Oct 06 2018 at 05:57):

that might prove your theorem now, but in the very next theorem you will probably want this relation again and you would have to prove rel_zero again

#### Johan Commelin (Oct 06 2018 at 05:57):

Yes, the VScode "Turn this goal into lemma" keyboard-shortcut will take care of the reuse.

#### Mario Carneiro (Oct 06 2018 at 05:58):

I don't think we have to worry about proof obligations much here

#### Johan Commelin (Oct 06 2018 at 05:58):

It will take everything between a pair of { .. } and turn it into a proof of the subgoal. It will suggest a name for the lemma. And it will apply that lemma where previously the { .. } were written.

#### Johan Commelin (Oct 06 2018 at 05:58):

But I'm getting distracted again :lol:

#### Mario Carneiro (Oct 06 2018 at 05:58):

it will usually already have all the info it needs to prove these obligations

Right.

#### Mario Carneiro (Oct 06 2018 at 05:59):

e.g. if you are proving rel_zero and rel_add that means you have a group iso and so you probably assumed it was a group iso, and so these theorems will already be proven

#### Mario Carneiro (Oct 06 2018 at 06:00):

The main point behind the rel stuff is to build up relations on bigger things, i.e. kernels and short exact sequences

#### Johan Commelin (Oct 06 2018 at 06:00):

But then interactive.transfer needs to remember that the rel came from an equiv. Then it could use type class search to find those results.

#### Johan Commelin (Oct 06 2018 at 06:00):

The main point behind the rel stuff is to build up relations on bigger things, i.e. kernels and short exact sequences

This could all be equiv.to_rel, right?

#### Mario Carneiro (Oct 06 2018 at 06:01):

there is nothing to remember, the relation is explicitly equiv.rel e

#### Mario Carneiro (Oct 06 2018 at 06:01):

not sure what you mean by that last bit

#### Johan Commelin (Oct 06 2018 at 06:01):

But then transfer will have a hard time finding theorems about e, not?

#### Johan Commelin (Oct 06 2018 at 06:02):

I meant that to me equiv seems a lot more natural than rel. And usually we will have an equiv floating around. Even for kernels and s.e.s's

#### Mario Carneiro (Oct 06 2018 at 06:02):

We will have to think about how to discover/supply rel theorems to transfer. Currently it just accepts a big ugly list of names

#### Johan Commelin (Oct 06 2018 at 06:02):

Or some Isom in a category. So we will need Isom.rel

#### Mario Carneiro (Oct 06 2018 at 06:03):

Note that rel is a lot more general

#### Mario Carneiro (Oct 06 2018 at 06:03):

The relation need not be an equiv

#### Johan Commelin (Oct 06 2018 at 06:03):

Yes, I know. I'm not sure if I care

#### Mario Carneiro (Oct 06 2018 at 06:03):

Almost all of these theorems hold with much weaker assumptions

#### Johan Commelin (Oct 06 2018 at 06:04):

I suggest that the interactive transfer generates a list of goals.
Then we can prove by transfer my_rel; tidy.

#### Mario Carneiro (Oct 06 2018 at 06:05):

I think it will discharge all its goals

#### Mario Carneiro (Oct 06 2018 at 06:05):

except the main goal

#### Mario Carneiro (Oct 06 2018 at 06:06):

I wonder whether it should deliver its iff statement instead of changing the goal... that way it can apply on hyps too

#### Andrew Ashworth (Oct 06 2018 at 06:44):

I was reading https://www21.in.tum.de/~kuncar/documents/huffman-kuncar-cpp2013.pdf again and I saw that Isabelle's transfer can do The transfer proof method can replace a universal with an equivalent bounded quantifier: e.g., (∀n::nat. n < n + 1) is transferred to (∀x::int ∈ {0..}. x < x + 1).

#### Andrew Ashworth (Oct 06 2018 at 06:45):

This sounds suspiciously like the number casting tactic mentioned in this chat earlier

#### Mario Carneiro (Oct 06 2018 at 06:46):

Of course our transfer is based on isabelle's transfer

#### Mario Carneiro (Oct 06 2018 at 06:46):

The number casting tactic uses rewrites instead of logical relations

#### Mario Carneiro (Oct 06 2018 at 06:46):

Maybe it would be better to use transfer for this ...?

#### Andrew Ashworth (Oct 06 2018 at 06:49):

I think transfer in Lean will want this anyway at some point, so the same machinery may as well do double duty...? I'm unsure of what the implications are

#### Andrew Ashworth (Oct 06 2018 at 06:50):

I do like that relations are stronger than rewrites

#### Andrew Ashworth (Oct 06 2018 at 06:50):

I'm reading some of the follow-on papers and there are some tactics that automatically generate refinement theorems for converting algorithms over finsets to concrete algorithms over data structures like rb-trees etc

#### Andrew Ashworth (Oct 06 2018 at 06:50):

using transfer or derivatives of

#### Andrew Ashworth (Oct 06 2018 at 06:53):

it appears someone in Coq wanted to port transfer too: https://arxiv.org/pdf/1505.05028.pdf

#### Andrew Ashworth (Oct 06 2018 at 06:53):

example 2 in the coq paper is exactly xnat and nat...

#### Johan Commelin (Oct 06 2018 at 06:54):

The number casting tactic would be transferring data as well, right? Not only proofs...

#### Kevin Buzzard (Oct 06 2018 at 09:56):

They are the same inductive type.

I remember when I used to go on about this sort of thing. For computer scientists there is a very precise notion of the same and it's asking a lot more than what we have -- it means they are literally the same object -- structurally equal. Two inductive types with canonically isomorphic definitions are just canonically isomorphic, which is a much weaker notion. For each notion of "the same" (these groups are "the same", these topological spaces are "the same") we have to formalise our notion of sameness (e.g. with an equiv or a beefed-up equiv structure with extra proof such as "...and the maps are also group homomorphisms") and then understand exactly which constructions descend to equivalence classes. "The same" is a fluid concept in mathematics, it is really a bunch of equivalence relations. I discovered in the schemes project that it was very costly to think of the open set U and the open set id'' U (the image of U under the identity map) as "the same", because they really were not the same. They were "equal because of a theorem" and this is a much weaker statement. Stuff like congr_arg and congr_fun work because eq (which is a random inductive type remember, not at all related to whether things are the same) has a good recursor.

#### Kevin Buzzard (Oct 06 2018 at 09:58):

There was a thread a while ago now, possibly on gitter, where I got extremely frustrated about how U and id'' U could even possibly not be the same and it took a lot of talking from Mario and Kenny to peel me off the ceiling. Once I realised that the correct map from $\mathcal{F}(U)$ to $\mathcal{F}(id(U))$ was not id but res all my problems went away.

#### Kevin Buzzard (Oct 06 2018 at 10:00):

$U$ and $id(U)$ are canonically isomorphic in the computer-scientist's version of the category of open sets on a topological space, but the moment you start treating them as the same you get a whole bunch of errors about motives not being type correct which Reid did show me how to fight against if necessary. However these techniques turned out not to be needed once I understood that the canonical isomorphisms were not id but res`.

#### Kevin Buzzard (Oct 06 2018 at 10:01):

In the mathematician's model of this category, these sets are the same.

Last updated: May 08 2021 at 18:17 UTC