## Stream: new members

### Topic: specific qs on intro exercises

#### Ron Stampler (Feb 10 2021 at 19:07):

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

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

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

#### Mario Carneiro (Feb 10 2021 at 19:13):

rewrite then assumption

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

#### Ron Stampler (Feb 10 2021 at 19:15):

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

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

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

#### Ron Stampler (Feb 10 2021 at 19:25):

can confirm it doesn't

#### Mario Carneiro (Feb 10 2021 at 19:25):

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

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

#### Ron Stampler (Feb 10 2021 at 19:27):

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

#### Bryan Gin-ge Chen (Feb 10 2021 at 19:27):

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

#### Ruben Van de Velde (Feb 10 2021 at 19:28):

unknown identifier 'occurences.pos'

#### Mario Carneiro (Feb 10 2021 at 19:29):

it's probably in a namespace

#### Ruben Van de Velde (Feb 10 2021 at 19:29):

But you can certainly avoid doing this in NNG

#### Ruben Van de Velde (Feb 10 2021 at 19:29):

If only because people finish it :)

#### Mario Carneiro (Feb 10 2021 at 19:30):

occurrences.pos is not in a namespace...

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

#### Mario Carneiro (Feb 10 2021 at 19:31):

rw [add_comm d a, hd]

#### Ron Stampler (Feb 10 2021 at 19:31):

can you walk me through the syntax there v briefly?

#### Mario Carneiro (Feb 10 2021 at 19:31):

rewrite with add_comm d a, then rewrite hd

#### Mario Carneiro (Feb 10 2021 at 19:32):

maybe NNG uses rw add_comm d a, rw hd

#### Ron Stampler (Feb 10 2021 at 19:32):

I'm with ya, cheers

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

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

at what goal?

#### Mario Carneiro (Feb 10 2021 at 19:36):

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

mysterious

#### Ron Stampler (Feb 10 2021 at 19:37):

just finishing up multiplication world

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

#### Ron Stampler (Feb 10 2021 at 19:39):

ok that makes some sense, cheers for the help!

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

#### Mario Carneiro (Feb 10 2021 at 19:53):

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

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

#### Mario Carneiro (Feb 10 2021 at 19:55):

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

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

#### Johan Commelin (Feb 10 2021 at 20:35):

@Ron Stampler Nope, there is no relation at all

#### Johan Commelin (Feb 10 2021 at 20:36):

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

#### Johan Commelin (Feb 10 2021 at 20:36):

Nothing needs to match

#### Johan Commelin (Feb 10 2021 at 20:36):

But of course it can be helpful to use such conventions

#### Ron Stampler (Feb 10 2021 at 20:37):

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

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

#### Johan Commelin (Feb 10 2021 at 20:37):

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

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

#### Johan Commelin (Feb 10 2021 at 20:38):

You can use a number of unicode symbols even

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

#### Johan Commelin (Feb 10 2021 at 20:39):

Lean remembers a lot of things behind the scenes

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

#### Bryan Gin-ge Chen (Feb 10 2021 at 20:40):

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

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

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

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

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

#### Ron Stampler (Feb 10 2021 at 20:49):

thanks for the explanation, that makes it clear

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

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

#### Mario Carneiro (Feb 10 2021 at 20:50):

What's the exercise?

#### Ron Stampler (Feb 10 2021 at 20:50):

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

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

#### Mario Carneiro (Feb 10 2021 at 20:51):

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

#### Bryan Gin-ge Chen (Feb 10 2021 at 20:52):

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

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

#### Mario Carneiro (Feb 10 2021 at 20:54):

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

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

#### Ron Stampler (Feb 10 2021 at 21:08):

or maybe I'm missing the point altogether

#### Mario Carneiro (Feb 10 2021 at 21:10):

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

#### Mario Carneiro (Feb 10 2021 at 21:11):

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

#### Ron Stampler (Feb 10 2021 at 21:11):

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

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

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

#### Mario Carneiro (Feb 10 2021 at 21:16):

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

#### Mario Carneiro (Feb 10 2021 at 21:18):

specifically chapter 2

#### Ron Stampler (Feb 10 2021 at 23:16):

what is the etymology behind the term "exact"?

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

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

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

#### Yakov Pechersky (Feb 11 2021 at 00:01):

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

#### Yakov Pechersky (Feb 11 2021 at 00:02):

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

#### Yakov Pechersky (Feb 11 2021 at 00:02):

otherwise, you'd have to construct the and term

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

#### Ron Stampler (Feb 11 2021 at 00:02):

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

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

#### Ron Stampler (Feb 11 2021 at 00:04):

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

#### Yakov Pechersky (Feb 11 2021 at 00:06):

Just using #backticks

#### Yakov Pechersky (Feb 11 2021 at 00:06):

In fact, Lean knows the following about propositions:

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


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

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

#### Mario Carneiro (Feb 11 2021 at 00:28):

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

#### Mario Carneiro (Feb 11 2021 at 00:29):

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

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

#### PsyMar#2210 (Feb 11 2021 at 01:35):

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

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

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

#### Ron Stampler (Feb 11 2021 at 01:59):

full text: intro h,
induction t with s hs,
exact h,
exact hs(succ_inj(h)),

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

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

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

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

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

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

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

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

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

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

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

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

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

#### Ron Stampler (Feb 11 2021 at 02:20):

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

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

#### Ron Stampler (Feb 11 2021 at 02:30):

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

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