我想创建 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.
这些策略的“问题”在于，它们只是试图盲目地交换术语，虽然这对于简单的求和来说效果很好，但如果我们混合其他运算符，如乘法、除法等，随机尝试所有的交换的复杂性将会激增，并且该策略将需要永远计算。
因此，我正在尝试编写一个“智能”策略，该策略决定操作数的特定顺序（理想情况下只是基于目标本身构建，而不是明确提供给策略），然后基于等式两边进行排序以此排序为独特的规范形式（这样仅仅
reflexity这在 Coq 中可能吗？我应该如何实现？
注意我的尝试：
我设法制定了一种策略，在给定操作数的排序的情况下，构建总和中操作数的索引列表（稍后可能用于对它们重新排序）：
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.
感谢 Feryll 的指点，我设法修复了问题中的两个错误策略。
我遗漏的主要内容是，不可能混合战术和术语，并且需要使用诸如
constr:(...)eval compute in ...固定代码：（看起来不太好，可能会受益于问题评论的建议，但至少它有效）
Require Import Init.Datatypes FMapList Init.Nat OrderedTypeEx List Rdefinitions Raxioms RIneq.
Open Scope R.
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_b := id_index b l in
let idx_c := id_index c l in
let idx_cmp := constr:(compare idx_b idx_c) 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_b := id_index b l in
let idx_c := id_index c l in
let idx_cmp := constr:(compare idx_b idx_c) 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.
Ltac build_list :=
let rec add_to_list id lst :=
lazymatch lst with
| id::?q => constr:(cons id q)
| ?a::?q => let id_q := add_to_list id q in constr:(cons a 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 := (build_id_list a lst) in
let lst_with_b := (build_id_list b lst_with_a) in
lst_with_b
| ?c =>
(add_to_list c lst)
end
in
lazymatch goal with
| |- ?a = ?b => build_id_list a (nil: list R)
| |- _ => fail "2"
end.
Ltac solve_sum_equality :=
repeat rewrite <- (Rplus_assoc _ _ _);
let operands_list := build_list in
repeat sort_sums_step operands_list;
reflexivity.
Theorem TestEasyTheorem (a b c d:R) : a + b + c + d = a + (d + c) + b.
Proof.
solve_sum_equality.
Qed.