Stream: Coq users

Topic: case analysis with a hypothesis in mind


view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Aug 25 2020 at 11:52):

Using destruct instead of case should do the trick if I am not mistaken.

view this post on Zulip 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.

view this post on Zulip zvezdin (Aug 25 2020 at 11:54):

thanks! works!

view this post on Zulip 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.

view this post on Zulip 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) ?

view this post on Zulip Karl Palmskog (Aug 25 2020 at 12:10):

there is also the case_eq tactic...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Aug 26 2020 at 10:18):

is PEanoNat.Nat.eqb the same as Nat.eqb? (try About Nat.eqb)

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Aug 26 2020 at 10:39):

right your lemma is an iff so it's trying setoid rewrite

view this post on Zulip 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?

view this post on Zulip 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 ^_^

view this post on Zulip 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.

view this post on Zulip Kenji Maillard (Aug 26 2020 at 19:49):

One possibility to achieve it should be generalize f; intros [_ ->%(fun H => H Hr_contrap)].

view this post on Zulip 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 (->).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 )

view this post on Zulip 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: Jan 29 2023 at 04:05 UTC