When using Coq, I am kind of tending to focus my current goal the Coq gives me.
However, there are cases where the current goal is inpossible to prove.

this is a (inproper?) example

``````Theorem double_injective_take2 : ∀ n m,
double n = double m →
n = m.
Proof.
intros n m.
(* n and m are both in the context *)
generalize dependent n.
(* Now n is back in the goal and we can do induction on
m and get a sufficiently general IH. *)
induction m as [| m' IHm'].
- (* m = O *) simpl. intros n eq. destruct n as [| n'] eqn:E.
+ (* n = O *) reflexivity.
+ (* n = S n' *) discriminate eq.
- (* m = S m' *) intros n eq. destruct n as [| n'] eqn:E.
+ (* n = O *) discriminate eq.
+ (* n = S n' *) apply f_equal.
apply IHm'. injection eq as goal. apply goal. Qed.
``````

If one forget to `generalize n`, the proof will stuck.
I wonder if there is a way to detect similar problems, or at least identify whether it is possible to prove current goal with evidence in hand?
I tried to search for similar things/papers (type checker stuff) online but no result.

• Generalizing a variable is one of the weaker generalizations that often works (so you should probably start with that). Following up `induction …` with `; intros …` often makes this unnoticeable to the proofs you’ve already worked through before the generalization.