Zulip Chat Archive

Stream: general

Topic: how to use transfer


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

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

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

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:28):

of course, that's the idea

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:28):

Should we take it to a different thread?

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

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

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:32):

And then I have several conflicting thoughts...

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:33):

All the structure and proofs should be transferable using automation.

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:34):

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:35):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:35):

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:35):

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

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:36):

..oh wait, that's group_iso etc

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:36):

Exactly

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:36):

so problem solved?

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:36):

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:37):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:37):

oh yes, that's a one liner

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:37):

rel for add is literally map_add with some dressing

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:37):

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:37):

Or something like that.

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:38):

we could put that in the theorems for group_iso

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:38):

But I am wary about constructing structure using transfer

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

view this post on Zulip 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],
  simp [add_comm]
end

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:40):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:40):

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:41):

@Mario Carneiro Why are you cautious about transfering structure?

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:41):

because it leads to bad definitional reduction

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:41):

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

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

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:45):

Hmm, I want to use more.

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:46):

They are the same inductive type.

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:46):

But I'm getting distracted, I think.

view this post on Zulip Scott Olson (Oct 06 2018 at 05:47):

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:48):

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

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:49):

That's the key part that makes transfer work

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:49):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:49):

you could remove everything else

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:49):

And it will ask me for a rel

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:50):

And I will answer: use this equiv

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:50):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:50):

That's fine, I think

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:50):

the user layer can handle that

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:50):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:51):

But the user layer here really needs work

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:51):

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

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:51):

Aaah...!

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:51):

Lol

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:52):

For me tactic implies interactive. Silly me.

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

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

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

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:53):

no, it doesn't even know the target

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

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:55):

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:55):

Would that be possible?

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:56):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:56):

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:56):

Cool

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:57):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:58):

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

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:58):

But I'm getting distracted again :lol:

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:58):

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:59):

Right.

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

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

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

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 06:01):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 06:01):

not sure what you mean by that last bit

view this post on Zulip Johan Commelin (Oct 06 2018 at 06:01):

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

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

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 06:02):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 06:03):

Note that rel is a lot more general

view this post on Zulip Mario Carneiro (Oct 06 2018 at 06:03):

The relation need not be an equiv

view this post on Zulip Johan Commelin (Oct 06 2018 at 06:03):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 06:03):

Almost all of these theorems hold with much weaker assumptions

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 06:05):

I think it will discharge all its goals

view this post on Zulip Mario Carneiro (Oct 06 2018 at 06:05):

except the main goal

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

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

view this post on Zulip Andrew Ashworth (Oct 06 2018 at 06:45):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 06:46):

Of course our transfer is based on isabelle's transfer

view this post on Zulip Mario Carneiro (Oct 06 2018 at 06:46):

The number casting tactic uses rewrites instead of logical relations

view this post on Zulip Mario Carneiro (Oct 06 2018 at 06:46):

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

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

view this post on Zulip Andrew Ashworth (Oct 06 2018 at 06:50):

I do like that relations are stronger than rewrites

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

view this post on Zulip Andrew Ashworth (Oct 06 2018 at 06:50):

using transfer or derivatives of

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

view this post on Zulip Andrew Ashworth (Oct 06 2018 at 06:53):

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

view this post on Zulip Johan Commelin (Oct 06 2018 at 06:54):

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

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

view this post on Zulip 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 F(U)\mathcal{F}(U) to F(id(U))\mathcal{F}(id(U)) was not id but res all my problems went away.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 10:00):

UU and id(U)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.

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