使用 Coq 证明存在量词
Prove existential quantifier using Coq
假设我们有一个归纳数据结构和一些谓词:
Inductive A : EClass :=
X | Y .
Definition P (a: A) : bool :=
match a with
X => true
| Y => false
end.
然后,我制定一个定理说存在一个元素 a
使得 P a
returns true:
Theorem test :
exists a: A, P a.
大概有很多种做法,我在想怎么用案例分析来证明,在我看来,大概是这样的:
- 记住有 2 种方法可以构造
A
- 一条一条地尝试每一种方式,如果我们找到一个
P a
成立的证人就停止。
我的 Coq 代码如下所示:
evar (a: A). (* introduce a candidate to manipulate *)
destruct a eqn: case_A. (* case analysis *)
- (* case where a = X *)
exists a.
rewrite case_A.
done.
- (* case where a = Y *)
(* stuck *)
我的问题是,
- 我的证明策略在逻辑上有缺陷吗?
- 如果不是,我的 Coq 就是问题所在,我如何向 Coq 传达我的工作已经完成,我找到了一个证人?可能我不应该
destruct
?
谢谢!
是的,你的证明有问题!您只需要先提供见证:
Inductive A := X | Y .
Definition P (a: A) : bool := match a with X => true | Y => false end.
Theorem test : exists a: A, P a = true.
Proof. now exists X. Qed.
如果你先做案例分析,你就会陷入死胡同。
这是一个粗略的框架,它演示了如何编写 Coq 策略来尝试将有限类型的所有元素作为见证。
(* Typeclass to register an enumeration of elements of a type. *)
Class Enumeration (A:Type) :=
enumerate : list A.
Arguments enumerate A [Enumeration].
(* Typeclass to register decision procedures to determine whether
a given proposition is true or false. *)
Class Decision (P:Prop) :=
decide : {P} + {~P}.
Arguments decide P [Decision].
(* Given a Coq list l, execute tactic t on every element of
l until we get a success. *)
Ltac try_list l t :=
match (eval hnf in l) with
| @cons _ ?hd ?tl => (t hd || try_list tl t)
end.
(* Tactic for "proof by reflection": use a decision procedure, and
if it returns "true", then extract the proof from the result. *)
Ltac by_decision :=
match goal with
|- ?P => let res := (eval hnf in (decide P)) in
match res with
| left ?p => exact p
end
end.
(* Combination to try to prove an (exists x:A, P) goal by trying
to prove P by reflection for each element in an enumeration of A. *)
Ltac try_enumerate :=
match goal with
|- @ex ?A ?P =>
try_list (enumerate A)
ltac:(fun x => exists x; by_decision)
end.
(* Demonstration on your example *)
Inductive A := X | Y.
Instance A_enum : Enumeration A :=
cons X (cons Y nil).
Instance bool_eq_dec : forall x y:bool,
Decision (x = y).
Proof.
intros. red. decide equality.
Defined.
Definition P (a:A) : bool :=
match a with
| X => true
| Y => false
end.
Goal exists a:A, P a = true.
Proof.
try_enumerate.
Qed.
假设我们有一个归纳数据结构和一些谓词:
Inductive A : EClass :=
X | Y .
Definition P (a: A) : bool :=
match a with
X => true
| Y => false
end.
然后,我制定一个定理说存在一个元素 a
使得 P a
returns true:
Theorem test :
exists a: A, P a.
大概有很多种做法,我在想怎么用案例分析来证明,在我看来,大概是这样的:
- 记住有 2 种方法可以构造
A
- 一条一条地尝试每一种方式,如果我们找到一个
P a
成立的证人就停止。
我的 Coq 代码如下所示:
evar (a: A). (* introduce a candidate to manipulate *)
destruct a eqn: case_A. (* case analysis *)
- (* case where a = X *)
exists a.
rewrite case_A.
done.
- (* case where a = Y *)
(* stuck *)
我的问题是,
- 我的证明策略在逻辑上有缺陷吗?
- 如果不是,我的 Coq 就是问题所在,我如何向 Coq 传达我的工作已经完成,我找到了一个证人?可能我不应该
destruct
?
谢谢!
是的,你的证明有问题!您只需要先提供见证:
Inductive A := X | Y .
Definition P (a: A) : bool := match a with X => true | Y => false end.
Theorem test : exists a: A, P a = true.
Proof. now exists X. Qed.
如果你先做案例分析,你就会陷入死胡同。
这是一个粗略的框架,它演示了如何编写 Coq 策略来尝试将有限类型的所有元素作为见证。
(* Typeclass to register an enumeration of elements of a type. *)
Class Enumeration (A:Type) :=
enumerate : list A.
Arguments enumerate A [Enumeration].
(* Typeclass to register decision procedures to determine whether
a given proposition is true or false. *)
Class Decision (P:Prop) :=
decide : {P} + {~P}.
Arguments decide P [Decision].
(* Given a Coq list l, execute tactic t on every element of
l until we get a success. *)
Ltac try_list l t :=
match (eval hnf in l) with
| @cons _ ?hd ?tl => (t hd || try_list tl t)
end.
(* Tactic for "proof by reflection": use a decision procedure, and
if it returns "true", then extract the proof from the result. *)
Ltac by_decision :=
match goal with
|- ?P => let res := (eval hnf in (decide P)) in
match res with
| left ?p => exact p
end
end.
(* Combination to try to prove an (exists x:A, P) goal by trying
to prove P by reflection for each element in an enumeration of A. *)
Ltac try_enumerate :=
match goal with
|- @ex ?A ?P =>
try_list (enumerate A)
ltac:(fun x => exists x; by_decision)
end.
(* Demonstration on your example *)
Inductive A := X | Y.
Instance A_enum : Enumeration A :=
cons X (cons Y nil).
Instance bool_eq_dec : forall x y:bool,
Decision (x = y).
Proof.
intros. red. decide equality.
Defined.
Definition P (a:A) : bool :=
match a with
| X => true
| Y => false
end.
Goal exists a:A, P a = true.
Proof.
try_enumerate.
Qed.