<commit_before>#+Title: Theorem Proving in Lean
#+Author: [[http://www.andrew.cmu.edu/user/avigad][<NAME>]]

* Quantifiers and Equality

The last chapter introduced you to methods that construct proofs of
statements involving the propositional connectives. In this chapter,
we extend the repertoire of logical constructions to include the
universal and existential quantifiers, and the equality relation.

** The Universal Quantifier

Notice that if =A= is any type, we can represent a unary predicate =p=
on =A= as an object of type =A → Prop=. In that case, given =x : A=,
=p x= denotes the assertion that =p= holds of =x=. Similarly, an
object =r : A → A → Prop= denotes a binary relation on =A=: given =x
y : A=, =r x y= denotes the assertion that =x= is related to =y=.

The universal quantifier, =∀ x : A, p x= is supposed to denote the
assertion that "for every =x : A=, =p x=" holds. As with the
propositional connectives, in systems of natural deduction, "forall"
is governed by an introduction and elimination rule. Informally, the
introduction rule states:
#+BEGIN_QUOTE
Given a proof of =p x=, in a context where =x : A= is arbitrary, we
obtain a proof =∀ x : A, p x=.
#+END_QUOTE
The elimination rule states:
#+BEGIN_QUOTE
Given a proof =∀ x : A, p x= and any term =t : A=, we obtain a proof of
=p t=.
#+END_QUOTE
As was the case for implication, the propositions-as-types
interpretation now comes into play. Remember the introduction and
elimination rules for Pi types:
#+BEGIN_QUOTE
Given a term =t= of type =B x=, in a context where =x : A= is
arbitrary, we have =(λ x : A, t) : Π x : A, B x=.
#+END_QUOTE
The elimination rule states:
#+BEGIN_QUOTE
Given a term =s : Π x : A, B x= and any term =t : A=, we have =s t : B t=.
#+END_QUOTE
In the case where =p x= has type =Prop=, if we replace =Π x : A, B x=
with =∀ x : A, p x=, we can read these as the correct rules for
building proofs involving the universal quantifier.

The Calculus of Inductive Constructions therefore identifies =Π= and
=∀= in this way. If =p= is any expression, =∀ x : A, p= is nothing more
than alternative notation for =Π x : A, p=, with the idea is that the
former is more natural in cases where where =p= is a
proposition. Typically, the expression =p= will depend on =x :
A=. Recall that, in the case of ordinary function spaces, we could
interpret =A → B= as the special case of =Π x : A, B= in which =B= does
not depend on =x=. Similarly, we can think of an implication =p → q=
between propositions as the special case of =∀ x : p, q= in which the
expression =q= does not depend on =x=.

Here is an example of how the propositions-as-types correspondence
gets put into practice.
#+BEGIN_SRC lean
variables (A : Type) (p q : A → Prop)

example : (∀ x : A, p x ∧ q x) → ∀ y : A, p y  :=
assume H : ∀ x : A, p x ∧ q x,
take y : A,
show p y, from and.elim_left (H y)
#+END_SRC

As a notational convention, we give the universal quantifier the
widest scope possible, so parentheses are needed to limit the
quantifier over =x= to the hypothesis in the example above. The
canonical way to prove =∀ y : A, p y= is to take an arbitrary =y=, and
prove =p y=. This is the introduction rule. Now, given that =H= has
type =∀ x : A, p x ∧ q x=, the expression =H y= has type =p y ∧ q
y=. This is the elimination rule. Taking the left conjunct gives the
desired conclusion, =p y=.

Remember that expressions which differ up to renaming of bound<commit_msg>fix(04): fix grammar, minor clarification<commit_after>#+Title: Theorem Proving in Lean
#+Author: [[http://www.andrew.cmu.edu/user/avigad][<NAME>]]

* Quantifiers and Equality

The last chapter introduced you to methods that construct proofs of
statements involving the propositional connectives. In this chapter,
we extend the repertoire of logical constructions to include the
universal and existential quantifiers, and the equality relation.

** The Universal Quantifier

Notice that if =A= is any type, we can represent a unary predicate =p=
on =A= as an object of type =A → Prop=. In that case, given =x : A=,
=p x= denotes the assertion that =p= holds of =x=. Similarly, an
object =r : A → A → Prop= denotes a binary relation on =A=: given =x
y : A=, =r x y= denotes the assertion that =x= is related to =y=.

The universal quantifier, =∀ x : A, p x= is supposed to denote the
assertion that "for every =x : A=, =p x=" holds. As with the
propositional connectives, in systems of natural deduction, "forall"
is governed by an introduction and elimination rule. Informally, the
introduction rule states:
#+BEGIN_QUOTE
Given a proof of =p x=, in a context where =x : A= is arbitrary, we
obtain a proof =∀ x : A, p x=.
#+END_QUOTE
The elimination rule states:
#+BEGIN_QUOTE
Given a proof =∀ x : A, p x= and any term =t : A=, we obtain a proof of
=p t=.
#+END_QUOTE
As was the case for implication, the propositions-as-types
interpretation now comes into play. Remember the introduction and
elimination rules for Pi types:
#+BEGIN_QUOTE
Given a term =t= of type =B x=, in a context where =x : A= is
arbitrary, we have =(λ x : A, t) : Π x : A, B x=.
#+END_QUOTE
The elimination rule states:
#+BEGIN_QUOTE
Given a term =s : Π x : A, B x= and any term =t : A=, we have =s t : B t=.
#+END_QUOTE
In the case where =p x= has type =Prop=, if we replace =Π x : A, B x=
with =∀ x : A, p x=, we can read these as the correct rules for
building proofs involving the universal quantifier.

The Calculus of Inductive Constructions therefore identifies =Π= and
=∀= in this way. If =p= is any expression, =∀ x : A, p= is nothing more
than alternative notation for =Π x : A, p=, with the idea that the
former is more natural than the latter in cases where where =p= is a
proposition. Typically, the expression =p= will depend on =x :
A=. Recall that, in the case of ordinary function spaces, we could
interpret =A → B= as the special case of =Π x : A, B= in which =B= does
not depend on =x=. Similarly, we can think of an implication =p → q=
between propositions as the special case of =∀ x : p, q= in which the
expression =q= does not depend on =x=.

Here is an example of how the propositions-as-types correspondence
gets put into practice.
#+BEGIN_SRC lean
variables (A : Type) (p q : A → Prop)

example : (∀ x : A, p x ∧ q x) → ∀ y : A, p y  :=
assume H : ∀ x : A, p x ∧ q x,
take y : A,
show p y, from and.elim_left (H y)
#+END_SRC

As a notational convention, we give the universal quantifier the
widest scope possible, so parentheses are needed to limit the
quantifier over =x= to the hypothesis in the example above. The
canonical way to prove =∀ y : A, p y= is to take an arbitrary =y=, and
prove =p y=. This is the introduction rule. Now, given that =H= has
type =∀ x : A, p x ∧ q x=, the expression =H y= has type =p y ∧ q
y=. This is the elimination rule. Taking the left conjunct gives the
desired conclusion, =p y=.

Remember that expressions which differ up to renaming of bound
{'fraction_non_alphanumeric': 0.09515545914678236, 'fraction_numerical': 0.00028922631959508316, 'mean_word_length': 3.887632508833922, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7462901', 'n_tokens_mistral': 2354, 'n_tokens_neox': 2184, 'n_words': 1245}