Я пытаюсь решить уравнение вида
A * B * C * D * E = F
где *
некоторая сложная левая ассоциативная операция.
На данный момент все непрозрачно (включая *
и A
до F
), и можно сделать прозрачным через autounfold with M_db
.
Проблема в том, что если я глобально разверну определение в формуле, упрощение затянется навсегда. Вместо этого я хочу сначала развернуть A * B
, применить некоторые тактики, чтобы привести его к нормальной форме X
, а затем сделать то же самое с X * C
и так далее.
Есть идеи, как мне это сделать? Вот мой текущий подход, но in A
или at A
не работает. Кроме того, мне непонятно, правильная ли это структура или reduce_m
должна что-то возвращать.
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.
Минималистичный пример:
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.