I'm trying to solve an equation of the form
A * B * C * D * E = F
where * some complicated left associative operation.
At the moment, everything is opaque (including * and A through F), and can be made transparent via autounfold with M_db.
The problem is that if I globally unfold the definition in the formula, simplification will take forever. Instead, I want to first unfold A * B, apply some tactics to reduce it to a normal form X, and then do the same with X * C and so forth.
Any idea how I would accomplish this? Here's my current approach but the in A or at A doesn't work. Also, it's not clear to me whether this is the right structure, or reduce_m ought to return something.
Ltac reduce_m M :=
match M with
| ?A × ?B => reduce_m A;
reduce_m B;
simpl;
autorewrite with C_db
| ?A => autounfold with M_db (* in A *);
simpl;
autorewrite with C_db
end.
Ltac simpl_m :=
match goal with
| [|- ?M = _ ] => reduce_m M
end.
A minimalish example:
Require Import Arith.
Definition add_f (f g : nat -> nat) := fun x => f x + g x.
Infix "+" := add_f.
Definition f := fun x => if x =? 4 then 1 else 0.
Definition g := fun x => if x <=? 4 then 3 else 0.
Definition h := fun x => if x =? 2 then 2 else 0.
Lemma ex : f + g + h = fun x => match x with
| 0 => 3
| 1 => 3
| 2 => 5
| 3 => 3
| 4 => 4
| _ => 0
end.