Stream: Coq users

Topic: false relation

view this post on Zulip sara lee (Dec 09 2022 at 15:57):

a=?b =false-> b=?a =false. To prove this which command i should apply?

view this post on Zulip Pierre Castéran (Dec 09 2022 at 18:03):

You may search into Coq's library the lemma about commutativity of Boolean comparison.

Search ((?x =? ?y) = (?y =? ?x)).

Goal forall a b, a=?b = false -> b=?a = false.
intros a b; rewrite Nat.eqb_sym; easy.
Qed.

view this post on Zulip Michael Soegtrop (Dec 09 2022 at 18:36):

I thought lia meanwhile does support boolean relational operators, but apparently it doesn't.

Last updated: Oct 13 2024 at 01:02 UTC