Require Import PeanoNat.
Import Nat.

Require Import Lists.List.
Import ListNotations.

Require Import Setoid.
Require Import Relation_Definitions.
Require Import Morphisms.

Require Import Relations.Relation_Operators.

Inductive type : Set :=
| tyvar : nat -> type
| tyfree : nat -> type
| arrow : type -> type -> type
| pi : type -> type.

Scheme Equality for type.

Inductive term : Set :=
| var : nat -> term
| free : nat -> term
| app1 : term -> term -> term
| app2 : term -> type -> term
| abs1 : type -> term -> term
| abs2 : term -> term.

Declare Custom Entry lambda.
Notation "<{ e }>" := e (e custom lambda at level 99).
Notation "( x )" := x (in custom lambda, x at level 99).
Notation "< x >" := (tyvar x) (in custom lambda, x at level 99).
Notation "{ x }" := x (x at level 99).
Notation "x" := x (in custom lambda at level 0, x constr at level 0).
Notation "S -> T" := (arrow S T) (in custom lambda at level 50, right associativity).
Notation "'Π' b" :=
  (pi b) (in custom lambda at level 90,
        b custom lambda at level 99, left associativity).
Notation "x · y" := (app1 x y) (in custom lambda at level 1, left associativity).
Notation "x ∙ y" := (app2 x y) (in custom lambda at level 1, left associativity).
Notation "'λ' t , x" :=
  (abs1 t x) (in custom lambda at level 90,
  t custom lambda at level 99,
  x custom lambda at level 99,
  left associativity).
Notation "'λ' , x" :=
  (abs2 x) (in custom lambda at level 90,
  x custom lambda at level 99,
  left associativity).
Coercion var : nat >-> term.

Definition context := list type.
Definition environment := list (nat * type).

Fixpoint lookup (E : environment) (x : nat) : option type :=
  match E with
  | [] => None
  | (x', σ) :: rest => if x =? x' then Some σ else lookup rest x
  end.

Lemma lookup_in : forall E x σ,
    lookup E x = Some σ -> In (x, σ) E.
Proof.
  induction E.
  - simpl; discriminate.
  - intros.
    destruct a as [y τ].
    simpl in H.
    destruct (x =? y) eqn:Heq.
    { apply eqb_eq in Heq; subst; inversion H; simpl; left; reflexivity. }
    simpl.
    right.
    auto.
Qed.

Reserved Notation "'[' x ':=' s ']' t" (in custom lambda at level 20).
Fixpoint substi (x : nat) (s t : term) : term :=
  match t with
  | var y => if x =? y then s else var y
  | free y => free y
  | <{ m · n }> => <{ ([x := s] m) · ([x := s] n) }>
  | <{ m ∙ n }> => <{ ([x := s] m) ∙ n }>
  | <{ λ α, m }> => <{ λ α, [{x + 1} := s] m }>
  | <{ λ , m }> => <{ λ , [x := s] m }>
  end

where "'[' x ':=' s ']' t" := (substi x s t) (in custom lambda).

Reserved Notation "'[' x ':=' s ']ₐ' t" (in custom lambda at level 20).
Fixpoint ty_subst (x : nat) (s : type) (t : type) : type :=
  match t with
  | tyvar n => if n =? x then s else tyvar n
  | tyfree y => tyfree y
  | <{ α -> β }> => <{ [ x := s ]ₐ α -> [ x := s ]ₐ β }>
  | <{ Π α }> => <{ Π [ {x + 1} := s ]ₐ α }>
  end

where "'[' x ':=' s ']ₐ' t" := (ty_subst x s t) (in custom lambda).

Reserved Notation "'[' x ':=' s ']ₜ' t" (in custom lambda at level 20).
Fixpoint substiₜ (x : nat) (s : type) (t : term) : term :=
  match t with
  | var y => var y
  | free y => free y
  | <{ m · n }> => <{ ([ x := s ]ₜ m) · ([ x := s ]ₜ n) }>
  | <{ m ∙ n }> => if type_eq_dec n (tyvar x) then
                    <{ m ∙ s }>
                  else <{ ([ x := s ]ₜ m) ∙ ([ x := s ]ₐ n) }>
  | <{ λ α, m }> => <{ λ α, [ x := s ]ₜ m }>
  | <{ λ , m }> => <{ λ , [ x := s ]ₜ m }>
  end

where "'[' x ':=' s ']ₜ' t" := (substiₜ x s t) (in custom lambda).

Reserved Notation "E ';' Γ '|-' t '::' T"
  (at level 101, t custom lambda, T custom lambda at level 0).

Inductive derivation : environment -> context -> term -> type -> Prop :=
| free_rule : forall E Γ x σ,
    lookup E x = Some σ -> E ; Γ |- {free x} :: σ
| var_rule : forall E Γ x σ,
    nth_error Γ x = Some σ -> E ; Γ |- x :: σ
| app_rule1 : forall E Γ t1 t2 σ τ,
    (E ; Γ |- t1 :: (σ -> τ)) ->
    (E ; Γ |- t2 :: σ) ->
    (E ; Γ |- t1 · t2 :: τ)
| app_rule2 : forall E Γ m a b,
    (E ; Γ |- m :: Π a) ->
    (E ; Γ |- m ∙ b :: ([ 0 := b ]ₐ a))
| abs_rule1 : forall E Γ σ τ m,
    (E ; σ :: Γ |- m :: τ) ->
    (E ; Γ |- λ σ, m :: (σ -> τ))
| abs_rule2 : forall E Γ m a,
    (E ; Γ |- m :: a) ->
    (E ; Γ |- λ, m :: Π a)

where "E ; Γ '|-' t '::' T" := (derivation E Γ t T).

Hint Constructors derivation : core.

Section examples.
  Let α := tyfree 0.
  Let β := tyfree 1.
  Let γ := tyfree 2.

  Example identity :
    [] ; [] |- λ , (λ <0>, 0) :: Π <0> -> <0>.
  Proof using Type.
    auto.
  Qed.

  Example identity_spec :
    [] ; [] |- (λ , λ <0>, 0) ∙ α :: (α -> α).
  Proof using Type.
    apply app_rule2 with (a := <{<0> -> <0>}>).
    exact identity.
  Qed.

  Example comp :
    [] ; [] |- λ , λ , λ , λ <2> -> <1>, λ <1> -> <0>, λ <2>, 1 · (2 · 0)
            :: Π Π Π (<2> -> <1>) -> (<1> -> <0>) -> <2> -> <0>.
  Proof using Type.
    repeat econstructor.
  Qed.

  Example comp_spec :
    [] ; [] |- ((λ , λ , λ , λ <2> -> <1>, λ <1> -> <0>, λ <2>, 1 · (2 · 0)) ∙ α ∙ β ∙ γ)
            :: ((α -> β) -> (β -> γ) -> α -> γ).
  Proof using Type.
    apply app_rule2 with (a := <{(α -> β) -> (β -> <0>) -> α -> <0>}>).
    apply app_rule2 with (a := <{Π (α -> <1>) -> (<1> -> <0>) -> α -> <0>}>).
    apply app_rule2 with (a := <{Π Π (<2> -> <1>) -> (<1> -> <0>) -> <2> -> <0>}>).
    repeat econstructor.
  Qed.

  Example book :
    [] ; [] |- λ , λ <0> -> <0>, λ <0>, 1 · (1 · 0) :: Π (<0> -> <0>) -> <0> -> <0>.
  Proof using Type.
    repeat econstructor.
  Qed.

End examples.

Theorem uniqueness_of_types : forall E Γ t σ τ,
    E ; Γ |- t :: σ -> E ; Γ |- t :: τ -> σ = τ.
Proof.
  intros E Γ t.
  generalize dependent Γ.
  induction t; intros; inversion H; inversion H0; subst;
    try (rewrite H4 in H9; inversion H9; reflexivity).
  - apply (IHt1 Γ <{σ0 -> σ}> <{σ1 -> τ}> H5) in H12.
    inversion H12.
    reflexivity.
  - assert (G : pi a = pi a0) ; eauto.
    inversion G.
    reflexivity.
  - assert (G : τ0 = τ1) ; eauto.
    subst.
    reflexivity.
  - apply (f_equal pi).
    eauto.
Qed.

Fixpoint find_type (E : environment) (Γ : context) (m : term) : option type :=
  match m with
  | var x => nth_error Γ x
  | free x => lookup E x
  | app1 t1 t2 => match find_type E Γ t1, find_type E Γ t2 with
                 | Some (<{ σ -> τ }>), Some σ' =>
                     if type_eq_dec σ σ'
                     then Some τ
                     else None
                 | _, _ => None
                 end
  | app2 t σ => match find_type E Γ t with
               | Some (pi τ) => Some <{[ 0 := σ ]ₐ τ}>
               | _ => None
               end
  | abs1 σ t => option_map (arrow σ) (find_type E (σ :: Γ) t)
  | abs2 t => option_map pi (find_type E Γ t)
  end.

Theorem find_type_correct : forall E Γ t σ,
    find_type E Γ t = Some σ -> E ; Γ |- t :: σ.
Proof.
  intros E Γ t.
  generalize dependent Γ.
  induction t ; auto.
  - intros.
    simpl in H.
    destruct (find_type E Γ t1) eqn:Heq ; inversion H.
    destruct t0 ; inversion H.
    destruct (find_type E Γ t2) eqn:Heq2; inversion H.
    destruct (type_eq_dec t0_1 t0); inversion H.
    subst.
    eauto.
  - intros.
    simpl in H.
    destruct (find_type E Γ t0) eqn:Heq; simpl in H; inversion H ; eauto.
    destruct t2; inversion H; auto.
  - intros.
    simpl in H.
    destruct (find_type E (t0 :: Γ) t1) eqn:Heq; inversion H.
    auto.
  - intros.
    simpl in H.
    destruct (find_type E Γ t0) eqn:Heq; inversion H.
    auto.
Qed.

Definition legal (t : term) := exists E Γ σ, E ; Γ |- t :: σ.

Lemma no_self_referential_types : forall σ τ,
    σ <> <{ σ -> τ }>.
Proof.
  induction σ; intros τ contra; inversion contra.
  apply (IHσ1 σ2).
  assumption.
Qed.

Theorem no_self_application : forall t,
    ~ (legal <{t · t}>).
Proof.
  intros t [E [Γ [σ H]]].
  inversion H.
  subst.
  assert (G : <{ σ0 -> σ }> = σ0).
  { apply uniqueness_of_types with (E := E) (Γ := Γ) (t := t); assumption. }
  symmetry in G.
  exact (no_self_referential_types σ0 σ G).
Qed.

Fixpoint β_reduce (m : term) : term :=
  match m with
  | var x => var x
  | free x => free x
  | <{ (λ α , m) · n }> => <{ [0 := n] m }>
  | <{ m · n }> => <{ {β_reduce m} · {β_reduce n} }>
  | <{ λ α, m }> => <{ λ α , {β_reduce m} }>
  | <{ (λ , m) ∙ n }> => <{ [0 := n]ₜ m }>
  | <{ m ∙ n }> => <{ {β_reduce m} ∙ n }>
  | <{ λ , m }> => <{ λ, {β_reduce m} }>
  end.

Reserved Notation "t1 '→β' t2" (at level 50).
Inductive β_reduce_r : term -> term -> Prop :=
| var_β : forall x, var x →β var x
| free_β : forall x, free x →β free x
| redex1_β : forall α m n, <{ (λ α, m) · n }> →β <{ [0 := n] m }>
| redex2_β : forall m n, <{ (λ , m) ∙ n }> →β <{ [0 := n]ₜ m }>
| app1_compat_β_l : forall m n m',  m →β m' -> <{ m · n }> →β <{ m' · n  }>
| app1_compat_β_r : forall m n n',  n →β n' -> <{ m · n }> →β <{ m  · n' }>
| app2_compat_β : forall m n m', m →β m' -> <{ m ∙ n }> →β <{ m' ∙ n }>
| abs1_compat_β : forall α m m', m →β m' -> <{ λ α, m }> →β <{ λ α, m' }>
| abs2_compat_β : forall m m', m →β m' -> <{ λ , m }> →β <{ λ , m' }>

where "t1 '→β' t2" := (β_reduce_r t1 t2).

Definition β_reduce_r_ext := clos_refl_sym_trans term β_reduce_r.

Notation "t1 '↠β' t2" := (β_reduce_r_ext t1 t2) (at level 50).

(* Section church_rosser. *)

(*   Reserved Notation "t1 '↠' t2" (at level 50). *)
(*   Inductive helper_relation : term -> term -> Prop := *)
(*   | sym_h : forall t, t ↠ t *)
(*   | abs1_compat_h : forall α m m', m ↠ m' -> <{ λ α, m }> ↠ <{ λ α, m' }> *)
(*   | abs2_compat_h : forall m m', m ↠ m' -> <{ λ , m }> ↠ <{ λ , m' }> *)
(*   | app1_compat_h : forall m m' n n', m ↠ m' -> n ↠ n' -> <{ m · n }> ↠ <{ m' · n' }> *)
(*   | app2_compat_h : forall m m' n, m ↠ m' -> <{ m ∙ n }> ↠ <{ m' ∙ n }> *)
(*   | redex1_h : forall α m n, <{ (λ α, m) · n }> ↠ <{ [0 := n] m }> *)
(*   | redex2_h : forall m n, <{ (λ , m) ∙ n }> ↠ <{ [0 := n]ₜ m }> *)

(*   where "t1 '↠' t2" := (helper_relation t1 t2). *)

(*   Lemma substitution_lemma : forall M N L x y, *)
(*       x < y -> *)
(*       <{[y := L] ([x := N] M)}> = <{[x := [y := L] N] ([{y + 1} := L] M)}>. *)
(*   Proof. *)
(*     induction M ; auto. *)
(*     - intros N L x y H. *)
(*       simpl. *)
(*       destruct (x =? n) eqn:Heq. *)
(*       + rewrite eqb_eq in Heq. *)
(*         subst. *)
(*         destruct (y =? n) eqn:Heq2. *)
(*         { rewrite eqb_eq in Heq2. symmetry in Heq2. apply lt_neq in H. contradiction. } *)
(*         apply lt_lt_add_r with (p := 1) in H. *)
(*         apply lt_neq in H. *)
(*         apply eqb_neq in H. *)
(*         rewrite eqb_sym in H. *)
(*         rewrite H. *)
(*         simpl. *)
(*         rewrite eqb_refl. *)
(*         reflexivity. *)
(*       + destruct (y =? n) eqn:Heq2. *)
(*         * simpl. *)
(*           rewrite Heq2. *)

(*         * simpl. *)
(*           rewrite Heq2. *)
(*           rewrite Heq. *)
(*           reflexivity. *)
(*     - intros n p x y H1 H2. *)
(*       simpl. *)
(*       rewrite IHm1 ; auto. *)
(*       rewrite IHm2 ; auto. *)
(*     - intros n p x y H1 H2. *)
(*       simpl. *)
(*       rewrite IHm ; auto. *)
(*     - intros n p x y H1 H2. *)
(*       simpl. *)
(*       rewrite IHm. *)
(*       + Abort. *)

(*   Lemma reduct_in_subst : forall m n n' x, *)
(*       n ↠ n' -> <{ [x := n] m }> ↠ <{ [x := n'] m }>. *)
(*   Proof. *)
(*     induction m ; try (intros; simpl; constructor; auto). *)
(*     intros ℓ ℓ' x H. *)
(*     simpl. *)
(*     destruct (x =? n) ; auto using helper_relation. *)
(*   Qed. *)

(*   Lemma subst_reduct : forall m m' n n' x, *)
(*       m ↠ m' -> n ↠ n' -> <{ [x := n] m }> ↠ <{ [x := n'] m' }>. *)
(*   intros m m' n n' x H. *)
(*   generalize dependent n. *)
(*   generalize dependent n'. *)
(*   generalize dependent x. *)
(*   induction H ; try (intros; simpl; auto using helper_relation; fail). *)
(*   - intros x n' n H. *)
(*     apply reduct_in_subst. *)
(*     assumption. *)
(*   - intros x p q H. *)
(*     simpl. *)
(*   (* | redex1_h : forall α m n, <{ (λ α, m) · n }> ↠ <{ [0 := n] m }> *) *)
(*     assert (G : <{ (λ α, [{x + 1} := q] m) · ([x := q] n) }> *)
(*   ↠ <{ [0 := [x := q] n] ([{x + 1} := q] m) }>). *)
(*     { apply redex1_h. } *)

(*   Lemma abs1_char : forall α m n, *)
(*       <{ λ α, m }> ↠ n -> exists m', n = <{ λ α, m' }> /\ m ↠ m'. *)
(*   Proof. *)
(*     intros α m n H1. *)
(*     inversion H1; subst. *)
(*     - exists m. *)
(*       split; auto. *)
(*       constructor. *)
(*     - exists m'. *)
(*       split; auto. *)
(*   Qed. *)

(*   Lemma abs2_char : forall m m', *)
(*       <{ λ, m }> ↠ m' -> exists n, m' = <{λ, n}> /\ m ↠ n. *)
(*   Proof. *)
(*     intros m m' H. *)
(*     inversion H; subst. *)
(*     - exists m. *)
(*       split; auto; try constructor. *)
(*     - exists m'0. *)
(*       split; auto; try constructor. *)
(*   Qed. *)

(*   Lemma app1_char : forall m n l, *)
(*       <{ m · n }> ↠ l *)
(*       -> (exists m' n', l = <{ m' · n' }> /\ m ↠ m' /\ n ↠ n') \/ *)
(*           (exists α p, m = <{ λ α, p }> /\ l = <{[0 := n] p}>). *)
(*   Proof. *)
(*     intros m n l H. *)
(*     inversion H ; subst ; auto. *)
(*     - left. *)
(*       exists m, n. *)
(*       split ; auto. *)
(*       split ; constructor. *)
(*     - left. *)
(*       exists m', n'. *)
(*       auto. *)
(*     - right. *)
(*       exists α, m0. *)
(*       auto. *)
(*   Qed. *)

(*   Lemma helper_diamond : forall m m1 m2, *)
(*       m ↠ m1 -> m ↠ m2 -> exists n, m1 ↠ n /\ m2 ↠ n. *)
(*   Proof. *)
(*     intros m m1 m2 H1. *)
(*     generalize dependent m2. *)
(*     induction H1. *)
(*     - intros m2 H2. *)
(*       exists m2. *)
(*       split ; try constructor; auto. *)
(*     - intros m2 H2. *)
(*       apply abs1_char in H2 as [t [G1 G2]]. *)
(*       subst. *)
(*       apply (IHhelper_relation t) in G2 as [n [F1 F2]]. *)
(*       exists <{λ α, n}>. *)
(*       split; constructor; assumption. *)
(*     - intros m2 H2. *)
(*       apply abs2_char in H2 as [n [G1 G2]]. *)
(*       subst. *)
(*       apply (IHhelper_relation n) in G2 as [n' [F1 F2]]. *)
(*       exists <{λ, n'}>. *)
(*       split; constructor; assumption. *)
(*     - intros m2 H2. *)
(*       apply app1_char in H2 as [[p [q [G1 [G2 G3]]]] | H2]; subst. *)
(*       + apply IHhelper_relation1 in G2 as [p' [Hp1 Hp2]]. *)
(*         apply IHhelper_relation2 in G3 as [q' [Hq1 Hq2]]. *)
(*         exists <{p' · q'}>. *)
(*         split; auto using helper_relation. *)
(*       + destruct H2 as [α [p [G1 G2]]]. *)
(*         subst. *)
(*         apply abs1_char in H1_ as [l [Hm Hl]]. *)
(*         subst. *)
(*         exists <{[0 := n'] l}>. *)
(*         split. *)
(*         * constructor. *)
(*         * *)
(*         (* apply IHhelper_relation1 in H1_. *) *)
(*         (* apply IHhelper_relation2 in H1_0. *) *)

(* End church_rosser. *)

Reserved Notation "t1 ≡ t2" (at level 50).
Inductive β_equiv : term -> term -> Prop :=
| reduce : forall t1 t2, β_reduce t1 = t2 -> t1 ≡ t2
| refl_β : forall t, t ≡ t
| sym_β : forall t1 t2, t1 ≡ t2 -> t2 ≡ t1
| trans_β : forall t1 t2 t3,
    t1 ≡ t2 -> t2 ≡ t3 -> t1 ≡ t3

where "t1 ≡ t2" := (β_equiv t1 t2).

Hint Constructors β_equiv : core.

Instance β_equiv_equiv : Equivalence β_equiv.
Proof.
  constructor; eauto.
Qed.

(* Proving these requires proving CR *)
Instance β_equiv_app1_l {t : term} : Proper (β_equiv ==> β_equiv) (fun s => app1 s t).
Proof.
Abort.

Instance β_equiv_app2 {σ : type} : Proper (β_equiv ==> β_equiv) (fun t => app2 t σ).
Proof.
Abort.

Instance β_equiv_abs2 : Proper (β_equiv ==> β_equiv) abs2.
Proof.
  intros x y H.
  induction H; auto.
  - constructor.
    simpl.
    rewrite H.
    reflexivity.
  - rewrite IHβ_equiv1.
    rewrite IHβ_equiv2.
    reflexivity.
Qed.

Example test t1 t2 : t1 ≡ t2 -> abs2 t1 ≡ abs2 t2.
Proof.
  intros H.
  rewrite H.
  reflexivity.
Qed.

Ltac simple_compute :=
    repeat (eapply trans_β;
      try (apply reduce; reflexivity)).

Section book_examples.
  Let α := tyfree 0.
  Let β := tyfree 1.
  Let γ := tyfree 2.

  Example ex3_2 :
    [] ; [] |- λ , λ , λ , λ <2> -> <1>, λ <1> -> <0>, λ <2>, 1 · (2 · 0)
            :: Π Π Π (<2> -> <1>) -> (<1> -> <0>) -> <2> -> <0>.
  Proof using Type.
    repeat econstructor.
  Qed.

  Let nat' := tyfree 3.
  Let bool' := tyfree 4.
  Example ex3_4 :
    [] ; [] |- (λ , λ , λ <1> -> <1>, λ <1> -> <0>, λ <1>, 1 · (2 · (2 · 0))) ∙ nat' ∙ bool'
            :: ((nat' -> nat') -> (nat' -> bool') -> nat' -> bool').
  Proof using Type.
    apply app_rule2 with (a := <{(nat' -> nat') -> (nat' -> <0>) -> nat' -> <0>}>).
    apply app_rule2 with (a := <{Π (<1> -> <1>) -> (<1> -> <0>) -> <1> -> <0>}>).
    repeat econstructor.
  Qed.

  Example ex3_5 : forall σ,
    [(0, <{Π <0>}>)] ; [] |- {free 0} ∙ σ :: σ.
  Proof using Type.
    intros.
    apply app_rule2 with (a := <{<0>}>).
    auto.
  Qed.

  Example ex3_6a : [] ; [] |-
    λ , λ , λ nat' -> <1>, λ <1> -> nat' -> <0> , λ nat', 1 · (2 · 0) · 0 ::
    Π Π (nat' -> <1>) -> (<1> -> nat' -> <0>) -> nat' -> <0>.
  Proof using Type.
    repeat econstructor.
  Qed.

  Example ex3_6b : [] ; [] |-
    λ, λ ((α -> γ) -> <0>), λ (α -> β), λ (β -> γ),
        2 · (λ α, 1 · (2 · 0)) ::
    Π ((α -> γ) -> <0>) -> (α -> β) -> (β -> γ) -> <0>.
  Proof using Type.
    repeat econstructor.
  Qed.
End book_examples.

Section numbers_bools.
  Definition nat' := <{Π (<0> -> <0>) -> <0> -> <0>}>.
  Definition zero := <{λ , λ <0> -> <0>, λ <0>, 0}>.
  Definition one  := <{λ , λ <0> -> <0>, λ <0>, 1 · 0}>.
  Definition two  := <{λ , λ <0> -> <0>, λ <0>, 1 · (1 · 0)}>.

  Definition succ := <{λ {nat'}, λ , λ <0> -> <0>, λ <0>, 1 · (2 ∙ <0> · 1 · 0)}>.
  Definition add  := <{λ {nat'}, λ {nat'}, λ , λ <0> -> <0>, λ <0>,
                  3 ∙ <0> · 1 · (2 ∙ <0> · 1 · 0)
        }>.

  Example zero_nat : [] ; [] |- zero :: nat'.
  Proof using Type.
    repeat econstructor.
  Qed.

  Example succ_nat_nat : [] ; [] |- succ :: (nat' -> nat').
  Proof using Type.
    unfold nat'.
    repeat econstructor.
    apply app_rule2 with (a := <{(<0> -> <0>) -> <0> -> <0>}>).
    repeat econstructor.
  Qed.

  Example succ_zero_one : app1 succ zero ≡ one.
  Proof using Type.
    simple_compute.
  Qed.

  Example succ_one_two : app1 succ one ≡ two.
  Proof using Type.
    simple_compute.
  Qed.

  Example one_p_one_two : <{{add} · {one} · {one}}> ≡ two.
  Proof using Type.
    simple_compute.
  Qed.

  Definition bool' := <{Π <0> -> <0> -> <0>}>.
  Definition true  := <{λ , λ <0>, λ <0>, 1}>.
  Definition false := <{λ , λ <0>, λ <0>, 0}>.
  Definition neg   := <{λ {bool'}, λ , (0 ∙ <0>) · ({false} ∙ <0>) · ((true) ∙ <0>)}>.

  Example neg_true_false : app1 neg true ≡ false.
  Proof using Type.
    simple_compute.
  Qed.

  Example neg_false_true : app1 neg false ≡ true.
  Proof using Type.
    simple_compute.
  Qed.

  Definition M := <{
    λ {bool'}, λ {bool'}, λ , λ <0>, λ <0>,
      3 ∙ <0> · (2 ∙ <0> · 1 · 0) · (2 ∙ <0> · 0 · 0)
  }>.

  (* M is and *)
  Example M_true_true : <{{M} · {true} · {true}}> ≡ true.
  Proof using Type.
    simple_compute.
  Qed.

  Example M_true_false : <{{M} · {true} · {false}}> ≡ false.
  Proof using Type.
    simple_compute.
  Qed.

  Example M_false_true : <{{M} · {false} · {true}}> ≡ false.
  Proof using Type.
    simple_compute.
  Qed.

  Example M_false_false : <{{M} · {false} · {false}}> ≡ false.
  Proof using Type.
    simple_compute.
  Qed.

  Definition or := <{
    λ {bool'}, λ {bool'},
        1 ∙ {bool'} · {true} · 0
  }>.

  Example or_true_true : <{{or} · {true} · {true}}> ≡ true.
  Proof using Type.
    simple_compute.
  Qed.

  Example or_true_false : <{{or} · {true} · {false}}> ≡ true.
  Proof using Type.
    simple_compute.
  Qed.

  Example or_false_true : <{{or} · {false} · {true}}> ≡ true.
  Proof using Type.
    simple_compute.
  Qed.

  Example or_false_false : <{{or} · {false} · {false}}> ≡ false.
  Proof using Type.
    simple_compute.
  Qed.

  Definition xor := <{
    λ {bool'}, λ {bool'}, 1 ∙ {bool'} · ({neg} · 0) · 0
  }>.

  Example xor_true_true : <{{xor} · {true} · {true}}> ≡ false.
  Proof using Type.
    simple_compute.
  Qed.

  Example xor_true_false : <{{xor} · {true} · {false}}> ≡ true.
  Proof using Type.
    simple_compute.
  Qed.

  Example xor_false_true : <{{xor} · {false} · {true}}> ≡ true.
  Proof using Type.
    simple_compute.
  Qed.

  Example xor_false_false : <{{xor} · {false} · {false}}> ≡ false.
  Proof using Type.
    simple_compute.
  Qed.

  Definition impl := <{
      λ {bool'}, λ {bool'},
          1 ∙ {bool'} · 0 · {true}
  }>.

  Example impl_true_true : <{{impl} · {true} · {true}}> ≡ true.
  Proof using Type.
    simple_compute.
  Qed.

  Example impl_true_false : <{{impl} · {true} · {false}}> ≡ false.
  Proof using Type.
    simple_compute.
  Qed.

  Example impl_false_true : <{{impl} · {false} · {true}}> ≡ true.
  Proof using Type.
    simple_compute.
  Qed.

  Example impl_false_false : <{{impl} · {false} · {false}}> ≡ true.
  Proof using Type.
    simple_compute.
  Qed.

  Definition is_zero := <{
      λ {nat'}, 0 ∙ {bool'} · (λ {bool'}, {false}) · {true}
  }>.

  Example zero_is_zero : app1 is_zero zero ≡ true.
  Proof using Type.
    simple_compute.
  Qed.

  Example one_not_zero : app1 is_zero one ≡ false.
  Proof using Type.
    simple_compute.
  Qed.

End numbers_bools.