基于Ltac的操作数确定性重写与排序Coq战术开发问询

我想要创建一个Coq战术，用来解决那些可以通过结合律、交换律等重写规则组合处理的等式子目标，比如证明a + b + c + d = a + (d + c) + b这类简单的和等式。

已实现的盲试交换战术 #

我先实现了一个盲试交换的战术，能处理简单和等式：

Require Import FMapList OrderedTypeEx List Rdefinitions Raxioms RIneq.
Open Scope R.

Ltac sort_sums_step :=
  let rec solve_sub_equality sub_equality :=
    lazymatch sub_equality with
    | ?a + ?c = ?b + ?c => solve_sub_equality (a = b)
    | ?a + ?c = ?b + ?d => rewrite (Rplus_comm (b) (d)); repeat rewrite <- (Rplus_assoc _ _ _)
    | _ => fail
    end
  in
  lazymatch goal with
  | |- ?a => solve_sub_equality a
  end.

Ltac solve_sum_equality :=
  repeat rewrite <- (Rplus_assoc _ _ _); repeat sort_sums_step; reflexivity.

Theorem TestEasyTheorem (a b c d:R) : a + b + c + d = a + (d + c) + b.
Proof.
  solve_sum_equality.
Qed.

但这个战术存在明显缺陷——它只会盲目尝试交换操作数，当等式中混合乘法、除法等复杂操作时，会因为复杂度爆炸导致计算耗时过长。因此我想开发一种更智能的战术：基于目标自动确定操作数的顺序，将等式两边都转化为唯一的规范形式，最后通过reflexivity完成证明。

已尝试的内容 #

生成操作数索引列表的战术

我实现了一个战术，能在给定操作数顺序时生成和中操作数的索引列表：

Ltac reverse_indices_of_left_sum_in_list l :=
  let rec id_index id lst :=
    lazymatch lst with
    | id::?q => O
    | ?a::?q => let idx1 := (id_index id q) in (constr:(S idx1))
    | _ => fail "1"
    end
  in
  let rec build_list sum_expr :=
    lazymatch sum_expr with
    | ?a + ?b => let q := (build_list a) in let idxb := (id_index b l) in (constr:(cons idxb q))
    | ?a => let idx := (id_index a l) in (constr:(cons idx nil))
    end
  in
  lazymatch goal with
  | |- ?a = ?b => let test := build_list a in pose (foo := test)
  | |- _ => fail "2"
  end.


Theorem TestEasyTheorem2 (a b c d:R) : (a + d + c + b)%R = (a + b + c + d)%R.
Proof.
  reverse_indices_of_left_sum_in_list (a::b::c::d::nil).
  (* Defines: foo := 1%nat :: 2%nat :: 3%nat :: 0%nat :: nil : list nat *)
Admitted.

尝试用索引排序和的战术

但当我尝试用索引对和进行排序时，代码执行失败：

Ltac sort_sums_step l :=
  let rec id_index id lst :=
    lazymatch lst with
    | id::?q => O
    | ?a::?q => let idx1 := (id_index id q) in (constr:(S idx1))
    | _ => fail "Identifier not found: " id
    end
  in
  let rec sort_sums sum_expr :=
    lazymatch sum_expr with
    | ?a + ?b + ?c => sort_sums (a + b) || (
      let idx_cmp := (compare (id_index b l) (id_index c l)) in
      match (eval compute in idx_cmp) with
      | Lt => fail "All good"
      | Eq => fail "All good"
      | Gt => rewrite (Rplus_assoc a b c); rewrite (Rplus_comm b c); rewrite <- (Rplus_assoc a c b)
      end)
    | ?b + ?c => let idx_cmp := compare (id_index b l) (id_index c l) in
      match (eval compute in idx_cmp) with
      | Lt => fail "All good"
      | Eq => fail "All good"
      | Gt => rewrite (Rplus_comm b c)
      end
    | ?a => fail "All good"
    end
  in
  lazymatch goal with
  | |- ?a = ?b => sort_sums a || sort_sums b
  | |- _ => fail "2"
  end.

Theorem TestEasyTheorem2 (a b c d:R) : (a + d + c + b)%R = (a + b + c + d)%R.
Proof.
  sort_sums_step (a::b::c::d::nil).

错误信息：

Variable id_index should be bound to a term but is bound to a tacvalue.

尝试自动构建操作数列表的战术

我还尝试从目标自动构建操作数列表，同样出现类似错误：

Ltac build_list :=
  let rec add_to_list id lst :=
    lazymatch lst with
    | id::?q => constr:(cons id q)
    | ?a::?q => constr:(cons a (add_to_list id q))
    | @nil => constr:(cons id nil)
    end
  in
  let rec build_id_list sum_expr lst :=
    lazymatch sum_expr with
    | ?a + ?b =>
      let lst_with_a := eval compute in (build_id_list a lst) in
      let lst_with_b := eval compute in (build_id_list b lst_with_a) in
      lst_with_b
    | ?c =>
      eval compute in (add_to_list c lst)
    end
  in
  lazymatch goal with
  | |- ?a = ?b => let bar := build_id_list a nil in let baz := (eval compute in bar) in pose (foo := baz)
  | |- _ => fail "2"
  end.

Theorem TestEasyTheorem3 (a b c:R) : a + b + c = a + c + b.
Proof.
  build_list.

错误信息：

Variable build_id_list should be bound to a term but is bound to a tacvalue.

请问在Coq中实现这种基于规范形式的等式证明战术是否可行？如果可行，该如何实现？

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