Prop

Prop

Prop는 Agda의 정의적 증명-비관련(definitionally proof-irrelevant) 명제의 내장 sort예요. Set sort와 비슷하지만, Prop의 타입에 있는 모든 원소는 (정의적으로) 같다고 간주돼요.

Prop의 구현은 Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau의 POPL 2019 논문 'Definitional Proof-Irrelevance without K'에 기반해요.

이것은 --prop 옵션으로 보호되는 Agda의 실험적 확장이에요.

사용 (Usage)

Set과 마찬가지로 Prop 안에서 데이터나 레코드 타입으로 새 타입을 정의할 수 있어요:

data ⊥ : Prop where

record ⊤ : Prop where
  constructor tt

Prop의 데이터 타입에서 Set의 타입으로의 함수를 정의할 때, 패턴 매칭은 부정 패턴 ()로 제한돼요:

absurd : (A : Set) → ⊥ → A
absurd A ()

Set과 달리 Prop의 타입의 모든 원소는 정의적으로 같아요. 이는 모든 absurd 적용이 같다는 것을 의미해요:

only-one-absurdity : {A : Set} → (p q : ⊥) → absurd A p ≡ absurd A q
only-one-absurdity p q = refl

Prop의 데이터 타입에 대한 패턴 매칭이 제한되어 있으므로, Prop의 타입을 귀납 데이터 타입보다 재귀 함수로 정의하는 것이 권장돼요. 예를 들어 자연수에 대한 관계 _≤_는 다음과 같이 정의할 수 있어요:

_≤_ : Nat → Nat → Prop
zero  ≤ y     = ⊤
suc x ≤ zero  = ⊥
suc x ≤ suc y = x ≤ y

_≤_에 대한 귀납 원리는 Nat 타입의 인자에 매칭하여 정의할 수 있어요:

module _ (P : (m n : Nat) → Set)
  (pzy : (y : Nat) → P zero y)
  (pss : (x y : Nat) → P x y → P (suc x) (suc y)) where

  ≤-ind : (m n : Nat) → m ≤ n → P m n
  ≤-ind zero    y       pf = pzy y
  ≤-ind (suc x) (suc y) pf = pss x y (≤-ind x y pf)
  ≤-ind (suc _) zero    ()

_≤_를 Prop의 데이터 타입으로 정의하는 것도 가능하지만, 매칭의 제한 때문에 그 버전은 사용하기 어렵다는 점에 주의하세요.

Set의 레코드 타입을 정의할 때 필드의 타입은 Set과 Prop 둘 다일 수 있어요. 예를 들어:

record Fin (n : Nat) : Set where
  constructor _[_]
  field
    ⟦_⟧   : Nat
    proof : suc ⟦_⟧ ≤ n
open Fin

Fin-≡ : ∀ {n} (x y : Fin n) → ⟦ x ⟧ ≡ ⟦ y ⟧ → x ≡ y
Fin-≡ x y refl = refl

Prop의 예측적 계층 (The predicative hierarchy of Prop)

Set과 마찬가지로 Agda에는 정렬의 예측적 계층 Prop₀ (= Prop), Prop₁, Prop₂, …, Propω₀ (= Propω), Propω₁, Propω₂, …이 있으며, 여기서 Prop₀ : Set₁, Prop₁ : Set₂, Prop₂ : Set₃, …, Propω₀ : Setω₁, Propω₁ : Setω₂, Propω₂ : Setω₃ 등이에요.

Set처럼 Prop도 유니버스 다형성(유니버스 레벨 참고)을 지원하므로 각 ℓ : Level에 대해 sort Prop ℓ이 있어요.

예를 들어:

True : ∀ {ℓ} → Prop (lsuc ℓ)
True {ℓ} = ∀ (P : Prop ℓ) → P → P

∀ {ℓ} → Prop (lsuc ℓ)(그리고 마찬가지로 임의의 ∀ {ℓ} → Prop (t ℓ))은 Propω가 아니라 Setω에 산다는 점에 주의하세요.

명제적 스쿼시 타입 (The propositional squash type)

Prop ℓ에서 데이터 타입을 정의할 때, 임의의 ℓ' ≤ ℓ에 대해 Set ℓ'의 인자를 갖는 생성자를 가지는 것이 허용돼요. 예를 들어, 이는 명제적 스쿼시 타입과 그 소거자를 정의할 수 있게 해요:

data Squash {ℓ} (A : Set ℓ) : Prop ℓ where
  squash : A → Squash A

squash-elim : ∀ {ℓ₁ ℓ₂} (A : Set ℓ₁) (P : Prop ℓ₂) → (A → P) → Squash A → P
squash-elim A P f (squash x) = f x

이 타입은 .A를 Squash A로 대체해 Agda의 기존 비관련 인자(irrelevance 참고)를 시뮬레이션할 수 있게 해요.

제한 사항 (Limitations)

Prop에서 동일성 타입을 다음과 같이 정의하는 것이 가능해요:

data _≐_ {ℓ} {A : Set ℓ} (x : A) : A → Prop ℓ where
  refl : x ≐ x

하지만 패턴 매칭의 제한 때문에 대응하는 소거자는 정의할 수 없어요. 결과적으로 이 동일성 타입은 불가능한 방정식을 반박하는 데만 유용해요:

0≢1 : 0 ≐ 1 → ⊥
0≢1 ()

더 알아보기 (Learn more)