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?

Using `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.

thanks! works!

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.

Wouldn't `case Eq: (M.find _ _)`

do the job (where `Eq`

is the name of the generated equality akind to `remember`

) ?

there is also the `case_eq`

tactic...

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

`invesion`

tactic 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 f`

results 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 `About Nat.eqb`

)

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

And `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 `Hr_contrap`

.

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 `Hr_contrap`

(that's `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