-- {{{ Logic/general definitions

-- import basic logic definitions from <logic.pg>

@include logic.pg
@include algebra.pg

def comp (A B C : *) (g : B -> C) (f : A -> B) (x : A) : C :=
  g (f x);

-- }}}

-- {{{ Axioms

-- Now we can define the Peano axioms. Unlike with equality, perga is not
-- powerful enough to construct the natural numbers (or at least to prove the
-- Peano axioms as theorems from a definition constructible in perga). However,
-- working with axioms is extremely common in math. As such, perga has a system
-- for doing just that, namely the *axiom* system.
-- 
-- In a definition, rather than give a value for the term, we can give it the
-- value axiom, in which case a type ascription is mandatory. Perga will then
-- trust our type ascription, and assume going forward that the identifier we
-- defined is a value of the asserted type. For example, we will use the axiom
-- system to assert the existence of a type of natural numbers

axiom nat : *;

-- As you can imagine, this can be risky. For instance, there's nothing stopping
-- us from saying
--     uh_oh : false := axiom;
-- or stipulating more subtly contradictory axioms. As such, as in mathematics,
-- axioms should be used with care.
-- 
-- There's another problem with axioms, namely that perga cannot do any
-- computations with axioms. The more you can define within perga natively, the
-- better, as computations done without axioms can be utilized by perga. For
-- example, in <computation.pg>, we define the natural numbers as Church
-- numerals entirely within perga. There, the proof that 1 + 1 = 2 is just
-- eq_refl, since they reduce to the same thing. Here, 1 + 1 = 2 will
-- require a proof, since perga is unable to do computations with things defined
-- as axioms.
-- 
-- With these warnings in place, the Peano axioms are proven to be consistent,
-- so we should be fine. I'm formalizing the second order axioms given in the
-- wikipedia article on the Peano axioms
-- (https://en.wikipedia.org/wiki/Peano_axioms).

-- axiom 1: 0 is a natural number
axiom zero : nat;

-- axiom 6: For every n, S n is a natural number.
axiom suc (n : nat) : nat;

-- axiom 7: If S n = S m, then n = m.
axiom suc_inj : forall (n m : nat), eq nat (suc n) (suc m) -> eq nat n m;

-- axiom 8: No successor of any natural number is zero.
axiom suc_nonzero : forall (n : nat), not (eq nat (suc n) zero);

-- axiom 9: Induction! For any proposition P on natural numbers, if P(0) holds,
-- and if for every natural number n, P(n) ⇒ P(S n), then P holds for all n.
axiom nat_ind : forall (P : nat -> *), P zero -> (forall (n : nat), P n -> P (suc n))
    -> forall (n : nat), P n;

-- }}}

-- {{{ Basic Definitions

-- Now that we have stipulated these axioms, we are free to use them to make
-- definitions, prove theorems, etc.
-- 
-- Our first theorem, as a warm up, is to prove that every natural number is
-- either 0 or the successor of another natural number.
-- 
-- First, we will make a bunch of abbreviations, since these terms get really
-- long and complicated really quickly.

-- Some abbreviations for common numbers.
def one   : nat := suc zero;
def two   : nat := suc one;
def three : nat := suc two;
def four  : nat := suc three;
def five  : nat := suc four;

-- First, the predecessor of n is m if n = suc m.
def pred (n m : nat) : * := eq nat n (suc m);

-- Our claim is a disjunction, whose first option is that n = 0.
def szc_l (n : nat) := eq nat n zero;

-- The second option is that n has a predecessor.
def szc_r (n : nat) := exists nat (pred n);

-- So the claim we are trying to prove is that either one of the above options
-- holds for every n.
def szc (n : nat) := or (szc_l n) (szc_r n);

-- And here's our proof!
def suc_or_zero : forall (n : nat), szc n :=
    -- We will prove this by induction.
    nat_ind szc
        -- For the base case, the first option holds, i.e. 0 = 0
        (or_intro_l (szc_l zero) (szc_r zero) (eq_refl nat zero))

        -- For the inductive case, suppose the theorem holds for n.
        (fun (n : nat) (_ : szc n) => 
            -- Then the right option holds for suc n, since suc n is the
            -- successor of n
            or_intro_r (szc_l (suc n)) (szc_r (suc n))
                (exists_intro nat (pred (suc n)) n (eq_refl nat (suc n))));

-- }}}

-- {{{ Recursive Definitions

-- The next step would normally be to define addition and prove properties of
-- addition. However, we need to take a very long and difficult detour in order
-- to be able to define addition in the first place. The normal way addition is
-- defined is by the following two equations:
--
-- 1)       n + 0 = n
-- 2) n + (suc m) = suc (n + m)
--
-- It is clear that this definition is ok, since m gets smaller with every
-- application of equation 2, until m reaches zero, whereupon we can use
-- equation 1. This argument, while perfectly reasonable, is deceptively
-- difficult to formalize. It turns out that this structure of recursively
-- defining a function by two equations similar to 1 and 2 is extremely common.
-- So, we will take the time to prove the following theorem.
--
-- Theorem (recursive definitions):
-- For every type A, element z : A, and function fS : nat -> A -> A, there
-- exists a unique function f : nat -> A satisfying
-- 1)                       f 0 = z
-- 2) forall n : nat, f (suc n) = fS n (f n)
--
-- Once we've proved this theorem, we can easily define addition such that,
-- i.e. that for any fixed n : nat, "n+" is the unique function satisfying
-- 1)                       n + 0 = n
-- 2) forall m : nat, n + (suc m) = suc (n + m)
-- Notice that this is the exact form we need in order to apply the theorem.
--
-- However, proving this theorem is *extremely long and difficult*. I would
-- recommend skipping this section and coming back to it after you are much
-- more used to perga. As such, I will go into a lot less detail on each of
-- these proofs than in the later sections.
--
-- Here's our game plan. We will define a relation R : nat -> A -> * such that
-- R x y iff for every relation Q : nat -> A -> * satisfying
-- 1) Q 0 z and
-- 2) forall (x : nat) (y : A), Q x y -> Q (suc x) (fS x y),
-- Q x y.
-- In more math lingo, we take R to be the intersection of every relation
-- satisfying 1 and 2. From there we will, with much effort, prove that R is
-- actually a function satisfying the equations we want it to.

-- {{{ Defining R
-- Here is condition 1 formally expressed in perga.
def cond1 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
    Q zero z;

-- Likewise for condition 2.
def cond2 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
    forall (n : nat) (y : A), Q n y -> Q (suc n) (fS n y);

-- From here we can define R.
def rec_rel (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
    forall (Q : nat -> A -> *), cond1 A z fS Q -> cond2 A z fS Q -> Q x y;
-- }}}

-- {{{ R is total
def total (A B : *) (R : A -> B -> *) := forall (a : A), exists B (R a);

def rec_rel_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel A z fS) :=
    fun (Q : nat -> A -> *) (h1 : cond1 A z fS Q) (h2 : cond2 A z fS Q) => h1;

def rec_rel_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel A z fS) :=
    fun (n : nat) (y : A) (h : rec_rel A z fS n y)
        (Q : nat -> A -> *) (h1 : cond1 A z fS Q) (h2 : cond2 A z fS Q) =>
        h2 n y (h Q h1 h2);

def rec_rel_total (A : *) (z : A) (fS : nat -> A -> A) : total nat A (rec_rel A z fS) :=
    let (R := rec_rel A z fS)
        (P (x : nat) := exists A (R x))
        (c1 := cond1 A z fS)
        (c2 := cond2 A z fS)
    in
    nat_ind P
    (exists_intro A (R zero) z (rec_rel_cond1 A z fS))
    (fun (n : nat) (IH : P n) =>
        exists_elim A (P (suc n)) (R n) IH
        (fun (y0 : A) (hy : R n y0) =>
            exists_intro A (R (suc n)) (fS n y0) (rec_rel_cond2 A z fS n y0 hy)))
    end;
-- }}}

-- {{{ Defining R2
def alt_cond1 (A : *) (z : A) (x : nat) (y : A) :=
    and (eq nat x zero) (eq A y z);

def cond_y2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A)
    (x2 : nat) (y2 : A) :=
        and (eq A y (fS x2 y2)) (rec_rel A z fS x2 y2);

def cond_x2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) (x2 : nat) :=
    and (pred x x2) (exists A (cond_y2 A z fS x y x2));

def alt_cond2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
    exists nat (cond_x2 A z fS x y);

def rec_rel_alt (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
    or (alt_cond1 A z x y) (alt_cond2 A z fS x y);
-- }}}

-- {{{ R = R2

-- {{{ R2 ⊆ R
def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
    rec_rel_alt A z fS x y -> rec_rel A z fS x y :=
    let (R := rec_rel A z fS)
        (R2 := rec_rel_alt A z fS)
        (ac1 := alt_cond1 A z x y)
        (ac2 := alt_cond2 A z fS x y)
    in
        fun (h : R2 x y) =>
            or_elim ac1 ac2 (R x y) h
            (fun (case1 : ac1) =>
                let
                    (x0 := and_elim_l (eq nat x zero) (eq A y z) case1)
                    (yz := and_elim_r (eq nat x zero) (eq A y z) case1)
                    (a1 := (eq_sym A y z yz) (R zero) (rec_rel_cond1 A z fS))
                in
                    (eq_sym nat x zero x0) (fun (n : nat) => R n y) a1
                end)
            (fun (case2 : ac2) =>
                let (h1 := cond_x2 A z fS x y)
                    (h2 := cond_y2 A z fS x y)
                in
                exists_elim nat (R x y) h1 case2
                (fun (x2 : nat) (hx2 : h1 x2) =>
                    let (hpred := and_elim_l (pred x x2) (exists A (h2 x2)) hx2)
                        (hex := and_elim_r (pred x x2) (exists A (h2 x2)) hx2)
                    in
                    exists_elim A (R x y) (h2 x2) hex
                    (fun (y2 : A) (hy2 : h2 x2 y2) =>
                        let (hpreim := and_elim_l (eq A y (fS x2 y2)) (R x2 y2) hy2)
                            (hR := and_elim_r (eq A y (fS x2 y2)) (R x2 y2) hy2)
                            (a1 := rec_rel_cond2 A z fS x2 y2 hR)
                            (a2 := (eq_sym A y (fS x2 y2) hpreim) (R (suc x2)) a1)
                        in
                            (eq_sym nat x (suc x2) hpred) (fun (n : nat) => R n y) a2
                        end)
                    end)
                end)
    end;
-- }}}

-- {{{ R ⊆ R2
def R2_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel_alt A z fS) :=
    or_intro_l (alt_cond1 A z zero z) (alt_cond2 A z fS zero z)
    (and_intro (eq nat zero zero) (eq A z z)
        (eq_refl nat zero)
        (eq_refl A z));

def R2_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel_alt A z fS) :=
    let (R := rec_rel A z fS)
        (R2 := rec_rel_alt A z fS)
    in
        fun (x2 : nat) (y2 : A) (h : R2 x2 y2) =>
        let (x := suc x2)
            (y := fS x2 y2)
            (cx2 := cond_x2 A z fS x y)
            (cy2 := cond_y2 A z fS x y x2)
        in
            or_intro_r (alt_cond1 A z x y) (alt_cond2 A z fS x y)
            (exists_intro nat cx2 x2
                (and_intro (pred x x2) (exists A cy2)
                    (eq_refl nat x)
                    (exists_intro A cy2 y2
                        (and_intro (eq A y y) (R x2 y2)
                            (eq_refl A y)
                            (R2_sub_R A z fS x2 y2 h)))))
        end
    end;

def R_sub_R2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
    rec_rel A z fS x y -> rec_rel_alt A z fS x y :=
    let (R := rec_rel A z fS)
        (R2 := rec_rel_alt A z fS)
    in
        fun (h : R x y) =>
            h R2 (R2_cond1 A z fS) (R2_cond2 A z fS)
    end;
-- }}}

-- }}}

-- {{{ R2 (hence R) is functional

def fl_in (A B : *) (R : A -> B -> *) (x : A) := forall (y1 y2 : B),
    R x y1 -> R x y2 -> eq B y1 y2;

def fl (A B : *) (R : A -> B -> *) := forall (x : A), fl_in A B R x;

def R2_zero (A : *) (z : A) (fS : nat -> A -> A) (y : A) :
    rec_rel_alt A z fS zero y -> eq A y z :=
    let (R2 := rec_rel_alt A z fS)
        (ac1 := alt_cond1 A z zero y)
        (ac2 := alt_cond2 A z fS zero y)
        (cx2 := cond_x2 A z fS zero y)
        (cy2 := cond_y2 A z fS zero y)
    in fun (h : R2 zero y) =>
        or_elim ac1 ac2 (eq A y z) h
        (fun (case1 : ac1) => and_elim_r (eq nat zero zero) (eq A y z) case1)
        (fun (case2 : ac2) =>
            exists_elim nat (eq A y z) cx2 case2
            (fun (x2 : nat) (h2 : cx2 x2) =>
                suc_nonzero x2
                (eq_sym nat zero (suc x2) (and_elim_l (pred zero x2) (exists A (cy2 x2)) h2))
                (eq A y z)))
    end;

def R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) :
    rec_rel_alt A z fS (suc x2) y -> exists A (cond_y2 A z fS (suc x2) y x2) :=
    let (R2 := rec_rel_alt A z fS)
        (x := suc x2)
        (ac1 := alt_cond1 A z x y)
        (ac2 := alt_cond2 A z fS x y)
        (cx2 := cond_x2 A z fS x y)
        (cy2 := cond_y2 A z fS x y)
        (goal := exists A (cy2 x2))
    in
        fun (h : R2 x y) =>
        or_elim ac1 ac2 goal h
        (fun (case1 : ac1) => suc_nonzero x2 (and_elim_l (eq nat x zero) (eq A y z) case1) goal)
        (fun (case2 : ac2) =>
            exists_elim nat goal cx2 case2
            (fun (x22 : nat) (hx22 : cx2 x22) =>
                let (hpred := and_elim_l (pred x x22) (exists A (cy2 x22)) hx22)
                    (hgoal := and_elim_r (pred x x22) (exists A (cy2 x22)) hx22)
                    (x2_x22 := suc_inj x2 x22 hpred)
                in
                    (eq_sym nat x2 x22 x2_x22)
                    (fun (n : nat) => exists A (cy2 n))
                    hgoal
                end))
    end;

def R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A z fS) :=
    let (R := rec_rel A z fS)
        (R2 := rec_rel_alt A z fS)
        (f_in := fl_in nat A R2)
    in nat_ind f_in
        (fun (y1 y2 : A) (h1 : R2 zero y1) (h2 : R2 zero y2) =>
            eq_trans A y1 z y2
            (R2_zero A z fS y1 h1)
            (eq_sym A y2 z (R2_zero A z fS y2 h2)))
        (fun (x2 : nat) (IH : f_in x2) (y1 y2 : A) (h1 : R2 (suc x2) y1) (h2 : R2 (suc x2) y2) =>
            let (x := suc x2)
                (cy1 := cond_y2 A z fS x y1 x2)
                (cy2 := cond_y2 A z fS x y2 x2)
                (goal := eq A y1 y2)
            in
                exists_elim A goal cy1 (R2_suc A z fS x2 y1 h1)
                (fun (y12 : A) (h12 : cy1 y12) =>
                    exists_elim A goal cy2 (R2_suc A z fS x2 y2 h2)
                    (fun (y22 : A) (h22 : cy2 y22) =>
                        let (y1_preim := and_elim_l (eq A y1 (fS x2 y12)) (R x2 y12) h12)
                            (y2_preim := and_elim_l (eq A y2 (fS x2 y22)) (R x2 y22) h22)
                            (R_x2_y12 := and_elim_r (eq A y1 (fS x2 y12)) (R x2 y12) h12)
                            (R_x2_y22 := and_elim_r (eq A y2 (fS x2 y22)) (R x2 y22) h22)
                            (R2_x2_y12 := R_sub_R2 A z fS x2 y12 R_x2_y12)
                            (R2_x2_y22 := R_sub_R2 A z fS x2 y22 R_x2_y22)
                            (y12_y22 := IH y12 y22 R2_x2_y12 R2_x2_y22)
                        in
                            eq_trans A y1 (fS x2 y12) y2
                            y1_preim
                            (eq_trans A (fS x2 y12) (fS x2 y22) y2
                                (eq_cong A A y12 y22 (fun (y : A) => fS x2 y) y12_y22)
                                (eq_sym A y2 (fS x2 y22) y2_preim))
                        end))
            end)
    end;

-- }}}

def rec_def (A : *) (z : A) (fS : nat -> A -> A) (x : nat) : A :=
    exists_elim A A (rec_rel A z fS x) (rec_rel_total A z fS x)
        (fun (y : A) (_ : rec_rel A z fS x y) => y);

-- }}}

-- -- For any such equations, there exists a function.
-- rec_def (A : *) (fzero : A) (fsuc : nat -> A -> A) : nat -> A := axiom;
--
-- -- Here's equation one.
-- rec_cond_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) := 
--   eq A (f zero) fzero;
--
-- -- And equation two.
-- rec_cond_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) :=
--   forall (n : nat) (y : A),
--     eq A (f n) y -> eq A (f (suc n)) (fsuc n y);
--
-- -- Said function satisfies the equations.
-- -- It satisfies equation one.
-- rec_def_sat_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) :
--   rec_cond_zero A fzero fsuc (rec_def A fzero fsuc) := axiom;
--
-- -- And two.
-- rec_def_sat_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) :
--   rec_cond_suc A fzero fsuc (rec_def A fzero fsuc) := axiom;
--
-- -- And, finally, this function is unique in the sense that if any other function
-- -- also satisfies the equations, it takes the same values as rec_def.
-- rec_def_unique (A : *) (fzero : A) (fsuc : nat -> A -> A) (f g : nat -> A) :
--   rec_cond_zero A fzero fsuc f ->
--   rec_cond_suc  A fzero fsuc f ->
--   rec_cond_zero A fzero fsuc g ->
--   rec_cond_suc  A fzero fsuc g ->
--   forall (x : nat), eq A (f x) (g x) := axiom;
--
-- -- Now we can safely define addition.
--
-- -- First, here's the RHS of equation 2 as a function, since it will show up
-- -- multiple times.
-- psuc (_ r : nat) := suc r;
--
-- -- And here's plus!
-- plus (n : nat) : nat -> nat := rec_def nat n psuc;
--
-- -- The first equation manifests itself as the familiar
-- --      n + 0 = 0.
-- plus_0_r (n : nat) : eq nat (plus n zero) n :=
--   rec_def_sat_zero nat n psuc;
--
-- -- The second equation, after a bit of massaging, manifests itself as the
-- -- likewise familiar
-- --      n + suc m = suc (n + m).
-- plus_s_r (n m : nat) : eq nat (plus n (suc m)) (suc (plus n m)) :=
--   rec_def_sat_suc nat n psuc m (plus n m) (eq_refl nat (plus n m));
--
-- -- We can now prove 1 + 1 = 2!
-- one_plus_one_two : eq nat (plus one one) two :=
--   -- 1 + (suc zero) = suc (1 + zero) = suc one
--   eq_trans nat (plus one one) (suc (plus one zero)) two
--
--   -- 1 + (suc zero) = suc (1 + zero)
--   (plus_s_r one zero)
--
--   -- suc (1 + zero) = suc one
--   (eq_cong nat nat (plus one zero) one suc (plus_0_r one));
--
-- -- 
-- -- We have successfully defined addition! Note that evaluating 1 + 1 to 2
-- -- requires a proof, unfortunately, since this computation isn't visible to
-- -- perga.
-- -- 
-- -- We will now prove a couple standard properties of addition.
-- -- 
--
-- -- First, associativity, namely that n + (m + p) = (n + m) + p.
-- plus_assoc : assoc nat plus := 
--   -- We prove this via induction on p.
--   nat_ind
--     (fun (p : nat) =>
--       forall (n m : nat),
--         eq nat (plus n (plus m p)) (plus (plus n m) p))
--
--     -- Base case: p = 0
--     -- WTS n + (m + 0) = (n + m) + 0
--     (fun (n m : nat) =>
--       -- n + (m + 0) = n + m = (n + m) + 0
--       (eq_trans nat (plus n (plus m zero)) (plus n m) (plus (plus n m) zero)
--         -- n + (m + 0) = n + m
--         (eq_cong nat nat (plus m zero) m (fun (p : nat) => plus n p) (plus_0_r m))
--
--         -- n + m = (n + m) + 0
--         (eq_sym nat (plus (plus n m) zero) (plus n m) (plus_0_r (plus n m)))))
--
--     -- Inductive step: IH = n + (m + p) = (n + m) + p
--     (fun (p : nat) (IH : forall (n m : nat), eq nat (plus n (plus m p)) (plus (plus n m) p)) (n m : nat) =>
--       -- WTS n + (m + suc p) = (n + m) + suc p
--       -- n + (m + suc p) = n + suc (m + p)
--       --                 = suc (n + (m + p))
--       --                 = suc ((n + m) + p)
--       --                 = (n + m) + suc p
--       eq_trans nat (plus n (plus m (suc p))) (plus n (suc (plus m p))) (plus (plus n m) (suc p))
--
--       -- n + (m + suc p) = n + suc (m + p)
--       (eq_cong nat nat (plus m (suc p)) (suc (plus m p)) (fun (a : nat) => (plus n a)) (plus_s_r m p))
--
--       -- n + suc (m + p) = (n + m) + suc p
--       (eq_trans nat (plus n (suc (plus m p))) (suc (plus n (plus m p))) (plus (plus n m) (suc p))
--         -- n + suc (m + p) = suc (n + (m + p))
--         (plus_s_r n (plus m p))
--
--         -- suc (n + (m + p)) = (n + m) + suc p
--         (eq_trans nat (suc (plus n (plus m p))) (suc (plus (plus n m) p)) (plus (plus n m) (suc p))
--           -- suc (n + (m + p)) = suc ((n + m) + p)
--           (eq_cong nat nat (plus n (plus m p)) (plus (plus n m) p) suc (IH n m))
--
--           -- suc ((n + m) + p) = (n + m) + suc p
--           (eq_sym nat (plus (plus n m) (suc p)) (suc (plus (plus n m) p))
--             (plus_s_r (plus n m) p)))));
--
-- -- Up next is commutativity, but we will need a couple lemmas first.
--
-- -- First, we will show that 0 + n = n.
-- plus_0_l : forall (n : nat), eq nat (plus zero n) n :=
--   -- We prove this by induction on n.
--   nat_ind (fun (n : nat) => eq nat (plus zero n) n)
--     -- base case: WTS 0 + 0 = 0
--     -- This is just plus_0_r 0
--     (plus_0_r zero)
--
--     -- inductive case
--     (fun (n : nat) (IH : eq nat (plus zero n) n) =>
--       -- WTS 0 + (suc n) = suc n
--       -- 0 + (suc n) = suc (0 + n) = suc n
--       eq_trans nat (plus zero (suc n)) (suc (plus zero n)) (suc n)
--       -- 0 + (suc n) = suc (0 + n)
--       (plus_s_r zero n)
--
--       -- suc (0 + n) = suc n
--       (eq_cong nat nat (plus zero n) n suc IH));
--
-- -- Next, we will show that (suc n) + m = suc (n + m).
-- plus_s_l (n : nat) : forall (m : nat), eq nat (plus (suc n) m) (suc (plus n m)) :=
--   -- We proceed by induction on m.
--   nat_ind (fun (m : nat) => eq nat (plus (suc n) m) (suc (plus n m)))
--     -- base case: (suc n) + 0 = suc (n + 0)
--     -- (suc n) + 0 = suc n = suc (n + 0)
--     (eq_trans nat (plus (suc n) zero) (suc n) (suc (plus n zero))
--       -- (suc n) + 0 = suc n
--       (plus_0_r (suc n))
--
--       -- suc n = suc (n + 0)
--       (eq_cong nat nat n (plus n zero) suc
--         -- n = n + 0
--         (eq_sym nat (plus n zero) n (plus_0_r n))))
--
--     -- inductive case
--     -- IH = suc n + m = suc (n + m)
--     (fun (m : nat) (IH : eq nat (plus (suc n) m) (suc (plus n m))) =>
--         -- WTS suc n + suc m = suc (n + suc m)
--         -- suc n + suc m = suc (suc n + m)
--         --               = suc (suc (n + m))
--         --               = suc (n + suc m)
--         (eq_trans nat (plus (suc n) (suc m)) (suc (plus (suc n) m)) (suc (plus n (suc m)))
--           -- suc n + suc m = suc (suc n + m)
--           (plus_s_r (suc n) m)
--
--           -- suc (suc n + m) = suc (n + suc m)
--           (eq_trans nat (suc (plus (suc n) m)) (suc (suc (plus n m))) (suc (plus n (suc m)))
--             -- suc (suc n + m) = suc (suc (n + m))
--             (eq_cong nat nat (plus (suc n) m) (suc (plus n m)) suc IH)
--
--             -- suc (suc (n + m)) = suc (n + suc m)
--             (eq_cong nat nat (suc (plus n m)) (plus n (suc m)) suc
--               -- suc (n + m) = n + suc m
--               (eq_sym nat (plus n (suc m)) (suc (plus n m)) (plus_s_r n m))))));
--
-- -- Finally, we can prove commutativity.
-- plus_comm (n : nat) : forall (m : nat), eq nat (plus n m) (plus m n) :=
--   -- As usual, we proceed by induction.
--   nat_ind (fun (m : nat) => eq nat (plus n m) (plus m n))
--
--   -- Base case: WTS n + 0 = 0 + n
--   -- n + 0 = n = 0 + n
--   (eq_trans nat (plus n zero) n (plus zero n)
--     -- n + 0 = n
--     (plus_0_r n)
--
--     -- n = 0 + n
--     (eq_sym nat (plus zero n) n (plus_0_l n)))
--
--   -- Inductive step:
--   (fun (m : nat) (IH : eq nat (plus n m) (plus m n)) =>
--     -- WTS n + suc m = suc m + n
--     -- n + suc m = suc (n + m)
--     --           = suc (m + n)
--     --           = suc m + n
--     (eq_trans nat (plus n (suc m)) (suc (plus n m)) (plus (suc m) n)
--       -- n + suc m = suc (n + m)
--       (plus_s_r n m)
--
--       -- suc (n + m) = suc m + n
--       (eq_trans nat (suc (plus n m)) (suc (plus m n)) (plus (suc m) n)
--         -- suc (n + m) = suc (m + n)
--         (eq_cong nat nat (plus n m) (plus m n) suc IH)
--
--         -- suc (m + n) = suc m + n
--         (eq_sym nat (plus (suc m) n) (suc (plus m n)) (plus_s_l m n)))));