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:

I have verified that this statement is provable in intuitionistic logic.
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))
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)

octachron · Accepted Answer · 2021-12-27 17:07:50Z

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.

Thank you for the hint. I could not imagine calling 2 functions in 'parallel' and then combining result. All the time I was thinking in sequences: f1(x1) (f2(x2)). Here is my implementation. I will do your code suggestions later. let left_branch: (('p, 'q) coprod -> empty) -> 'p -> empty = fun f x -> f(Left(x));; let right_branch: (('p, 'q) coprod -> empty) -> 'q -> empty = fun f x -> f(Right(x));; let ex513: (('p, 'q) coprod -> empty) -> ('p -> empty) * ('q -> empty) = fun f -> left_branch(f),right_branch(f)

1 Answer 1