How to implement OCaml function with the next type?

Question

I am studying Curry–Howard correspondence.

Given propositional logic statement: ¬(p ∨ q) -> (¬p ∧ ¬q).

I need to define a type (as proposition) and a function (as a proof) in OCaml.

I have defined type but do not know how to implement function:

type empty = | 
type ('a , 'b) coprod = Left of 'a | Right of 'b
let ex513: (('p, 'q) coprod -> empty) -> ('p -> empty) * ('q -> empty) = fun ?

What I did before posting a question:

1. I have verified that this statement is provable in intuitionistic logic.
2. Tried to understand constructively: if there is function1 that converts proof of p or proof of q to ⊥ then we can construct tuple (function2 that converts proof of p to ⊥, function3 that converts proof of q to ⊥). Implementation (function1(p), function1(q))
3. Implemented similar task to better understand the problem: p ∨ q -> ¬(¬p ∧ ¬q).

code:

let func1: ('p, 'q) coprod -> ('p-> empty) * ('q-> empty) -> empty = fun x (f, g)->
    match x with 
    | Left x -> f(x)
    | Right x -> g(x)

Answer 1

Defining

type 'a not = 'a -> empty

for the sake of concision, it is indeed a good idea to write a function

let left_branch: type p q. (p,q) coprod not -> p not = ...

and

let right_branch: type p q. (p,q) coprod not -> q not = ...

Once you have defined both functions (in other words proved the corresponding lemma), the solution can be reached by applying both lemma:

let de_morgan_law: type p q. (p,q) coprod not -> p not * q not =
  fun not_p_or_q -> left_branch not_p_or_q, right_branch not_p_or_q

If you have trouble writing the left_branch (or right function), remember that

let left x = Left x

has type 'a -> ('a,'any) coprod.