The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 05/28/2012 01:33 PM, Bingzhou wrote:
> 1. I write the following scripts:
>
> Definition binFn : Type := R ->  R ->  R.
>
> Definition nonEmptyDomain (f: binFn): Prop :=
>   exists x: R, exists y: R, exists z: R, z = f x y.
>    

This is an overly complicated definition.  A proposition [nonEmptyDomain 
f] is true iff the type [R] has at least one element.  That is, the 
definition of [f] doesn't matter, so you probably want to rethink your 
formalization.

> Inductive domain (f: binFn) : Type :=
> | eDom: ~nonEmptyDomain f ->  domain f
> | neDom: nonEmptyDomain f ->  domain f.
>
> Lemma domain_dec: forall f:binFn, domain f.
>    

I don't think this theorem is provable without nonstandard axioms.  If 
such a value as [domain_dec] existed, it would be easy to use it to 
build a halting problem oracle (set [R] equal to propositions about 
Turing machines), so you should ask yourself if this is really what you 
want to prove.

> proof.
>
>      *** Declarative Mode ***
> ______________________________________
> thesis :=
>   forall f : binFn, domain f
>
> I read 11.3 Language description of Coq Reference-Manual, but I cannot
> understand what "Declarative Mode" really means in this proof.
>    

Coq has a "declarative mode" with very few users, and I don't recommend 
using it.  Perhaps you just meant to type [Proof] instead of [proof]?  
Writing [proof] explicitly asks to use the declarative mode.

> 2. I want to write a procedure which returns different values based on if the
> domain of a binary function is empty or not. I wonder if the way that I define
> the domain of a binary function above is correct. If not, what should I
> formalize it?
>    

You could certainly write functions that discriminate on whether a type 
is empty or not, if an appropriate proof is passed in.  However, I've 
never seen this done, so probably the most useful thing is for you to 
explain more context on your development, so that we can offer 
bigger-picture advice.