(* A demonstration of Lambdas/Exponentials as Codatatypes in Coq
 * See https://blog.ielliott.io/lambdas-are-codatatypes *)

(* In Coq, we can define the type as follows: *)
CoInductive Lambda {A B : Set} : Set := Abst { Apply : A -> B }.
Arguments Abst {A B}.

(* Here is the example definition and an example of it being used: *)
Definition inc x := x + 1.
Definition inc' : Lambda := (Abst inc).

(* As we see, inc' has to be explicitly applied, while inc is
   evaluated by/inside of Gallina itself. *)
Compute (inc 0).                (* = 1 : bool *)
Compute (Apply inc' 0).         (* = 1 : bool *)

(* It turns out that this is rather trivial in Coq, as this amounts to
   not much more than your average joe's higher order abstract syntax. *)
Theorem eta_apply : forall (A B : Set) (f : A -> B),
    (Apply (Abst f)) = f.
Proof. easy. Qed.