Coq连通图性质引理证明求助：无路径到f值更小顶点

问题背景 #

我们需要在Coq中证明一个连通图的引理，图的性质如下：

• 顶点类型为V:Type，存在函数f: V -> nat为每个顶点关联自然数；
• 若两个顶点v1、v2相邻，则满足f v1 = f v2 ∨ f v1 = S (f v2) ∨ S (f v1) = f v2；
• 存在自然数n，当顶点v满足f v = n时，其所有相邻顶点vj的f值满足f vj = n ∨ f vj = S n，且图中存在顶点vi满足f vi = n。

需证明的引理：不存在顶点vn，使得存在从vi到vn的路径且f vn < f vi，即~exist vn, path vi vn /\ f vn < f vi。

已编写的部分代码 #

Section myGraph.

   Variable V   : Type.
   Variable vi  : V.
   Variable n   : nat.
   Variable adj : V -> V -> Prop.
   Variable f   : V -> nat.

   Hypothesis adj_relation   : forall v1 v2 : V, adj v1 v2 -> f v1 = f v2 \/ f v1 = S (f v2) \/ S (f v1) = f v2.
   Hypothesis nvalue         : f vi = n.
   Hypothesis both_ways      : forall v1 v2: V, adj v1 v2 -> adj v2 v1.
   Hypothesis special_vertex : forall vj v : V, f v = n -> adj v vj -> f vj = n \/ f vj = S n.

   (* The path relation *)
   Inductive path : V -> V -> Prop :=
     | path_refl  : forall v, path v v
     | path_step  : forall v1 v2, adj v1 v2 -> path v1 v2
     | path_trans : forall v1 v2 v3, path v1 v2 -> path v2 v3 -> path v1 v3.

   (* The graph is connected *)
   Hypothesis connected : forall v1 v2 : V, path v1 v2.

  (* Lemma to prove: There is no vertex vn such that f vn < f vi *)
  Lemma no_vertex_less_than_vi : ~ (exists vn : V, path vi vn /\ f vn < f vi).
  Proof.
    intros [vn H].
    assert (Hpath : path vn vi) by apply (connected vn vi).

    induction Hpath.
    - lia.
    - destruct (adj_relation v1 v2 H0) as [Hf_eq | [Hf_succ | Hf_pred]].
      + lia.
      + lia.
      + apply both_ways in H0.
        destruct (special_vertex v1 v2 nvalue) as [Hspec_eq | Hspec_succ].
        -- ?

    - ??

补全剩余证明步骤 #

1. 处理path_step分支的剩余部分 #

在destruct (special_vertex ...)后的两个分支，直接利用自然数的算术矛盾即可：

• 分支Hspec_eq：即f v1 = n，结合Hf_pred的S (f v1) = f v2，可得S n = f v2，但前提是f v2 < n，这与自然数性质矛盾，用lia自动推导。
• 分支Hspec_succ：即f v1 = S n，结合Hf_pred的S (f v1) = f v2，可得S (S n) = f v2，同样S (S n) < n不可能，用lia解决。

补充代码：

-- lia.
        -- lia.

2. 处理path_trans归纳步骤 #

对于路径传递的情况，我们需要利用归纳假设传递矛盾：

• 先将第二个归纳假设IHpath2特化到当前顶点v1；
• 构造出path v3 v2（通过path_trans结合已有的path v3 v1和path v1 v2），再结合f v3 < n的前提，触发IHpath2的矛盾。

补充代码：

- specialize (IHpath2 v1).
      destruct IHpath2 as [contra].
      apply contra.
      split.
      + apply path_trans with v2.
        assumption.
        assumption.
      + assumption.

完整证明代码 #

整合后的完整证明部分：

Proof.
  intros [vn H].
  destruct H as [H_path_vi_vn H_f_lt].
  assert (Hpath : path vn vi) by apply (connected vn vi).

  induction Hpath.
  - (* path_refl: path v v *)
    lia.
  - (* path_step: adj v1 v2 -> path v1 v2 *)
    destruct (adj_relation v1 v2 H0) as [Hf_eq | [Hf_succ | Hf_pred]].
    + (* f v1 = f v2 *)
      lia.
    + (* f v1 = S (f v2) *)
      lia.
    + (* S (f v1) = f v2 *)
      apply both_ways in H0.
      destruct (special_vertex v1 v2 nvalue H0) as [Hspec_eq | Hspec_succ].
      -- lia.
      -- lia.
  - (* path_trans: path v1 v2 -> path v2 v3 -> path v1 v3 *)
    specialize (IHpath2 v1).
    destruct IHpath2 as [contra].
    apply contra.
    split.
    + apply path_trans with v2.
      assumption.
      assumption.
    + assumption.
Qed.

说明 #

• lia（Linear Integer Arithmetic）工具可以自动处理自然数的不等式矛盾，大幅简化证明过程；
• path_trans步骤中，通过归纳假设的特化和路径的传递构造，将矛盾从终点回溯到起点，完成推导。

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