Disclaimer: I'm trying to use a small library built on mathcomp for some pretty simple stuff. But, I've never used mathcomp itself, so I understand that the answer to this question might just be "read the mathcomp book" (in which case, please let me know).
I have a hypothesis of the form H: x <> y
, and an if
-statement of the form if x == y then foo else bar
. I figure I can use ifN_eq : x != y -> (if x == y then vT else vF) = vF
, but that requires me to prove (x != y) = false
. Try as I might, I'm having trouble proving this, as simple as it seems.
Hi @Joshua Grosso , usually you can use rewrite directly with this term
move/eqP: H will transform your hyp
ut
but
let me just check the code i send works
One solution would be to use contraposition, as in
Lemma foo (x y : nat) : x <> y -> x != y.
Proof. by apply: contraPneq => ->. Qed.
rewrite (introF eqP H).
does the trick
For positive equalities you can actually use the coercion so rewrite (eqP H)
works directly, likely there is a way to make this work directly
Only caveat of course you need your types to be an eqtype
but they already are
negPf
would also be useful in this case, e.g., move/eqP/negPf: H
.
Pierre Jouvelot said:
One solution would be to use contraposition, as in
Lemma foo (x y : nat) : x <> y -> x != y. Proof. by apply: contraPneq => ->. Qed.
That one you can just use the view, so by move/eqP
will also work
Emilio Jesús Gallego Arias said:
For positive equalities you can actually use the coercion so
rewrite (eqP H)
works directly, likely there is a way to make this work directly
Tho in this case you'll do instead rewrite H eqxx
, rewrite (eqP H)
is for the other direction, from x == y to x = y
"read the mathcomp book" (in which case, please let me know).
Since you are already familiar with Coq you should be able to go through the first chapter very quickly...
Enrico Tassi said:
"read the mathcomp book" (in which case, please let me know).
Since you are already familiar with Coq you should be able to go through the first chapter very quickly...
Good to know, I'll do that!
As an update to my original problem, I'm finding rwP : forall (P : Prop) (b : bool), reflect P b -> P <-> b
very useful in conjunction with e.g. orP
.
@Joshua Grosso indeed, note that this lemma does require setoid rewriting tho as to interpret <->
properly in rewrite
Last updated: Oct 13 2024 at 01:02 UTC