# Zulip Chat Archive

## Stream: new members

### Topic: Calc to tactics

#### 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
```

#### 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`

?

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

#### 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 `

#### 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`

.

#### 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`

.

#### 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`

?

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

#### Rick Love (Aug 19 2020 at 17:15):

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

#### 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`

#### 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

#### 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

#### 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