how to use transfer

Stream: general

[Mario Carneiro]

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 _

instance : has_add xnat :=
⟨λ 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],
  simp [add_comm]
end

[Scott Olson]

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]

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

[Mario Carneiro]

of course, that's the idea

[Scott Olson]

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]

Should we take it to a different thread?

[Johan Commelin]

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

instance : has_add xnat :=
⟨λ 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],
  simp [add_comm]
end

[Johan Commelin]

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

[Johan Commelin]

And then I have several conflicting thoughts...

[Johan Commelin]

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

[Johan Commelin]

All the structure and proofs should be transferable using automation.

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

..oh wait, that's group_iso etc

[Johan Commelin]

Exactly

[Mario Carneiro]

so problem solved?

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

oh yes, that's a one liner

[Mario Carneiro]

rel for add is literally map_add with some dressing

[Johan Commelin]

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

[Johan Commelin]

Or something like that.

[Mario Carneiro]

we could put that in the theorems for group_iso

[Mario Carneiro]

But I am wary about constructing structure using transfer

[Mario Carneiro]

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]

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],
  simp [add_comm]
end

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

@Mario Carneiro Why are you cautious about transfering structure?

[Mario Carneiro]

because it leads to bad definitional reduction

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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]

Hmm, I want to use more.

[Johan Commelin]

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]

They are the same inductive type.

[Johan Commelin]

But I'm getting distracted, I think.

[Scott Olson]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

That's the key part that makes transfer work

[Johan Commelin]

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

[Mario Carneiro]

you could remove everything else

[Johan Commelin]

And it will ask me for a rel

[Johan Commelin]

And I will answer: use this equiv

[Mario Carneiro]

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

[Mario Carneiro]

That's fine, I think

[Johan Commelin]

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

[Mario Carneiro]

the user layer can handle that

[Johan Commelin]

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

[Mario Carneiro]

But the user layer here really needs work

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

Aaah...!

[Johan Commelin]

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

[Johan Commelin]

Lol

[Johan Commelin]

For me tactic implies interactive. Silly me.

[Mario Carneiro]

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]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

no, it doesn't even know the target

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

Would that be possible?

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

Cool

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

But I'm getting distracted again :lol:

[Mario Carneiro]

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

[Johan Commelin]

Right.

[Mario Carneiro]

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]

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

[Johan Commelin]

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]

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]

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

[Mario Carneiro]

not sure what you mean by that last bit

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

[Mario Carneiro]

Note that rel is a lot more general

[Mario Carneiro]

The relation need not be an equiv

[Johan Commelin]

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

[Mario Carneiro]

Almost all of these theorems hold with much weaker assumptions

[Johan Commelin]

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

[Mario Carneiro]

I think it will discharge all its goals

[Mario Carneiro]

except the main goal

[Mario Carneiro]

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

[Andrew Ashworth]

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]

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

[Mario Carneiro]

Of course our transfer is based on isabelle's transfer

[Mario Carneiro]

The number casting tactic uses rewrites instead of logical relations

[Mario Carneiro]

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

[Andrew Ashworth]

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]

I do like that relations are stronger than rewrites

[Andrew Ashworth]

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]

using transfer or derivatives of

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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

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