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 take care with the statements you post.
Ok, thank u.
Last updated: Oct 13 2024 at 01:02 UTC