<commit_before>#+Author: [[http://www.andrew.cmu.edu/user/avigad][<NAME>]]
#+Title: Quantifiers and Equality

* 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 on 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
import logic

section
  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
#+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=, =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
variables are considered to be equivalent. So, for example, we could
have used the same variable, =x=, in both the hypothesis and
conclusion, or chosen the variable =z= instead of =y= in the proof:
#+BEGIN_SRC lean
import logic

section
  variables (A : Type) (p q : A → Prop)

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

As another example, here is how we can express the fact that a
relation, =r=, is transitive:
#+BEGIN_SRC lean
section
  variables (A : Type) (r : A → A → Prop)
  variable (trans_r : ∀x y z, r x y → r y z → r x z)

  variables (a b c : A)
  variables (Hab : r a b) (Hbc : r b c)

  check trans_r
  check trans_r a b c
  check trans_r a b c Hab
  check trans_r a b c Hab Hbc
end
#+END_SRC
Think about what is going on here. When we instantiate =trans_r= at
the values =a b c=, we end up with a proof of =r a b → r b c → r a
c=. Applying this to the "hypothesis" =Hab : r a b=, we get a proof of
the implication =r b c → r a c=. Finally, applying it to the
hypothesis =Hbc= yields a proof of the conlusion =r a c=.

In situtations like this, it can be tedious to supply the arguments =a
b c=, when they can be inferred from =Hab Hbc=. For that reason, it is
common to make these arguments implicit:
#+BEGIN_SRC lean
section
  variables (A : Type) (r : A → A → Prop)
  variable (trans_r : ∀{x y z}, r x y → r y z → r x z)

  variables (a b c : A)
  variables (Hab : r a b) (Hbc : r b c)

  check trans_r
  check trans_r Hab
  check trans_r Hab Hbc
end
#+END_SRC
The advantage is that we can simply write =trans_r Hab Hbc= as a proof
of =r a c=. The disadvantage is that Lean does not have enough
information to infer the types of the arguments in the expressions
=trans_r= and =trans_r Hab=. In the output of the =check= command, an
expression like =?z A r trans_r a b c Hab Hbc= indicates an arbitrary
value, that may depend on any of the values listed (in this case, all
the variables in the section).

Here is an example of how we can carry out elementary reasoning with
an equivalence relation:
#+BEGIN_SRC lean
section
  variables (A : Type) (r : A → A → Prop)

  variable (refl_r : ∀x, r x x)
  variable (symm_r : ∀{x y}, r x y → r y x)
  variable (trans_r : ∀{x y z}, r x y → r y z → r x z)

  example (a b c d : A) (Hab : r a b) (Hcb : r c b) (Hcd : r c d) : r a d :=
  trans_r (trans_r Hab (symm_r Hcb)) Hcd
end
#+END_SRC
You might want to try to prove some of these equivalences:
#+BEGIN_SRC lean
import logic

section
  variables (A : Type) (P Q : A → Prop)

  example : (∀x, P x ∧ Q x) ↔ (∀x, P x) ∧ (∀x, Q x) := sorry
  example : (∀x, P x → Q x) → (∀x, P x) → (∀x, Q x) := sorry
  example : (∀x, P x) ∨ (∀x, Q x) → ∀x, P x ∨ Q x := sorry
end
#+END_SRC
You should also try to understand why the reverse implication is not
derivable in the last example.

It is often possible to bring a component outside a universal
quantifier, when it does not depend on the quantified variable:
#+BEGIN_SRC lean
section
  variables (A : Type) (P Q : A → Prop)
  variable R : Prop

  example : (∀x : A, R) ↔ R := sorry
  example : (∀x, P x ∨ R) ↔ (∀x, P x) ∨ R := sorry
  example : (∀x, R → P x) ↔ (R → ∀x, P x) := sorry
end
#+END_SRC

As a final example, consider the "barber paradox", that is, the claim
that in a certain town there is a (male) barber that shaves all and only the
men who do not shave themselves. Prove that this implies a
contradiction:
#+BEGIN_SRC lean
section
  variables (men : Type) (barber : men) (shaves : men → men → Prop)

  example (H : ∀x : men, shaves barber x ↔ ¬shaves x x) : false := sorry
end
#+END_SRC

** Equality

Let us now turn to one of the most fundamental relations defined in
Lean's library, namely, the equality relation. In the next chapter, we
will explain /how/ equality is defined, from the primitives of Lean's
logical framework. In the meanwhile, here we explain how to use it.

Of course, a fundamental property of equality is that it is an
equivalence relation:
#+BEGIN_SRC lean
import logic.eq

check eq.refl
check eq.symm
check eq.trans
#+END_SRC
Thus, for example, we can specialize the example from the previous section
to the equality relation:
#+BEGIN_SRC lean
example (A : Type) (a b c d : A) (Hab : a = b) (Hcb : c = b) (Hcd : c = d) :
  a = d :=
eq.trans (eq.trans Hab (eq.symm Hcb)) Hcd
#+END_SRC

If we "open" the eq namespace, the names become shorter:
#+BEGIN_SRC lean
open eq

example (A : Type) (a b c d : A) (Hab : a = b) (Hcb : c = b) (Hcd : c = d) :
  a = d :=
trans (trans Hab (symm Hcb)) Hcd
#+END_SRC
Lean even defines convenient notation for writing proofs like this:
#+BEGIN_SRC lean
open eq.ops

example (A : Type) (a b c d : A) (Hab : a = b) (Hcb : c = b) (Hcd : c = d) :
  a = d :=
Hab ⬝ Hcb⁻¹ ⬝ Hcd
#+END_SRC
You can use =\tr= to enter the transitivity dot, and =\sy= to enter
the inverse/symmetry symbol.

Reflexivity is more powerful than it looks. Recall that terms in the
Calculus of Inductive Constructions have a computational
interpretation, and that the logical framework treats terms with a
common reduct as the same. As a result, some nontrivial identities can
be proved by reflexivity:
#+BEGIN_SRC lean
import data.nat data.prod
open nat prod

example (A B : Type) (f : A → B) (a : A) : (λx, f x) a = f a := eq.refl _
example (A B : Type) (a : A) (b : A) : pr1 (a, b) = a := eq.refl _
example : 2 + 3 = 5 := eq.refl _
#+END_SRC
This feature of the framework is so important that the library defines
a notation =rfl= for =eq.refl _=:
#+BEGIN_SRC lean
import data.nat data.prod
open nat prod
-- BEGIN
example (A B : Type) (f : A → B) (a : A) : (λx, f x) a = f a := rfl
example (A B : Type) (a : A) (b : A) : pr1 (a, b) = a := rfl
example : 2 + 3 = 5 := rfl
-- END
#+END_SRC

Equality is much more than an equivalence relation, however. It has
the important property that every assertion respects the equivalence,
in the sense that we can substitute equal expressions without changing
the truth value.
#+BEGIN_SRC lean
open eq.ops
-- BEGIN
example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b :=
eq.subst H1 H2

example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b :=
H1 ▸ H2
-- END
#+END_SRC
The triangle in the second presentation is, once again, made available
by opening =eq.ops=, and you can use =\t= to enter it.

Here is an example of a calculation in the natural numbers that uses
substitution combined with associativity, commutativity, and
distributivity of the natural numbers. Of course, carrying out such
calculations require being able to invoke such supporting
theorems. You can find a number of identities involving the natural
numbers in the associated library files, for example, in the module
[[https://github.com/leanprover/lean/blob/master/library/data/nat/basic.lean][data.nat.basic]]. In the next chapter, we will have more to say about
how to find theorems in Lean's library.
#+BEGIN_SRC lean
import data.nat
open nat eq.ops

example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
have H1 : (x + y) * (x + y) = (x + y) * x + (x + y) * y, from !mul.left_distrib,
have H2 : (x + y) * (x + y) = x * x + y * x + (x * y + y * y),
  from !mul.right_distrib ▸ !mul.right_distrib ▸ H1,
!add.assoc⁻¹ ▸ H2
#+END_SRC

Remember that the exclamation mark adds implicit arguments as
necessary. In the statement of the example, remember that addition
implicitly associates to the left, so the last step of the proof
puts the right-hand side of =H2= in the required form.

It is often important to be able to carry out substitutions like this
by hand, but it is tedious to prove examples like the one above in
this way. Fortunately, Lean provides an environment that provides
better support for such calculations, which we will turn to now.

** The Calculation Environment

A calculational proof is just a chain of intermediate results that are
meant to be composed by basic principles such as the transitivity of
===. In Lean, a calculation proof starts with the keyword =calc=, and has
the following syntax:

#+BEGIN_SRC text
calc
  <expr>_0  'op_1'  <expr>_1  ':'  <proof>_1
    '...'   'op_2'  <expr>_2  ':'  <proof>_2
     ...
    '...'   'op_n'  <expr>_n  ':'  <proof>_n
#+END_SRC
Each =<proof>_i= is a proof for =<expr>_{i-1} op_i <expr>_i=. The
=<proof>_i= may also be of the form ={ <pr> }=, where =<pr>= is a
proof for some equality =a = b=. The form ={ <pr> }= is just syntactic
sugar for =eq.subst <pr> (refl <expr>_{i-1})= In other words, we are
claiming we can obtain =<expr>_i= by replacing =a= with =b= in
=<expr>_{i-1}=.

Here is an example:
#+BEGIN_SRC lean
import data.nat
open nat

section
  variables (a b c d e : nat)
  variable H1 : a = b
  variable H2 : b = c + 1
  variable H3 : c = d
  variable H4 : e = 1 + d

  theorem T : a = e :=
  calc
    a     = b      : H1
      ... = c + 1  : H2
      ... = d + 1  : {H3}
      ... = 1 + d  : add.comm d 1
      ... =  e     : eq.symm H4
end
#+END_SRC

The =calc= command can be configured for any relation that supports
some form of transitivity. It can even combine different relations.
#+BEGIN_SRC lean
import data.nat
open nat

theorem T2 (a b c : nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0 :=
calc
  a     = b      : H1
    ... = c + 1  : H2
    ... = succ c : add_one c
    ... ≠ 0      : succ_ne_zero c
#+END_SRC

Lean offers some nice additional features. If the justification for a
line of a calculations proof is =foo=, Lean will try adding implicit
arguments if =foo= alone fails to do the job. If that doesn't work,
Lean will try the symmetric version, =foo⁻¹=, again adding arguments
if necessary. If that doesn't work, Lean proceeds to try ={foo}= and
={foo⁻¹}=, again, adding arguments if necessary. This can simplify the
presentation of a =calc= proof considerably. Consider, for example,
the following proof of the identity in the last section:
#+BEGIN_SRC lean
import data.nat
open nat

-- BEGIN
example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
calc
  (x + y) * (x + y) = (x + y) * x + (x + y) * y  : mul.left_distrib
    ... = x * x + y * x + (x + y) * y            : mul.right_distrib
    ... = x * x + y * x + (x * y + y * y)        : mul.right_distrib
    ... = x * x + y * x + x * y + y * y          : add.assoc
-- END
#+END_SRC
As an exercise, we suggest carrying out a similar expansion of =(x -
y) * (x - y)=, using the theorems =mul_sub_distr_right= and
=mul_sub_distr_right= in the module [[https://github.com/leanprover/lean/blob/master/library/data/nat/sub.lean][data.nat.sub]].

** The Simplifier

[TO DO: this section needs to be written. Emphasize that the
simplifier can be used in conjunction with calc.]

** The Existential Quantifier

Finally, consider the existential quantifier, which can be written as
either =exists x : A, p x= or =∃x : A, p x=. Both versions are
actually notationally convenient abbreviations for a more long-winded
expression, =Exists (λx : A, p x)=, defined in Lean's library.

As you should by now expect, the library includes both an introduction
rule and an elimination rule. The introduction rule is
straightforward: to prove =∃x : A, p x=, it suffices to provide a
suitable term =t= and a proof of =p t=. Here are some examples:
#+BEGIN_SRC lean
import data.nat
open nat

example : ∃x, x > 0 :=
have H : 1 > 0, from succ_pos 0,
exists.intro 1 H

example (x : ℕ) (H : x > 0) : ∃y, y < x :=
exists.intro 0 H

example (x y z : ℕ) (Hxy : x < y) (Hyz : y < z) : ∃w, x < w ∧ w < z :=
exists.intro y (and.intro Hxy Hyz)

check @exists.intro
#+END_SRC
Note that =exists.intro= has implicit arguments: Lean has to infer the
predicate =p : A → Prop= in the conclusion =∃x, p x=. This is not a
trivial affair. For example, if we have have =Hg : g 0 0 = 0= and
write =exists.intro 0 Hg=, there are many possible values for the
predicate =p=, corresponding to the theorems =∃ x, g x x = x=, =∃ x, g
x x = 0=, =∃ x, g x 0 = x=, etc. Lean uses the context to infer which
one is appropriate. This is illustrated in the following example, in
which we set the option =pp.implicit= to true to ask Lean's
pretty-printer to show the implicit arguments.

#+BEGIN_SRC lean
import data.nat
open nat

section
  variable g : ℕ → ℕ → ℕ
  variable Hg : g 0 0 = 0

  theorem gex1 : ∃ x, g x x = x := exists.intro 0 Hg
  theorem gex2 : ∃ x, g x 0 = x := exists.intro 0 Hg
  theorem gex3 : ∃ x, g 0 0 = x := exists.intro 0 Hg
  theorem gex4 : ∃ x, g x x = 0 := exists.intro 0 Hg

  set_option pp.implicit true  -- display implicit arguments
  check gex1
  check gex2
  check gex3
  check gex4
end
#+END_SRC

We can view =exists.intro= as an information-hiding operation: we are
"hiding" the witness to the body of the assertion. The existential
elimination rule, =exists.elim=, performs the opposite operation. It
allows us to prove a proposition =q= from =∃x : A, p x=, by showing
that =q= follows from =p w= for an arbitrary value =w=. Roughly
speaking, since we know there is an =x= satisfying =p x=, we can give
it a name, say, =w=. Showing that =q= follows from =p w=, where =q=
does not mention =w=, is tantamount to showing the =q= follows from
the existence of any such =x=.

(It may be helpful to compare the exists-elimination rule to the
or-elimination rule. The assertion =∃x : A, p x= can be thought of as
a big disjunction of the propositions =p a=, as =a= ranges over all
the elements of =A=.)

Notice that exists introduction and elimination are very similar to the
sigma introduction =sigma.mk= and elimination.
The difference is that given =a : A= and =h : p a=, =exists.intro a h=
has type =(∃x : A, p x) : Prop= and =sigma.mk a h= has type
=(Σ x : A, p x) : Type=. The similarity
between =∃= and =Σ= is another instance of the Curry-Howard isomorphism.

In the following example, we define =even a= as =∃ b, a = 2*b=, and
then we show that the sum of two even numbers is an even number.
#+BEGIN_SRC lean
import data.nat
open nat

definition even (a : nat) := ∃b, a = 2*b

theorem even_plus_even {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) :=
exists.elim H1 (fun (w1 : nat) (Hw1 : a = 2*w1),
exists.elim H2 (fun (w2 : nat) (Hw2 : b = 2*w2),
  exists.intro (w1 + w2)
    (calc
      a + b = 2*w1 + b      : Hw1
        ... = 2*w1 + 2*w2   : Hw2
        ... = 2*(w1 + w2)   : mul.left_distrib)))
#+END_SRC

Lean provides syntactic sugar for =exists.elim=, with expressions of
the form =obtain _, from _, _=. With this syntax, the example above
can be presented in a more natural way:           :
#+BEGIN_SRC lean
import data.nat
open nat

definition even (a : nat) := ∃b, a = 2*b

theorem even_plus_even {a b : nat} (H1 : even a) (H2 : even b) :
  even (a + b) :=
obtain (w1 : nat) (Hw1 : a = 2*w1), from H1,
obtain (w2 : nat) (Hw2 : b = 2*w2), from H2,
exists.intro (w1 + w2)
  (calc
    a + b = 2*w1 + b      : Hw1
      ... = 2*w1 + 2*w2   : Hw2
      ... = 2*(w1 + w2)   : mul.left_distrib)
#+END_SRC

What follows are some common identities involving the existential
quantifier. We encourage you to prove as many as you can. Be careful:
many of them are nonconstructive, and require the use of the law of
the excluded middle.
#+BEGIN_SRC lean
import logic

section
  variables (A : Type) (p q : A → Prop)
  variable r : Prop

  example : (∃x, p x ∨ q x) ↔ (∃x, p x) ∨ (∃x, q x) := sorry

  example : (∃x : A, r) ↔ r := sorry
  example : (∃x, p x ∧ r) ↔ (∃x, p x) ∧ r := sorry
  example : (∀x, p x → r) ↔ (∃x, p x) → r := sorry
  example : (∃x, p x → r) ↔ (∀x, p x → r) := sorry
  example : (∃x, r → p x) ↔ (r → ∃x, p x) := sorry

  example : (∃x, p x) ↔ (∀x, ¬p x) := sorry
  example : (∀x, p x) ↔ (∃x, ¬p x) := sorry
  example : (¬∃x, p x) ↔ (∀x, ¬p x) := sorry
  example : (¬∀x, p x) ↔ (∃x, ¬p x) := sorry
end
#+END_SRC
<commit_msg>fix(04_Quantifiers_and_Equality.org): fix examples at the end of the Universal Quantifier section<commit_after>#+Author: [[http://www.andrew.cmu.edu/user/avigad][<NAME>]]
#+Title: Quantifiers and Equality

* 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 on 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
import logic

section
  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
#+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=, =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
variables are considered to be equivalent. So, for example, we could
have used the same variable, =x=, in both the hypothesis and
conclusion, or chosen the variable =z= instead of =y= in the proof:
#+BEGIN_SRC lean
import logic

section
  variables (A : Type) (p q : A → Prop)

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

As another example, here is how we can express the fact that a
relation, =r=, is transitive:
#+BEGIN_SRC lean
section
  variables (A : Type) (r : A → A → Prop)
  variable (trans_r : ∀x y z, r x y → r y z → r x z)

  variables (a b c : A)
  variables (Hab : r a b) (Hbc : r b c)

  check trans_r
  check trans_r a b c
  check trans_r a b c Hab
  check trans_r a b c Hab Hbc
end
#+END_SRC
Think about what is going on here. When we instantiate =trans_r= at
the values =a b c=, we end up with a proof of =r a b → r b c → r a
c=. Applying this to the "hypothesis" =Hab : r a b=, we get a proof of
the implication =r b c → r a c=. Finally, applying it to the
hypothesis =Hbc= yields a proof of the conlusion =r a c=.

In situtations like this, it can be tedious to supply the arguments =a
b c=, when they can be inferred from =Hab Hbc=. For that reason, it is
common to make these arguments implicit:
#+BEGIN_SRC lean
section
  variables (A : Type) (r : A → A → Prop)
  variable (trans_r : ∀{x y z}, r x y → r y z → r x z)

  variables (a b c : A)
  variables (Hab : r a b) (Hbc : r b c)

  check trans_r
  check trans_r Hab
  check trans_r Hab Hbc
end
#+END_SRC
The advantage is that we can simply write =trans_r Hab Hbc= as a proof
of =r a c=. The disadvantage is that Lean does not have enough
information to infer the types of the arguments in the expressions
=trans_r= and =trans_r Hab=. In the output of the =check= command, an
expression like =?z A r trans_r a b c Hab Hbc= indicates an arbitrary
value, that may depend on any of the values listed (in this case, all
the variables in the section).

Here is an example of how we can carry out elementary reasoning with
an equivalence relation:
#+BEGIN_SRC lean
section
  variables (A : Type) (r : A → A → Prop)

  variable (refl_r : ∀x, r x x)
  variable (symm_r : ∀{x y}, r x y → r y x)
  variable (trans_r : ∀{x y z}, r x y → r y z → r x z)

  example (a b c d : A) (Hab : r a b) (Hcb : r c b) (Hcd : r c d) : r a d :=
  trans_r (trans_r Hab (symm_r Hcb)) Hcd
end
#+END_SRC
You might want to try to prove some of these equivalences:
#+BEGIN_SRC lean
import logic

section
  variables (A : Type) (P Q : A → Prop)

  example : (∀x, P x ∧ Q x) ↔ (∀x, P x) ∧ (∀x, Q x) := sorry
  example : (∀x, P x → Q x) → (∀x, P x) → (∀x, Q x) := sorry
  example : (∀x, P x) ∨ (∀x, Q x) → ∀x, P x ∨ Q x := sorry
end
#+END_SRC
You should also try to understand why the reverse implication is not
derivable in the last example.

It is often possible to bring a component outside a universal
quantifier, when it does not depend on the quantified variable (one
direction of the second of these requires classical logic):
#+BEGIN_SRC lean
section
  variables (A : Type) (P Q : A → Prop)
  variable R : Prop

  example : A → (∀x : A, R) ↔ R := sorry
  example : (∀x, P x ∨ R) ↔ (∀x, P x) ∨ R := sorry
  example : (∀x, R → P x) ↔ (R → ∀x, P x) := sorry
end
#+END_SRC

As a final example, consider the "barber paradox", that is, the claim
that in a certain town there is a (male) barber that shaves all and only the
men who do not shave themselves. Prove that this implies a
contradiction:
#+BEGIN_SRC lean
section
  variables (men : Type) (barber : men) (shaves : men → men → Prop)

  example (H : ∀x : men, shaves barber x ↔ ¬shaves x x) : false := sorry
end
#+END_SRC

** Equality

Let us now turn to one of the most fundamental relations defined in
Lean's library, namely, the equality relation. In the next chapter, we
will explain /how/ equality is defined, from the primitives of Lean's
logical framework. In the meanwhile, here we explain how to use it.

Of course, a fundamental property of equality is that it is an
equivalence relation:
#+BEGIN_SRC lean
import logic.eq

check eq.refl
check eq.symm
check eq.trans
#+END_SRC
Thus, for example, we can specialize the example from the previous section
to the equality relation:
#+BEGIN_SRC lean
example (A : Type) (a b c d : A) (Hab : a = b) (Hcb : c = b) (Hcd : c = d) :
  a = d :=
eq.trans (eq.trans Hab (eq.symm Hcb)) Hcd
#+END_SRC

If we "open" the eq namespace, the names become shorter:
#+BEGIN_SRC lean
open eq

example (A : Type) (a b c d : A) (Hab : a = b) (Hcb : c = b) (Hcd : c = d) :
  a = d :=
trans (trans Hab (symm Hcb)) Hcd
#+END_SRC
Lean even defines convenient notation for writing proofs like this:
#+BEGIN_SRC lean
open eq.ops

example (A : Type) (a b c d : A) (Hab : a = b) (Hcb : c = b) (Hcd : c = d) :
  a = d :=
Hab ⬝ Hcb⁻¹ ⬝ Hcd
#+END_SRC
You can use =\tr= to enter the transitivity dot, and =\sy= to enter
the inverse/symmetry symbol.

Reflexivity is more powerful than it looks. Recall that terms in the
Calculus of Inductive Constructions have a computational
interpretation, and that the logical framework treats terms with a
common reduct as the same. As a result, some nontrivial identities can
be proved by reflexivity:
#+BEGIN_SRC lean
import data.nat data.prod
open nat prod

example (A B : Type) (f : A → B) (a : A) : (λx, f x) a = f a := eq.refl _
example (A B : Type) (a : A) (b : A) : pr1 (a, b) = a := eq.refl _
example : 2 + 3 = 5 := eq.refl _
#+END_SRC
This feature of the framework is so important that the library defines
a notation =rfl= for =eq.refl _=:
#+BEGIN_SRC lean
import data.nat data.prod
open nat prod
-- BEGIN
example (A B : Type) (f : A → B) (a : A) : (λx, f x) a = f a := rfl
example (A B : Type) (a : A) (b : A) : pr1 (a, b) = a := rfl
example : 2 + 3 = 5 := rfl
-- END
#+END_SRC

Equality is much more than an equivalence relation, however. It has
the important property that every assertion respects the equivalence,
in the sense that we can substitute equal expressions without changing
the truth value.
#+BEGIN_SRC lean
open eq.ops
-- BEGIN
example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b :=
eq.subst H1 H2

example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b :=
H1 ▸ H2
-- END
#+END_SRC
The triangle in the second presentation is, once again, made available
by opening =eq.ops=, and you can use =\t= to enter it.

Here is an example of a calculation in the natural numbers that uses
substitution combined with associativity, commutativity, and
distributivity of the natural numbers. Of course, carrying out such
calculations require being able to invoke such supporting
theorems. You can find a number of identities involving the natural
numbers in the associated library files, for example, in the module
[[https://github.com/leanprover/lean/blob/master/library/data/nat/basic.lean][data.nat.basic]]. In the next chapter, we will have more to say about
how to find theorems in Lean's library.
#+BEGIN_SRC lean
import data.nat
open nat eq.ops

example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
have H1 : (x + y) * (x + y) = (x + y) * x + (x + y) * y, from !mul.left_distrib,
have H2 : (x + y) * (x + y) = x * x + y * x + (x * y + y * y),
  from !mul.right_distrib ▸ !mul.right_distrib ▸ H1,
!add.assoc⁻¹ ▸ H2
#+END_SRC

Remember that the exclamation mark adds implicit arguments as
necessary. In the statement of the example, remember that addition
implicitly associates to the left, so the last step of the proof
puts the right-hand side of =H2= in the required form.

It is often important to be able to carry out substitutions like this
by hand, but it is tedious to prove examples like the one above in
this way. Fortunately, Lean provides an environment that provides
better support for such calculations, which we will turn to now.

** The Calculation Environment

A calculational proof is just a chain of intermediate results that are
meant to be composed by basic principles such as the transitivity of
===. In Lean, a calculation proof starts with the keyword =calc=, and has
the following syntax:

#+BEGIN_SRC text
calc
  <expr>_0  'op_1'  <expr>_1  ':'  <proof>_1
    '...'   'op_2'  <expr>_2  ':'  <proof>_2
     ...
    '...'   'op_n'  <expr>_n  ':'  <proof>_n
#+END_SRC
Each =<proof>_i= is a proof for =<expr>_{i-1} op_i <expr>_i=. The
=<proof>_i= may also be of the form ={ <pr> }=, where =<pr>= is a
proof for some equality =a = b=. The form ={ <pr> }= is just syntactic
sugar for =eq.subst <pr> (refl <expr>_{i-1})= In other words, we are
claiming we can obtain =<expr>_i= by replacing =a= with =b= in
=<expr>_{i-1}=.

Here is an example:
#+BEGIN_SRC lean
import data.nat
open nat

section
  variables (a b c d e : nat)
  variable H1 : a = b
  variable H2 : b = c + 1
  variable H3 : c = d
  variable H4 : e = 1 + d

  theorem T : a = e :=
  calc
    a     = b      : H1
      ... = c + 1  : H2
      ... = d + 1  : {H3}
      ... = 1 + d  : add.comm d 1
      ... =  e     : eq.symm H4
end
#+END_SRC

The =calc= command can be configured for any relation that supports
some form of transitivity. It can even combine different relations.
#+BEGIN_SRC lean
import data.nat
open nat

theorem T2 (a b c : nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0 :=
calc
  a     = b      : H1
    ... = c + 1  : H2
    ... = succ c : add_one c
    ... ≠ 0      : succ_ne_zero c
#+END_SRC

Lean offers some nice additional features. If the justification for a
line of a calculations proof is =foo=, Lean will try adding implicit
arguments if =foo= alone fails to do the job. If that doesn't work,
Lean will try the symmetric version, =foo⁻¹=, again adding arguments
if necessary. If that doesn't work, Lean proceeds to try ={foo}= and
={foo⁻¹}=, again, adding arguments if necessary. This can simplify the
presentation of a =calc= proof considerably. Consider, for example,
the following proof of the identity in the last section:
#+BEGIN_SRC lean
import data.nat
open nat

-- BEGIN
example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
calc
  (x + y) * (x + y) = (x + y) * x + (x + y) * y  : mul.left_distrib
    ... = x * x + y * x + (x + y) * y            : mul.right_distrib
    ... = x * x + y * x + (x * y + y * y)        : mul.right_distrib
    ... = x * x + y * x + x * y + y * y          : add.assoc
-- END
#+END_SRC
As an exercise, we suggest carrying out a similar expansion of =(x -
y) * (x - y)=, using the theorems =mul_sub_distr_right= and
=mul_sub_distr_right= in the module [[https://github.com/leanprover/lean/blob/master/library/data/nat/sub.lean][data.nat.sub]].

** The Simplifier

[TO DO: this section needs to be written. Emphasize that the
simplifier can be used in conjunction with calc.]

** The Existential Quantifier

Finally, consider the existential quantifier, which can be written as
either =exists x : A, p x= or =∃x : A, p x=. Both versions are
actually notationally convenient abbreviations for a more long-winded
expression, =Exists (λx : A, p x)=, defined in Lean's library.

As you should by now expect, the library includes both an introduction
rule and an elimination rule. The introduction rule is
straightforward: to prove =∃x : A, p x=, it suffices to provide a
suitable term =t= and a proof of =p t=. Here are some examples:
#+BEGIN_SRC lean
import data.nat
open nat

example : ∃x, x > 0 :=
have H : 1 > 0, from succ_pos 0,
exists.intro 1 H

example (x : ℕ) (H : x > 0) : ∃y, y < x :=
exists.intro 0 H

example (x y z : ℕ) (Hxy : x < y) (Hyz : y < z) : ∃w, x < w ∧ w < z :=
exists.intro y (and.intro Hxy Hyz)

check @exists.intro
#+END_SRC
Note that =exists.intro= has implicit arguments: Lean has to infer the
predicate =p : A → Prop= in the conclusion =∃x, p x=. This is not a
trivial affair. For example, if we have have =Hg : g 0 0 = 0= and
write =exists.intro 0 Hg=, there are many possible values for the
predicate =p=, corresponding to the theorems =∃ x, g x x = x=, =∃ x, g
x x = 0=, =∃ x, g x 0 = x=, etc. Lean uses the context to infer which
one is appropriate. This is illustrated in the following example, in
which we set the option =pp.implicit= to true to ask Lean's
pretty-printer to show the implicit arguments.

#+BEGIN_SRC lean
import data.nat
open nat

section
  variable g : ℕ → ℕ → ℕ
  variable Hg : g 0 0 = 0

  theorem gex1 : ∃ x, g x x = x := exists.intro 0 Hg
  theorem gex2 : ∃ x, g x 0 = x := exists.intro 0 Hg
  theorem gex3 : ∃ x, g 0 0 = x := exists.intro 0 Hg
  theorem gex4 : ∃ x, g x x = 0 := exists.intro 0 Hg

  set_option pp.implicit true  -- display implicit arguments
  check gex1
  check gex2
  check gex3
  check gex4
end
#+END_SRC

We can view =exists.intro= as an information-hiding operation: we are
"hiding" the witness to the body of the assertion. The existential
elimination rule, =exists.elim=, performs the opposite operation. It
allows us to prove a proposition =q= from =∃x : A, p x=, by showing
that =q= follows from =p w= for an arbitrary value =w=. Roughly
speaking, since we know there is an =x= satisfying =p x=, we can give
it a name, say, =w=. Showing that =q= follows from =p w=, where =q=
does not mention =w=, is tantamount to showing the =q= follows from
the existence of any such =x=.

(It may be helpful to compare the exists-elimination rule to the
or-elimination rule. The assertion =∃x : A, p x= can be thought of as
a big disjunction of the propositions =p a=, as =a= ranges over all
the elements of =A=.)

Notice that exists introduction and elimination are very similar to the
sigma introduction =sigma.mk= and elimination.
The difference is that given =a : A= and =h : p a=, =exists.intro a h=
has type =(∃x : A, p x) : Prop= and =sigma.mk a h= has type
=(Σ x : A, p x) : Type=. The similarity
between =∃= and =Σ= is another instance of the Curry-Howard isomorphism.

In the following example, we define =even a= as =∃ b, a = 2*b=, and
then we show that the sum of two even numbers is an even number.
#+BEGIN_SRC lean
import data.nat
open nat

definition even (a : nat) := ∃b, a = 2*b

theorem even_plus_even {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) :=
exists.elim H1 (fun (w1 : nat) (Hw1 : a = 2*w1),
exists.elim H2 (fun (w2 : nat) (Hw2 : b = 2*w2),
  exists.intro (w1 + w2)
    (calc
      a + b = 2*w1 + b      : Hw1
        ... = 2*w1 + 2*w2   : Hw2
        ... = 2*(w1 + w2)   : mul.left_distrib)))
#+END_SRC

Lean provides syntactic sugar for =exists.elim=, with expressions of
the form =obtain _, from _, _=. With this syntax, the example above
can be presented in a more natural way:           :
#+BEGIN_SRC lean
import data.nat
open nat

definition even (a : nat) := ∃b, a = 2*b

theorem even_plus_even {a b : nat} (H1 : even a) (H2 : even b) :
  even (a + b) :=
obtain (w1 : nat) (Hw1 : a = 2*w1), from H1,
obtain (w2 : nat) (Hw2 : b = 2*w2), from H2,
exists.intro (w1 + w2)
  (calc
    a + b = 2*w1 + b      : Hw1
      ... = 2*w1 + 2*w2   : Hw2
      ... = 2*(w1 + w2)   : mul.left_distrib)
#+END_SRC

What follows are some common identities involving the existential
quantifier. We encourage you to prove as many as you can. Be careful:
many of them are nonconstructive, and require the use of the law of
the excluded middle.
#+BEGIN_SRC lean
import logic

section
  variables (A : Type) (p q : A → Prop)
  variable r : Prop

  example : (∃x, p x ∨ q x) ↔ (∃x, p x) ∨ (∃x, q x) := sorry

  example : (∃x : A, r) ↔ r := sorry
  example : (∃x, p x ∧ r) ↔ (∃x, p x) ∧ r := sorry
  example : (∀x, p x → r) ↔ (∃x, p x) → r := sorry
  example : (∃x, p x → r) ↔ (∀x, p x → r) := sorry
  example : (∃x, r → p x) ↔ (r → ∃x, p x) := sorry

  example : (∃x, p x) ↔ (∀x, ¬p x) := sorry
  example : (∀x, p x) ↔ (∃x, ¬p x) := sorry
  example : (¬∃x, p x) ↔ (∀x, ¬p x) := sorry
  example : (¬∀x, p x) ↔ (∃x, ¬p x) := sorry
end
#+END_SRC

{'fraction_non_alphanumeric': 0.11230043541364296, 'fraction_numerical': 0.00725689404934688, 'mean_word_length': 3.2169398907103823, 'pattern_counts': {'":': 0, '<': 51, '<?xml version=': 0, '>': 47, 'https://': 4, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 22, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4111035', 'n_tokens_mistral': 14422, 'n_tokens_neox': 13572, 'n_words': 6700}