Zulip Chat Archive

Stream: new members

Topic: specific qs on intro exercises


view this post on Zulip Ron Stampler (Feb 10 2021 at 19:07):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:09):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:11):

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?

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:13):

rewrite then assumption

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:14):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:15):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:20):

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.

view this post on Zulip Ruben Van de Velde (Feb 10 2021 at 19:22):

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

view this post on Zulip Johan Commelin (Feb 10 2021 at 19:24):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:25):

can confirm it doesn't

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:25):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:26):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:27):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 19:27):

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

view this post on Zulip Ruben Van de Velde (Feb 10 2021 at 19:28):

unknown identifier 'occurences.pos'

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:29):

it's probably in a namespace

view this post on Zulip Ruben Van de Velde (Feb 10 2021 at 19:29):

But you can certainly avoid doing this in NNG

view this post on Zulip Ruben Van de Velde (Feb 10 2021 at 19:29):

If only because people finish it :)

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:30):

occurrences.pos is not in a namespace...

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:30):

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.

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:31):

rw [add_comm d a, hd]

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:31):

can you walk me through the syntax there v briefly?

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:31):

rewrite with add_comm d a, then rewrite hd

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:32):

maybe NNG uses rw add_comm d a, rw hd

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:32):

I'm with ya, cheers

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:32):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:35):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:36):

at what goal?

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:36):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:37):

mysterious

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:37):

just finishing up multiplication world

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:38):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:39):

ok that makes some sense, cheers for the help!

view this post on Zulip Ron Stampler (Feb 10 2021 at 19:47):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:53):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:54):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 19:55):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 20:33):

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

view this post on Zulip Johan Commelin (Feb 10 2021 at 20:35):

@Ron Stampler Nope, there is no relation at all

view this post on Zulip Johan Commelin (Feb 10 2021 at 20:36):

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

view this post on Zulip Johan Commelin (Feb 10 2021 at 20:36):

Nothing needs to match

view this post on Zulip Johan Commelin (Feb 10 2021 at 20:36):

But of course it can be helpful to use such conventions

view this post on Zulip Ron Stampler (Feb 10 2021 at 20:37):

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

view this post on Zulip Johan Commelin (Feb 10 2021 at 20:37):

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

view this post on Zulip Johan Commelin (Feb 10 2021 at 20:37):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 20:38):

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

view this post on Zulip Johan Commelin (Feb 10 2021 at 20:38):

You can use a number of unicode symbols even

view this post on Zulip Johan Commelin (Feb 10 2021 at 20:38):

Ron Stampler said:

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

keyword: type inference

view this post on Zulip Johan Commelin (Feb 10 2021 at 20:39):

Lean remembers a lot of things behind the scenes

view this post on Zulip Ron Stampler (Feb 10 2021 at 20:39):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 20:40):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 20:42):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 20:45):

"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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 20:47):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 20:48):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 20:49):

thanks for the explanation, that makes it clear

view this post on Zulip Ron Stampler (Feb 10 2021 at 20:49):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 20:50):

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)

view this post on Zulip Mario Carneiro (Feb 10 2021 at 20:50):

What's the exercise?

view this post on Zulip Ron Stampler (Feb 10 2021 at 20:50):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 20:51):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 20:51):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 20:52):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 20:53):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 20:54):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 21:07):

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.

view this post on Zulip Ron Stampler (Feb 10 2021 at 21:08):

or maybe I'm missing the point altogether

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:10):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:11):

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

view this post on Zulip Ron Stampler (Feb 10 2021 at 21:11):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:14):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:16):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:16):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 21:18):

specifically chapter 2

view this post on Zulip Ron Stampler (Feb 10 2021 at 23:16):

what is the etymology behind the term "exact"?

view this post on Zulip Ron Stampler (Feb 10 2021 at 23:59):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 00:00):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 00:01):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 00:01):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 00:02):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 00:02):

otherwise, you'd have to construct the and term

view this post on Zulip Ron Stampler (Feb 11 2021 at 00:02):

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

view this post on Zulip Ron Stampler (Feb 11 2021 at 00:02):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 00:03):

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

view this post on Zulip Ron Stampler (Feb 11 2021 at 00:04):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 00:06):

Just using #backticks

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 00:06):

In fact, Lean knows the following about propositions:

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 00:11):

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.

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 00:12):

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.

view this post on Zulip Mario Carneiro (Feb 11 2021 at 00:28):

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

view this post on Zulip Mario Carneiro (Feb 11 2021 at 00:29):

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

view this post on Zulip PsyMar#2210 (Feb 11 2021 at 01:34):

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.

view this post on Zulip PsyMar#2210 (Feb 11 2021 at 01:35):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 01:48):

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?

view this post on Zulip Ron Stampler (Feb 11 2021 at 01:58):

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.

view this post on Zulip Ron Stampler (Feb 11 2021 at 01:59):

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

view this post on Zulip Mario Carneiro (Feb 11 2021 at 02:05):

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

view this post on Zulip Mario Carneiro (Feb 11 2021 at 02:06):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 02:06):

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.

view this post on Zulip Ron Stampler (Feb 11 2021 at 02:08):

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

view this post on Zulip Ron Stampler (Feb 11 2021 at 02:10):

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.

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 02:10):

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.

view this post on Zulip Ron Stampler (Feb 11 2021 at 02:11):

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?

view this post on Zulip Ron Stampler (Feb 11 2021 at 02:12):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 02:13):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 02:13):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 02:15):

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.

view this post on Zulip Ron Stampler (Feb 11 2021 at 02:16):

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.

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 02:18):

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?

view this post on Zulip Ron Stampler (Feb 11 2021 at 02:20):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 02:23):

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.

view this post on Zulip Ron Stampler (Feb 11 2021 at 02:30):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 11 2021 at 02:39):

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.


Last updated: May 15 2021 at 00:39 UTC