## Stream: new members

### Topic: Problem with convert

#### Vivek Rajesh Joshi (Aug 24 2023 at 04:55):

image.png

I want to use cs4 to close the goal, and according to what I have read in "Mathematics in Lean", convert should do the job. But instead it is leaving me with a goal that I cannot understand.

image.png

Could someone explain why, and what the goal means?

#### Ruben Van de Velde (Aug 24 2023 at 05:16):

Convert is going too far. Try convert cs4 using 1 with increasing numbers until you get something sensible

#### Martin Dvořák (Aug 24 2023 at 06:35):

What does using do?

#### Damiano Testa (Aug 24 2023 at 07:16):

using n instructs congr to descend n layers into the expressions before leaving what is left as a side-goal. Approximately.

#### Damiano Testa (Aug 24 2023 at 07:19):

So (untested) congr on

a + b + c = b + a + c


probably asks to prove all equalities of the variables. congr 2 (or 1?) might leave

a + b = b + a


Definitely test this!!

#### Damiano Testa (Aug 24 2023 at 07:20):

(note that congr attempts to prove the side-goal, so the c = c goal disappears due to this extra mechanism)

#### Martin Dvořák (Aug 24 2023 at 07:21):

I just tried congr 1 is it.

#### Martin Dvořák (Aug 24 2023 at 07:26):

Using

example {a b c : ℕ} {R : ℕ → Prop} (hyp : R (a + b + c)) : R (b + a + c) := by
convert hyp using 0


produces

⊢ R (b + a + c) ↔ R (a + b + c)


Using

example {a b c : ℕ} {R : ℕ → Prop} (hyp : R (a + b + c)) : R (b + a + c) := by
convert hyp using 1


produces

⊢ b + a + c = a + b + c


Using

example {a b c : ℕ} {R : ℕ → Prop} (hyp : R (a + b + c)) : R (b + a + c) := by
convert hyp using 2


produces

⊢ b + a = a + b


Using

example {a b c : ℕ} {R : ℕ → Prop} (hyp : R (a + b + c)) : R (b + a + c) := by
convert hyp using 3


produces

⊢ b = a
⊢ a = b


#### Damiano Testa (Aug 24 2023 at 08:13):

Ah, using 0 converts to ↔: of course, this must be how congr begins its descent into the expressions!
EDIT[I was confused by the fact that this is now convert, and no longer congr!]

#### Kyle Miller (Aug 24 2023 at 08:54):

(Small point of information, convert starts with =. It uses congr! internally to apply congruence lemmas, and as a cleanup operation congr! converts = to ↔ when both sides are Props.)

#### Vivek Rajesh Joshi (Aug 24 2023 at 10:35):

Got it, my question was resolved with convert cs4 using 1. Thanks a lot!

Last updated: Dec 20 2023 at 11:08 UTC