The Coq mailing list

[Gregory Malecha <gregory AT bedrocksystems.com>]

Hi Richard --

I would hope that there is a nicer solution to your problem, but there isn't enough context in your email for me to know exactly where you're going. In general, if you want Coq to use information of this sort, you need to express it explicitly using a dependent pattern match. In many cases, you can wrap this up in a definition, but essentially what it would look like is the eliminator for the equality type:

About eq_rect.

eq_rect : forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, x = y -> P y

Note that here you get to pick anything that you want for [P]. In your context, you would set [P := fun x => x], and the equality proof would be the one that you want to "use". Depending on what way you want to use it, you can either use [eq_sym] to swap the order, or rewrite the equality to be the other direction.

Hope this helps.

Just as an FYI, the last time that I worked on encoding objects inside Coq, was before universe polymorphism and at that point I quickly ran into universe issues. I think it should be more tractable at this point though.

On Sun, Sep 6, 2020 at 3:14 PM richard Dapoigny <richard.dapoigny AT univ-smb.fr> wrote:

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. ******

--

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING