Automatic variable names

Stream: general

[Patrick Stevens]

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

[Kenny Lau]

post your code?

[Patrick Stevens]

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

[Andrew Ashworth]

^ can you paste it in a formatted code block

[Patrick Stevens]

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

[Patrick Stevens]

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,
    have (my_add (myNat.succ m_a) myNat.zero) = (myNat.succ (my_add m_a myNat.zero)), from
    begin
        sorry
    end
end

[Kenny Lau]

have :

[Patrick Stevens]

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

[Kenny Lau]

it was

[Patrick Stevens]

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

[Patrick Stevens]

Sorry

[Kenny Lau]

have : sets the name to this

[Kenny Lau]

have hq : sets the names to hq

[Patrick Stevens]

cheers

[Kevin Buzzard]

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

[Kevin Buzzard]

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