The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

I've just tried some solution, but it seems rather heavy.

Inductive vars : Set := _x | _y.
Inductive preds : nat -> Set :=
    | _donkey : preds 1
    | _farmer : preds 1.

Inductive consts : Set := .


 Definition sigma : Signature.
 split.
 exact vars.
 exact consts.
 exact preds.
Defined.

Definition x : V sigma := _x.

Definition y : V sigma := _y.

Definition donkey : P sigma 1 := _donkey.

etc.

With this trick,
the formula definition like

Definition f : dForm sigma :=
    dall x dtrue.

is accepted.

Pierre


Pierre Casteran wrote:
> Hello,
>
>   I have some problems with type equivalence.
>
>    Let us consider the following declarations:
>
> Set Implicit Arguments.
>
> Record Signature : Type := {
>   V : Set; (* variables *)
>   C : Set; (* constants *)
>   P : nat -> Set (* predicates with arity *)
> }.
>
> Section form_def.
> Variable sigma : Signature.
>
> Inductive dForm : Set :=
>   |   dall : V sigma -> dForm -> dForm
>   |   dtrue : dForm.
>
> End form_def.
>
> Ok, I want to build some signature for an example:
>
> Inductive vars: Set := x | y.
> Inductive consts : Set :=.
> Inductive preds : nat -> Set :=
>   | donkey : preds 1
>   | farmer : preds 1.
>
> Definition sigma : Signature.
>  split.
>  exact vars.
>  exact consts.
>  exact preds.
> Defined.
>
> But I cannot build simply a formula :
>
> Implicit Arguments dtrue [sigma].
>
>
>
> Definition f : dForm sigma :=
>     dall x dtrue.
>
> Toplevel input, characters 99-100
>  > Definition f : dForm sigma :=     dall x dtrue.
>  >                                        ^
> Error: The term "x" has type "vars" while it is expected to have type "V 
> ?5"
>
>
> Nevertheless, putting explicit type constraint on x will work, but I 
> don't know why I should be so explicit, cause, by constraining the type 
> of f
> I gave enough information, no?
>
> Definition f0 : dForm sigma :=
>    dall (x:V sigma) dtrue.
>
> f0 is defined.
>
> Is there some way to avoid explicit type constraints like (x: V sigma) ?
>
> Pierre



--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran