Calc to tactics

Stream: new members

[Auguste Poiroux]

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

[Alex J. Best]

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?

[Alex J. Best]

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,},

[Alex J. Best]

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

[Alex J. Best]

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.

[Alex J. Best]

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.

[Auguste Poiroux]

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?

[Rick Love]

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 = )

[Rick Love]

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

[Yakov Pechersky]

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`

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

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