Stream: new members

Topic: Leave term mode/calc once you enter it?

Abhimanyu Pallavi Sudhir (Oct 11 2018 at 12:22):

Part of my proof involved calc, but now I want to return to tactic mode to complete my proof. How do I do this?

Abhimanyu Pallavi Sudhir (Oct 11 2018 at 12:23):

The way I've done this in the past is to do the term mode in a separate lemma.

Andrew Ashworth (Oct 11 2018 at 12:30):

just type begin end again

Mario Carneiro (Oct 11 2018 at 12:31):

depends on how you have set it up. You could have the calc block inside tactic mode, or you could have a tactic block in one of the steps of a calc block

Kevin Buzzard (Oct 11 2018 at 12:54):

example : 2 + 2 = 5 :=
begin
show 3 + 1 = 5,
exact calc 3 + 1 = 1 + 3 : by simp
...        = 2 + 2 : by simp
...        = 5     : begin
show 2 + 2 = 5,
-- I'm not getting anywhere
sorry
end,
end


@Abhimanyu Pallavi Sudhir -- post a MWE if what I said doesn't help.

Abhimanyu Pallavi Sudhir (Oct 11 2018 at 13:23):

Here's the code:

import tactic.norm_num
definition cong_mod_37 (a b : ℤ) := ∃ k : ℤ, 37 * k = a - b

theorem cong_mod_37_equiv_reln : equivalence cong_mod_37 :=
begin
split,
rw reflexive,
intro x,
rw cong_mod_37,
rw sub_self,
fapply exists.intro,
exact 0,
norm_num,
split,
rw symmetric,
intros x y,
intro HXY,
rw cong_mod_37,
rw cong_mod_37 at HXY,
cases HXY with n Hn,
fapply exists.intro,
exact -n,
show 37 * -n = y - x,
exact calc 37 * -n = -(37*n) : by rw ←neg_mul_eq_mul_neg
... = -(x - y) : by rw Hn
... = y - x : by rw neg_sub
--split,
rw transitive,

end


Abhimanyu Pallavi Sudhir (Oct 11 2018 at 13:23):

I did what you said, but that doesn't work.

Rob Lewis (Oct 11 2018 at 13:24):

You need a comma at the end of the calc.

Abhimanyu Pallavi Sudhir (Oct 11 2018 at 13:25):

Oh... thanks. Yep, now it's working.

Last updated: May 08 2021 at 18:17 UTC