Coq证明enumerate与range索引序列等价性遇阻求解

我正在尝试在Coq中证明如下两个Python构造的等价性：

• for i, _ in enumerate(l, s)
• for i in range(s, len(l) + s)

我已经完成了enumerate与range函数的递归定义，同时提出了若干辅助定理支撑核心目标的证明，且已完成这些辅助定理的证明。

但证明中途受阻，当前得到的证明目标为[] = [s]，该式显然为假。我尝试特化（specialize）nil_cons引理后使用discriminate策略消解矛盾，但策略报错："No primitive equality found."，无法继续推进证明。

我确信存在可行的证明路径但暂未找到，以下是我当前编写的完整Coq代码：

Require Import Coq.Lists.List Coq.Bool.Bool Coq.Arith.Minus.

Import Coq.Lists.List.ListNotations.

Fixpoint _range (a b d : nat) :=
  match d with
    | 0 => []
    | S n => a :: _range (S a) b n
  end.

Definition range a b := _range a b (b - a).

(*
Fixpoint less n m : bool :=
  match n, m with
    | 0, 0       => false
    | 0, S _     => true
    | S _, 0     => false
    | S n, S m   => less n m
  end.

Fixpoint range (a b : nat) :=
  if less a b then
     match b with
       | 0 => []
       | S n => range a n ++ [n]
     end
  else [].
*)

Eval compute in range 0 0.
Eval compute in range 0 5.
Eval compute in range 5 0.
Eval compute in range 5 10.

Theorem range_eq_empty : forall (s : nat),
                         range s s = [].
Proof.
   induction s. reflexivity. unfold range. rewrite <- minus_n_n. reflexivity.
Qed.

Fixpoint enumerate (T : Type) (l : list T) (s : nat) :=
  match l with
    | [] => []
    | h :: t => (s, h) :: enumerate T t (S s) 
  end.

Eval simpl in enumerate nat [0;1;2;3;4] 0.
Eval simpl in enumerate nat [5;6;7;8;9] 5.

Theorem enum_prop_fwd : forall (T : Type) (l : list T) (s : nat),
                        enumerate T l s = [] -> l = [].
Proof.
   intros. induction l. reflexivity. pose proof nil_cons. symmetry. specialize (H0 T a l). discriminate.
Qed.

Theorem enum_prop_bwd : forall (T : Type) (l : list T) (s : nat),
                        l = [] -> enumerate T l s = [].
Proof.
   intros. rewrite H. reflexivity.
Qed.

Theorem enum_map_prop_fwd : forall (T : Type) (l : list T) (s : nat),
                            enumerate T l s = [] -> map fst (enumerate T l s) = [].
Proof.
   intros. rewrite H. reflexivity.
Qed.

Theorem enum_map_prop_bwd : forall (T : Type) (l : list T) (s : nat),
                            map fst (enumerate T l s) = [] -> enumerate T l s = [].
Proof.
   intros. pose proof (enum_prop_bwd T l s). induction l. reflexivity.
   apply H0. symmetry. pose proof nil_cons. specialize (H1 T a l). discriminate.
Qed.

Theorem enum_revert : forall (T : Type) (l : list T) (a : T) (s : nat),
                      s :: map fst (enumerate T l (S s)) = map fst (enumerate T (a :: l) s).
Proof.
   intros. induction s; reflexivity.
Qed.

(* for i, _ in enumerate(l, s) = for i in range(s, len(l) + s) *)
Theorem abc : forall (T : Type) (l : list T) (s : nat),
              map fst (enumerate T l s) = range s (length l + s).
Proof.
   intros. induction (length l). induction l. induction s. rewrite range_eq_empty. reflexivity.
   rewrite range_eq_empty. reflexivity. rewrite range_eq_empty. rewrite <- enum_revert. symmetry.
   rewrite range_eq_empty in IHl. pose proof (enum_prop_fwd T l s (enum_map_prop_bwd T l s IHl)). 
   rewrite H. compute. pose proof nil_cons. specialize (H0 nat s []). discriminate.

证明卡住的核心原因是归纳方式选择错误：对length l做归纳时，会出现length l = 0但l为非空列表的矛盾分支，这类分支本身在Coq逻辑中不可能成立，但原证明逻辑没有正确消解这个矛盾，反而推出了[] = [s]的假目标；同时在错误的上下文中调用nil_cons，导致discriminate策略找不到可消解的原始等式，因此报错。

正确的证明不需要绕过多冗余辅助引理，直接对列表l做结构归纳即可，步骤如下：

1. 基础步：l = []时，两边都化简为空列表，用已证明的range_eq_empty即可直接得证。
2. 归纳步：l = a :: t时，先化简左边map fst (enumerate T (a::t) s)，用已写好的enum_revert可以得到左边等于s :: map fst (enumerate T t (S s))。
3. 调用归纳假设，将起始值替换为S s，可得map fst (enumerate T t (S s)) = range (S s) (length t + S s)。
4. 补充一个关于_range的简单展开引理（直接由递归定义可得），代入后右边range s (S (length t) + s)可化简为s :: range (S s) (length t + S s)，通过等号传递即可完成证明。

修复后的核心证明代码如下：

(* 补充_range的展开引理，由fixpoint定义直接可得 *)
Lemma _range_succ : forall a b n, _range a b (S n) = a :: _range (S a) b n.
Proof. intros. reflexivity. Qed.

Theorem abc : forall (T : Type) (l : list T) (s : nat),
              map fst (enumerate T l s) = range s (length l + s).
Proof.
  intros T l. induction l as [| a t IHt]; intros s.
  - (* 基础步：空列表场景 *)
    simpl. rewrite range_eq_empty. reflexivity.
  - (* 归纳步：非空列表场景 *)
    simpl length. rewrite enum_revert. rewrite IHt with (s := S s).
    unfold range. rewrite Nat.add_succ_r.
    replace (S (length t) + s - s) with (S (length t)) by (rewrite Nat.add_succ_r; apply Nat.sub_add).
    rewrite _range_succ. f_equal.
    unfold range. replace (length t + S s - S s) with (length t) by apply Nat.sub_add.
    reflexivity.
Qed.

注：原有range定义在b < a时会因为自然数减法截断返回不符合预期的结果，但本定理场景下b = length l + s >= s = a，不会触发该问题。

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