module PLFA.Quantifiers where import Relation.Binary.PropositionalEquality as Eq open Eq -- using (_≡_; refl) open Eq.≡-Reasoning open import Data.Nat using (ℕ; zero; suc; _+_; _*_) open import Relation.Nullary using (¬_) open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) open import Data.Sum using (_⊎_; inj₁; inj₂) open import PLFA.Isomorphism using (_≃_; extensionality) ---------------------------------------------------------------------- data even : ℕ → Set data odd : ℕ → Set data even where even-zero : even zero even-suc : ∀ {n : ℕ} → odd n ------------ → even (suc n) data odd where odd-suc : ∀ {n : ℕ} → even n ----------- → odd (suc n) ---------------------------------------------------------------------- -- * -- Universals postulate +-comm : ∀ m n → m + n ≡ n + m -- +-comm = λ m n → {!!} -- the evidence (proof term) for a propostion of the form -- ∀ (x : A) (B x) -- is a *dependent* function where the result *type* can depend on the input *value* -- λ (x : A) (M x) -- corresponds to introduction of a universal type -- often named ∀-I -- compare to implication: -- A → B -- evidence is a function -- λ x → M -- here it's only that the result *value* can depend on the input *value*, but the result *type* is fixed once and forall. {- Naming of dependent features is a nightmare!! Another name for dependent function: dependent product In a product: A₁ × A₂ × ⋯ × An each Aᵢ can be a different type Can regard that as a function from (i : { 1, 2, ⋯, n }) → A i Generalizing ...: Π (i : ℕ) → A i can avoid this naming confusion by using the name Π-type. -} -- ∀-elim ∀-elim : ∀ {A : Set} {B : A → Set} → (∀ (a : A) → (B a)) → (a : A) → -------------------- B a ∀-elim f a = f a -- * -- Existentials -- ∃ (a : A) (B a) -- evidence is a pair of a witness for a and a proof that B a holds for that witness -- before: product A × B --- here A and B are independent -- now: product with dependency where the *type* of the second component depends on the *value* of the first component record Σ (A : Set) (B : A → Set) : Set where constructor <_,_> field proj₁ : A proj₂ : B proj₁ _ : Σ ℕ (λ n → n ≡ 0) _ = < 0 , refl > -- _ = record { proj₁ = 42 ; proj₂ = {!!} } -- can't complete! -- _ = record { proj₁ = 0 ; proj₂ = refl } Σ-syntax = Σ infix 2 Σ-syntax syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B _ : Σ[ n ∈ ℕ ] n ≡ 0 _ = < 0 , refl > {- more about naming... there are a number of different names for Σ-types * dependent product * dependent sum: consider a sum type A₁ + A₂ + ⋯ + An viewed from another perspective: the elments are pairs where * the first component is an element of { 1, 2, ⋯ , n } * the second component is an element of A i -} ∃ : ∀ {A : Set} (B : A → Set) → Set -- ∃ {A} f = Σ A f ∃ f = Σ _ f ∃-syntax = ∃ syntax ∃-syntax (λ x → B) = ∃[ x ] B ∃-elim : ∀ {A : Set}{B : A → Set} {C : Set} → (∀ x → B x → C) → ∃[ x ] B x → -------------------- C ∃-elim f < a , ba > = f a ba -- ∀∃-currying : {A C : Set}{B : A → Set} → (∀ x → B x → C) ≃ (∃[ x ] B x → C) ∀∃-currying {A}{C}{B} = record { to = λ{ f < a , ba > → f a ba }; from = λ f a ba → f < a , ba > ; from∘to = λ f → refl ; to∘from = λ g → refl } -- existential example even-∃ : ∀ {n : ℕ} → even n → ∃[ m ] ( m * 2 ≡ n) odd-∃ : ∀ {n : ℕ} → odd n → ∃[ m ] (1 + m * 2 ≡ n) even-∃ even-zero = < zero , refl > even-∃ (even-suc odd-n) with odd-∃ odd-n ... | < m , refl > = < suc m , refl > -- alternatively: -- ... | < m , 1+m*2=n > = < (suc m) , (cong suc 1+m*2=n) > odd-∃ (odd-suc even-n) with even-∃ even-n ... | < m , refl > = < m , refl > -- how about the reverse direction? ∃-even : ∀ {n : ℕ} → ∃[ m ] ( m * 2 ≡ n) → even n ∃-odd : ∀ {n : ℕ} → ∃[ m ] (1 + m * 2 ≡ n) → odd n ∃-even < zero , refl > = even-zero ∃-even {suc .(suc (m * 2))} < suc m , refl > = even-suc (∃-odd < m , refl >) ∃-odd < m , refl > = odd-suc (∃-even < m , refl >) -- * -- Existentials, Universals, and Negation ¬∃≃∀¬ : ∀ {A : Set} {B : A → Set} → (¬ ∃[ x ] B x) ≃ ∀ x → ¬ B x ¬∃≃∀¬ = record { to = λ ¬∃b a ba → ¬∃b < a , ba > ; from = λ{ a→¬b < a , ba > → a→¬b a ba }; from∘to = λ ¬∃b → refl ; to∘from = λ ∀¬b → refl }