Zulip Chat Archive

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