Zulip Chat Archive

Stream: new members

Topic: interactive tactics in calc

Miguel Marco (Jan 22 2022 at 18:54):

When using the calc tactic, we must provide a proof for each step, but I can't see the context and goal when writing it.

Is there a way to get it?

Also, I am being unable to prove this (apparently) simple goal:

c e : ,
h : c < 0
 c * e / -c = -e

I tried the usual simp, field_simp, norm_num, library_searchand so on, but they don't work.

Kyle Miller (Jan 22 2022 at 18:56):

When I want to see a context and goal somewhere, I usually insert a begin end or a by { }. (Sometimes you need parentheses, like (by { }).)

Kyle Miller (Jan 22 2022 at 18:59):

It seems that that the lemmas involved need that c is not equal to zero, rather than c is positive. You can get that fact from h.ne (or ne_of_le h, I believe).

A proof I found:

example (c e : ) (h : c < 0) : c * e / -c = -e :=
  rw [div_neg, neg_inj, mul_comm],
  simp [h.ne],

Ruben Van de Velde (Jan 22 2022 at 19:00):

A lemma like div_self is the main part of the argument; you just need to rearrange the terms until that applies

Last updated: Dec 20 2023 at 11:08 UTC