Hi,
I only recently started using mathcomp and often find myself tinkering with seemingly simple lemmas such as for example this one:
is_true (Zp1 != Zp0)
I found
Check Zp_nontrivial.
Zp_nontrivial
: ∀ p' : nat, is_true (Zp1 != 0)
Application of course fails:
apply Zp_nontrivial.
Unable to unify "(Zp1 != 0) = true" with "(Zp1 != Zp0) = true".
But then there is the problem of converting from Zp
to nat
?
In fact, this is a recurring problem and I have not found the proper way to deal with it yet.
In 99% of the case, I have (in)equalities where I'm only interested in the nat
representation of the Zp
-Ordinal
.
How do I transform such a Zp
term into a nat
term?
For example, how do I convert the above into
is_true (1 != 0)
Any advice would be greatly appreciated.
A trick is to use
rewrite (inj_eq val_inj) /=.
to replace an equality on ordinals to an equality on nat
s.
You need to remember replace your equality by a boolean one, though, which you can do using reflection via eqP
.
In this particular case you can actually bypass manual injectivity reasoning withby apply: contra (Zp_nontrivial p')=>/eqP->.
Dears,
I'm sorry but even with the advice above I'm unable to finish off seemingly simple lemmas.
Here is an example (that is just a variant of the one above):
Lemma Zp1neqInZp0 : forall q:nat, 1 < q -> is_true (@Zp1 q != @inZp q 0).
I start with the advice from above to handle the inequality
move => q q_gt1.
apply: contra (Zp_nontrivial q).
rewrite /Zp1.
The goal now is
is_true (inZp 1 == inZp 0) → is_true (inZp 1 == 0)
Now there are 2 options:
f_equal
When following the first option, I fail to apply f_equal
because what actually looks like a
perfect candidate for f_equal
isn't:
move/eqP. f_equal.
rewrite /inZp.
The goal now is:
Ordinal (n:=q.+1) (m:=1 %% q.+1) (ltn_pmod 1 (d:=q.+1) (ltn0Sn q)) =
Ordinal (n:=q.+1) (m:=0 %% q.+1) (ltn_pmod 0 (d:=q.+1) (ltn0Sn q))
→ is_true (Ordinal (n:=q.+2) (m:=1 %% q.+2) (ltn_pmod 1 (d:=q.+2) (ltn0Sn q.+1)) == 0)
The Ordinal
s do not only differ in m
but also in the last argument.
If I try to follow the second option then the rewrites from above do not work out:
move/eqP. (* Going back to a boolean equality. *)
rewrite (inj_eq val_inj).
The error is
Error: The LHS of inj_eq
(_ _ == _ _)
does not match any subterm of the goal
What am I missing here?
Sebastian Ertel has marked this topic as unresolved.
In this particular case, you probably need a -
before the rewrite
with inj_eq
:
rewrite -(inj_eq val_inj) //=.
You can also take advantage of some computation of eqb
and inZp
:
Lemma Zp1neqInZp0 : forall q:nat, 1 < q -> is_true (@Zp1 q != @inZp q 0).
Proof. by case. Qed.
@Pierre Jouvelot, that was indeed the missing bit. Thanks a lot.
@Laurent Théry , wow, that solution is of course much neater. I checked again but the docs do not say anything about case
doing any other computation. What is case
doing to solve this goal?
My understanding is that the case
construct destructs the inductive top value (here q
) into 0
and S q'
, and substitutes these values into the body of the forall
, yielding two cases. The first case is trivially true (since 1 < 0
is false), while the second yields the expected inequality by partial evaluation of the body. @Laurent Théry could certainly explain this much better, though :smile:
@inZp q 1
constructs an ordinal on top of the modulo 1 %% (q.+1)
. By computaton, we get no information on this expression, it can be 0
if q = 0
or 1
if q > 0
. Doing the case on q
makes it becomes1 %% (q'.+2)
and this time it computes to 1
. So the goal becomes Zp 0 != Zp 1
and this is solve by computation of eqb
.
not sure it is very clear....
@Sebastian Ertel the other answers are correct but if you're wondering "what solved the goal", you might want to observe that by case
means case; done
— and done
tries quite a few trivial steps (https://github.com/coq/coq/blob/v8.16/theories/ssr/ssreflect.v#L415-L421)
Last updated: Oct 13 2024 at 01:02 UTC