Dear Coq masters,
I am trying to do a case analysis on the output of a function, such that in my environment I already have a constraint on that output. Assume the following situation: https://pastebin.com/v2QeLQs2
Where (vm p) is a FmapList from a nat to a nat.
When I do:
case (M.find (elt:=nat) u (vm p)).
I get: https://pastebin.com/tb1iYNBD
Which does not allow me to make the connection between the first subgoal and my hypothesis in order to carry out the proof. How can I go about this?
destruct instead of
case should do the trick if I am not mistaken.
Otherwise you can give a name to the expression using
remember and destruct the resulting variable.
destruct tries to abstract over the expression it is given, but sometimes this doesn't work so you have to explicitly set it somehow, in which case
remember comes in very handy.
case Eq: (M.find _ _) do the job (where
Eq is the name of the generated equality akind to
there is also the
Thank you for the help! I have another (likely silly) problem which I spent too much time on yet still am not making progress. In particular I need to convert a hypothesis from
Some x <> Some y to
x <> y. I need it in order to rewrite with the lemma
f in the following: https://pastebin.com/39vfsPy3
invesiontactic doesn't work here as
option is not an inductive type.
there's no case analysis here (it would still be true even if Some was some arbitrary function instead of a constructor), it's the contrapositive of f_equal
You are right! I managed to build
x <> y by building the contrapositive of f_equal. Yet still, rewriting
f fails and I have no idea why. Environment: https://pastebin.com/sQdCP6XV
rewrite fresults in
Found no subterm matching "PeanoNat.Nat.eqb ?n ?n0 = false" in the current goal.
Which is weird. Surely the subgoal can be refined if we know that this is false?
is PEanoNat.Nat.eqb the same as Nat.eqb? (try
it seems so, I have proven similar properties using
PeanoNat.nat.eqb_refl . I've changed the specification to use
PeanoNat.nat.eqb instead (now subgoal is
(if PeanoNat.Nat.eqb c' n then Some c' else None) = None) and same error is seen.
right your lemma is an iff so it's trying setoid rewrite
setoid_rewrite is not able to find the necessary constraints (right side of
iff)? How can I provide these constraints?
I'm not sure where I can further read, so If anyone can bring insight that would be immensely helpful ^_^
What you want to rewrite is not
f but the second implication in
f applied to your hypothesis
One possibility to achieve it should be
generalize f; intros [_ ->%(fun H => H Hr_contrap)].
This is a bit cryptic: generalize will push the hypothesis
f onto the goal, then intros will first split it into 2 implications (
[pat1 pat2]), drop the first component (
_), evaluate the second component on
pat2%(fun H => H Hr_contrap)) and finally rewrite with the result (
Actually, an easier way to proceed here might be to use
replace (Nat.eqb _ _) with false. and then prove the remaining goal with simpler tactics.
@zvezdin FWIW, you might want to use "pose proof" instead of e.g. "pose" to put proofs in context. That'll drop their bodies.
And quite a few tactics work better on assumptions without bodies (like H : T) than assumptions with bodies ( H := body : T )
Works! And I learned quite a bit about Coq in the meantime, thank you @Kenji Maillard and @Paolo Giarrusso !
Last updated: Jan 29 2023 at 04:05 UTC