2

I have just run into the issue of the Coq induction discarding information about constructed terms while reading a proof from here.

The authors used something like:

remember (WHILE b DO c END) as cw eqn:Heqcw.

to rewrite a hypothesis H before the actual induction induction H. I really don't like the idea of having to introduce a trivial equality as it looks like black magic.

Some search here in SO shows that actually the remember trick is necessary. One answer here, however, points out that the new dependent induction can be used to avoid the remember trick. This is nice, but the dependent induction itself now seems a bit magical.

I have a hard time trying to understand how dependent induction works. The documentation gives an example where dependent induction is required:

Lemma le_minus : forall n:nat, n < 1 -> n = 0.

I can verify how induction fails and dependent induction works in this case. But I can't use the remember trick to replicate the dependent induction result.

What I tried so far to mimic the remember trick is:

Require Import Coq.Program.Equality.

Lemma le_minus : forall n:nat, n < 1 -> n = 0.
intros n H. (* dependent induction H works*) 
remember (n < 1) as H0. induction H.

But this doesn't work. Anyone can explain how dependent induction works here in terms of the remember-ing?

4

1 回答 1

1

你可以做

Require Import Coq.Program.Equality.

Lemma le_minus : forall n:nat, n < 1 -> n = 0.
Proof.
intros n H.
remember 1 as m in H. induction H.
- inversion Heqm. reflexivity.
- inversion Heqm. subst m.
  inversion H.
Qed.

如此处所述，问题在于 Coq 无法跟踪出现在您正在对其进行归纳的事物类型中出现的术语的形状。换句话说，对“小于”关系进行归纳会指示 Coq 尝试证明有关通用上限的某些信息，而不是您正在考虑的特定上限 (1)。

请注意，通过稍微概括您的结果，总是可以在没有rememberor的情况下证明这样的目标：dependent induction

Lemma le_minus_aux :
  forall n m, n < m ->
    match m with
    | 1 => n = 0
    | _ => True
    end.
Proof.
intros n m H. destruct H.
- destruct n; trivial.
- destruct H; trivial.
Qed.

Lemma le_minus : forall n, n < 1 -> n = 0.
Proof.
intros n H.
apply (le_minus_aux n 1 H).
Qed.
于 2015-12-04T15:58:23.727 回答