いくつかの証明では、カウンタの例として2つのInductive定義を使用しています。私はこれらの定義をSectionで囲んでカプセル化したいと思います。通常のDefinitionsはLetを使用して非表示にできますが、これはInductiveの定義でも可能ですか？そして、Theoremさんはどうですか？ローカル帰納的定義と定理
私が達成しようとしている実際のことを私に教えてください。私はそれを最初から間違った方法で行っているかもしれません。ロバート・ゴールドブラットによる優れた本「時間と計算の論理」のすべての証明と演習を公式に公式化したいと思います。
私たちは古典的な論理を取ります。
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.
クリプリケフレームを使用したセマンティクスの定義。
(* 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に関する。
Lemma satisfies_Not
: forall M x f
, satisfies M x (Not f) = ~ satisfies M x f
.
Proof. auto.
Qed.
次に、モデルを完成させるためにセマンティクスを持ち上げます。
そして、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.
ここには事があります。上記の補題の逆は成り立たないので、これを反例で示して、それが成立しないモデルを提示したいと思います。冗長assert Sを入力してから私を解放
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。
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は同等ではないと主張する。