specific qs on intro exercises

Stream: new members

[Ron Stampler]

I think this is what it's telling me to do.

[Ron Stampler]

Hi everyone! I don't know if I'll be here much but I just started out on the intro exercises.

[Ron Stampler]

in multiplication world, the text casually introduces "repeat" and "rwa" but doesn't define them, and they aren't listed in the existing "tactics". Repeat seems obvious, but what does rwa do?

[Mario Carneiro]

rewrite then assumption

[Mario Carneiro]

that is, it does the same as rw [...] but tries to match the result of the goal after rewriting to something in the context

[Ron Stampler]

oh, so like "rewrite then check if i'm done"

[Ron Stampler]

Cheers Mario. Also, when using rw, is there a way to specify the operand? Like, if I do rw \l one_mul d, it changes all instances of d to 1 * d, which isn't useful when I was gonna use that to factorise into a multiplication. Maybe I want just, say, the 4th instance of d to be rw'd.

[Ruben Van de Velde]

nth_rewrite: https://leanprover-community.github.io/mathlib_docs/tactics.html#nth_rewrite%20/%20nth_rewrite_lhs%20/%20nth_rewrite_rhs

[Johan Commelin]

I'm not sure nth_rewrite works in the natural number game. It uses a modified tactic monad

[Ron Stampler]

can confirm it doesn't

[Mario Carneiro]

you can also use conv, although that might not work for the same reason

[Mario Carneiro]

but surprisingly often you can get away with not doing this by rewriting the other side of the equation or something along those lines

[Ron Stampler]

yeah i got round it last time by multiplying out instead of factoring

[Bryan Gin-ge Chen]

Does the occs option work? For examples, see e.g. this thread.

[Ruben Van de Velde]

unknown identifier 'occurences.pos'

[Mario Carneiro]

it's probably in a namespace

[Ruben Van de Velde]

But you can certainly avoid doing this in NNG

[Ruben Van de Velde]

If only because people finish it :)

[Mario Carneiro]

occurrences.pos is not in a namespace...

[Ron Stampler]

same problem again, I have (after some manipulation):

case mynat.succ
a t d : mynat,
hd : (a + d) * t = a * t + d * t
⊢ (d + a) * t + t = a * t + (d + 1) * t

and I can't insert the inductive hypothesis because add_comm goes for the outer addition instead of the ( d + a ) that i want it to replace.

[Mario Carneiro]

rw [add_comm d a, hd]

[Ron Stampler]

can you walk me through the syntax there v briefly?

[Mario Carneiro]

rewrite with add_comm d a, then rewrite hd

[Mario Carneiro]

maybe NNG uses rw add_comm d a, rw hd

[Ron Stampler]

I'm with ya, cheers

[Mario Carneiro]

the point being that you can substitute into a lemma before the actual rewrite to limit the matching occurrences

[Ron Stampler]

in NNG, if I finish by typing "simp" because it's equal up to addition order, it doesn't close out the exercise :-S

[Mario Carneiro]

at what goal?

[Mario Carneiro]

you might need simp [add_comm] if it's not a simp lemma

[Ron Stampler]

mysterious

[Ron Stampler]

just finishing up multiplication world

[Mario Carneiro]

simp only uses the lemmas that are given to it, plus lemmas that are marked as simp lemmas. In this case add_comm is not a simp lemma so you have to provide it explicitly if you want it to be used

[Ron Stampler]

ok that makes some sense, cheers for the help!

[Ron Stampler]

oof done this twice now, repeat { blah } causes infinite loop and lean locks up - any way to help it unstuck?

[Mario Carneiro]

NNG doesn't handle lean timeouts very well, I think you have to reload the page

[Mario Carneiro]

repeat { tac } repeats tac until it fails, so if you use it with something that always succeeds (like repeat { rw add_comm } which will rewrite a + b to b + a and back) then it will just run forever

[Mario Carneiro]

there is a variation on repeat that only runs a fixed number of times, iterate n

[Ron Stampler]

so if you have a type (uppercaseletter), is intro (lowercaseletter) always assumed to be of the type matching the letter?

[Johan Commelin]

@Ron Stampler Nope, there is no relation at all

[Johan Commelin]

You can have types whose name is lowercase and terms whose name is uppercase

[Johan Commelin]

Nothing needs to match

[Johan Commelin]

But of course it can be helpful to use such conventions

[Ron Stampler]

not even the letters? like type U, intro blep is fine?

[Johan Commelin]

People will be confused if we a : B and x : C and b : X and c : A

[Johan Commelin]

@Ron Stampler If you want you can have qUuX : fO___baR

[Ron Stampler]

aye and confusion isn't our game - but I'm trying to get my head around function world. you type intro this and exact f(this) and it's like... how did it know that this : T, or whatever

[Johan Commelin]

You can use a number of unicode symbols even

[Johan Commelin]

Ron Stampler said:

and it's like... how did it know that this : T, or whatever

keyword: type inference

[Johan Commelin]

Lean remembers a lot of things behind the scenes

[Ron Stampler]

but if you don't give it a type or anything, it's just like shrug that's fine

[Bryan Gin-ge Chen]

The types are always there, but they might not be displayed.

[Ron Stampler]

and if there's a number of possibilities, it doesn't worry about it until it can infer it, or?

[Ron Stampler]

"Whatever the sets P and Q and R are, we make an element of Hom(Hom(P,Hom(Q,R)),Hom(Hom(P,Q),Hom(P,R)))" ... why do I have to perform mental acrobatics? :-S

[Mario Carneiro]

Ron Stampler said:

aye and confusion isn't our game - but I'm trying to get my head around function world. you type intro this and exact f(this) and it's like... how did it know that this : T, or whatever

When you use intro this, the goal will be \forall x: T, p x or something like that, and so lean knows the type that this is supposed to have, it's the type in the forall

[Mario Carneiro]

That also applies if the goal is an implication; if the goal is T -> U and you intro x then x will have type T

[Ron Stampler]

thanks for the explanation, that makes it clear

[Ron Stampler]

I'm a bit baffled that, when learning what amounts to a new language, someone thought one of the intro exercises should be a twisted sentence like this one...

[Mario Carneiro]

There aren't really a "number of possibilities" except in very rare cases. Usually it's a sort of continuous family of possibilities represented by a type with a metavariable in it (which looks like ?m_1 in printing)

[Mario Carneiro]

What's the exercise?

[Ron Stampler]

the one I just copied and pasted, it's function world 6

[Mario Carneiro]

well if you don't worry about how type inference works and just use it it's just type tetris

[Mario Carneiro]

there's really only one thing to do at every stage

[Bryan Gin-ge Chen]

My vague memory was that the "Hom(Hom(..." sentence was a joke...

[Ron Stampler]

still trying to get head round the notation, exercise is like "here's a tongue twister in it"... I can see why someone already versed in the language might think that funny...

[Mario Carneiro]

that theorem is certainly a lot easier to read with arrows instead of Hom

[Ron Stampler]

I guess it illustrates that lean will be more clear than the person writing the exercise, but I think that exercise a poor choice for a language learner.

[Ron Stampler]

or maybe I'm missing the point altogether

[Mario Carneiro]

The point is to prove (A -> B -> C) -> ((A -> B) -> (A -> C)) by intro and apply

[Mario Carneiro]

I'm not sure whether you are confused about how to do this

[Ron Stampler]

no i did the exercise, forgive me, I whinge too much

[Mario Carneiro]

Do you think that the task you performed was too difficult to figure out? Proving that is all that is being asked. The hom stuff is just trolling

[Mario Carneiro]

NNG will teach you how to get a sort of operational understanding of lean but it doesn't dwell on the fundamentals very much, so all the tactics and stuff are just pulled out of a hat

[Mario Carneiro]

if you want to learn about dependent type theory and foundations, #tpil is a better choice

[Mario Carneiro]

specifically chapter 2

[Ron Stampler]

what is the etymology behind the term "exact"?

[Ron Stampler]

in NNG, level 4 of advanced proposition world, shouldn't the statement of iff_trans be (P ↔ Q)∧(Q ↔ R) → (P ↔ R)? The statement there might be logically equivalent, but...

[Yakov Pechersky]

The fact that they're "logically equivalent" is a lemma to be proved (maybe already proved in NNG by that point?).

[Yakov Pechersky]

But I think iff_trans is easier to use in the (P ↔ Q)→(Q ↔ R) → (P ↔ R) case in Lean because:

[Yakov Pechersky]

If I have h1 : (P ↔ Q) and h2 : (Q ↔ R) then h1.trans h2 = (P ↔ R)

[Yakov Pechersky]

If you have a lemma iff.trans : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := sorry

[Yakov Pechersky]

otherwise, you'd have to construct the and term

[Ron Stampler]

yeah that's good justification for the definition, but the statement presupposes the result, as it were

[Ron Stampler]

as a point of order, you're right : it was the previous exercise.

[Yakov Pechersky]

You're just so deeply familiar with logic and the laws that things you've internalized seem to obviously true

[Ron Stampler]

you write inline code in here... is that in the latex markup?

[Yakov Pechersky]

Just using #backticks

[Yakov Pechersky]

In fact, Lean knows the following about propositions:

example : (↔) = (=) :=
by { ext, simp }

[Yakov Pechersky]

That is, ↔ can substituted precisely for =! So then, of course iff.trans is true, because eq.trans is true; and eq.trans is true because equalities allow for substitution, which is axiomatic by how they're defined.

[Yakov Pechersky]

Now, if you check the proof for

example : (↔) = (=) :=
by { ext, simp }

you'll see it doesn't actually use eq.trans, but still uses equality substitution in one place, and another axiom of propositional extensionality in another place.

[Mario Carneiro]

By the way, this is basically the logical version of currying

[Mario Carneiro]

it's more convenient to work with iterated implication in functional languages than tuples

[PsyMar#2210]

I've been going crazy for hours upon hours with Advanced Multiplication level 4, help! I got as far as
hd : a * succ b = a * d → succ b = d
but the goal is this with succ d instead of d.

[PsyMar#2210]

I think I've spent longer on this problem than every other problem combined.

[Yakov Pechersky]

The boss level! Of course, with that goal and hypothesis combo, it isn't solvable. You took a wrong turn somewhere. What's your current tactic sequence?

[Ron Stampler]

I don't like it but I finished Advanced Addition 5 with "exact hs(succ_inj(h))," ... is there a better way? I want to say, like, "apply succ_inj at h" but it doesn't let me.

[Ron Stampler]

full text: intro h,
induction t with s hs,
rw add_zero at h,
rw add_zero at h,
exact h,
rw succ_eq_add_one at h,
rw ← add_assoc at h,
rw ← add_assoc at h,
rw ← succ_eq_add_one at h,
rw ← succ_eq_add_one at h,
exact hs(succ_inj(h)),

[Mario Carneiro]

you can say apply hs, apply succ_inj, exact h if you want to replicate the behavior of exact hs (succ_inj h)

[Mario Carneiro]

If you want to work forward by applying succ_inj on h you can say have h := succ_inj h

[Yakov Pechersky]

You're doing a lot of forward reasoning -- modifying your hypothesis to try to get it to match the goal. Lean and mathlib also like to do reverse reasoning -- modifying the goal to match the hypotheses you have.

[Ron Stampler]

re: forward reasoning, in this instance use of "at h" was encouraged by the example text, I guess I went all-in.

[Ron Stampler]

Mario Carneiro said:

If you want to work forward by applying succ_inj on h you can say have h := succ_inj h

yeah i think this is what I want, h isn't replaced, it's a way of saying a consequence of h is succ_inj(h) and keeping that around.

[Yakov Pechersky]

Totally. And it's valid, as you can see you have a proof. Reverse reasoning ends up being shorter syntactically, since you will likely have fewer rw ← and more rw and fewer at h. Of course, sometimes you do have to rewrite at a hypothesis.

[Ron Stampler]

obviously I'm very early on but are there "proof simplifiers"? Like, tactics that look at proofs and say "this contradiction unnecessary, this reasoning backwards" etc and pump out a neater version of a proof?

[Ron Stampler]

maybe half the point of this project is that the nuance isn't important, in the face of a method like "cc" or "simp" the details may be irrelevant

[Yakov Pechersky]

There are, of different kinds. If you know what some collection of lemmas will solve the goal, but you don't care to think about their order, simp [lemma3, lemma1, lemma2] will still work. Some tactics are just to solve specific types of goals, like linarith for inequalities, ring for statements that have to do with associativity, commutativity, and distributivity of rings, norm_num to deal with statements about numerals...

[Yakov Pechersky]

We now also have lean-gptf which is scouring the library and reducing proofs using a ML based method

[Yakov Pechersky]

Yeah, the exact order of the tactic steps to prove why matrix.det ![![a, b], ![c, d]] = a * d - b * c aren't that interesting.

[Ron Stampler]

I feel like... if I had this machinery as an undergrad, I could have proved stuff a lot quicker but understood it a lot less. Would that have been a good thing or a bad thing? Nobody counts on their fingers any more, nobody does multiplication on paper, and you don't even have to differentiate functions any more - mathematica or whatever can do it all for you. Is this the next step of reducing once complicated stuff to mere footnotes? I'm daunted.

[Yakov Pechersky]

When Mathematica can't, for some reason, differentiate a function for you, or when you are trying to explain why swapping the order of rotations of a Rubick's cube aren't equivalent, what will you do then? When a proof in Lean breaks, how will you know how to fix it?

[Ron Stampler]

and, after all, bits do flip occasionally...

[Yakov Pechersky]

Additionally, some material in mathlib is at such a high level of generalization that it might not always be accessible why something is true, because it's using a level of theory deeper than one's understanding. In principle I know epsilon-delta analysis works. But I don't know filters, which is what mathlib uses and which are more powerful.

[Ron Stampler]

when one area of maths retires another, will lean automatically spot a library as superfluous?

[Bryan Gin-ge Chen]

Ron Stampler said:

I feel like... if I had this machinery as an undergrad, I could have proved stuff a lot quicker but understood it a lot less. Would that have been a good thing or a bad thing? Nobody counts on their fingers any more, nobody does multiplication on paper, and you don't even have to differentiate functions any more - mathematica or whatever can do it all for you. Is this the next step of reducing once complicated stuff to mere footnotes? I'm daunted.

This post reminds me of a previous discussion near the beginning of this thread.