I have a function:
Fixpoint eval (fuel : nat) (env : environment) (e : exp) :=
match fuel with
| 0 => None
| S fuel' => (...)
end
I'm now proving a property of such function, and I have a hypothesis:
IHfuel : eval 0 env (IfThenElse e1 e2 e3) = Some v -> star red (Interm (IfThenElse e1 e2 e3, env)) (Result v)
I used the simpl in IHfuel. tactic, and obtained:
IHfuel : None = Some v -> star red (Interm (IfThenElse e1 e2 e3, env)) (Result v)
Now what I would expect is that None = Some v is False, and therefore the implication should be trivially True.
Coq doesn't seem to agree. I even tried to use destruct (Some v), to see what it would do, and it created two goals: one with:
IHfuel : None = Some v0 -> star red (Interm (IfThenElse e1 e2 e3, env)) (Result v)
and the other with:
IHfuel : None = None -> star red (Interm (IfThenElse e1 e2 e3, env)) (Result v)
Why? I would not expect Some v to split into Some v0 and None...
Your question provides two things: One is a direct question, and the other is some larger confusion about Coq in general.
To answer the direct question, which is why destruct (Some v) gives you two cases: This is how destruct works: It looks at the type of the thing you are destructing, and then does a case distinction over it. In this case, you are doing a case distinction over something of type option T, so you get new goals, in which all occurrences of Some v are replaced by None or Some v2 (for a fresh v2), respectively. Now usually, you destruct an otherwise free variable, or perhaps the result of some function call (like n1 <=? n2 to distinguish n1 <= n2 from n1 > n2, i.e. do a case distinction on their order). As you have noticed, it does not make a lot of sense to destruct something when you already know its shape.
In the indirect question, you expected Coq to do something here, which it didn't. Unfortunately, you did not quite say what you expected to happen. So here's an explanation of what happened, so that you can perhaps spot where your train of thought went wrong.
When you simplify in an expression, Coq will reduce it. Reduction in Coq is something very specific, and it basically means that you take function calls (or constants) and evaluate them some more. In your example, this evaluated the eval 0 env (IfThenElse e1 e2 e3) to None, since this is what this function reduces to. Once this happens, your term is fully evaluated--there are no further function calls in there.
Now, you seem to have expected that the equality None = Some v would somehow change. However, it never will: Equality is not a function with computational content. Instead, it is a "first-class¹" proposition, that does not reduce further. As a proposition, it can be true or false,² but since deciding which it is is undecidable in general, you need to prove this. Even if there is a way for Coq to know that this specific equality is contradictory, this does not mean it is False: In Coq's type theory, everything has a type, and the type False is not the same as the type None = Some v. Both might have no inhabitants, but that's a very specific corner case. You just can't, in general, take two different types and just change the one for the other, that's not how things work.³
Now, it is true that None = Some v is always contradictory, i.e. there are no proofs of it. This means that it is equivalent to False, but not that it is the same. To exploit that it is contradictory, you can use the discriminate H tactic, assuming that you have some assumption H : None = Some v. So Coq does indeed recognize that these two are not equal, but you need to tell it to look.
However, in your case, there is nothing to exploit. You have the assumption IHfuel, but it is useless, since it is (as you said) "trivially true." There is no meaningful information to be gained from a trivially true proposition, so you can do nothing with it. You could turn it into False -> ..., but that would not be useful, since you still can not do anything with the hypothesis. The most useful thing would be to remove it from your context, i.e. use clear IHfuel. If you still want to have IHfuel : True in your context, just pose proof (I:True) as IHfuel (but that would, again, not be useful).
1: You can actually define it in the logic, but that's likely a bit too advanced for you. See https://xavierleroy.org/CdF/2018-2019/10.pdf for an introduction.
2: Assuming that our logic is classical, which it is not in Coq.
3: Turns out that people would really like to, so they designed Coq such that axioms like propositional extensionality, which indeed allows you to assume that equivalent propositions are equal (at the type level), are consistent. But to understand when this axiom is needed (quite rarely), you need to first understand why usually, it is not (like in your case).