Lemma bool_sy: forall a b c d e f,

((a=?b) && (c=?d) && (e=?f)=true)= ((b=?a) && (d=?c) && (d=?c)=true). Want to apply bool symmtry command but it is not working.

This is not direct answer to your question, but will it be possible in the future to properly format your code ?

you can sandwich it between a pair of three backticks like this

```
` ` `
Lemma bool_sy: forall a b c d e f, ((a=?b) && (c=?d) && (e=?f)=true)= ((b=?a) && (d=?c) && (d=?c)=true)
` ` `
```

without spaces between the `s

The way it will end up looking will be like this:

```
Lemma bool_sy: forall a b c d e f,
((a=?b) && (c=?d) && (e=?f)=true)= ((b=?a) && (d=?c) && (d=?c)=true)
```

Which in my personal opinion looks easier to read.

Also `=?`

to the bet of my knowledge is not a polymorphic function and is defined per type and depending on your type, you will need a custom `eqb_sym`

.

```
Lemma eqb_sym: forall x y : string, (x =? y)%string = (y =? x)%string
```

The way you would use it in your case would be:

```
rewrite (eqb_sym a b).
```

But in your `bool_sy`

rhs and lhs are not equal.

Ok, thank you. I have searched bool_sy but get msg "The reference bool_sy was not found in the current

environment.". How i can find this ?

`bool_sy`

is the name of Lemma you are trying to prove me, the second word you typed.

Your lemma `bool_sy`

is false. Here is a counter example.

```
Lemma Not_bool_sy:
(forall a b c d e f: nat,
((a=?b) && (c=?d) && (e=?f)=true)=
((b=?a) && (d=?c) && (d=?c)=true)) -> False.
Proof.
intro H; specialize (H 1 1 2 2 3 4). simpl in H.
assert (false = true) by (rewrite H; auto).
discriminate.
Qed.
```

Please pay attention to the statements you post.

Btw, your statement is artificially restricted to types where equality is decidable. Your statement could have been as follows (Please note that I replaced the equality between propositions with a logical equivalence).

```
Lemma bool_sty {A: Type} (a b c d e f: A) :
(a = b /\ c = d /\ e = f) <-> (b = a /\ d = c /\ f = e).
Proof.
split; intros [? [? ?]]; repeat split; congruence.
Qed.
```

Ok, thank u.

Last updated: Jun 16 2024 at 01:42 UTC