Prop
p-Formを指し示すことに使われるPropというものを導入します。Propを紹介するときは、それが指し示すp-Formを右側に書きます。
wordの定義と思えるPropは . が付きます。\(=\)と\(\emptyset\) の定義を挙げてみます。
\({=.}\)【\(X = Y \Longleftrightarrow X = Y\)】
\({\emptyset.}\)【\(\emptyset = \{ x \mid {\perp} \} \)】
\(\downarrow\) は次のように計算されます。
\(=.\) ≃【\(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)】
\(\emptyset.\) ≃【\(\forall x \, ( x \in \emptyset \Longleftrightarrow \, {\perp} )\)】
p-Formのinputに < > を付けてもPropを作れます。例 emp. \(=\) <emp =_ {cls x | false}>未実装
rule
2つの$Formは、$var同士の変換、$Var同士の変換、等で移り変わるとき同じとみなされます。
Formを$Formに変換する関数 $ を作ります。varを$Varに置き換えます。例 $【\(X \in Y\)】=【\({\sf X} \in {\sf Y}\)】
ただし、束縛されたvarは$varに替えます。例 $【\(\forall X ( X \in Y )\)】=【\(\forall {\sf x} ( {\sf x} \in {\sf Y} )\)】
\(=\) か \(\Leftrightarrow\) で始まるPropに対して、Prop変換の規則が作られます。
\({\rm rule}({\tt X} = {\tt Y})\) … $\({\tt X}\) ≃ $\({\tt Y}\)
\({\rm rule}({\tt P} \Leftrightarrow {\tt Q})\) … $\({\tt P}\) ≃ $\({\tt Q}\)
さらに \({\rm rule}(\forall{\tt x P})\) = \({\rm rule}({\tt P})\) とします。
例 \({\rm rule}({=.})\) … 【\({\sf X} = {\sf Y}\)】≃【\(\forall {\sf x} \, ( {\sf x} \in {\sf X} \Leftrightarrow {\sf x} \in {\sf Y} )\)】
例 \({\rm rule}({\emptyset.})\) … 【\({\sf X} \in \emptyset\)】≃【\({\perp}\)】
完全には実装できていません。
slash
Prop \({\tt F}\) を \({\rm rule}({\tt P})\) で変形した結果を \({\tt F}{\bf /}{\tt P}\) とします。変形できるsub Formをすべて変形します。\(\emptyset0{\bf /}{\emptyset.}\) ≃【\(\neg {\perp}\)】
部分Formに対してruleを適用したいことがあります。\(\downarrow\)をしたときの場所を指定できます。
例えば \([n]\) の部分Formに対して \({\bf /}\) を適用することを \({\bf /}^n\) と書き、\(\emptyset0{\bf /}^{1}{\emptyset.}\) = \(\emptyset0{\bf /}{\emptyset.}\) となります。
\([m][n]\) の部分Formに対して \({\bf /}\) を適用することを \({\bf /}^{mn}\) と書きます。
\({\bf /}\) や \({\bf /}^n\) などはL結合とされます。\({\tt P}{\bf /}{\tt Q}{\bf /}{\tt R}\) = \(({\tt P}{\bf /}{\tt Q}){\bf /}{\tt R}\)
定義によるslash
\(\text{rule}({\tt w}.)\)の左辺の\([0]\)が\({\tt w}\) のとき \({\tt w}\) は0-definedと言われます。例 \(=\) はdefined
\(\text{rule}({\tt w}.)\) の左辺が \({\sf X}\in{\tt w}(\cdots)\) となる \({\tt w}\) は\(\in\)-definedと言われます。
例 \(\emptyset\) は \(\in\)-defined
\(\text{rule}({\tt w}.)\) (\({\tt w}\)は0-definedか\(\in\)-defined) の形のruleを可能な限り全てに継時的に適用した結果を \({\bf /}\mathbb{D}.\) で作ります。
\(\text{rule}({=}{.})\) だけは、部分p-Formで\([0]\)が\(=\)のものに対し\([1],[2]\)のどちらかでも\([0]\)が\(\in\)-definedなら適用、した結果を \({\bf /}{\rm d\!I}.\) で作ります。
例 \(\emptyset0{\bf /}\mathbb{D}.\) = \(\emptyset0{\bf /}{\rm d\!I}.\) = \(\emptyset0{\bf /}{\emptyset.}\)
\({\tt f}.\)だけ除外したいときには / D.-\({\tt f}.\) または / d.-\({\tt f}.\) のようにinputします。
PropのThm
Propは紹介時に「どのPropから推論可能か」というThmが付くことがあります。\(\blacktriangleleft\) をクリックすると出てきます。例えば\(\emptyset0\)【\(x \notin \emptyset\)】\(\blacktriangleleft\)
次に注意しましょう。 \({\tt Q}\blacktriangleright{\tt P}\Leftrightarrow{\tt P}{\bf /}{\tt Q}\)
一般にAssumptionsは少ない方が証明が簡単になります。上のProp紹介はより強い次のものにした方が良いです。
\(\emptyset0\)【\(x \notin \emptyset\)】\(\blacktriangleleft\)