CODEWITHSUNDEEP
functioncoq
osseum
osseum

Reputation: 186

Defining function in Coq

Let assume that: 

Axiom inverse1: forall a:G, exists b:G, P a b.
Axiom only_one: forall a b1 b2:G, P a b1 /\ P a b2 -> b1 = b2.

These two axioms define a map G -> G. I want to define this mapping as a Coq function.

Upvotes: 1

Views: 685

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23622

You can't define this function in Coq without relying on extra information or axioms. The problem is that the exists quantifier lives in sort Prop (i.e., it is a proposition), and Coq's logic prevents one from using the proof of a proposition or an axiom to build terms of computational nature in most cases (i.e. things whose type lives in Type or Set, as G in your example probably is). Check the reference manual (section 4.5.4) for more information. Instead of assuming axioms like the ones you gave, theories in Coq would tend to assume just the existence of a function:

Axiom f : G -> G.
Axiom f_in_P : forall x : G, P x (f x).

Upvotes: 2

Related Questions