transitive closure

Stream: new members

[Damiano Testa]

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?

[Reid Barton]

docs#eqv_gen

[Damiano Testa]

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

[Damiano Testa]

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]

I'm sure the recursor will be there somewhere!

[Mario Carneiro]

you can use the builtin one too

[Mario Carneiro]

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

[Reid Barton]

Oops yes, I applied the mathematician's filter again

[Damiano Testa]

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?

[Mario Carneiro]

tactic#induction

[Damiano Testa]

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]

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

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]

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

[Damiano Testa]

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

[Damiano Testa]

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]

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

[Kyle Miller]

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]

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

[Damiano Testa]

Hmm, I still get an error...

[Mario Carneiro]

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]

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

[Kyle Miller]

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

[Mario Carneiro]

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]

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]

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]

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

[Kyle Miller]

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

[Mario Carneiro]

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

[Damiano Testa]

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]

rfl

[Yakov Pechersky]

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

[Mario Carneiro]

oh wait, what you said is false

[Mario Carneiro]

oh wait, what I said is false

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Damiano Testa]

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

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]

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

[Mario Carneiro]

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]

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]

@[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]

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

[Mario Carneiro]

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

[Mario Carneiro]

there are lots of ways to write proofs in lean

[Mario Carneiro]

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]

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]

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

[Damiano Testa]

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]

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

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

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]

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]

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]

Great, I understand now! Thanks a lot!

[Kyle Miller]

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]

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]

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

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]

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

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

If you want more details, watch the videos by Rob

[Johan Commelin]

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