# curry howard – Axiomatic Geometry expressed with algebraic data types & functions

I’ve been trying to express an axiomatic geometry (1) using a typed functional language (OCaml so far).
My motivation comes from (2) and the claim “Programs correspond to logical proofs”.
In particular, I understand it as, should the program compile and type-check, then the proof is valid.

So far I am struggling to even express a simple proposition resulting from 2 axioms:

• A1: for two points a, b, the segment ab is congruent to the segment ba
• A2: if ab is congruent to pq, and also congruent to rs, then pq is congruent to rs
• P1: for two points a,b, ab is congruent to ab (reflexivity of congruence).

I particularly struggle with expressing dependencies in function arguments. For example A2 is a function that takes two congruences as input and outputs a new one, provided that the two input congruences share the first segment.

How would one go about it?

I am aware of previous work done with theorem provers (Coq,..) for this particular geometry. My understanding of this area is limited, and I am not sure that they only use the type theory assumed in (2) (in addition to hiding lots of things under the hood).

(1) W. SchwabhÃ¤user, W. Szmielew, A. Tarski (1983). Metamathematische Methoden in derGeometrie