sara lee (Dec 09 2022 at 15:57): sara lee (Dec 09 2022 at 15:57):a=?b =false-> b=?a =false. To prove this which command i should apply?
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.
I thought lia meanwhile does support boolean relational operators, but apparently it doesn't.
Last updated: Apr 19 2024 at 16:01 UTC