zvezdin (Aug 25 2020 at 11:47): zvezdin (Aug 25 2020 at 11:47):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?
Pierre-Marie Pédrot (Aug 25 2020 at 11:52):Using destruct instead of case should do the trick if I am not mistaken.
Pierre-Marie Pédrot (Aug 25 2020 at 11:52):Otherwise you can give a name to the expression using remember and destruct the resulting variable.
zvezdin (Aug 25 2020 at 11:54):thanks! works!
Pierre-Marie Pédrot (Aug 25 2020 at 11:55):FTR, 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.
Kenji Maillard (Aug 25 2020 at 12:01):Wouldn't case Eq: (M.find _ _) do the job (where Eq is the name of the generated equality akind to remember) ?
Karl Palmskog (Aug 25 2020 at 12:10):there is also the case_eq tactic...
zvezdin (Aug 26 2020 at 05:07):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.
Gaëtan Gilbert (Aug 26 2020 at 08:20):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
zvezdin (Aug 26 2020 at 10:15):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?
Gaëtan Gilbert (Aug 26 2020 at 10:18):is PEanoNat.Nat.eqb the same as Nat.eqb? (try About Nat.eqb)
zvezdin (Aug 26 2020 at 10:26):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.
Gaëtan Gilbert (Aug 26 2020 at 10:39):right your lemma is an iff so it's trying setoid rewrite
zvezdin (Aug 26 2020 at 10:50):And setoid_rewrite is not able to find the necessary constraints (right side of iff)? How can I provide these constraints?
zvezdin (Aug 26 2020 at 19:30):I'm not sure where I can further read, so If anyone can bring insight that would be immensely helpful ^_^
Kenji Maillard (Aug 26 2020 at 19:47):What you want to rewrite is not f but the second implication in f applied to your hypothesis Hr_contrap.
Kenji Maillard (Aug 26 2020 at 19:49):One possibility to achieve it should be generalize f; intros [_ ->%(fun H => H Hr_contrap)].
Kenji Maillard (Aug 26 2020 at 19:52):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 Hr_contrap (that's pat2%(fun H => H Hr_contrap)) and finally rewrite with the result (->).
Kenji Maillard (Aug 26 2020 at 20:29):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.
Paolo Giarrusso (Aug 26 2020 at 22:12):@zvezdin FWIW, you might want to use "pose proof" instead of e.g. "pose" to put proofs in context. That'll drop their bodies.
Paolo Giarrusso (Aug 26 2020 at 22:13):And quite a few tactics work better on assumptions without bodies (like H : T) than assumptions with bodies ( H := body : T )
zvezdin (Aug 27 2020 at 05:34):Works! And I learned quite a bit about Coq in the meantime, thank you @Kenji Maillard and @Paolo Giarrusso !
Last updated: Oct 04 2023 at 23:01 UTC