I would like to create Coq tactics for solving a wide range of equality subgoals that may be solved by using a mix of rewrite rules such as associativity and commutativity of operators.
Although this is not my end goal, a simple example would be to solve equality of sums, e.g. show that a + b + c + d = a + (d + c) + b for instance.
I know that I can do this using a rule like:
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.
The 'problem' with these tactics is that they're just trying to swap terms blindly, and while this works well here for a simple sum, if we mix in other operators like multiplication, division, etc., randomly trying out all the swaps would blow up in complexity and the tactic would take forever to compute.
Thus, I'm trying to code a 'smart' tactic that decides on a specific ordering of operands (ideally just built based on the goal itself, rather than explicitly provided to the tactic), and then sorts both sides of the equation based on that ordering to a unique canonical form (so that a mere reflexity may then solve the equality goal).
Is this possible in Coq, and how should I got about it?
Note on what I tried out:
I managed to make a tactic that, given an ordering of operands, builds the list of indices of the operands in the sum (which could potentially later be used to re-order them):
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.
However, when I try to use the indices to sort the sums, none of my attempts succeeded. For instance:
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).
fails with:
Variable id_index should be bound to a term but is bound to a tacvalue.
I also get a similar error when I try to build the list from the goal itself:
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.
gives:
Variable build_id_list should be bound to a term but is bound to a tacvalue.
Thanks to Feryll's pointers, I managed to fix the two broken tactics in my question.
The main takeaway I was missing is that it's not possible to mix tactics and terms, and one needs to use things like constr:(...) to use (construct) a term in a tactic. Similarly, eval compute in ... is only useful on constructed terms, not tactic calls (which are directly evaluated).
Fixed code: (doesn't look great, and would probably benefit from the suggestions from the question comments, but at least it works)
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.