在 Coq 中简化子公式
Simplifying Subformulas in Coq
我正在尝试求解形式为
的方程
A * B * C * D * E = F
其中 * 一些复杂的左结合运算。
目前，所有内容都是不透明的（包括 * 和 A 到 F），可以通过 autounfold with M_db 使其透明。
问题是，如果我全局展开公式中的定义，化简将永远进行下去。相反，我想先展开 A * B，应用一些策略将其缩小为正常形式 X，然后对 X * C 等进行同样的操作。
知道我将如何完成这个吗？这是我当前的方法，但 in A 或 at A 不起作用。另外，我不清楚这是否是正确的结构，或者 reduce_m 应该 return 什么。
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.
您可以将您的术语放入假设中，然后 autounfold 放入其中。即可以替换
autounfold with M_db (* in A *)
和
let Aterm := fresh in
set (Aterm := A);
autounfold with M_db in Aterm;
subst Aterm
如果您的 A 太大，这会很慢，因为 set 稍微复杂并且会进行某种缩减。如果是这种情况，您可以设定您的目标：
HA : A' = A
HB : B' = B
HC : C' = C
HD : D' = D
HE : E' = E
HAB : AB = A' * B'
HABC : ABC = AB * C'
HABCD : ABCD = ABC * D'
HABCDE : ABCDE = ABCD * E'
------------------------
ABCDE = F
然后你可以做类似
的事情
Ltac reduce H :=
autounfold with M_db in H; simpl in H; autorewrite with C_db in H.
reduce HA; reduce HB; reduce HC; reduce HD; reduce HE;
subst A' B'; reduce HAB;
subst AB C'; reduce HABC;
subst ABC D'; reduce HABCD;
subst ABCD E'; reduce HABCDE;
subst ABCDE.
更新以说明示例：
要对您的函数进行归约，您确实需要函数可扩展性，或者使用 = 以外的关系。但是，您不需要功能扩展性来执行模块化位：
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.
Ltac save x x' H :=
remember x as x' eqn:H in *.
Lemma ex : f + g + h = fun x => match x with
| 0 => 3
| 1 => 3
| 2 => 5
| 3 => 3
| 4 => 4
| _ => 0
end.
Proof.
save f f' Hf; save g g' Hg; save h h' Hh;
save (f' + g') fg Hfg; save (fg + h') fgh Hfgh.
cbv [f g] in *.
subst f' g'.
cbv [add_f] in Hfg.
(* note: if you want to simplify [(if x =? 4 then 1 else 0) +
(if x <=? 4 then 3 else 0)], then you need function
extensionality. However, you don't need it simply to
modularize the simplification. *)
或者，如果您以不同的方式设置目标，则可以避免函数扩展性：
Require Import Arith Coq.Classes.RelationClasses Coq.Setoids.Setoid Coq.Classes.Morphisms.
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.
Ltac save x x' H :=
remember x as x' eqn:H in *.
Definition nat_case (P : nat -> Type) (o : P 0) (s : forall n, P (S n)) (x : nat) : P x
:= match x with
| 0 => o
| S n' => s n'
end.
Lemma nat_case_plus (a a' : nat) (b b' : nat -> nat) (x : nat)
: (nat_case _ a b x + nat_case _ a' b' x)%nat = nat_case _ (a + a')%nat (fun x => b x + b' x)%nat x.
Proof. destruct x; reflexivity. Qed.
Lemma nat_case_plus_const (a : nat) (b : nat -> nat) (x : nat) (y : nat)
: (nat_case _ a b x + y)%nat = nat_case _ (a + y)%nat (fun x => b x + y)%nat x.
Proof. destruct x; reflexivity. Qed.
Global Instance nat_case_Proper {P} : Proper (eq ==> forall_relation (fun _ => eq) ==> forall_relation (fun _ => eq)) (nat_case P).
Proof.
unfold forall_relation; intros x x' ? f f' Hf [|a]; unfold nat_case; auto.
Qed.
Global Instance nat_case_Proper' {P} : Proper (eq ==> pointwise_relation _ eq ==> forall_relation (fun _ => eq)) (nat_case (fun _ => P)).
Proof.
unfold forall_relation, pointwise_relation; intros x x' ? f f' Hf [|a]; unfold nat_case; auto.
Qed.
Global Instance nat_case_Proper'' {P} {x} : Proper (pointwise_relation _ eq ==> eq ==> eq) (nat_case (fun _ => P) x).
Proof.
intros ??? a b ?; subst b; destruct a; simpl; auto.
Qed.
Global Instance nat_case_Proper''' {P} {x} : Proper (forall_relation (fun _ => eq) ==> eq ==> eq) (nat_case (fun _ => P) x).
Proof.
intros ??? a b ?; subst b; destruct a; simpl; auto.
Qed.
Ltac reduce :=
let solve_tac := unfold nat_case; repeat match goal with |- context[match ?x with O => _ | _ => _ end] => destruct x end; reflexivity in
repeat match goal with
| [ H : context[if ?x =? 4 then ?a else ?b] |- _ ]
=> replace (if x =? 4 then a else b) with (match x with 4 => a | _ => b end) in H by solve_tac
| [ H : context[if ?x =? 2 then ?a else ?b] |- _ ]
=> replace (if x =? 2 then a else b) with (match x with 2 => a | _ => b end) in H by solve_tac
| [ H : context[if ?x <=? 4 then ?a else ?b] |- _ ]
=> replace (if x <=? 4 then a else b) with (match x with 0 | 1 | 2 | 3 | 4 => a | _ => b end) in H by solve_tac
| [ H : context G[match ?x as x' in nat return @?T x' with O => ?a | S n => @?s n end] |- _ ]
=> let G' := context G[@nat_case T a s x] in
change G' in H
| [ H : context G[fun v => match @?x v as x' in nat return @?T x' with O => ?a | S n => @?s n end] |- _ ]
=> let G' := context G[fun v => @nat_case T a s (x v)] in
change G' in H; cbv beta in *
| [ H : context[(nat_case _ _ _ _ + nat_case _ _ _ _)%nat] |- _ ]
=> progress repeat setoid_rewrite nat_case_plus in H; simpl in H
| [ H : context[(nat_case _ _ _ _ + _)%nat] |- _ ]
=> progress repeat setoid_rewrite nat_case_plus_const in H; simpl in H
end.
Lemma ex : forall x, (f + g + h) x = match x with
| 0 => 3
| 1 => 3
| 2 => 5
| 3 => 3
| 4 => 4
| _ => 0
end.
Proof.
intro x; cbv [add_f].
save (f x) f' Hf; save (g x) g' Hg; save (h x) h' Hh; save (f' + g')%nat fg Hfg; save (fg + h')%nat fgh Hfgh.
cbv [f g] in *.
subst f' g'; reduce.
cbv [h] in *; reduce.
subst fg h'; reduce.
subst fgh.
unfold nat_case.
reflexivity.
Qed.
我正在尝试求解形式为
的方程A * B * C * D * E = F
其中 * 一些复杂的左结合运算。
目前，所有内容都是不透明的（包括 * 和 A 到 F），可以通过 autounfold with M_db 使其透明。
问题是，如果我全局展开公式中的定义，化简将永远进行下去。相反，我想先展开 A * B，应用一些策略将其缩小为正常形式 X，然后对 X * C 等进行同样的操作。
知道我将如何完成这个吗？这是我当前的方法，但 in A 或 at A 不起作用。另外，我不清楚这是否是正确的结构，或者 reduce_m 应该 return 什么。
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.
您可以将您的术语放入假设中，然后 autounfold 放入其中。即可以替换
autounfold with M_db (* in A *)
和
let Aterm := fresh in
set (Aterm := A);
autounfold with M_db in Aterm;
subst Aterm
如果您的 A 太大，这会很慢，因为 set 稍微复杂并且会进行某种缩减。如果是这种情况，您可以设定您的目标：
HA : A' = A
HB : B' = B
HC : C' = C
HD : D' = D
HE : E' = E
HAB : AB = A' * B'
HABC : ABC = AB * C'
HABCD : ABCD = ABC * D'
HABCDE : ABCDE = ABCD * E'
------------------------
ABCDE = F
然后你可以做类似
的事情Ltac reduce H :=
autounfold with M_db in H; simpl in H; autorewrite with C_db in H.
reduce HA; reduce HB; reduce HC; reduce HD; reduce HE;
subst A' B'; reduce HAB;
subst AB C'; reduce HABC;
subst ABC D'; reduce HABCD;
subst ABCD E'; reduce HABCDE;
subst ABCDE.
更新以说明示例：
要对您的函数进行归约，您确实需要函数可扩展性，或者使用 = 以外的关系。但是，您不需要功能扩展性来执行模块化位：
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.
Ltac save x x' H :=
remember x as x' eqn:H in *.
Lemma ex : f + g + h = fun x => match x with
| 0 => 3
| 1 => 3
| 2 => 5
| 3 => 3
| 4 => 4
| _ => 0
end.
Proof.
save f f' Hf; save g g' Hg; save h h' Hh;
save (f' + g') fg Hfg; save (fg + h') fgh Hfgh.
cbv [f g] in *.
subst f' g'.
cbv [add_f] in Hfg.
(* note: if you want to simplify [(if x =? 4 then 1 else 0) +
(if x <=? 4 then 3 else 0)], then you need function
extensionality. However, you don't need it simply to
modularize the simplification. *)
或者，如果您以不同的方式设置目标，则可以避免函数扩展性：
Require Import Arith Coq.Classes.RelationClasses Coq.Setoids.Setoid Coq.Classes.Morphisms.
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.
Ltac save x x' H :=
remember x as x' eqn:H in *.
Definition nat_case (P : nat -> Type) (o : P 0) (s : forall n, P (S n)) (x : nat) : P x
:= match x with
| 0 => o
| S n' => s n'
end.
Lemma nat_case_plus (a a' : nat) (b b' : nat -> nat) (x : nat)
: (nat_case _ a b x + nat_case _ a' b' x)%nat = nat_case _ (a + a')%nat (fun x => b x + b' x)%nat x.
Proof. destruct x; reflexivity. Qed.
Lemma nat_case_plus_const (a : nat) (b : nat -> nat) (x : nat) (y : nat)
: (nat_case _ a b x + y)%nat = nat_case _ (a + y)%nat (fun x => b x + y)%nat x.
Proof. destruct x; reflexivity. Qed.
Global Instance nat_case_Proper {P} : Proper (eq ==> forall_relation (fun _ => eq) ==> forall_relation (fun _ => eq)) (nat_case P).
Proof.
unfold forall_relation; intros x x' ? f f' Hf [|a]; unfold nat_case; auto.
Qed.
Global Instance nat_case_Proper' {P} : Proper (eq ==> pointwise_relation _ eq ==> forall_relation (fun _ => eq)) (nat_case (fun _ => P)).
Proof.
unfold forall_relation, pointwise_relation; intros x x' ? f f' Hf [|a]; unfold nat_case; auto.
Qed.
Global Instance nat_case_Proper'' {P} {x} : Proper (pointwise_relation _ eq ==> eq ==> eq) (nat_case (fun _ => P) x).
Proof.
intros ??? a b ?; subst b; destruct a; simpl; auto.
Qed.
Global Instance nat_case_Proper''' {P} {x} : Proper (forall_relation (fun _ => eq) ==> eq ==> eq) (nat_case (fun _ => P) x).
Proof.
intros ??? a b ?; subst b; destruct a; simpl; auto.
Qed.
Ltac reduce :=
let solve_tac := unfold nat_case; repeat match goal with |- context[match ?x with O => _ | _ => _ end] => destruct x end; reflexivity in
repeat match goal with
| [ H : context[if ?x =? 4 then ?a else ?b] |- _ ]
=> replace (if x =? 4 then a else b) with (match x with 4 => a | _ => b end) in H by solve_tac
| [ H : context[if ?x =? 2 then ?a else ?b] |- _ ]
=> replace (if x =? 2 then a else b) with (match x with 2 => a | _ => b end) in H by solve_tac
| [ H : context[if ?x <=? 4 then ?a else ?b] |- _ ]
=> replace (if x <=? 4 then a else b) with (match x with 0 | 1 | 2 | 3 | 4 => a | _ => b end) in H by solve_tac
| [ H : context G[match ?x as x' in nat return @?T x' with O => ?a | S n => @?s n end] |- _ ]
=> let G' := context G[@nat_case T a s x] in
change G' in H
| [ H : context G[fun v => match @?x v as x' in nat return @?T x' with O => ?a | S n => @?s n end] |- _ ]
=> let G' := context G[fun v => @nat_case T a s (x v)] in
change G' in H; cbv beta in *
| [ H : context[(nat_case _ _ _ _ + nat_case _ _ _ _)%nat] |- _ ]
=> progress repeat setoid_rewrite nat_case_plus in H; simpl in H
| [ H : context[(nat_case _ _ _ _ + _)%nat] |- _ ]
=> progress repeat setoid_rewrite nat_case_plus_const in H; simpl in H
end.
Lemma ex : forall x, (f + g + h) x = match x with
| 0 => 3
| 1 => 3
| 2 => 5
| 3 => 3
| 4 => 4
| _ => 0
end.
Proof.
intro x; cbv [add_f].
save (f x) f' Hf; save (g x) g' Hg; save (h x) h' Hh; save (f' + g')%nat fg Hfg; save (fg + h')%nat fgh Hfgh.
cbv [f g] in *.
subst f' g'; reduce.
cbv [h] in *; reduce.
subst fg h'; reduce.
subst fgh.
unfold nat_case.
reflexivity.
Qed.