Decomposing equality of constructors with match expressions in Coq

Question

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?

Bac

Answer 1

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.

Quasimodo

Answer 2

I am having trouble understanding your motivation. In your example, it is easier to prove your result with a more general lemma:

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 n : positive n = Some n.
Proof.
  now induction n as [|n IH]; simpl; trivial; rewrite IH.
Qed.

Lemma positiveness' n : Some (S n) = positive (S n).
Proof. now rewrite positiveness. Qed.

Perhaps the case analysis you want to perform is better suited for a different application?

Octameter

Yes, this was my attempt at an MWE. I agree that it's silly. Is my question answerable like this, or shall I edit it to give a more meaningful example? – Bac

@Keelan Yes, having a better example would be useful. In Coq, we often end up complicating our lives by trying to implement a difficult solution to a problem that can be solved in much simpler ways. So knowing why exactly you need your case analysis would help solving your problem. – Octameter

Sorry, it's a bit complicated: this is for a homework assignment, and I don't want to post too much - but on the other hand I don't manage to find another example where this situation comes up naturally. I will discuss with my teacher. Sorry for using your time. – Bac