Coq中归纳假设与目标无法统一时的改写及使用方法

相关定义与当前证明代码 #

Fixpoint insert (x : nat) (l : list nat) : list nat :=
  match l with
  | [] => [x]
  | h :: t => if x <=? h then x :: h :: t else h :: insert x t
  end.

Inductive list_PQ_property : list nat -> Prop :=
| sorted_empty : list_PQ_property []
| sorted_one : forall x, list_PQ_property [x]
| sorted_add : forall x y l,
    x <= y ->
    list_PQ_property (y :: l) ->
    list_PQ_property (x :: y :: l).

Theorem insert_correctness :
  forall (pq : list nat) (x : nat),  (* 注：原代码中PQ和el应为list nat和nat的别名，此处修正为实际类型 *)
    list_PQ_property pq ->
    list_PQ_property (insert x pq).
Proof.
  intros pq x H.
  induction H as [ | y | a b l Hab IHl].
  - simpl. apply sorted_one.
  - simpl. destruct (x <=? y) eqn:E.
    + apply Nat.leb_le in E. apply sorted_add.
      * apply E.
      * apply sorted_one.
    + apply Nat.leb_gt in E.
      apply Nat.lt_le_incl in E.
      apply sorted_add.
      * apply E.
      * apply sorted_one.
  - simpl. destruct (x <=? a) eqn:E.
    + apply Nat.leb_le in E.
      apply sorted_add.
      * apply E.
      * apply sorted_add.
        -- apply Hab.
        -- apply IHl.
    + destruct (x <=? b) eqn:E'.
      * apply Nat.leb_le in E'.
        apply sorted_add.
        apply Nat.lt_le_incl.
        apply Nat.leb_gt in E. apply E.
        apply sorted_add.
          ++ apply E'.
          ++ apply IHl.
      * apply Nat.leb_gt in E'.
        apply sorted_add.
        -- apply Hab.
Admitted.

遇到的问题 #

证明前两个case进展顺利，但第三个case（对应sorted_add构造子的归纳）出现障碍：

• 最初在apply sorted_add. ++ apply E'. ++ apply IHl.处卡壳，目标要求b <= x但假设E'是x <= b，后来通过Coq的Nat库函数绕过了传递性问题。
• 当前核心问题：归纳假设IHIHl是list_PQ_property (insert x (b :: l))，但当前目标是list_PQ_property (b :: insert x l)，二者无法直接统一，无法直接使用IHIHl完成证明。

当前的证明目标状态：

1 goal
x : nat
a, b : nat
l : list nat
Hab : a <= b
IHl : list_PQ_property (b :: l)
IHIHl : list_PQ_property (insert x (b :: l))
E : (x <=? a) = false
E' : b < x
______________________________________(1/1)
list_PQ_property (b :: insert x l)

解决思路指导 #

1. 修正归纳策略（推荐方案） #

当前对list_PQ_property的归纳方式存在缺陷：sorted_add构造子的归纳假设IHl是针对b::l的，而非我们需要的l的归纳假设。换为直接对列表pq做结构归纳，而非对list_PQ_property pq的证明树归纳：

Theorem insert_correctness :
  forall (pq : list nat) (x : nat),
    list_PQ_property pq ->
    list_PQ_property (insert x pq).
Proof.
  intros pq x H.
  induction pq as [ | h t IHt].  (* 改为对列表pq做结构归纳 *)
  - (* pq = [] *)
    simpl. apply sorted_one.
  - (* pq = h :: t *)
    destruct H as [ | ? Hab Ht].  (* 利用H拆解h::t满足list_PQ_property的条件 *)
    + (* 不可能的情况：h::t无法匹配sorted_empty *)
      inversion H.
    + (* 对应sorted_one：t是空列表，h是唯一元素 *)
      simpl. destruct (x <=? h) eqn:E.
      * apply Nat.leb_le in E. apply sorted_add; [apply E | apply sorted_one].
      * apply Nat.leb_gt in E. apply Nat.lt_le_incl in E.
        apply sorted_add; [apply E | apply sorted_one].
    + (* 对应sorted_add：h <= hd t，且t满足list_PQ_property *)
      simpl. destruct (x <=? h) eqn:E.
      * apply Nat.leb_le in E. apply sorted_add; [apply E | apply H].
      * apply Nat.leb_gt in E. apply Nat.lt_le_incl in E.
        apply sorted_add; [apply E | apply IHt Ht].
Qed.

2. 补充辅助引理（适配原归纳方式） #

如果坚持基于list_PQ_property的归纳树证明，可先证明辅助引理填补归纳假设与目标的差距：

Lemma insert_preserve_suffix :
  forall x y l,
    list_PQ_property (y :: l) ->
    y < x ->
    list_PQ_property (y :: insert x l).
Proof.
  intros x y l H Hlt.
  induction H as [ | ? | a b l' Hab IHl].
  - inversion H.
  - (* y::l是单元素列表 *)
    simpl. apply sorted_add; [apply Nat.lt_le_incl Hlt | apply sorted_one].
  - (* y::l = a::b::l'，且a <= b，list_PQ_property (b::l') *)
    simpl. destruct (x <=? b) eqn:E.
    + apply Nat.leb_le in E. apply sorted_add; [apply Hab | apply sorted_add; [apply E | apply IHl]].
    + apply Nat.leb_gt in E. apply sorted_add; [apply Hab | apply IHl (Nat.lt_le_incl E)].
Qed.

然后在原证明的第三个case最后一个分支调用该引理：

* apply Nat.leb_gt in E'.
        apply insert_preserve_suffix with (y := b) (l := l); [apply IHl | apply E'].

内容的提问来源于stack exchange，提问作者balllerz21