有限段階上の整列順序

舞台となるのは、周囲の累積階層 $V$ の上に構成される構成可能宇宙である。排中律はここで明示的な仮定として現れる。モジュールは、階層 ℓ-suc ℓ のすべての命題に対する判定を与えるパラメータ lem を受け取る。本章が必要とするのはこの一つの階層だけで、以下の構成はどれもこの固定された判定を用いる。表示されている定理が実際に証明する範囲を超えて、他の階層の命題については何も主張しない。

module L.Choice.FiniteStageOrders {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

本章では、数項で添字づけられた各段階が有限であることを証明し、最初の相違による整列順序を与える。さらに段階番号と局所順序を組み合わせて極限段階を整列順序づける。

先の選択の構成は、族の各セルについて、そのセルが初めて要素を持つ段階を特定し、その段階が後者であることを示した。したがって、ちょうどそこに現れるセルの各要素は、同一の集合上の定義可能部分集合、すなわち単一の段階に書かれた名前である。いまだ欠けているのは、それらの名前を比較する方法であり、本章が塔の底部で築くのはまさにこの比較である。

本章は二つの主張に依拠する。第一に、数項で添字づけられた各段階は有限である、という主張である。その正確な意味は下で述べる。すなわち、その段階は自身のすべての要素を含む有限な集合のリストを備える。第二に、有限段階は整列順序を担う、という主張である。これは、二つの要素をそれらが最初に相違する位置で比較し、その位置を含むほうを大きいとするものである。

第二の主張こそが数学的内容であり、本質的に有限集合についての主張である。同じ方式を自然数の部分集合に適用すると、無限降下が生じる。まず全自然数、次に 1 以上の全体、さらに 2 以上の全体、というように、各歩で生存者の中の最初の点を削り、厳密に低いところへ落ちていく。方式そのものはこれを禁じない。有限の基底でこれを禁じるのは、有限の基底の部分集合が有限個しかなく、したがって最小元を探す探索が必ず終わることである。以下の整礎性の証明はまさにこの方法をとる。有限なリストと線形順序があれば、非空な任意の性質に対し、リストを走査して各歩でそれまでの最小候補を保持することにより最小の要素が得られる。「非空な任意の性質は最小元を持つ」が、古典的には整礎性にほかならない。

有限性は塔を上へと伝播する。有限集合の定義可能部分集合はそのすべての部分集合であり、リストを持つ集合の部分集合は、そのリスト上の各ビットベクトルに一つずつ、有限個しかないからである。よって段階のリストから次の段階のリストが得られ、この帰納だけで構成全体を進められる。

極限段階の構成には、有限段階の順序どうしの整合性を仮定したり証明したりする必要がない。まず要素が初めて現れる段階番号を比較し、番号が等しいときだけ、その段階自身の順序を用いる。したがって異なる段階の要素は段階番号で、同じ段階に初めて現れる要素は局所順序で比較される。

以下で使う名前は構成可能階層のものである。塔の段階 Lset α、段階の定義可能部分集合を生み出す演算子 𝒟ₒ、そして数項 # n が順序数であるという事実 numeral-ord である。したがって各有限段階 Lset (# n) は正真正銘の段階であり、これが後の節の帰納が数項を登れる理由である。ここではさらに Lset-suc と FinOf の仕組みも取り込み、段階とその内部の有限集合とを結びつける。

比較には三分律を満たす基底順序が必要である。自然数上の順序 natOrder は、厳格で強整礎な線形順序であり、SWO としてまとめられ、その三つの場合の比較 Tri は lt、eq、gt に分かれる。後の節の探索手続きはこのインターフェースに対して書かれているため、任意の SWO に適用でき、自然数の実例が数項を順序づけるものになる。

module SemV = FOL.Semantics 𝒮ᵥ

open import Cubical.Data.Bool using ( false≢true )

ブール値はマスクとして登場する。数え上げられた集合の部分集合を列挙するには、各項目を保持するか捨てるかを Bool の true か false で記録し、false≢true が両者を区別する。添字の側では、自然数を厳格順序 _<_ で比較する。これは推移的かつ整礎で、¬m<m によりループを排除し、_≟_ で判定可能である。これらは、ある性質を証拠立てる最小の添字を見つけるため、また走査の中で各歩の判定を下すために、まさに必要となる性質である。

open import Cubical.Data.Nat.Order using ( _<_; <-trans; ¬m<m; <-wellfounded; _≟_ )
import Cubical.Data.Nat.Order as NatOrder

ここでの整礎性は、到達可能性の述語 Acc で表される。ある点が到達可能であるのはそのすべての先行元が到達可能なときであり、構成子 acc でまとめられる。関係のすべての点が到達可能なとき、その関係は型 WellFounded を持つ。Acc に関する証明義務は命題であり、この事実は isPropAcc として記録され、「単に存在する」データから到達可能性の主張への除去に使われる。モジュール WFI は整礎な関係を消費する帰納原理を提供する。

open import Cubical.Induction.WellFounded
  using ( Acc; acc; WellFounded; isPropAcc; module WFI )

累積階層の集合 x に対し、⟪ x ⟫ はその小さな表示型であり、⟪ x ⟫↪ はその型を階層へ埋め込む。同値 ∈∈ₛ は表示上の所属と階層の所属を結び、∈-asFiber は所属証明から添字とその同一視のパスを取り出す。空集合が零段階を与え、フォン・ノイマン数項 # n とその極限 ω が有限段階と極限の添字になる。

open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )

以下の所属命題は命題に値を取る。したがって ⟨ x ∈ˢ A ⟩ は x が A に属する証拠の型であり、数え上げはこの形を、各項の所属の証明と全要素が表現されるという主張の双方に用いる。

open InfinitySet using ( #_; ω )

open hPropView 𝒮ᵥ

有限な数え上げ

Tally は集合の全要素を有限添字族で提示し、重複を許し、単射性も決定可能な等しさも要求しない。

有限性は数え上げとして導入される。それは、一つの数、その個数だけの集合からなりすべて A に属する族、そして「A のすべての要素はそれらのうちのどれかである」という主張である。onto は、すべての要素がこの族の中に単に表現されていることを記録する。

重複も等しさの決定不能性も問題にならない。走査は同じ要素を再び訪れてよく、二つの位置が同じ集合を指していても、ビットベクトルは位置ごとに選択を記録できる。したがって、この意図的に弱い有限性の概念は次の段階の構成で保たれる。

集合 A の数え上げは三つのデータ欄を持つ。数 size が列挙する項目数を決め、item が各正当な位置、すなわち Fin size の要素を集合 item i に対応させ、欄 inside が列挙された各項目が実際に A に属することを証明する。これがなければ、長いリストは小さな集合を自明に被覆してしまう。同じ要素が複数の位置に現れても構わない。record はそれを禁じず、二つの位置の集合が等しいかを尋ねる欄もない。

record Tally (A : S) : Type (ℓ-suc ℓ) where
  field
    size   : ℕ
    item   : Fin size → S
    inside : (i : Fin size) → ⟨ item i ∈ˢ A ⟩

第四の欄は被覆を述べる。x とその A への所属証明から、onto は添字 i とパス item i ≡ x の命題的切断を返す。したがって添字は単に存在するだけで、選ばれた位置は外へ現れない。後では、この切断された証人を目標が命題である場合にだけ除去する。

    onto   : (x : S) → ⟨ x ∈ˢ A ⟩ → ∥ Σ[ i ∶ Fin size ] (item i ≡ x) ∥₁

有限添字を分割する

splitFin と joinFin は和より小さい添字を一方の加数の添字に対応させ、マスクの列挙に必要な算術を与える。

冪集合を数え上げることはビットベクトルを列挙することであり、長さ n + 1 のベクトルの個数は長さ n のもののちょうど二倍である。そこで一つの添字算術が必要になる。a + b より小さい添字とは、a より小さい添字か b より小さい添字のどちらかであり、逆も成り立つ。往復のうち片方向しか後で使われないため、その方向だけが証明される。bumpLeft は a 上の再帰が型検査を通るようにするずらしである。

具体的な図が助けになる。a = 2、b = 3 とすると、5 より小さい添字とは「2 より小さい添字か 3 より小さい添字」のいずれかにほかならない。joinFin は左の加数を最初の二つの枠に、右の加数を残り三つの枠に送り、splitFin は一つの添字がどちらの領域に落ちたかを尋ねる。ここで重複は無関係である。これらの写像は位置についてのものであり、後にそこへ置かれる項目についてのものではないからである。

最初の写像は、左側が一つ伸びる和に関するものである。bumpLeft は a か b のいずれかの添字を受け取り、suc a か b のいずれかの添字を返す。左の添字は一つ先へずらされ、右の添字はそのままである。それ自体には内容はなく、splitFin の再帰の各歩が左の加数から一つを剥がすため、左の添字を正しい型へ戻すずらしが必要だというだけのものである。joinFin は Fin a ⊎ Fin b から Fin (a + b) への方向だけが与えられ、a は再帰がパターン照合できるよう明示されている点にも注意してほしい。

bumpLeft : {a b : ℕ} → Fin a ⊎ Fin b → Fin (suc a) ⊎ Fin b
bumpLeft (inl i) = inl (suc i)
bumpLeft (inr j) = inr j

joinFin : (a : ℕ) {b : ℕ} → Fin a ⊎ Fin b → Fin (a + b)
joinFin     (inr j)       = j

joinFin と splitFin は形の上では互いの逆であるが、証明される往復は一方向だけである。joinFin は a 上の再帰である。a が零のとき、0 + b より小さい添字はそのまま b より小さい添字であり、後者のときは最初の枠が左の加数に属するので、位置零の左の添字は零番の枠へ写り、残りはすべて一つ上へずれる。splitFin は同じ再帰を逆向きにたどる。a + b より小さい添字はまず a より小さいかを問い、後者の場合は bumpLeft で剥がされた型を復元する。

joinFin (suc a) (inl zero)    = zero
joinFin (suc a) (inl (suc i)) = suc (joinFin a (inl i))
joinFin (suc a) (inr j)       = suc (joinFin a (inr j))

splitFin : (a : ℕ) {b : ℕ} → Fin (a + b) → Fin a ⊎ Fin b
splitFin     j       = inr j

往復 split-join は、つねに合されたばかりの添字を分割すればもとの左か右かの添字に戻る、という主張である。各節は refl か再帰呼び出しに対する合同性のどちらかである。splitFin (joinFin x) の計算はすでに再帰の答えへの bumpLeft の適用に簡約され、cong bumpLeft がそのずらしを通して帰納仮定を運ぶ。逆向きの合成は主張されず、ここでは合が単射であるという主張も一切ない。

splitFin (suc a) zero    = inl zero
splitFin (suc a) (suc i) = bumpLeft (splitFin a i)

split-join : (a : ℕ) {b : ℕ} (x : Fin a ⊎ Fin b) → splitFin a (joinFin a x) ≡ x
split-join     (inr j)       = refl
split-join (suc a) (inl zero)    = refl

この算術がマスクの節にもたらすのは、規模の正確な簿記である。長さ suc n のマスクの列挙が maskCount n で添字を半分に分けるとき、splitFin が先頭ビットが false か true かを決め、残りの添字を n での再帰に渡す。そこで mask-onto と split-join が合わさって、すべてのビットベクトルが届くことを示す。

split-join (suc a) (inl (suc i)) = cong bumpLeft (split-join a (inl i))
split-join (suc a) (inr j)       = cong bumpLeft (split-join a (inr j))

マスクを列挙する

maskAt は固定長のすべてのブール・ベクトルを列挙し、mask-onto は各選択パターンが現れることを証明する。

長さ n のマスクとは n ビットのベクトルであり、数え上げられた集合についてどの項目を残すかを指示する。その個数は maskCount n、すなわち繰り返し二倍として書かれた 2 の n 乗である。maskAt は添字をマスクとして読む。添字を半分に分け、どちらの半分に落ちたかで先頭ビットが決まり、残りが尾を与える。すべてのマスクがなんらかの添字から読み出されること、これが mask-onto であり、この列挙について必要とされる唯一の性質である。逐点的な単射性は要求されない。

n = 2 では、四つの添字が false ∷ false ∷ [] から true ∷ true ∷ [] までの四つのマスクを与える。この構成は実際には重複なく列挙するが、後の数え上げの議論が用いるのは証明済みの被覆 mask-onto だけであり、単射性には依存しない。

マスクの個数は、それを列挙する再帰そのものに沿って定義される。長さ零のマスクはちょうど一つ、長さ suc n のマスクは先頭ビットと長さ n のマスクの組であり、個数は maskCount n + maskCount n となる。これは繰り返し二倍として書かれた 2 の n 乗であり、加えられる二つの数が等しいので、splitFin が期待する形に正確に一致する。

maskCount : ℕ → ℕ
maskCount     = 
maskCount (suc n) = maskCount n + maskCount n

maskCons : (n : ℕ) → (Fin (maskCount n) → Vec Bool n)
         → Fin (maskCount n) ⊎ Fin (maskCount n) → Vec Bool (suc n)

maskCons は先頭ビットを、添字の対応する半分から読んだ尾に接ぐ。左の加数なら false、右なら true を選ぶ。そして maskAt が添字をマスクとして読む。長さ零では唯一のマスクは空ベクトル、長さ suc n では maskCount (suc n) = maskCount n + maskCount n より小さい添字が半分に分けられ、落ちた半分が先頭ビットを、内側の添字が尾を名指す。この読みは定理ではなく定義であり、ただ計算するだけのものである。

maskCons n r (inl j) = false ∷ r j
maskCons n r (inr j) = true  ∷ r j

maskAt : (n : ℕ) → Fin (maskCount n) → Vec Bool n
maskAt     j = []
maskAt (suc n) j = maskCons n (maskAt n) (splitFin (maskCount n) j)

被覆こそが mask-onto の内容であり、ここでは意図的に切断を行わない。ベクトル v が与えられると、この主張は実際の添字と、そこから読んだマスクから v への経路とをともに作り出す。基底の場合、空ベクトルは零番の添字から来る。列挙の中で単なる存在ではなくデータを渡さねばならないのはここだけであるが、再帰がベクトルそのものに沿って進むため、それが可能になる。

mask-onto : (n : ℕ) (v : Vec Bool n) → Σ[ j ∶ Fin (maskCount n) ] (maskAt n j ≡ v)
mask-onto     []          = zero , refl
mask-onto (suc n) (false ∷ v) =
  joinFin (maskCount n) (inl (mask-onto n v .fst))
  , (cong (maskCons n (maskAt n)) (split-join (maskCount n) (inl (mask-onto n v .fst)))

後者の段階ではベクトルが分岐を決める。先頭が false なら、尾の添字は joinFin で左半分に合され、経路は二歩で組み立てられる。まず split-join によって、合された添字の分割が主張どおり左半分を復元することを示し、次に cong (false ∷_) で再帰の経路を先頭ビットの下へ運ぶ。true の場合は右半分に替わるだけで、それ以外はそっくり同じである。個数と合わせて、これは数え上げられた集合のマスクが Fin (maskCount size) に被覆されることを意味し、まさに Tally の欄が期待する形である。

     ∙ cong (false ∷_) (mask-onto n v .snd))
mask-onto (suc n) (true ∷ v)  =
  joinFin (maskCount n) (inr (mask-onto n v .fst))
  , (cong (maskCons n (maskAt n)) (split-join (maskCount n) (inr (mask-onto n v .fst)))
     ∙ cong (true ∷_) (mask-onto n v .snd))

部分族を選び出す

select はブール・マスクで有限族を絞り込み、その要素補題は選ばれた項と真に印づけられた位置を対応させる。

select はマスクを族に適用する。ビットが true の項目を残し、それらを再び族として、その長さとともに返す。長さは再帰が生み出すものであり、これが要点である。何かを数える必要はなく、答えとマスクを結びつける算術も要らない。

二つの仕様が結果に何が含まれるかを述べ、どちらも切断を含まない。どちらも同じ再帰から直接読み取れるからである。marks は逆向きに走り、項目への判定を、それを記録するマスクへ変える。

小さな例が重複との相互作用を示す。同じ項目が二度現れる族と、両方の写しを残すマスクを取ると、選ばれた族はその項目を二度含み、二つの写しはそれぞれ固有のもとの位置とともに補題によって答えられる。何かが失われたり併合されたりすることはない。一意であることはそもそも要求されていないからである。

補助関数 selectStep は絞り込みの一歩を行う。項目 x とすでに選ばれた族が与えられると、x を先頭に付け、新しい長さ suc k を報告する。その結果の型は族と長さを依存対としてまとめるため、再帰はマスクに算術を一切用いずに長さを伸ばせる。

selectStep : {ℓ' : Level} {X : Type ℓ'} → X → Σ[ k ∶ ℕ ] (Fin k → X)
           → Σ[ k ∶ ℕ ] (Fin k → X)
selectStep {X = X} x (k , g) = suc k , h
  where
  h : Fin (suc k) → X

select はマスク上の再帰である。空のマスクは何も選ばず、それを荒謬パターンで示す。長さ零の族には位置が存在しないからである。先頭が false なら頭を落としてずらした族に再帰し、true なら selectStep で頭を残す。各歩で族が一つずらされること、これが随所の λ i → f (suc i) が記録しているものである。

  h zero    = x
  h (suc i) = g i

select : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) → (Fin n → X) → Vec Bool n
       → Σ[ k ∶ ℕ ] (Fin k → X)
select     f v           = zero , λ ()

最初の仕様 select-out は選択を順方向に読む。選ばれた族の各位置 j は、ビットが true であるもとの位置 i から来ており、そこにある項目は実際にもとの項目 f i である。この主張は単なる存在ではなくデータである。実際の証人が作り出され、ビットも等式も明示的に与えられる。

select (suc n) f (false ∷ v) = select n (λ i → f (suc i)) v
select (suc n) f (true ∷ v)  = selectStep (f zero) (select n (λ i → f (suc i)) v)

select-out : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) (f : Fin n → X) (v : Vec Bool n)
             (j : Fin (select n f v .fst))
           → Σ[ i ∶ Fin n ] ((lookup i v ≡ true) × (select n f v .snd j ≡ f i))

証明は定義と同じ再帰をたどる。false の場合は頭が落ちているため、尾で j に答えるもとの位置は、全ベクトルでは suc i ずり上げられる。局所的な step がこの簿記を、証人三つ組に対してまさに行う。

select-out     f []          ()
select-out (suc n) f (false ∷ v) j       = step (select-out n (λ i → f (suc i)) v j)
  where
  step : Σ[ i ∶ Fin n ] ((lookup i v ≡ true)
           × (select n (λ i → f (suc i)) v .snd j ≡ f (suc i)))

true の場合は二つの下位の場合に分かれる。選ばれた位置が最初なら、答えは頭そのものであり、select が頭をそのまま零番の枠として返すため、二つの等式はともに refl で成立する。そうでなければ再帰が尾の位置に答え、同じずらしがそのまま当てはまる。

       → Σ[ i ∶ Fin (suc n) ] ((lookup i (false ∷ v) ≡ true)
           × (select (suc n) f (false ∷ v) .snd j ≡ f i))
  step (i , e , q) = suc i , (e , q)
select-out (suc n) f (true ∷ v)  zero    = zero , (refl , refl)
select-out (suc n) f (true ∷ v)  (suc j) = step (select-out n (λ i → f (suc i)) v j)

第二の下位の場合は同じずらしの簿記を、頭がある状態で繰り返す。true ∷ v の選ばれた族は頭に尾の選択が続いたものなので、頭より先の位置は尾で答えられ、suc i へと写し戻される。二つの分岐が異なるのはこの配置替えだけであり、だからこそそれぞれに step が必要なのである。

  where
  step : Σ[ i ∶ Fin n ] ((lookup i v ≡ true)
           × (select n (λ i → f (suc i)) v .snd j ≡ f (suc i)))
       → Σ[ i ∶ Fin (suc n) ] ((lookup i (true ∷ v) ≡ true)
           × (select (suc n) f (true ∷ v) .snd (suc j) ≡ f i))

逆の仕様 select-in は、印づけられた項目はすべて選ばれることを述べる。ビットが true であるもとの位置 i には、項目が f i である選ばれた位置 j が対応する。ここでも主張は明示的なデータ、実際の j と経路である。どちらの向きも切断を含まないことが、後の所属の議論で選択の両側に実際の証人を渡せる理由である。

  step (i , e , q) = suc i , (e , q)

select-in : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) (f : Fin n → X) (v : Vec Bool n)
            (i : Fin n) → lookup i v ≡ true
          → Σ[ j ∶ Fin (select n f v .fst) ] (select n f v .snd j ≡ f i)
select-in     f []          ()      e

その証明は同じ再帰を逆向きに映する。空の族の位置は荒謬であり、false の場合は頭が真に印づけられることはないので仮定 e は false≢true と矛盾し、ずらされた位置は再帰する。true の場合は頭が零番の位置で答え、より深い位置は再帰する。

select-in (suc n) f (false ∷ v) zero    e = ⊥₀-rec (false≢true e)
select-in (suc n) f (false ∷ v) (suc i) e = select-in n (λ i → f (suc i)) v i e
select-in (suc n) f (true ∷ v)  zero    e = zero , refl
select-in (suc n) f (true ∷ v)  (suc i) e = step (select-in n (λ i → f (suc i)) v i e)
  where

最後の節は先頭付けの簿記を行う。尾で見つかった位置は、頭が前に付いた族では suc j となり、項目の等式はそのまま保たれる。二つの仕様を合わせると、選択はマスクが印づけたものより大きくも小さくもないことが分かるが、位置の対応の二つの仕方が互いに逆であるという主張はない。

  step : Σ[ j ∶ Fin (select n (λ i → f (suc i)) v .fst) ]
           (select n (λ i → f (suc i)) v .snd j ≡ f (suc i))
       → Σ[ j ∶ Fin (select (suc n) f (true ∷ v) .fst) ]
           (select (suc n) f (true ∷ v) .snd j ≡ f (suc i))
  step (j , q) = suc j , q

marks は絞り込みを逆向きに使う。マスクを読んで項目を残す代わりに、項目へのブールの判定 d を受け取り、それを記録するマスクを書き出す。一位置につき一ビットである。基底は空ベクトルで、ステップは頭で d を尋ね、ずらした族に再帰する。

marks : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) → (Fin n → X) → (X → Bool) → Vec Bool n
marks     f d = []
marks (suc n) f d = d (f zero) ∷ marks n (λ i → f (suc i)) d

marks-lookup : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) (f : Fin n → X) (d : X → Bool)
               (i : Fin n) → lookup i (marks n f d) ≡ d (f i)

marks-lookup は、記録されたマスクが各位置で判定に正しく答えることを裏付ける。marks n f d の位置 i を参照すると d (f i) が得られる。頭の場合は marks の計算規則により refl であり、深い位置は再帰する。この補題があるため、後の maskOf が書き出したマスクが与えられた部分集合を再現することを証明できるのである。

marks-lookup (suc n) f d zero    = refl
marks-lookup (suc n) f d (suc i) = marks-lookup n (λ i → f (suc i)) d i

真理値を一ビットに決定する

排中律は各命題をマスクで使うブール値へ変え、二つの仕様はそのビットから真と偽をそれぞれ読み戻す。

排中律が渡すのは判定であり、マスクが必要とするのは一ビットである。そこで両者をつなぐ必要がある。判定は定義の内部で求めるのではなく実引数として受け取る。これにより二つの往復補題は判定に対する照合で証明でき、真理値そのものも明示的に与え、往復の仕様が意図した命題を引数に取るようにする。

この変換は、数え上げの構成における排中律の具体的な用途の一つである。所属命題を判定し、その答えを一ビットとして記録する。

decideOf は判定を一ビットへ変える。yes は ⟨ P ⟩ の証明を運び、true として記録される。no は反証を運び、false として記録される。命題 P 自体は計算に関係せず、照合されるのは判定だけである。だからこそこの定義は一組の等式であって証明ではない。

decideOf : (P : hProp (ℓ-suc ℓ)) → Dec ⟨ P ⟩ → Bool
decideOf P (yes _) = true
decideOf P (no _) = false

decide-true : (P : hProp (ℓ-suc ℓ)) (s : Dec ⟨ P ⟩) → ⟨ P ⟩ → decideOf P s ≡ true
decide-true P (yes _) p = refl

二つの往復がビットを真理値へと結び戻す。decide-true は、⟨ P ⟩ の証明がビットを true に強いることを述べる。反証の分岐ではその証明自体が反証され、それが矛盾である。decide-sound は逆向きに読む。ビットが true なら ⟨ P ⟩ の証明が得られ、左の分岐から直接取られるか、右の分岐が false ≡ true を強いることになるために得られる。合わせて、渡された判定に対してビットが ⟨ P ⟩ の成立を忠実に答えることを示す。

decide-true P (no np) p = ⊥₀-rec (np p)

decide-sound : (P : hProp (ℓ-suc ℓ)) (s : Dec ⟨ P ⟩) → decideOf P s ≡ true → ⟨ P ⟩
decide-sound P (yes p) _ = p
decide-sound P (no _) e = ⊥₀-rec (false≢true e)

数え上げられた段階の定義可能部分集合

有限性はこの節を通して塔を一段ずつ上る。順序数 σ と段階 Lset σ の数え上げを固定し、目標は 𝒟ₒ (Lset σ) (この段階の定義可能部分集合全体) の数え上げを得ることである。与えられた数え上げの各項目はその段階の要素であるから、段階の小さな要素型の中に対応する名前を持つ。マスクはどの名前を残すかを指定し、part は残った名前を有限集合に張り合わせる。基本公理の章の finSet∈𝒟ₒ により、こうして張られた集合はその段階の定義可能部分集合であり、「これらの項目のいずれかに等しい」という有限論理和で定義される。逆に、段階の任意の定義可能部分集合 x も復元できる。各項目を x への決定可能な所属関係に従って印づけると、そのマスクで張った集合はちょうど x になる。ここで包含 𝒟ₒ∋⊆ が、x の各要素がそもそも数え上げに列挙されていることを保証する。したがって maskCount size 個のマスクがすべての定義可能部分集合を単に覆っており、これこそ Tally が要求する性質である。

Lset σ の要素は集合としてその段階にあるが、finSet には小さな要素型 ⟪ Lset σ ⟫ の名前が必要である。埋め込み ⟪ Lset σ ⟫↪ はその名前を集合として読む。所属は切り詰められたファイバーとして提示されるが、この埋め込みのファイバーは命題なので、∈-asFiber は切り詰めを消去し、明示的な名前と、それが item i に等しいというパスを返せる。index i と index-eq i は、このファイバー要素の二つの射影である。重複を許す有限な数え上げの任意のファイバーから添字を選ぶこととは異なり、そちらのファイバーは命題とは限らない。

module PowerStep (σ : S) (oσ : IsOrd σ) (t : Tally (Lset σ)) where

open Tally t
open FinOf σ oσ using ( finSet∈𝒟ₒ )

index : Fin size → ⟪ Lset σ ⟫
index i = ∈-asFiber {a = item i} {b = Lset σ} (inside i) .fst

index-eq : (i : Fin size) → ⟪ Lset σ ⟫↪ (index i) ≡ item i
index-eq i = ∈-asFiber {a = item i} {b = Lset σ} (inside i) .snd

chosen : Vec Bool size → Σ[ k ∶ ℕ ] (Fin k → ⟪ Lset σ ⟫)
chosen v = select size index v

part : Vec Bool size → S

part v = finSet (chosen v .fst) (λ j → ⟪ Lset σ ⟫↪ (chosen v .snd j))

part-def : (v : Vec Bool size) → ⟨ part v ∈ˢ 𝒟ₒ (Lset σ) ⟩
part-def v = finSet∈𝒟ₒ (chosen v .fst) (chosen v .snd)

part-out : (v : Vec Bool size) (y : S) → ⟨ y ∈ˢ part v ⟩
         → ∥ Σ[ i ∶ Fin size ] ((lookup i v ≡ true) × (item i ≡ y)) ∥₁

part-out v y y∈ = map₁ step
  (finSet-out (chosen v .fst) (λ j → ⟪ Lset σ ⟫↪ (chosen v .snd j)) y y∈)
  where
  step : Σ[ j ∶ Fin (chosen v .fst) ] (⟪ Lset σ ⟫↪ (chosen v .snd j) ≡ y)
       → Σ[ i ∶ Fin size ] ((lookup i v ≡ true) × (item i ≡ y))

  step (j , q) = out .fst
               , ( out .snd .fst
                 , (sym (index-eq (out .fst))
                    ∙ cong ⟪ Lset σ ⟫↪ (sym (out .snd .snd)) ∙ q) )
    where

    out : Σ[ i ∶ Fin size ] ((lookup i v ≡ true) × (chosen v .snd j ≡ index i))
    out = select-out size index v j

part-mem : (v : Vec Bool size) (i : Fin size) → lookup i v ≡ true
         → ⟨ item i ∈ˢ part v ⟩
part-mem v i e = subst (λ w → ⟨ w ∈ˢ part v ⟩) path

  (finSet-in (chosen v .fst) (λ j → ⟪ Lset σ ⟫↪ (chosen v .snd j))
    (⟪ Lset σ ⟫↪ (chosen v .snd (ins .fst))) ∣ ins .fst , refl ∣₁)
  where
  ins : Σ[ j ∶ Fin (chosen v .fst) ] (chosen v .snd j ≡ index i)
  ins = select-in size index v i e

  path : ⟪ Lset σ ⟫↪ (chosen v .snd (ins .fst)) ≡ item i
  path = cong ⟪ Lset σ ⟫↪ (ins .snd) ∙ index-eq i

maskOf : S → Vec Bool size
maskOf x = marks size item
  (λ y → decideOf (y ∈ˢ x) (SemV.decideMembership lem y x))

part-mask : (x : S) → ⟨ x ∈ˢ 𝒟ₒ (Lset σ) ⟩ → part (maskOf x) ≡ x

part-mask x x∈ = extensionalV (λ y → ⇔toPath (fwd y) (bwd y))
  where
  fwd : (y : S) → ⟨ y ∈ˢ part (maskOf x) ⟩ → ⟨ y ∈ˢ x ⟩
  fwd y y∈ = rec₁ ((y ∈ˢ x) .snd) step (part-out (maskOf x) y y∈)
    where

    step : Σ[ i ∶ Fin size ] ((lookup i (maskOf x) ≡ true) × (item i ≡ y))
         → ⟨ y ∈ˢ x ⟩
    step (i , e , q) = subst (λ w → ⟨ w ∈ˢ x ⟩) q
      (decide-sound (item i ∈ˢ x) (SemV.decideMembership lem (item i) x)
        (sym (marks-lookup size item

               (λ z → decideOf (z ∈ˢ x) (SemV.decideMembership lem z x)) i) ∙ e))
  bwd : (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ part (maskOf x) ⟩
  bwd y y∈x = rec₁ ((y ∈ˢ part (maskOf x)) .snd) step
    (onto y (𝒟ₒ∋⊆ (Lset σ) x x∈ y y∈x))
    where

    step : Σ[ i ∶ Fin size ] (item i ≡ y) → ⟨ y ∈ˢ part (maskOf x) ⟩
    step (i , q) = subst (λ w → ⟨ w ∈ˢ part (maskOf x) ⟩) q
      (part-mem (maskOf x) i
        (marks-lookup size item
           (λ z → decideOf (z ∈ˢ x) (SemV.decideMembership lem z x)) i
         ∙ decide-true (item i ∈ˢ x)
           (SemV.decideMembership lem (item i) x)

             (subst (λ w → ⟨ w ∈ˢ x ⟩) (sym q) y∈x)))

powerTally : Tally (𝒟ₒ (Lset σ))
powerTally = record
  { size   = maskCount size
  ; item   = λ j → part (maskAt size j)

  ; inside = λ j → part-def (maskAt size j)
  ; onto   = cover }
  where
  cover : (x : S) → ⟨ x ∈ˢ 𝒟ₒ (Lset σ) ⟩
        → ∥ Σ[ j ∶ Fin (maskCount size) ] (part (maskAt size j) ≡ x) ∥₁

  cover x x∈ = ∣ mask-onto size (maskOf x) .fst
               , (cong part (mask-onto size (maskOf x) .snd) ∙ part-mask x x∈) ∣₁

最小要素と整礎性

この節では、先につくった数え上げを使う側の議論を進める。型と、その上の三岐・非反射・推移的な関係を固定する。これは整列順序が要求する性質のうち整礎性を除くすべてである。手続き scan は有限族をたどり、截断を一切伴わずに、述語を満たし満たすものの中で最小である項目か、満たす項目が存在しないことの反駁を返す。長さについての素朴な再帰であり、各段階では外から与えられた判定手続きが頭部の述語を判定し、三岐性が頭部とそれまでの最良の候補を比較する。したがって走査自体は各点での決定可能性に相対して構成的であり、任意の述語について排中律を要求しない。有限族が型を単に被覆するとき、Search.Over.least は単に非空な決定可能述語の最小要素を与える。後の整礎性証明が必要とする特定の判定手続きは、本章の古典的仮定から供給される。

A 上の狭義関係 ≺ が三岐性・非反射性・推移性を満たすとする。整礎性は仮定せず、有限な被覆族から導く。述語 P に対し、Least P m は m が P を満たすことと、より小さい充足者がすべて矛盾を導くことを記録する。

module Search {A : Type (ℓ-suc ℓ)} (_≺_ : A → A → Type (ℓ-suc ℓ))
              (tri : (a b : A) → Tri (a ≺ b) (a ≡ b) (b ≺ a))
              (irr : (a : A) → a ≺ a → ⊥₀)
              (trans : (a b c : A) → a ≺ b → b ≺ c → a ≺ c) where

Least : (P : A → hProp (ℓ-suc ℓ)) → A → Type (ℓ-suc ℓ)

Least P m = ⟨ P m ⟩ × ((b : A) → ⟨ P b ⟩ → b ≺ m → ⊥₀)

Found : (P : A → hProp (ℓ-suc ℓ)) (n : ℕ) (f : Fin n → A) → Type (ℓ-suc ℓ)
Found P n f =
  (Σ[ i ∶ Fin n ] (⟨ P (f i) ⟩ × ((j : Fin n) → ⟨ P (f j) ⟩ → f j ≺ f i → ⊥₀)))
  ⊎ ((i : Fin n) → ⟨ P (f i) ⟩ → ⊥₀)

scan : (P : A → hProp (ℓ-suc ℓ))
     → ((a : A) → Dec ⟨ P a ⟩)
     → (n : ℕ) (f : Fin n → A) → Found P n f
scan P decP     f = inr (λ ())
scan P decP (suc n) f = combine (scan P decP n (λ i → f (suc i))) (decP (f zero))
  where
  combine : Found P n (λ i → f (suc i))

          → Dec ⟨ P (f zero) ⟩ → Found P (suc n) f
  combine (inl (i , pi , mi)) (yes p₀) = decide (tri (f zero) (f (suc i)))
    where
    decide : Tri (f zero ≺ f (suc i)) (f zero ≡ f (suc i)) (f (suc i) ≺ f zero)
           → Found P (suc n) f

    decide (lt h) = inl (zero , (p₀ , minAt))
      where
      minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f zero → ⊥₀
      minAt zero    pj hj = irr (f zero) hj
      minAt (suc j) pj hj = mi j pj (trans (f (suc j)) (f zero) (f (suc i)) hj h)

    decide (eq h) = inl (suc i , (pi , minAt))
      where
      minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f (suc i) → ⊥₀
      minAt zero    pj hj = irr (f (suc i)) (subst (λ w → w ≺ f (suc i)) h hj)
      minAt (suc j) pj hj = mi j pj hj

    decide (gt h) = inl (suc i , (pi , minAt))
      where
      minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f (suc i) → ⊥₀
      minAt zero    pj hj = irr (f (suc i)) (trans (f (suc i)) (f zero) (f (suc i)) h hj)
      minAt (suc j) pj hj = mi j pj hj

  combine (inl (i , pi , mi)) (no n₀) = inl (suc i , (pi , minAt))
    where
    minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f (suc i) → ⊥₀
    minAt zero    pj hj = ⊥₀-rec (n₀ pj)
    minAt (suc j) pj hj = mi j pj hj

  combine (inr none) (yes p₀) = inl (zero , (p₀ , minAt))
    where
    minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f zero → ⊥₀
    minAt zero    pj hj = irr (f zero) hj
    minAt (suc j) pj hj = ⊥₀-rec (none j pj)

  combine (inr none) (no n₀) = inr atAll
    where
    atAll : (i : Fin (suc n)) → ⟨ P (f i) ⟩ → ⊥₀
    atAll zero    p = n₀ p
    atAll (suc i) p = none i p

module Over (n : ℕ) (f : Fin n → A)
            (cov : (a : A) → ∥ Σ[ i ∶ Fin n ] (f i ≡ a) ∥₁) where

least : (P : A → hProp (ℓ-suc ℓ)) → ((a : A) → Dec ⟨ P a ⟩)
      → ∥ Σ[ a ∶ A ] ⟨ P a ⟩ ∥₁ → Σ[ m ∶ A ] Least P m
least P decP h = decide (scan P decP n f)
  where

  nowhere : ((i : Fin n) → ⟨ P (f i) ⟩ → ⊥₀) → ⊥₀
  nowhere none = rec₁ isProp⊥ atWitness h
    where
    atWitness : Σ[ a ∶ A ] ⟨ P a ⟩ → ⊥₀
    atWitness (a , pa) = rec₁ isProp⊥

      (λ { (i , q) → none i (subst (λ w → ⟨ P w ⟩) (sym q) pa) }) (cov a)
  decide : Found P n f → Σ[ m ∶ A ] Least P m
  decide (inl (i , pi , mi)) = f i , (pi , everywhere)
    where
    everywhere : (b : A) → ⟨ P b ⟩ → b ≺ f i → ⊥₀

    everywhere b pb hb = rec₁ isProp⊥
      (λ { (j , q) → mi j (subst (λ w → ⟨ P w ⟩) (sym q) pb)
                          (subst (λ w → w ≺ f i) (sym q) hb) }) (cov b)
  decide (inr none) = ⊥₀-rec (nowhere none)

wellFounded : WellFounded _≺_

wellFounded a = fromDec (lem (Acc _≺_ a , isPropAcc a))
  where
  fromDec : Dec (Acc _≺_ a) → Acc _≺_ a
  fromDec (yes h) = h
  fromDec (no nh) = ⊥₀-rec (found .snd .fst (acc below))

    where
    NotAcc : A → hProp (ℓ-suc ℓ)
    NotAcc b = (Acc _≺_ b → ⊥₀) , isProp→ isProp⊥
    found : Σ[ m ∶ A ] Least NotAcc m
    found = least NotAcc (λ b → lem (NotAcc b)) ∣ a , nh ∣₁

    below : (b : A) → b ≺ found .fst → Acc _≺_ b
    below b hb = pick (lem (Acc _≺_ b , isPropAcc b))
      where
      pick : Dec (Acc _≺_ b) → Acc _≺_ b
      pick (yes h) = h

      pick (no nb) = ⊥₀-rec (found .snd .snd b nb hb)

最初の相違

この節は、有限段階が担う順序を定義する。集合 A と、集合の上の関係 R を固定する。R は A の要素の上の順序と読む。A の二つの部分集合は、どこで食い違うかによって比較される。「x が y に先行する」ことの証人は、A の要素 z であって、y に属し x には属さず、かつ x と y が z の下で一致するものである。つまり R が z の前に置く A の各要素は、一方に属するならばちょうど他方にも属するということである。逆向きに読めば、z が最初の相違点であり、それを持つのが y である。関係 precedes R A はそのような証人の截断された存在であり、非反射性は直ちに成り立ち、まったく仮定を要しない。x 自身に対する証人は x に属すると同時に属さないことになるからである。続く証明は基底の順序への仮定から三岐性と推移性を確立し、整礎性には有限性を用いる。

二つの材料は別々に述べられる。Agrees R A x y z は、R が z の前に置く A の各要素 w について、x への所属と y への所属が双方向に一致することを言う。Witness R A x y z は続いて完全な証人を組み立てる。z は A に属し、y に属し、x には属さず、その下で一致が成り立つ、ということである。所属条項の向きこそが、比較でどちらが勝つかを決める。

Agrees : (R : S → S → hProp (ℓ-suc ℓ)) (A x y z : S) → Type (ℓ-suc ℓ)
Agrees R A x y z = (w : S) → ⟨ w ∈ˢ A ⟩ → ⟨ R w z ⟩
                 → (⟨ w ∈ˢ x ⟩ → ⟨ w ∈ˢ y ⟩) × (⟨ w ∈ˢ y ⟩ → ⟨ w ∈ˢ x ⟩)

Witness : (R : S → S → hProp (ℓ-suc ℓ)) (A x y z : S) → Type (ℓ-suc ℓ)
Witness R A x y z =

precedes R A x y は、そのような証人が単に存在するという命題であり、squash₁ とともに真理値としてまとめられている。証人は截断の後ろに隠れているので、主張されるのはその存在だけで、z が選ばれることはない。非反射性はそこで一行で済む。截断を命題である空の型へと消去すれば、z ∈ x と z ∉ x を同時に持つ証人が現れ、第二の条項を第一に施せば矛盾である。

  ⟨ z ∈ˢ A ⟩ × ⟨ z ∈ˢ y ⟩ × (⟨ z ∈ˢ x ⟩ → ⊥₀) × Agrees R A x y z

precedes : (R : S → S → hProp (ℓ-suc ℓ)) (A : S) → S → S → hProp (ℓ-suc ℓ)
precedes R A x y = ∥ Σ[ z ∶ S ] Witness R A x y z ∥₁ , squash₁

precedes-irrefl : (R : S → S → hProp (ℓ-suc ℓ)) (A x : S) → ⟨ precedes R A x x ⟩ → ⊥₀
precedes-irrefl R A x = rec₁ isProp⊥ (λ { (z , _ , z∈ , z∉ , _) → z∉ z∈ })

最初の相違による順序の推移性と三岐性は、基底の順序への仮定を indeed 必要とし、しかも両者は異なる仮定を要するので、一つのモジュールにまとめられる。そのパラメータは、A の要素の上での R の三岐性と推移性、およびそれらの要素の上での R の最小要素原理である。塔の中では、これらは下の段階から供給される。

推移性は二つの証人の比較である。x が p で y に先行し、y が q で z に先行するなら、p は y に属し q は属さないので p と q は等しくありえず、両者のうち小さいほうが x が z に先行することの証人となる。どちらの枝でも確かめることは同じ二つである。小さいほうの点が正しい側にあることと、その下での一致が合成できることである。

このモジュールは、最初の相違の順序が受け継ぐ三つの前提を集める。baseTri と baseTrans は、A の要素に制限した R が三岐かつ推移的であると言い、baseLeast は A の上の最小要素原理である。A の要素のある性質が単に非空であることから、その性質を満たし、より小さい A の要素がどれも満たさない要素を返す。結論の形に注意してほしい。呼び出し側が実際の最小要素を必要とするので、截断ではなく明示的なデータである。

module Difference (R : S → S → hProp (ℓ-suc ℓ)) (A : S)
  (baseTri : (a b : S) → ⟨ a ∈ˢ A ⟩ → ⟨ b ∈ˢ A ⟩ → Tri ⟨ R a b ⟩ (a ≡ b) ⟨ R b a ⟩)
  (baseTrans : (a b c : S) → ⟨ R a b ⟩ → ⟨ R b c ⟩ → ⟨ R a c ⟩)
  (baseLeast : (P : S → hProp (ℓ-suc ℓ)) → ∥ Σ[ a ∶ S ] (⟨ a ∈ˢ A ⟩ × ⟨ P a ⟩) ∥₁
             → Σ[ m ∶ S ] (⟨ m ∈ˢ A ⟩ × ⟨ P m ⟩
                 × ((b : S) → ⟨ b ∈ˢ A ⟩ → ⟨ P b ⟩ → ⟨ R b m ⟩ → ⊥₀)))
  where

precedes-trans : (x y z : S) → ⟨ precedes R A x y ⟩ → ⟨ precedes R A y z ⟩
               → ⟨ precedes R A x z ⟩
precedes-trans x y z hxy hyz =

  rec₁ squash₁ (λ wp → rec₁ squash₁ (both wp) hyz) hxy
  where
  both : Σ[ p ∶ S ] Witness R A x y p → Σ[ q ∶ S ] Witness R A y z q
       → ⟨ precedes R A x z ⟩
  both (p , p∈A , p∈y , p∉x , agp) (q , q∈A , q∈z , q∉y , agq) =

    decide (baseTri p q p∈A q∈A)
    where
    decide : Tri ⟨ R p q ⟩ (p ≡ q) ⟨ R q p ⟩ → ⟨ precedes R A x z ⟩
    decide (lt h) = ∣ p , (p∈A , (agq p p∈A h .fst p∈y , (p∉x , ag))) ∣₁
      where