Stream: Coq users

Topic: use of bool symtry

zohaze (May 22 2023 at 11:21):

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.

walker (May 22 2023 at 11:36):

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.

walker (May 22 2023 at 11:46):

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.

zohaze (May 22 2023 at 13:40):

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 ?

walker (May 22 2023 at 14:24):

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

Pierre Castéran (May 22 2023 at 15:22):

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

zohaze (Jun 03 2023 at 17:58):

Ok, thank u.

Last updated: Jun 16 2024 at 01:42 UTC