Zulip Chat Archive

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

Kenny Lau (May 29 2018 at 21:30):

post your code?

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

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

it was

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

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

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

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

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

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: Dec 20 2023 at 11:08 UTC