The Coq mailing list

[Bingzhou <bingzhou.zheng AT gmail.com>]

Hi,

I am new to Coq. I have two questions now. 

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.

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

Lemma domain_dec: forall f:binFn, domain f.
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. 

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?

Thanks a lot,
Bingzhou