## Stream: general

### Topic: Automatic variable names

#### Patrick Stevens (May 29 2018 at 21:29):

Another noob question, sorry. I haven't found an answer out there because everyone always proves this theorem using simp.

I've defined myNat in the obvious inductive way (zero : myNat, and succ : myNat -> myNat), and then defined my_add by cases as | myNat.zero n := n and | (myNat.succ m) n := myNat.succ (my_add m n). To prove the theorem addZero : (forall m : myNat, my_add m myNat.zero = m) without using simp, I entered tactic mode and began with assume m : myNat, induction m, refl to take care of the base case. Now I have the goal to prove it for the successor case, and the Tactic State tells me that I have m_a : myNat and m_ih : my_add m_a myNat.zero = m_a. But when I try to reference these terms with have (my_add (myNat.succ m_a) myNat.zero) = (myNat.succ (my_add m_a myNat.zero)), from sorry, I get multiple syntax errors, one of which is "unknown identifier 'm_a'".

#### Patrick Stevens (May 29 2018 at 21:30):

Have I got some syntax wrong, and if not, how do I reference variables that induction introduced?

#### Andrew Ashworth (May 29 2018 at 21:30):

^ can you paste it in a formatted code block

#### Patrick Stevens (May 29 2018 at 21:31):

Sorry - it really did come out pretty unreadable, hang on

#### Patrick Stevens (May 29 2018 at 21:33):

inductive myNat : Type
| zero : myNat
| succ : myNat → myNat

axiom zeroIsNotASuccessor : (∀ n : myNat, ¬(myNat.succ n = myNat.zero))
axiom succPreservesInequality: (∀ n m : myNat, (¬(m = n)) → ¬(myNat.succ m = myNat.succ n))

definition my_add : myNat -> myNat -> myNat
| myNat.zero n := n
| (myNat.succ m) n := myNat.succ (my_add m n)

theorem addZero : (∀ m : myNat, my_add m myNat.zero = m) :=
begin
assume m : myNat,
induction m,
refl,
begin
sorry
end
end


#### Kenny Lau (May 29 2018 at 21:33):

have :

#### Patrick Stevens (May 29 2018 at 21:35):

Ah, thanks - why was that colon not necessary in e.g.

example:p ∧ ¬q → ¬(p → q):=
begin
intro h,
assume hpq : p → q,
cases h with hp hnq,
have hq : q, from hpq hp,
exact hnq hq
end


it was

#### Patrick Stevens (May 29 2018 at 21:35):

Oh, I get it - an anonymous member of the equality type

Sorry

#### Kenny Lau (May 29 2018 at 21:35):

have : sets the name to this

#### Kenny Lau (May 29 2018 at 21:35):

have hq : sets the names to hq

cheers

#### Kevin Buzzard (May 29 2018 at 22:17):

I never know whether using have :... (and thus making a variable called this) is bad style.

#### Kevin Buzzard (May 29 2018 at 22:18):

I tend to name all my have variables except for the ones I instantly use and throw away on the next line

Last updated: May 12 2021 at 03:23 UTC