The Coq mailing list

[richard Dapoigny <richard.dapoigny AT univ-smb.fr>]

Dear Coq users,

I have the following problem with the code fragment:

Record object : Type := {

ob_class : Type;

ob : ob_class}.

Class Lives : Type := {

n01 : nationalities;

h01 : house;

pr01 : lives h01 = n01

}.

Class hasColor : Type := {

h02 : house;

c01 : color;

pr03 : Color c01 = h02

}.

Hypothesis A001 : forall (x:hasColor)(y:Lives)(Xob:object), @ob_class Xob = house /\ @h02 x = @ob Xob /\ Color Red = (@h02 x) /\ lives (@h02 x) = Englishman.

I get the following error: Illegal application (Non-functional construction):
The _expression_ "ob" of type "house" cannot be applied to the term  "Xob" : "object"

The problem is that the type of @ob Xob is @ob_class Xob which is equal to house from the first assertion. The second assertion cannot take this assertion in account. So the question is: is there a way to overcome this behavior?

Thanks in advance for your answer,

Richard

--
Richard Dapoigny
Associate Professor - LISTIC Laboratory
University Savoie Mont-Blanc
5, chemin de Bellevue
Po. Box 80439
Annecy-le-Vieux 74940
FRANCE
https://www.listic.univ-smb.fr/en/presentation-en/members/lecturers/richard-dapoigny-en/

****** People who don't know history are condemned to repeat it. ******