# How to use calc #

`calc`

is an environment -- so a "mode" like tactic mode, term mode and
conv mode. Documentation and basic examples for how to use
it are in Theorem Proving In Lean, in
section 4.

Basic example usage:

```
example (a b c : ℕ) (H1 : a = b + 1) (H2 : b = c) : a = c + 1 :=
calc a = b + 1 := H1
_ = c + 1 := by rw [H2]
```

`calc`

is also available in tactic mode. You can leave `?_`

s to create a
new goal:

```
example (a b c : ℕ) (H1 : a = b + 1) (H2 : b = c) : a = c + 1 := by
calc
a = b + 1 := ?_
_ = c + 1 := ?_
· exact H1
· rw [H2]
```

In fact, `calc A = B := H ...`

in tactic mode functions exactly like a
call to `refine (calc A = B := H ...)`

.

## Getting effective feedback while using calc #

To get helpful error messages, keep the calc structure even before the
proof is complete. Use `_`

as in the example above or `sorry`

to stand
for missing justifications. `sorry`

will suppress error messages
entirely, while `_`

will generate a guiding error message.

If the structure of calc is incorrect (e.g., missing `:=`

or the
justification after it), you may see error messages that are obscure
and/or red squiggles that end up under a random `_`

. To avoid these,
you might first populate a skeleton proof such as:

```
example (A B C D : ℝ ) : A = D :=
calc A = B := sorry
_ = C := _
_ = D := sorry
```

and then fill in the `sorry`

and `_`

gradually.

```
example (A B C D : ℝ ) : A = D := by
calc A = B := sorry
_ = C := ?_
_ = D := sorry
sorry
```

There is also a Calc widget that makes this easier here is a video demonstrating it.

## Using operators other than equality #

Many of the basic examples in TPIL use equality for most or all of
the operators, but actually `calc`

will work with any relation for which
we have created an instance of `Trans`

```
def r : ℕ → ℕ → Prop := sorry
variable (a b c: ℕ)
def r_trans {a b c} (h₁ : r a b) (h₂ : r b c) : r a c := sorry
instance : Trans r r r where
trans := r_trans
infix:50 "***" => r
example (a b c : ℕ) (H1 : a *** b) (H2 : b *** c) : a *** c :=
calc a *** b := H1
_ *** c := H2
```

## Using more than one operator #

This is possible, for example:

```
theorem T2 (a b c d : ℕ)
(h1 : a = b) (h2 : b ≤ c) (h3 : c + 1 < d) : a < d :=
calc
a = b := h1
_ < b + 1 := Nat.lt_succ_self b
_ ≤ c + 1 := Nat.succ_le_succ h2
_ < d := h3
```

What is actually going on here? The proofs themselves are not a mystery,
for example `Nat.succ_le_succ h2`

is a proof of `b + 1 ≤ c + 1`

. The
clever part is that lean can put all of these together to correctly
deduce that if `U = V < W ≤ X < Y`

then `U < Y`

. The way this is done,
Kevin thinks (can someone verify this?) is that Lean continually tries
to amalgamate the first two operators in the list, until there
is only one left. In other words, Lean will attempt to reduce
the equations thus:

```
U = V < W ≤ X < Y
U < W ≤ X < Y
U < X < Y
U < Y
```

Note the following subtlety: given `U op1 V`

and `V op2 W`

Lean
has to conclude `U op3 W`

for some operator, which might be `op1`

or `op2`

(or even, as we shall see, a new operator). How is Lean
doing this? The easiest case is when one of `op1`

and `op2`

is `=`

. Lean knows

```
#check trans_rel_right -- {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c
#check trans_rel_left -- {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c
```

and (Kevin believes) uses them if one of the operators is an equality operator. If however neither
operator is the equality operator, Lean looks through the instances of
`Trans`

and applies these instead.

## Using user-defined operators #

It is as simple as creating the relevant `Trans`

instances. For example

```
def r : ℕ → ℕ → Prop := sorry
def s : ℕ → ℕ → Prop := sorry
def t : ℕ → ℕ → Prop := sorry
theorem rst_trans {a b c : ℕ} : r a b → s b c → t a c := sorry
infix:50 "****" => r
infix:50 "^^^^" => s
infix:50 "%%%%" => t
instance : Trans r s t where
trans := rst_trans
example (a b c : ℕ) (H1 : a **** b) (H2 : b ^^^^ c) : a %%%% c :=
calc a **** b := H1
_ ^^^^ c := H2
```

This example shows us that the third operator `op3`

can be different to both `op1`

and `op2`

.