coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Problem with Coq, Index and Parameter types.

From: Theo Belaire <theo.belaire AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Problem with Coq, Index and Parameter types.
Date: Mon, 11 Apr 2016 16:03:26 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tyr.god.of.war42 AT gmail.com; spf=Pass smtp.mailfrom=tyr.god.of.war42 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ig0-f170.google.com
Ironport-phdr: 9a23:0h4XexRBB4nvIkPvSMPDvkbST9psv+yvbD5Q0YIujvd0So/mwa64YBSN2/xhgRfzUJnB7Loc0qyN4/CmBT1LuMrY+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq82VP1QD3WbkKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7uXqswPCRE2B/CgySGITxyZIDg+Nxhz+V5brv2Ouqupw32+QMMn/TKo5cTun5qZvDhTvjXFUZHYC7GjLh5ko3+pgqxW7qkknzg==

Hello, I have a problem relating to index vs parameterized types.

Here is the full source code, and the line where everything goes wrong.
https://github.com/tbelaire/FJ-Formalization/blob/wip/FJ_Definitions.v#L1326

I am working on a variant of Feather Weight Java, and the key types are ctable as a list [(Child_class, (Parent_class, fields, methods))].

I'm trying to prove some things about subsets and strict subsets.

The definition

Inductive ssub_ (CT:ctable) : typ -> typ -> Prop :=
| ssub_trans : forall t1 t2 t3,
ssub_ CT t1 t2 ->
ssub_ CT t2 t3 ->
ssub_ CT t1 t3
| ssub_extends : forall t1 t2, extends_ CT t1 t2 -> ssub_ CT t1 t2.

generates the inductive principle:

ssub__ind :
forall (CT : ctable) (P : typ -> typ -> Prop),
(forall t1 t2 t3 : typ,
ssub_ CT t1 t2 -> P t1 t2 -> ssub_ CT t2 t3 -> P t2 t3 -> P t1 t3) ->
(forall t1 t2 : cname, extends_ CT t1 t2 -> P t1 t2) ->
forall C D : typ, ssub_ CT C D -> P C D

but in my particular case I'm trying to apply it:

https://github.com/tbelaire/FJ-Formalization/blob/wip/FJ_Definitions.v#L1326

I need to have CT instantiated with (C, (F, fs2, ms2)) :: CT, which references C,

before I do the forall, causing the forall to generate a fresh variable C0, and get my proof to become stuck,

as the C referenced in P C D isn't the same as the C in the class table that it also mentions.

I do not know how to solve it, since changing the definition to:

Inductive ssub_ : ctable -> typ -> typ -> Prop :=

| ssub_trans : forall CT t1 t2 t3,

ssub_ CT t1 t2 ->

ssub_ CT t2 t3 ->

ssub_ CT t1 t3

| ssub_extends : forall CT t1 t2, extends_ CT t1 t2 -> ssub_ CT t1 t2.

is causing my more problems in my existing proofs, where induction on

H_sub: ssub_ (A, (B, fs, ms)) ::CT C D just throws out the information about A and B,

as the induction wants to be forall CTs, not just ones with A and B in front.

I have proven the old (parametric) induction principle in terms of the new (indexed) one,

and if it's possible to even just go `induction H_sub using ssub__ind_old.` to get the old

behaviour instead of needing to use `refine` to get it to work, that would be quite helpful.

[Coq-Club] Problem with Coq, Index and Parameter types., Theo Belaire, 04/11/2016