diff --git a/index.md b/index.md index fa93c616..079990ee 100644 --- a/index.md +++ b/index.md @@ -21,17 +21,17 @@ http://homepages.inf.ed.ac.uk/wadler/ - [Basics: Functional Programming in Agda]({{ "/Basics" | relative_url }}) --> - - [Naturals: Natural numbers]({{ "/Naturals" | relative_url }}) - - [Properties: Proof by induction]({{ "/Properties" | relative_url }}) - - [PropertiesAns: Solutions to exercises]({{ "/PropertiesAns" | relative_url }}) - - [Relations: Inductive Definition of Relations]({{ "/Relations" | relative_url }}) - - [RelationsAns: Solutions to exercises]({{ "/RelationsAns" | relative_url }}) - - [Logic: Logic]({{ "/Logic" | relative_url }}) - - [LogicAns: Solutions to exercises]({{ "/LogicAns" | relative_url }}) + - [Naturals: Natural numbers](Naturals) + - [Properties: Proof by induction](Properties) + - [PropertiesAns: Solutions to exercises](PropertiesAns) + - [Relations: Inductive Definition of Relations](Relations) + - [RelationsAns: Solutions to exercises](RelationsAns) + - [Logic: Logic](Logic) + - [LogicAns: Solutions to exercises](LogicAns) ## Part 2: Programming Language Foundations - - [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }}) - - [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }}) - - [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }}) + - [Maps: Total and Partial Maps](Maps) + - [Stlc: The Simply Typed Lambda-Calculus](Stlc) + - [StlcProp: Properties of STLC](StlcProp) diff --git a/out/Logic.md b/out/Logic.md index 779143e5..9754218b 100644 --- a/out/Logic.md +++ b/out/Logic.md @@ -3825,7 +3825,7 @@ operator. >4 _,_ {% endraw %} @@ -7727,114 +7727,130 @@ isomorphism. ## Implication is function Given two propositions `A` and `B`, the implication `A → B` holds if -whenever `A` holds then `B` must also hold. We formalise this idea in -terms of the function type. Evidence that `A → B` holds is of the form +whenever `A` holds then `B` must also hold. We formalise implication using +the function type, which has appeared throughout this book. - λ (x : A) → N +Evidence that `A → B` holds is of the form -where `N` is a term of type `B` containing as a free variable `x` of type `A`. -In other words, evidence that `A → B` holds is a function that converts -evidence that `A` holds into evidence that `B` holds. + λ (x : A) → N[x] +where `N[x]` is a term of type `B` containing as a free variable `x` of type `A`. +Given a term `L` providing evidence that `A → B` holds, and a term `M` +providing evidence that `A` holds, the term `L M` provides evidence that +`B` holds. In other words, evidence that `A → B` holds is a function that +converts evidence that `A` holds into evidence that `B` holds. + +Put another way, if we know that `A → B` and `A` both hold, +then we may conclude that `B` holds. In medieval times, this rule was +known by the name *modus ponens*. + +If we introduce an implication and then immediately eliminate it, we can +always simplify the resulting term. Thus + + (λ (x : A) → N[x]) M + +simplifies to `N[M]` of type `B`, where `N[M]` stands for the term `N[x]` with each +free occurrence of `x` replaced by `M` of type `A`. + + Implication binds less tightly than any other operator. Thus, `A ⊎ B → B ⊎ A` parses as `(A ⊎ B) → (B ⊎ A)`. @@ -7849,336 +7865,336 @@ type `Bool` with two members and a type `Tri` with three members, as defined earlier. The the type `Bool → Tri` has nine (that is, three squared) members: - {true→aa;false→aa} {true→aa;false→bb} {true→aa;false→cc} - {true→bb;false→aa} {true→bb;false→bb} {true→bb;false→cc} - {true→cc;false→aa} {true→cc;false→bb} {true→cc;false→cc} + {true → aa; false → aa} {true → aa; false → bb} {true → aa; false → cc} + {true → bb; false → aa} {true → bb; false → bb} {true → bb; false → cc} + {true → cc; false → aa} {true → cc; false → bb} {true → cc; false → cc} For example, the following function enumerates all possible arguments of the type `Bool → Tri`: 
{% raw %}
-→-count : (Bool → Tri) → ℕ
 →-count f with f true | f false
 ...                       | aa    | aa      = 1
 ...                       | aa    | bb      = 2  
 ...                       | aa    | cc      = 3
 ...                       | bb    | aa      = 4
 ...                       | bb    | bb      = 5
 ...                       | bb    | cc      = 6
 ...                       | cc    | aa      = 7
 ...                       | cc    | bb      = 8
 ...                       | cc    | cc      = 9
 {% endraw %}
@@ -8197,483 +8213,483 @@ and evidence that `B` holds can return evidence that `C` holds. This isomorphism sometimes goes by the name *currying*. The proof of the right inverse requires extensionality. 
{% raw %}
-postulate
   extensionality : ∀ {A B : Set} → {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
   
 currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
 currying =
   record
     { to   =  λ f → λ { (x , y) → f x y }
     ; fro  =  λ g → λ x → λ y → g (x , y)
     ; invˡ =  λ f → refl
     ; invʳ =  λ g → extensionality (λ { (x , y) → refl })
     }
 {% endraw %}
@@ -8713,452 +8729,452 @@ That is, the assertion that if either `A` holds or `B` holds then `C` holds is the same as the assertion that if `A` holds then `C` holds and if `B` holds then `C` holds. 
{% raw %}
-→-distributes-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
 →-distributes-⊎ =
   record
     { to   = λ f → ( (λ x → f (inj₁ x)) , (λ y → f (inj₂ y)) ) 
     ; fro  = λ {(g , h) → λ { (inj₁ x) → g x ; (inj₂ y) → h y } }
     ; invˡ = λ f → extensionality (λ { (inj₁ x) → refl ; (inj₂ y) → refl })
     ; invʳ = λ {(g , h) → refl}
     }
 {% endraw %}
@@ -9173,499 +9189,499 @@ is the same as the assertion that if `A` holds then `B` holds and if `A` holds then `C` holds. The proof requires that we recognise the eta rule for products, which states that `(fst w , snd w) ≡ w` for any product `w`. 
{% raw %}
-postulate
   η-× : ∀ {A B : Set} → ∀ (w : A × B) → (fst w , snd w) ≡ w
 
 →-distributes-× : ∀ {A B C : Set} → (A → B × C) ≃ ((A → B) × (A → C))
 →-distributes-× =
   record
     { to   = λ f → ( (λ x → fst (f x)) , (λ y → snd (f y)) ) 
     ; fro  = λ {(g , h) → (λ x → (g x , h x))}
     ; invˡ = λ f → extensionality (λ x → η-× (f x))
     ; invʳ = λ {(g , h) → refl}
     }
 {% endraw %}
@@ -9676,1058 +9692,1058 @@ rule for products, which states that `(fst w , snd w) ≡ w` for any product `w` Products distributes over sum, up to isomorphism. The code to validate this fact is similar in structure to our previous results. 
{% raw %}
-×-distributes-⊎ : ∀ {A B C : Set} → ((A ⊎ B) × C) ≃ ((A × C) ⊎ (B × C))
 ×-distributes-⊎ =
   record
     { to   = λ { ((inj₁ x) , z) → (inj₁ (x , z)) 
                ; ((inj₂ y) , z) → (inj₂ (y , z))
                }
     ; fro  = λ { (inj₁ (x , z)) → ((inj₁ x) , z)
                ; (inj₂ (y , z)) → ((inj₂ y) , z)
                }
     ; invˡ = λ { ((inj₁ x) , z) → refl
                ; ((inj₂ y) , z) → refl
                }
     ; invʳ = λ { (inj₁ (x , z)) → refl
                ; (inj₂ (y , z)) → refl
                }               
     }
 {% endraw %}
Sums do not distribute over products up to isomorphism, but it is an embedding. 
{% raw %}
-⊎-distributes-× : ∀ {A B C : Set} → ((A × B) ⊎ C) ≲ ((A ⊎ C) × (B ⊎ C))
 ⊎-distributes-× =
   record
     { to   = λ { (inj₁ (x , y)) → (inj₁ x , inj₁ y)
                ; (inj₂ z)       → (inj₂ z , inj₂ z)
                }
     ; fro  = λ { (inj₁ x , inj₁ y) → (inj₁ (x , y))
                ; (inj₁ x , inj₂ z) → (inj₂ z)
                ; (inj₂ z , _ )     → (inj₂ z)
                }
     ; invˡ = λ { (inj₁ (x , y)) → refl
                ; (inj₂ z)       → refl
                }
     }
 {% endraw %}
@@ -10756,48 +10772,48 @@ Given a proposition `A`, the negation `¬ A` holds if `A` cannot hold. We formalise this idea by declaring negation to be the same as implication of false. 
{% raw %}
-¬_ : Set → Set
 ¬ A = A → ⊥
 {% endraw %}
@@ -10815,84 +10831,84 @@ that `A` holds into evidence that `⊥` holds. Given evidence that both `¬ A` and `A` hold, we can conclude that `⊥` holds. In other words, if both `¬ A` and `A` hold, then we have a contradiction. 
{% raw %}
-¬-elim : ∀ {A : Set} → ¬ A → A → ⊥
 ¬-elim ¬a a = ¬a a
 {% endraw %}
@@ -10903,15 +10919,15 @@ means that `¬a` must be a function of type `A → ⊥`, and hence the applicati We set the precedence of negation so that it binds more tightly than disjunction and conjunction, but more tightly than anything else. 
{% raw %}
-infix 3 ¬_
 {% endraw %}
@@ -10921,80 +10937,80 @@ In *classical* logic, we have that `A` is equivalent to `¬ ¬ A`. As we discuss below, in Agda we use *intuitionistic* logic, wher we have only half of this equivalence, namely that `A` implies `¬ ¬ A`. 
{% raw %}
-¬¬-intro : ∀ {A : Set} → A → ¬ ¬ A
 ¬¬-intro a ¬a = ¬a a
 {% endraw %}
@@ -11007,96 +11023,96 @@ shown `¬ ¬ A`. We cannot show that `¬ ¬ A` implies `A`, but we can show that `¬ ¬ ¬ A` implies `¬ A`. 
{% raw %}
-¬¬¬-elim : ∀ {A : Set} → ¬ ¬ ¬ A → ¬ A
 ¬¬¬-elim ¬¬¬a a = ¬¬¬a (¬¬-intro a)
 {% endraw %}
@@ -11110,120 +11126,120 @@ can conclude `¬ ¬ A` (evidenced by `¬¬-intro a`). Then from Another law of logic is the *contrapositive*, stating that if `A` implies `B`, then `¬ B` implies `¬ A`. 
{% raw %}
-contrapositive : ∀ {A B : Set} → (A → B) → (¬ B → ¬ A)
 contrapositive a→b ¬b a = ¬b (a→b a)
 {% endraw %}
@@ -11244,40 +11260,40 @@ we know for arithmetic, where Indeed, there is exactly one proof of `⊥ → ⊥`. 
{% raw %}
-id : ⊥ → ⊥
 id x = x
 {% endraw %}
@@ -11289,114 +11305,114 @@ including a variant of the story from Call-by-Value is Dual to Call-by-Name.] The law of the excluded middle is irrefutable. 
{% raw %}
-excluded-middle-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
 excluded-middle-irrefutable k = k (inj₂ (λ a → k (inj₁ a)))
 {% endraw %}
@@ -11449,497 +11465,497 @@ a disjoint sum. **Exercise** Prove the following six formulas are equivalent. 
{% raw %}
-lone ltwo : Level
 lone = lsuc lzero
 ltwo = lsuc lone
 
 ¬¬-elim excluded-middle peirce implication de-morgan : Set lone
 ¬¬-elim = ∀ {A : Set} → ¬ ¬ A → A
 excluded-middle = ∀ {A : Set} → A ⊎ ¬ A
 peirce = ∀ {A B : Set} → (((A → B) → A) → A)
 implication = ∀ {A B : Set} → (A → B) → ¬ A ⊎ B
 de-morgan = ∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B
 de-morgan′ = ∀ {A B : Set} → ¬ (¬ A ⊎ ¬ B) → A × B
 {% endraw %}
@@ -11957,142 +11973,551 @@ of `double-negation` and the others defines a type, we need to use ## Universals +Given a variable `x` of type `A` and a proposition `B[x]` which +contains `x` as a free variable, the universally quantified +proposition `∀ (x : A) → B[x]` holds if for every term `M` of type +`A` the proposition `B[M]` holds. Here `B[M]` stands for +the proposition `B[x]` with each free occurrence of `x` replaced by +`M`. The variable `x` appears free in `B[x]` but bound in +`∀ (x : A) → B[x]`. We formalise universal quantification using the +dependent function type, which has appeared throughout this book. + +Evidence that `∀ (x : A) → B[x]` holds is of the form + + λ (x : A) → N[x] + +where `N[x]` is a term of type `B[x]`; here `N[x]` is a term and `B[x]` +is a proposition (or type) both containing as a free variable `x` of +type `A`. Given a term `L` providing evidence that `∀ (x : A) → B[x]` +holds and a term `M` of type `A`, the term `L M` provides evidence +that `B[M]` holds. In other words, evidence that `∀ (x : A) → B[x]` +holds is a function that converts a term `M` of type `A` into evidence +that `B[M]` holds. + +Put another way, if we know that `∀ (x : A) → B[x]` holds and that `M` +is a term of type `A` then we may conclude that `B[M]` holds. In +medieval times, this rule was known by the name *dictum de omni*. + +If we introduce a universal and the immediately eliminate it, we can +always simplify the resulting term. Thus + + (λ (x : A) → N[x]) M + +simplifies to `N[M]` of type `B[M]`, where `N[M]` stands for the term +`N[x]` with each free occurrence of `x` replaced by `M` of type `A`. + +Unlike with conjunction, disjunction, and implication, there is no simple +analogy between universals and arithmetic. + + ## Existentials +Given a variable `x` of type `A` and a proposition `B[x]` which +contains `x` as a free variable, the existentially quantified +proposition `∃ (λ (x : A) → B[x])` holds if for some term `M` of type +`A` the proposition `B[M]` holds. Here `B[M]` stands for +the proposition `B[x]` with each free occurrence of `x` replaced by +`M`. The variable `x` appears free in `B[x]` but bound in +`∃ (λ (x : A) → B[x])`. + +It is common to adopt a notation such as `∃[ x : A ]→ B[x]`, +which introduces `x` as a bound variable of type `A` that appears +free in `B[x]` and bound in `∃[ x : A ]→ B[x]`. We won't do +that here, but instead use the lambda notation built-in to Agda +to introduce `x` as a bound variable. + +We formalise existential quantification by declaring a suitable +inductive type. +
{% raw %}
+data ∃ : ∀ {A : Set} → (A → Set) → Set where
+  _,_ : ∀ {A : Set} {B : A → Set} → (x : A) → B x → ∃ B
+{% endraw %}
+Evidence that `∃ (λ (x : A) → B[x])` holds is of the form +`(M , N)` where `M` is a term of type `A`, and `N` is evidence +that `B[M]` holds. + +Given evidence that `∃ (λ (x : A) → B[x])` holds, and +given evidence that `∀ (x : A) → B[x] → C` holds, where `C` does +not contain `x` as a free variable, we may conclude that `C` holds. +
{% raw %}
+∃-elim : ∀ {A : Set} {B : A → Set} {C : Set} → ∃ B → (∀ (x : A) → B x → C) → C
+∃-elim (M , N) P = P M N
+{% endraw %}
+In other words, if we know for every `x` of type `A` that `B[x]` +implies `C`, and we know for some `x` of type `A` that `B[x]` holds, +then we may conclude that `C` holds. This is because we may +instantiate that proof that `∀ (x : A) → B[x] → C` to any `x`, and we +may choose the particular `x` provided by the evidence that `∃ (λ (x : +A) → B[x])`. + + +As an example, recall the definitions of `even` and `odd` from +Chapter [Relations](Relations). + ## Decidability 
{% raw %}
-data Dec : Set → Set where
   yes : ∀ {A : Set} → A → Dec A
   no  : ∀ {A : Set} → (¬ A) → Dec A
 {% endraw %}
@@ -12113,620 +12538,620 @@ Two halves of de Morgan's laws hold intuitionistically. The other two halves are each equivalent to the law of double negation. 
{% raw %}
-dem1 : ∀ {A B : Set} → A × B → ¬ (¬ A ⊎ ¬ B)
 dem1 (a , b) (inj₁ ¬a) = ¬a a
 dem1 (a , b) (inj₂ ¬b) = ¬b b
 
 dem2 : ∀ {A B : Set} → A ⊎ B → ¬ (¬ A × ¬ B)
 dem2 (inj₁ a) (¬a , ¬b) = ¬a a
 dem2 (inj₂ b) (¬a , ¬b) = ¬b b
 {% endraw %}
For the other variant of De Morgan's law, one way is an isomorphism. 
{% raw %}
-dem-≃ : ∀ {A B : Set} → (¬ (A ⊎ B)) ≃ (¬ A × ¬ B)
 dem-≃ = →-distributes-⊎
 {% endraw %}
The other holds in only one direction. 
{% raw %}
-dem-half : ∀ {A B : Set} → ¬ A ⊎ ¬ B → ¬ (A × B)
 dem-half (inj₁ ¬a) (a , b) = ¬a a
 dem-half (inj₂ ¬b) (a , b) = ¬b b
 {% endraw %}
@@ -12738,317 +13163,317 @@ intuitionistically or equivalent to classical logic. For several of the laws equivalent to classical logic, the reverse direction holds in intuitionistic long. 
{% raw %}
-implication-inv : ∀ {A B : Set} → (¬ A ⊎ B) → A → B
 implication-inv (inj₁ ¬a) a = ⊥-elim (¬a a)
 implication-inv (inj₂ b)  a = b
 
 demorgan-inv : ∀ {A B : Set} → A ⊎ B → ¬ (¬ A × ¬ B)
 demorgan-inv (inj₁ a) (¬a , ¬b) =  ¬a a
 demorgan-inv (inj₂ b) (¬a , ¬b) =  ¬b b
 {% endraw %}
diff --git a/src/Logic.lagda b/src/Logic.lagda index 01ca0575..9554423a 100644 --- a/src/Logic.lagda +++ b/src/Logic.lagda @@ -695,15 +695,32 @@ isomorphism. ## Implication is function Given two propositions `A` and `B`, the implication `A → B` holds if -whenever `A` holds then `B` must also hold. We formalise this idea in -terms of the function type. Evidence that `A → B` holds is of the form +whenever `A` holds then `B` must also hold. We formalise implication using +the function type, which has appeared throughout this book. - λ (x : A) → N +Evidence that `A → B` holds is of the form -where `N` is a term of type `B` containing as a free variable `x` of type `A`. -In other words, evidence that `A → B` holds is a function that converts -evidence that `A` holds into evidence that `B` holds. + λ (x : A) → N[x] +where `N[x]` is a term of type `B` containing as a free variable `x` of type `A`. +Given a term `L` providing evidence that `A → B` holds, and a term `M` +providing evidence that `A` holds, the term `L M` provides evidence that +`B` holds. In other words, evidence that `A → B` holds is a function that +converts evidence that `A` holds into evidence that `B` holds. + +Put another way, if we know that `A → B` and `A` both hold, +then we may conclude that `B` holds. In medieval times, this rule was +known by the name *modus ponens*. + +If we introduce an implication and then immediately eliminate it, we can +always simplify the resulting term. Thus + + (λ (x : A) → N[x]) M + +simplifies to `N[M]` of type `B`, where `N[M]` stands for the term `N[x]` with each +free occurrence of `x` replaced by `M` of type `A`. + + Implication binds less tightly than any other operator. Thus, `A ⊎ B → B ⊎ A` parses as `(A ⊎ B) → (B ⊎ A)`. @@ -727,24 +743,24 @@ type `Bool` with two members and a type `Tri` with three members, as defined earlier. The the type `Bool → Tri` has nine (that is, three squared) members: - {true→aa;false→aa} {true→aa;false→bb} {true→aa;false→cc} - {true→bb;false→aa} {true→bb;false→bb} {true→bb;false→cc} - {true→cc;false→aa} {true→cc;false→bb} {true→cc;false→cc} + {true → aa; false → aa} {true → aa; false → bb} {true → aa; false → cc} + {true → bb; false → aa} {true → bb; false → bb} {true → bb; false → cc} + {true → cc; false → aa} {true → cc; false → bb} {true → cc; false → cc} For example, the following function enumerates all possible arguments of the type `Bool → Tri`: \begin{code} →-count : (Bool → Tri) → ℕ →-count f with f true | f false -... | aa | aa = 1 -... | aa | bb = 2 -... | aa | cc = 3 -... | bb | aa = 4 -... | bb | bb = 5 -... | bb | cc = 6 -... | cc | aa = 7 -... | cc | bb = 8 -... | cc | cc = 9 +... | aa | aa = 1 +... | aa | bb = 2 +... | aa | cc = 3 +... | bb | aa = 4 +... | bb | bb = 5 +... | bb | cc = 6 +... | cc | aa = 7 +... | cc | bb = 8 +... | cc | cc = 9 \end{code} Exponential on types also share a property with exponential on @@ -1078,8 +1094,105 @@ of `double-negation` and the others defines a type, we need to use ## Universals +Given a variable `x` of type `A` and a proposition `B[x]` which +contains `x` as a free variable, the universally quantified +proposition `∀ (x : A) → B[x]` holds if for every term `M` of type +`A` the proposition `B[M]` holds. Here `B[M]` stands for +the proposition `B[x]` with each free occurrence of `x` replaced by +`M`. The variable `x` appears free in `B[x]` but bound in +`∀ (x : A) → B[x]`. We formalise universal quantification using the +dependent function type, which has appeared throughout this book. + +Evidence that `∀ (x : A) → B[x]` holds is of the form + + λ (x : A) → N[x] + +where `N[x]` is a term of type `B[x]`; here `N[x]` is a term and `B[x]` +is a proposition (or type) both containing as a free variable `x` of +type `A`. Given a term `L` providing evidence that `∀ (x : A) → B[x]` +holds and a term `M` of type `A`, the term `L M` provides evidence +that `B[M]` holds. In other words, evidence that `∀ (x : A) → B[x]` +holds is a function that converts a term `M` of type `A` into evidence +that `B[M]` holds. + +Put another way, if we know that `∀ (x : A) → B[x]` holds and that `M` +is a term of type `A` then we may conclude that `B[M]` holds. In +medieval times, this rule was known by the name *dictum de omni*. + +If we introduce a universal and the immediately eliminate it, we can +always simplify the resulting term. Thus + + (λ (x : A) → N[x]) M + +simplifies to `N[M]` of type `B[M]`, where `N[M]` stands for the term +`N[x]` with each free occurrence of `x` replaced by `M` of type `A`. + +Unlike with conjunction, disjunction, and implication, there is no simple +analogy between universals and arithmetic. + + ## Existentials +Given a variable `x` of type `A` and a proposition `B[x]` which +contains `x` as a free variable, the existentially quantified +proposition `∃ (λ (x : A) → B[x])` holds if for some term `M` of type +`A` the proposition `B[M]` holds. Here `B[M]` stands for +the proposition `B[x]` with each free occurrence of `x` replaced by +`M`. The variable `x` appears free in `B[x]` but bound in +`∃ (λ (x : A) → B[x])`. + +It is common to adopt a notation such as `∃[ x : A ]→ B[x]`, +which introduces `x` as a bound variable of type `A` that appears +free in `B[x]` and bound in `∃[ x : A ]→ B[x]`. We won't do +that here, but instead use the lambda notation built-in to Agda +to introduce `x` as a bound variable. + +We formalise existential quantification by declaring a suitable +inductive type. +\begin{code} +data ∃ : ∀ {A : Set} → (A → Set) → Set where + _,_ : ∀ {A : Set} {B : A → Set} → (x : A) → B x → ∃ B +\end{code} +Evidence that `∃ (λ (x : A) → B[x])` holds is of the form +`(M , N)` where `M` is a term of type `A`, and `N` is evidence +that `B[M]` holds. + +Given evidence that `∃ (λ (x : A) → B[x])` holds, and +given evidence that `∀ (x : A) → B[x] → C` holds, where `C` does +not contain `x` as a free variable, we may conclude that `C` holds. +\begin{code} +∃-elim : ∀ {A : Set} {B : A → Set} {C : Set} → ∃ B → (∀ (x : A) → B x → C) → C +∃-elim (M , N) P = P M N +\end{code} +In other words, if we know for every `x` of type `A` that `B[x]` +implies `C`, and we know for some `x` of type `A` that `B[x]` holds, +then we may conclude that `C` holds. This is because we may +instantiate that proof that `∀ (x : A) → B[x] → C` to any `x`, and we +may choose the particular `x` provided by the evidence that `∃ (λ (x : +A) → B[x])`. + +[It would be better to have even and odd as an exercise. Is there +a simpler example that I could start with?] + +As an example, recall the definitions of `even` and `odd` from +Chapter [Relations](Relations). +\begin{code} +mutual + data even : ℕ → Set where + ev-zero : even zero + ev-suc : ∀ {n : ℕ} → odd n → even (suc n) + data odd : ℕ → Set where + od-suc : ∀ {n : ℕ} → even n → odd (suc n) +\end{code} +We show that a number `n` is even if and only if there exists +another number `m` such that `n ≡ 2 * m`, and is odd if and only +if there is another number `m` such that `n ≡ 1 + 2 * m`. + +Here is the proof in the forward direction. +\begin{code} + +\end{code} + ## Decidability \begin{code}