Zulip Chat Archive

Stream: new members

Topic: Calc to tactics


view this post on Zulip Auguste Poiroux (Aug 19 2020 at 16:00):

Hello!

I'm trying to convert automatically calc proofs to tactic proofs.
I currently have a way to transform automatically the intermediate steps of a calc proof into tactics. But I don't know how to combine them to get the final result.
For example, below I have a simple example of a calc proof and a tactic proof deduced from the calc proof. The transformation of the calc steps is done with have and exact. But I can't find a way to automate the combination of all these steps.
Do you know how I could do that?

Thank you in advance!

example (a b c d : )
(h1 : a = b) (h2 : b  c) (h3 : c + 1 < d) : a < d :=
begin
  calc
    a     = b     : h1
      ... < b + 1 : nat.lt_succ_self b
      ...  c + 1 : nat.succ_le_succ h2
      ... < d     : h3,
end
example (a b c d : )
(h1 : a = b) (h2 : b  c) (h3 : c + 1 < d) : a < d :=
begin
  have hyp1: a=b,
  exact h1,
  have hyp2: b<b+1,
  exact nat.lt_succ_self b,
  have hyp3: b+1  c+1,
  exact nat.succ_le_succ h2,
  have hyp4: c+1 < d,
  exact h3,

  have hyp5: a<b+1,
  rwa hyp1,
  have hyp6: a<c+1,
  exact gt_of_ge_of_gt hyp3 hyp5,
  transitivity c+1,
  repeat{assumption},
end

view this post on Zulip Alex J. Best (Aug 19 2020 at 16:06):

Well first of all calc is a tactic, so a calc proof is a tactic proof, I guess you want to only use simpler tactics like have exact and apply?

view this post on Zulip Alex J. Best (Aug 19 2020 at 16:07):

You can use show_term  to see the proof calc really generated under the hood like this

  show_term{
  calc
    a     = b     : h1
      ... < b + 1 : nat.lt_succ_self b
      ...  c + 1 : nat.succ_le_succ h2
      ... < d     : h3,},

view this post on Zulip Alex J. Best (Aug 19 2020 at 16:07):

and you should see exact lt_trans (lt_of_lt_of_le (trans_rel_right has_lt.lt h1 (nat.lt_succ_self b)) (nat.succ_le_succ h2)) h3

view this post on Zulip Alex J. Best (Aug 19 2020 at 16:10):

So to simulate calc you can go through these steps from outside in, once you have all your assumptions, you can do apply lt_trans to be left with two goals which you then use exact one_of_your_assumptions.

view this post on Zulip Alex J. Best (Aug 19 2020 at 16:11):

Also instead of doing

  have hyp2: b<b+1,
  exact nat.lt_succ_self b,

I'd recommend just, have hyp2: b<b+1 := nat.lt_succ_self b.

view this post on Zulip Auguste Poiroux (Aug 19 2020 at 16:32):

Thank you for your answers! It works very well!
I try to do these transformations with a python script. So I can call show_term with the Lean server. But it's a bit cumbersome and I'd rather do without it. Do you have other ideas how to do this without using things like show_term?

view this post on Zulip Rick Love (Aug 19 2020 at 17:12):

Well, you have all the haves :-) Can you just call 'apply' on each in reverse order?

(I'm not sure if that would work with the inequalities, but I think it would work if all = )

view this post on Zulip Rick Love (Aug 19 2020 at 17:15):

You might be able to call linarith a few times at the end

view this post on Zulip Yakov Pechersky (Aug 19 2020 at 17:20):

calc is special in that it calls the necessary transitivity lemmas too: https://leanprover-community.github.io/extras/calc.html#using-operators-other-than-equality`

view this post on Zulip Mario Carneiro (Aug 19 2020 at 20:08):

Alex J. Best said:

Well first of all calc is a tactic, so a calc proof is a tactic proof, I guess you want to only use simpler tactics like have exact and apply?

Actually calc isn't a tactic, you can write theorem foo := calc ... and you can't do that for tactics. It is actually begin calc ... end that is the oddity; there is code in the parser to magically transform calc ... into exact calc ... when used in tactic position

view this post on Zulip Mario Carneiro (Aug 19 2020 at 20:15):

I think we have a missing transitivity' tactic here, that receives the proofs up front and picks the appropriate transitivity lemma

view this post on Zulip Yury G. Kudryashov (Aug 20 2020 at 04:41):

Mario Carneiro said:

Actually calc isn't a tactic, you can write theorem foo := calc ... and you can't do that for tactics. It is actually begin calc ... end that is the oddity; there is code in the parser to magically transform calc ... into exact calc ... when used in tactic position

Into refine calc, not exact calc. E.g., you can do

begin
calc a = b : _
... = c : _,
-- 2 goals : a = b and b = c
end

Last updated: May 13 2021 at 20:13 UTC