Zulip Chat Archive

Stream: new members

Topic: transitive closure


view this post on Zulip Damiano Testa (Aug 18 2020 at 13:51):

If I start with a relation on a type T, is there a way way to produce another relation that is the transitive closure of T?

view this post on Zulip Reid Barton (Aug 18 2020 at 13:55):

docs#eqv_gen

view this post on Zulip Damiano Testa (Aug 18 2020 at 13:56):

Thanks! I will try to play with it, in order to understand how it works!

view this post on Zulip Damiano Testa (Aug 18 2020 at 15:55):

Thanks a lot: this was exactly what I needed! Now I have a follow up question: can I use this to prove inductively properties of the transitive closure?

view this post on Zulip Kevin Buzzard (Aug 18 2020 at 16:08):

I'm sure the recursor will be there somewhere!

view this post on Zulip Mario Carneiro (Aug 18 2020 at 16:16):

you can use the builtin one too

view this post on Zulip Mario Carneiro (Aug 18 2020 at 16:17):

eqv_gen is the reflexive symmetric transitive closure of a relation. You want docs#relation.trans_gen

view this post on Zulip Reid Barton (Aug 18 2020 at 16:21):

Oops yes, I applied the mathematician's filter again

view this post on Zulip Damiano Testa (Aug 18 2020 at 16:32):

I had figured out the reflexive/symmetry/transitive issue! I am still not able to find the induction command: should it be something like

induction something with something?

view this post on Zulip Mario Carneiro (Aug 18 2020 at 16:33):

tactic#induction

view this post on Zulip Damiano Testa (Aug 18 2020 at 17:33):

Thank you for your help, but I am really struggling with this. I have produced an easy example where I cannot use induction on the transitive closure to prove the goal. What should I apply induction to?

import tactic

inductive zo : Type
| z : zo
| o : zo

def myzo : zo  zo  Prop :=
begin
    intros w1 w2,
        cases w1,
        cases w2,
            exact false,
            exact true,
        cases w2,
            exact true,
            exact false,
end

def mytot := relation.trans_gen myzo

lemma isrefl : mytot zo.o zo.o :=
begin
    fconstructor,
    induction (relation.trans_gen zo.o),
end

(I have produced a shorter example.)

view this post on Zulip Damiano Testa (Aug 18 2020 at 17:34):

(Also, any suggestion on how to make the previous example less bulky would definitely by welcome! I know this is a very bad example, but I have very little knowledge of how to use Lean correctly...)

view this post on Zulip Yakov Pechersky (Aug 18 2020 at 17:51):

Definitions shouldn't be made using tactics, so you could do something like this:

def myzo : zo -> zo -> Prop
| z o := true
| o z := true
| _ _ := false

view this post on Zulip Damiano Testa (Aug 18 2020 at 17:52):

Ok, I did not know this. I also did not know how you could write a function without using a tactic...

view this post on Zulip Damiano Testa (Aug 18 2020 at 17:53):

(I assume that the underscores _ _ mean that anything not already defines is false, right?)

view this post on Zulip Damiano Testa (Aug 18 2020 at 17:56):

If I use your code, I get an error on the third colon:

| o z := true.

Lean says

equation compiler error, equation #2 has not been used in the compilation (possible solution: delete equation)

view this post on Zulip Yakov Pechersky (Aug 18 2020 at 17:58):

You might need a z _ := false prior to it

view this post on Zulip Kyle Miller (Aug 18 2020 at 17:58):

Damiano Testa said:

(I assume that the underscores _ _ mean that anything not already defines is false, right?)

Yeah, for pattern matching, _ means "match anything", and pattern expressions effectively are tried one at a time, so | _ _ := ... would be a catch-all at the end. (The _ for arguments to functions is sort of conceptually related in that you are giving a pattern for the Lean elaborator to fill in.)

view this post on Zulip Damiano Testa (Aug 18 2020 at 17:59):

Ah, I see! That explains why the z _ := false would fix it! Thanks!!

view this post on Zulip Damiano Testa (Aug 18 2020 at 17:59):

Hmm, I still get an error...

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:01):

You certainly don't need tactics to write everything. You can do entire proofs without them, and it is recommended to avoid tactics while writing definitions

view this post on Zulip Kevin Buzzard (Aug 18 2020 at 18:01):

your z and o are variables because you're not in the namespace.

view this post on Zulip Kyle Miller (Aug 18 2020 at 18:02):

You can use open zo to use z and o, or explicitly refer to zo.z and zo.o.

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:02):

the problem with Yakov's code is that you did not open zo first, so z and o are treated as variables in the first pattern, making the others redundant

view this post on Zulip Kevin Buzzard (Aug 18 2020 at 18:02):

import tactic

inductive zo : Type
| z : zo
| o : zo

namespace zo

def myzo : zo -> zo -> Prop
| z o := true
| o z := true
| _ _ := false


example : myzo z o = true := rfl
example : myzo o z = true := rfl
example : myzo z z = false := rfl
example : myzo o o = false := rfl

end zo

view this post on Zulip Damiano Testa (Aug 18 2020 at 18:03):

Great: this taught me something about definitions and the fact that you do not need tactics (although I do not know how to code without using tactics...)

view this post on Zulip Kevin Buzzard (Aug 18 2020 at 18:03):

You write definitions in term mode and prove theorems in tactic mode.

view this post on Zulip Kyle Miller (Aug 18 2020 at 18:04):

You can inspect the term-mode proofs that tactic mode generates by using the #print command

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:04):

However I think a better definition for this function is def myzo (a b : zo) := a ≠ b

view this post on Zulip Damiano Testa (Aug 18 2020 at 18:04):

Is there a way now to get Lean to realize that mytot z z = true, using induction and the fact that mytot z o = true and mytot o z = true?

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:04):

rfl

view this post on Zulip Yakov Pechersky (Aug 18 2020 at 18:05):

Sorry for the incomplete suggestion, difficult to type out all the precise statements on a phone keyboard...

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:05):

oh wait, what you said is false

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:05):

oh wait, what I said is false

view this post on Zulip Damiano Testa (Aug 18 2020 at 18:05):

Yakov Pechersky said:

Sorry for the incomplete suggestion, difficult to type out all the precise statements on a phone keyboard...

No problem! To be fair, I think that I learned more from understanding where the mistake was, than by directly seeing correct code!

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:06):

you can prove mytot z z by applying the constructor for trans_gen

view this post on Zulip Damiano Testa (Aug 18 2020 at 18:06):

I imagine that "applying the constructor" has a meaning, but it escapes me...

view this post on Zulip Damiano Testa (Aug 18 2020 at 18:08):

(I am really sorry: I can see that the questions that I am asking are completely basic, but I am having a hard time getting my head around to how to tell Lean to do simple things...)

view this post on Zulip Kyle Miller (Aug 18 2020 at 18:09):

For this definition,

def mytot := relation.trans_gen myzo

it turns out relation.trans_gen is an inductive type. Try following it's definition into the mathlib source code. You'll see it has two constructors.

view this post on Zulip Kyle Miller (Aug 18 2020 at 18:10):

(I only know the emacs command to follow the definition, M-.)

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:11):

import tactic

inductive zo : Type
| z : zo
| o : zo
open zo

def myzo : zo -> zo -> Prop
| z o := true
| o z := true
| _ _ := false

def mytot := relation.trans_gen myzo

lemma isrefl : mytot o o :=
begin
  have hzo : myzo z o := trivial,
  have hoz : myzo o z := trivial,
  have toz : mytot o z := relation.trans_gen.single hoz,
  exact relation.trans_gen.tail toz hzo,
end

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:13):

lemma isrefl : mytot o o :=
begin
  apply relation.trans_gen.tail,
  { apply relation.trans_gen.single,
    show myzo o z, trivial },
  { show myzo z o, trivial },
end

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:15):

@[trans] theorem mytot.trans {a b c} : mytot a b  mytot b c  mytot a c :=
relation.trans_gen.trans

theorem mytot.single {a b} : myzo a b  mytot a b :=
relation.trans_gen.single

lemma isrefl : mytot o o :=
begin
  transitivity z,
  exact mytot.single trivial,
  exact mytot.single trivial,
end

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:16):

lemma isrefl : mytot o o := by transitivity z; exact mytot.single trivial

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:18):

lemma isrefl : mytot o o :=
relation.trans_gen.tail (relation.trans_gen.single ⟨⟩ : mytot o z) ⟨⟩

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:18):

there are lots of ways to write proofs in lean

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:20):

You should try #tpil to get a feel for the basics of constructing proof terms, dealing with inductive types and other such foundational (not basic!) stuff

view this post on Zulip Kyle Miller (Aug 18 2020 at 18:21):

Yet another variation:

lemma isrefl : mytot o o :=
begin
  dunfold mytot,
  transitivity z;
    exact relation.trans_gen.single trivial,
end

(undeleted; actually is different from Mario's)

view this post on Zulip Mario Carneiro (Aug 18 2020 at 18:24):

actually yours used transitivity of trans_gen while mine defined a trans lemma for mytot specifically

view this post on Zulip Damiano Testa (Aug 18 2020 at 18:47):

Dear All, thank you very much for your insights! I will take a very close look at what you sent, process it and absorb it, and I will see if I have further questions! I am really really grateful!

view this post on Zulip Damiano Testa (Aug 18 2020 at 21:05):

@Mario Carneiro your multiple proofs of transitivity are incredibly useful to me! I only started looking seriously at Lean since less than two weeks and I have no programming experience. Thus, I encounter lots of traps everywhere!

view this post on Zulip Damiano Testa (Aug 19 2020 at 06:24):

@Mario Carneiro Now that I had a chance to look at your proofs carefully, I have a follow up question. What is the difference between a comma and a semicolon, for instance in

lemma isrefl : mytot o o := by transitivity z; exact mytot.single trivial?

Moreover, why after transitivity z do you only need to prove mytot o z and not also mytot z o?

I am sorry if these are more silly questions! Thank you very much for your time!

view this post on Zulip Kyle Miller (Aug 19 2020 at 06:24):

Semicolon means that the following tactic applies to all the subgoals generated by the previous one. The transitivity tactic generates two subgoals.

Try changing the by into a begin ... end block and replace the semicolon with a comma.

view this post on Zulip Damiano Testa (Aug 19 2020 at 06:25):

Ah, is this the reason why Lean then only prints out one goal? Because all goals should be solved by the same string of commands?

view this post on Zulip Damiano Testa (Aug 19 2020 at 06:26):

Kyle Miller said:

Try changing the by into a begin ... end block and replace the semicolon with a comma.

I am going to do that now!

view this post on Zulip Damiano Testa (Aug 19 2020 at 06:27):

Great, I understand now! Thanks a lot!

view this post on Zulip Kyle Miller (Aug 19 2020 at 06:28):

This is also using a syntax trick: the ; is an operator that composes tactics. If it had been a comma, the tactics after by would need to be enclosed in curly braces since commas have many meanings in Lean. You can enclose the tactic proof in (unnecessary) curly braces:

lemma isrefl : mytot o o := by { transitivity z; exact mytot.single trivial }

view this post on Zulip Damiano Testa (Aug 19 2020 at 06:31):

Ok, it is still a bit hazy, but now it is starting to make more sense! There is a lot of work that Lean does trying to figure out what it is that you are doing. This is sometimes confusing to me, as I am never sure about what Lean is going to ask me to prove next. But all these conversations are really really helping me! Thank you so much!

view this post on Zulip Scott Morrison (Aug 19 2020 at 06:45):

@Kyle Miller, the style guide in fact suggests not using ; unless you are actually creating multiple goals. It can sometimes save some characters, but is also creates an extra hurdle to a human parsing your proof, who now has to work if there really are multiples goals or not.

view this post on Zulip Kyle Miller (Aug 19 2020 at 06:48):

That's a good point, but that was just a counterfactual about syntax, since it might be unclear why the curly braces are omitted -- I prefer using curly braces regardless. (The ; is needed there.)

view this post on Zulip Kyle Miller (Aug 19 2020 at 07:00):

@Damiano Testa This is my basic understanding of tactics, in case it helps:

When you write a Lean expression, there are a few kinds of holes you can leave in your code to signal that Lean should, in some capacity, help fill in the details for you. One example is a tactic expression, with the notation begin tactics-separated-by-commas end or by single-tactic. Lean will defer dealing with these for as long as possible. At some point, once it figures out the type that the tactic expression should have (for example, it might be inferred from the lemma statement), it enters tactic mode. Tactic mode is a special imperative programming language for constructing proofs. Each tactic in the tactic expression is executed sequentially, and the effect of each is to somehow modify the hypotheses and goals while, in the background, constructing the thing that should eventually replace the tactic expression itself.

It turns out tactics are themselves Lean objects (though in the meta level), and you can compose tactics in different ways to produce new tactics. We've seen ;, which takes two tactics and produces a tactic that runs the second tactic on each goal produced by the first. There's also { tactic1, tactic2, ..., tacticn } which evaluates tactics sequentially, failing when the first one fails. There's try tactic to attempt a tactic, but not itself fail if the tactic fails. There's tactic1 <|> tactic2 to try the first tactic, and if it fails continue with the second. And so on. (These can be helpful for writing short proofs that involve lots of case analysis.)

So, when you are using tactic mode to prove a lemma, you're writing a program that writes a program that represents a proof!

view this post on Zulip Damiano Testa (Aug 19 2020 at 07:16):

@Kyle Miller Your description polishes up and clarifies lots of misty concepts that were floating around in my mind! Also, I did not know that you could compose tactics with the syntaxes that you described! Thanks a lot!

view this post on Zulip Johan Commelin (Aug 19 2020 at 07:18):

If you want more details, watch the videos by Rob

view this post on Zulip Johan Commelin (Aug 19 2020 at 07:19):

https://www.youtube.com/watch?v=o6oUjcE6Nz4&list=PLlF-CfQhukNnq2kDCw2P_vI5AfXN7egP2


Last updated: May 10 2021 at 18:22 UTC