局部归纳定义和定理
Local Inductive definitions and Theorems
我在一些证明中使用了几个 Inductive
定义作为反例。然而,我想通过将它们包含在 Section
中来封装这些定义。可以使用 Let
隐藏常规 Definitions
,但这是否也适用于 Inductive
定义?那么 Theorem
s 呢?
让我给出我正在努力实现的实际目标,因为我一开始可能会以完全错误的方式去做。我想将 Robert Goldblatt 的优秀书籍 "Logics of Time and Computation" 的所有证明和练习形式化为 Coq。
对于初学者,我们采用经典逻辑,因为这也是本书所做的。
Require Import Classical_Prop.
Require Import Classical_Pred_Type.
接下来我们定义标识符的方式与在软件基础中所做的方式相同。
Inductive id : Type := Id : nat -> id.
语法定义。
Inductive modal : Type :=
| Bottom : modal
| V : id -> modal
| Imp : modal -> modal -> modal
| Box : modal -> modal
.
Definition Not (f : modal) : modal := Imp f Bottom.
使用 Kripke 框架定义语义。
(* Inspired by: www.cs.vu.nl/~tcs/mt/dewind.ps.gz
*)
Record frame : Type :=
{ Worlds : Type
; WorldsExist : exists w : Worlds, True
; Rel : Worlds -> Worlds -> Prop
}.
Record kripke : Type :=
{ Frame : frame
; Label : (Worlds Frame) -> id -> Prop
}.
Fixpoint satisfies (M : kripke) (x : (Worlds (Frame M))) (f : modal) : Prop
:= match f with
| Bottom => False
| V v => (Label M x v)
| Imp f1 f2 => (satisfies M x f1) -> (satisfies M x f2)
| Box f => forall y : (Worlds (Frame M)), (Rel (Frame M) x y) -> (satisfies M y f)
end.
第一个引理将模态 Not
与 Coq 的模态联系起来。
Lemma satisfies_Not
: forall M x f
, satisfies M x (Not f) = ~ satisfies M x f
.
Proof. auto.
Qed.
接下来我们提升语义以完成模型。
Definition M_satisfies (M : kripke) (f : modal) : Prop
:= forall w : Worlds (Frame M), satisfies M w f.
我们将展示它对 Not
连接词的意义。
Lemma M_satisfies_Not : forall M f
, M_satisfies M (Not f) -> ~ M_satisfies M f
.
Proof.
unfold M_satisfies.
intros M f Hn Hcontra.
destruct (WorldsExist (Frame M)).
specialize (Hn x); clear H.
rewrite satisfies_Not in Hn.
specialize (Hcontra x). auto.
Qed.
事情来了。上述引理的反面不成立,我想通过一个反例来展示这一点,展示一个它不成立的模型。
Inductive Wcounter : Set := | x1:Wcounter | x2:Wcounter | x3:Wcounter.
Lemma Wcounter_not_empty : exists w : Wcounter, True.
Proof. exists x1. constructor. Qed.
Inductive Rcounter (x : Wcounter) (y : Wcounter) : Prop :=
| E1 : x = x1 -> y = x2 -> Rcounter x y
| E2 : x = x2 -> y = x3 -> Rcounter x y
.
Definition Lcounter : Wcounter -> id -> Prop
:= fun x i => match x with
| x1 => match i with | Id 0 => True | _ => False end
| x2 => match i with | Id 1 => True | _ => False end
| x3 => match i with | Id 0 => True | _ => False end
end.
Definition Fcounter : frame := Build_frame Wcounter Wcounter_not_empty Rcounter.
Definition Kcounter : kripke := Build_kripke Fcounter Lcounter.
接下来是一个 Ltac
,它使我免于输入冗长的 assert
s。
Ltac counter_example H Hc := match type of H with
| ?P -> ~ ?Q => assert(Hc: Q)
| ?P -> (?Q -> False) => assert(Hc: Q)
| ?P -> ?Q => assert(Hc: ~Q)
end.
最后我用这个反例来证明下面的Lemma
.
Lemma M_not_satisfies_Not : ~ forall M f
, (~ M_satisfies M f) -> M_satisfies M (Not f)
.
Proof.
apply ex_not_not_all. exists Kcounter.
apply ex_not_not_all. exists (V (Id 0)).
unfold M_satisfies. simpl.
intro Hcontra. unfold not in Hcontra.
counter_example Hcontra Hn2.
apply ex_not_not_all. exists x1. simpl. auto.
apply Hn2. apply Hcontra. apply ex_not_not_all; exists x2. simpl. auto.
Qed.
我最好使用 remember
策略在证明中定义反例,但我认为它不能用于 Inductive
定义。所有与反例相关的定义都作为我的理论的一部分导出,我不想这样做。它仅用于M_not_satisfies_Not
的证明。实际上我什至不想导出这个 Lemma
因为它不是很有用。我把它放在那里只是为了证明 M_satisfies_Not
不能等价。
Section
不隐藏定义,而是使用 Module
。例如将计数器示例放在模块中。
Module CounterExample.
Import Definitions.
Inductive Wcounter : Set := x1 | x2 | x3.
...
Lemma M_not_satisfies_Not : ...
End CounterExample.
在这个阶段,顶层只定义了CounterExample
。
如果您也不想这样做,那么您可以将定义放在一个 .v
文件中,将反例放在另一个导入定义的文件中。实际上,它的工作方式是将 .v
个文件变成单独的模块。
我在一些证明中使用了几个 Inductive
定义作为反例。然而,我想通过将它们包含在 Section
中来封装这些定义。可以使用 Let
隐藏常规 Definitions
,但这是否也适用于 Inductive
定义?那么 Theorem
s 呢?
让我给出我正在努力实现的实际目标,因为我一开始可能会以完全错误的方式去做。我想将 Robert Goldblatt 的优秀书籍 "Logics of Time and Computation" 的所有证明和练习形式化为 Coq。
对于初学者,我们采用经典逻辑,因为这也是本书所做的。
Require Import Classical_Prop.
Require Import Classical_Pred_Type.
接下来我们定义标识符的方式与在软件基础中所做的方式相同。
Inductive id : Type := Id : nat -> id.
语法定义。
Inductive modal : Type :=
| Bottom : modal
| V : id -> modal
| Imp : modal -> modal -> modal
| Box : modal -> modal
.
Definition Not (f : modal) : modal := Imp f Bottom.
使用 Kripke 框架定义语义。
(* Inspired by: www.cs.vu.nl/~tcs/mt/dewind.ps.gz
*)
Record frame : Type :=
{ Worlds : Type
; WorldsExist : exists w : Worlds, True
; Rel : Worlds -> Worlds -> Prop
}.
Record kripke : Type :=
{ Frame : frame
; Label : (Worlds Frame) -> id -> Prop
}.
Fixpoint satisfies (M : kripke) (x : (Worlds (Frame M))) (f : modal) : Prop
:= match f with
| Bottom => False
| V v => (Label M x v)
| Imp f1 f2 => (satisfies M x f1) -> (satisfies M x f2)
| Box f => forall y : (Worlds (Frame M)), (Rel (Frame M) x y) -> (satisfies M y f)
end.
第一个引理将模态 Not
与 Coq 的模态联系起来。
Lemma satisfies_Not
: forall M x f
, satisfies M x (Not f) = ~ satisfies M x f
.
Proof. auto.
Qed.
接下来我们提升语义以完成模型。
Definition M_satisfies (M : kripke) (f : modal) : Prop
:= forall w : Worlds (Frame M), satisfies M w f.
我们将展示它对 Not
连接词的意义。
Lemma M_satisfies_Not : forall M f
, M_satisfies M (Not f) -> ~ M_satisfies M f
.
Proof.
unfold M_satisfies.
intros M f Hn Hcontra.
destruct (WorldsExist (Frame M)).
specialize (Hn x); clear H.
rewrite satisfies_Not in Hn.
specialize (Hcontra x). auto.
Qed.
事情来了。上述引理的反面不成立,我想通过一个反例来展示这一点,展示一个它不成立的模型。
Inductive Wcounter : Set := | x1:Wcounter | x2:Wcounter | x3:Wcounter.
Lemma Wcounter_not_empty : exists w : Wcounter, True.
Proof. exists x1. constructor. Qed.
Inductive Rcounter (x : Wcounter) (y : Wcounter) : Prop :=
| E1 : x = x1 -> y = x2 -> Rcounter x y
| E2 : x = x2 -> y = x3 -> Rcounter x y
.
Definition Lcounter : Wcounter -> id -> Prop
:= fun x i => match x with
| x1 => match i with | Id 0 => True | _ => False end
| x2 => match i with | Id 1 => True | _ => False end
| x3 => match i with | Id 0 => True | _ => False end
end.
Definition Fcounter : frame := Build_frame Wcounter Wcounter_not_empty Rcounter.
Definition Kcounter : kripke := Build_kripke Fcounter Lcounter.
接下来是一个 Ltac
,它使我免于输入冗长的 assert
s。
Ltac counter_example H Hc := match type of H with
| ?P -> ~ ?Q => assert(Hc: Q)
| ?P -> (?Q -> False) => assert(Hc: Q)
| ?P -> ?Q => assert(Hc: ~Q)
end.
最后我用这个反例来证明下面的Lemma
.
Lemma M_not_satisfies_Not : ~ forall M f
, (~ M_satisfies M f) -> M_satisfies M (Not f)
.
Proof.
apply ex_not_not_all. exists Kcounter.
apply ex_not_not_all. exists (V (Id 0)).
unfold M_satisfies. simpl.
intro Hcontra. unfold not in Hcontra.
counter_example Hcontra Hn2.
apply ex_not_not_all. exists x1. simpl. auto.
apply Hn2. apply Hcontra. apply ex_not_not_all; exists x2. simpl. auto.
Qed.
我最好使用 remember
策略在证明中定义反例,但我认为它不能用于 Inductive
定义。所有与反例相关的定义都作为我的理论的一部分导出,我不想这样做。它仅用于M_not_satisfies_Not
的证明。实际上我什至不想导出这个 Lemma
因为它不是很有用。我把它放在那里只是为了证明 M_satisfies_Not
不能等价。
Section
不隐藏定义,而是使用 Module
。例如将计数器示例放在模块中。
Module CounterExample.
Import Definitions.
Inductive Wcounter : Set := x1 | x2 | x3.
...
Lemma M_not_satisfies_Not : ...
End CounterExample.
在这个阶段,顶层只定义了CounterExample
。
如果您也不想这样做,那么您可以将定义放在一个 .v
文件中,将反例放在另一个导入定义的文件中。实际上,它的工作方式是将 .v
个文件变成单独的模块。