I have a question similar to Decomposing equality of constructors coq, however, my equality contains a match expression. Consider the example (which is nonsensical, but just used for clarification):
Fixpoint positive (n : nat) :=
match n with
| O => Some O
| S n => match positive n with
| Some n => Some (S n)
| None => None (* Note that this never happens *)
end
end.
Lemma positiveness : forall n : nat, Some (S n) = positive (S n).
Proof.
intro.
simpl.
At this point, with n : nat in the environment, the goal is:
Some (S n) =
match positive n with
| Some n0 => Some (S n0)
| None => None
end
I want to transform this to two subgoals in the environment n, n0 : nat:
positive n = Some n0 (* Verifying the match *)
S n = S n0 (* Verifying the result *)
And I would expect that if the match to prove equality on has multiple cases that might work, the new goal is a disjunction of all possibilities, so e.g. for
Some (S n) =
match positive n with
| Some (S n0) => Some (S (S n0))
| Some O => Some (S O)
| None => None
end
I would expect
(positive n = Some (S n0) /\ S n = S (S n0)) (* First alternative *)
\/ (positive n = Some O /\ S n = S O) (* Second alternative *)
Is there a Coq tactic which does this or something similar?
Is there a Coq tactic which does this or something similar?
If you run destruct (positive n) eqn:H, you will get two subgoals. In the first subgoal, you get:
n, n0 : nat
H : positive n = Some n0
============================
Some (S n) = Some (S n0)
and in the second subgoal you get
n : nat
H : positive n = None
============================
Some (S n) = None
This is not exactly what you asked for, but in the second subgoal, you can write assert (exists n0, positive n = Some n0); this will give you the goal you seek, and you can discharge the remaining goal by destructing the exists and using congruence or discriminate to show that positive n cannot be None and Some at the same time.