Basic questions

Stream: new members

[Johan Commelin]

Nope... we should make apply_fun more flexible, but isn't exactly what you are looking for.

[Johan Commelin]

Note that replace is like have but -- you know -- replaces a hypothesis

[Scott Morrison]

See also the very useful tactic#specialize

[Benjamin]

Sometimes when playing the natural number game, I encountered weird variables like ?m_1, ?m_2, and so on after using apply. What do these mean?

I also have a question about substituting some value into a theorem. I have the following: mul_pos (a b : mynat) : a ≠ 0 → b ≠ 0 → a * b ≠ 0. How can I use this theorem but substituting succ(a) and succ(b) into a and b respectively?

[Mario Carneiro]

they are metavariables, they are expressions that are concrete but not known yet. They often go away if you just pretend they already have the expression you want in there

[Mario Carneiro]

to substitute that theorem use mul_pos (succ a) (succ b)

[Mario Carneiro]

usually a and b will be implicit though (written like {a : mynat}), in which case you would have to write @mul_pos (succ a) (succ b), or let lean figure it out with mul_pos

[Benjamin]

Thanks. Another issue I ran into is I have the following two hypotheses: k : a * succ d = a * d → succ d = d, i : a * succ d = a * h. I want to do a rewrite do I type "rw i at k", which gives me the error "rewrite tactic failed, lemma lhs is a metavariable". What does this mean? And how do I fix it?

[Kevin Buzzard]

The error is surprising -- do you have more than one thing called i? But you look to me like you're in trouble with the maths here, not the lean. How can you use k when its hypothesis is almost always false?

[Kevin Buzzard]

If you want some help you should post an #mwe or, if you're doing the natural number game, send a link to the level you're on and post the code you wrote so far to solve it

[Benjamin]

I'm on the last level of the advanced multiplication part of the natural number game. Here's what I have so far (I renamed i to j2 to insure it wasn't causing any trouble): revert b, induction c with d hd, rw mul_zero, have p := mul_eq_zero_iff, intro h, intro j, cases h, refl, have i := mul_eq_zero_iff a (succ h), cases i with i1 i2, have i3 := i1(j), cc, intro h, have j := hd(h), have k := hd(succ d), intro j2, symmetry at j2, rw j2 at k,

[Johan Commelin]

@Benjamin pro tip: #backticks (-;

[Ruben Van de Velde]

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=9&level=4

revert b,
induction c with d hd,
rw mul_zero,
have p := mul_eq_zero_iff,
intro h,
intro j,
cases h,
refl,
have i := mul_eq_zero_iff a (succ h),
cases i with i1 i2,
have i3 := i1(j),
cc,
intro h,
have j := hd(h),
have k := hd(succ d),
intro j2,
symmetry at j2,
rw j2 at k,

[Ruben Van de Velde]

That's certainly weird

[Benjamin]

I think my math is off anyway, but I don't know why rw didn't work there. FWIW, changing both with mul_suc and then doing rw worked.

[Benjamin]

I think I'm somewhat close up to cc. After that, did I go down the right path? I'm not sure whether I'm manipulating the universal statements right.

[Ruben Van de Velde]

Your k : a * succ d = a * d → succ d = d doesn't seem useful; the consequent is false

[Ruben Van de Velde]

I started with

intros b hb,
cases b,

[Ruben Van de Velde]

Does that help?

[Benjamin]

Much obliged, I figured it out

[Benjamin]

How can I introduce an existential? For example, if I have a = succ(a) + c, I want to get the existential statement to get succ(a) <= a (this is for a proof by contradiction of course).

[Ruben Van de Velde]

Probably use c,

[Ruben Van de Velde]

That is,

have : \exists m, a = succ a + m,
{ use b, sorry },

[Benjamin]

I'm getting this error failed to instantiate goal with (frozen_name has_add.add) c1 c2 What I have is h2_h : a = succ a + c1 + c2 and I typed have p := ∃ m, a = succ a + m, {use c1 + c2},.

[Ruben Van de Velde]

:, not :=

[Benjamin]

That fixed one error, but now I think there's a problem because use acts on the goal, and I need it to act on h2_h. Is there a way to do that? The error is solve1 tactic failed, focused goal has not been solved.

[Reid Barton]

After use you still have a goal: to prove that the value you provided satisfies whatever property it's supposed to.

[Benjamin]

How can I say that it's true by h2_h? Also, is there a better way to go from a = succ a + c1 + c2, to succ a <= a?

[Benjamin]

Ah, nvm, I think I see how this works now

[Benjamin]

Got it! Thanks for the help.