Stream: Coq users

Topic: use of bool symtry


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip walker (May 22 2023 at 14:24):

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

view this post on Zulip 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.

view this post on Zulip zohaze (Jun 03 2023 at 17:58):

Ok, thank u.


Last updated: Jun 16 2024 at 01:42 UTC