## Stream: new members

### Topic: transitive closure

#### 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?

docs#eqv_gen

#### Damiano Testa (Aug 18 2020 at 13:56):

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

#### 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?

#### Kevin Buzzard (Aug 18 2020 at 16:08):

I'm sure the recursor will be there somewhere!

#### Mario Carneiro (Aug 18 2020 at 16:16):

you can use the builtin one too

#### 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

#### Reid Barton (Aug 18 2020 at 16:21):

Oops yes, I applied the mathematician's filter again

#### 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?

tactic#induction

#### 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.)

#### 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...)

#### 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


#### 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...

#### Damiano Testa (Aug 18 2020 at 17:53):

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

#### 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)

#### Yakov Pechersky (Aug 18 2020 at 17:58):

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

#### 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.)

#### Damiano Testa (Aug 18 2020 at 17:59):

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

#### Damiano Testa (Aug 18 2020 at 17:59):

Hmm, I still get an error...

#### 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

#### Kevin Buzzard (Aug 18 2020 at 18:01):

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

#### 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.

#### 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

#### 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


#### 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...)

#### Kevin Buzzard (Aug 18 2020 at 18:03):

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

#### Kyle Miller (Aug 18 2020 at 18:04):

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

#### 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

#### 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?

#### Mario Carneiro (Aug 18 2020 at 18:04):

rfl

#### 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...

#### Mario Carneiro (Aug 18 2020 at 18:05):

oh wait, what you said is false

#### Mario Carneiro (Aug 18 2020 at 18:05):

oh wait, what I said is false

#### 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!

#### Mario Carneiro (Aug 18 2020 at 18:06):

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

#### Damiano Testa (Aug 18 2020 at 18:06):

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

#### 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...)

#### 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.

#### Kyle Miller (Aug 18 2020 at 18:10):

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

#### 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


#### 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


#### 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


#### Mario Carneiro (Aug 18 2020 at 18:16):

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


#### Mario Carneiro (Aug 18 2020 at 18:18):

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


#### Mario Carneiro (Aug 18 2020 at 18:18):

there are lots of ways to write proofs in lean

#### 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

#### 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)

#### Mario Carneiro (Aug 18 2020 at 18:24):

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

#### 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!

#### 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!

#### 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!

#### 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.

#### 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?

#### 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!

#### Damiano Testa (Aug 19 2020 at 06:27):

Great, I understand now! Thanks a lot!

#### 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 }


#### 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!

#### 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.

#### 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.)

#### 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!

#### 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!

#### Johan Commelin (Aug 19 2020 at 07:18):

If you want more details, watch the videos by Rob

#### 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