More informative response to stucked proofs?

Using Coq
1

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.

Thanks in advance.

2

You can’t create an algorithm that always tells you if the proof is impossible for the given evidence because that would let you create an algorithm to tell if any statement is provable, which we know is not possible. Heuristics may be able to determine impossibility for some cases. I’m not aware that Coq has any feature like that.

3

Generalizing a variable is the top of the iceberg and may be dealt with by doing generalize dependent, but most of the time you need to come up with a non-trivial generalization of your property.

1 Like
4

Reiterating Matafou’s point: when an inductive proof gets stuck, you usually have to generalize.

  • 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.
  • Otherwise, you often need to generalize the property being proved, which does two things:
    1. The induction hypothesis is stronger (yay!), so we can use it show more things.
    2. The property being proved is stronger (boo!), so now we have to prove more things. This may necessitate yet more generalization/constraint.