The Coq mailing list

[Colm Bhandal <bhandalc AT tcd.ie>]

Interesting,

I had not heard of A :< B before. Well, at least I know now that Parameter override is complex and unimplemented as of yet, so I will quit trying to hack it and return to my current solution which is to simply do everything in "Section A ... End A" blocks with hypotheses and generalise all my proofs and definitions. A tedious approach in comparison, but it still allows for unlimited layers of abstraction/refinement.

Thanks,

Colm

On 24 January 2013 12:39, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

2013/1/24 Colm Bhandal <bhandalc AT tcd.ie>:

> Hi Pierre,
>
> This is useful, but they key feature is lacks, and the one I am most
> interested in, is the ability to override Parameters with new definitions. I
> probably should have made that more clear. Consider the following.

I see. Overriding definitions is a much more complicated problem.
There would be a need to determine which proofs must be proved again
when a functor is applied etc. There has been a phd on this subject by
E. Soubiran I think.

> The problem with the proposed fix "you can rename the inductive type and
> give a definition to map the old name to the new name." is that the
> definitional equality inside a Module is for some reason not recognised
> outside it, and thus cbv reduction fails outside the Module. So it would be
> nice to get this sorted too:

For this problem you can use "Module A :< B" instead of "Module A:B"
in order to let A be transparent. The type of A is only checked
against B but A is not casted to type B. A has its own type but can be
used as of type B at any time (inside a functor for instance).

Cheers,
P.C.

> 1. Allow instantiation of a parameter by an inductive type.
> 2. Recognise definitional equality outside the Module where the definition
> occurred. Perhaps there is a workaround for this that I am not aware of, but
> it would be nice if it could be seamlessly built into the "simpl" tactic.
>
> All the best,
>
> Colm
>
>
>
>
> On 24 January 2013 11:58, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:
>>
>> Hello, notice that "Include A" allows to include all definitions of
>> module (type) A in the current module (type).
>>
>> This not subtyping but often helps to develop modules layer by layer.
>>
>> see: http://coq.inria.fr/coq/refman/Reference-Manual004.html#@command52
>>
>> Hope this helps,
>> Pierre
>>
>> 2013/1/24  <bhandalc AT tcd.ie>:
>> > Hi,
>> >
>> > I notice that Coq does not allow Module Sub-Typing, which would
>> > facilitate
>> > some really nice inheritance i.e.
>> >
>> > Module Type A
>> >
>> > ...
>> >
>> > Module Type B : A
>> >
>> > Right now, all that can be done is:
>> >
>> > Module Type A
>> >
>> > ...
>> >
>> > Module B : A
>> >
>> > If I am incorrect please stop me here? If not, read on.
>> >
>> > The above allows B to inherit all the results of A as long as B
>> > redefines the
>> > Parameters of A. Redefining the parameters is much like function
>> > override in
>> > OO programming and inheritance. Except in Coq it's enforced. It would be
>> > nice
>> > if the parameters didn't HAVE to be redefined. But the real problem is
>> > that
>> > after one step, you can't go any further i.e. it is impossible to then
>> > write:
>> >
>> > Module C : B
>> >
>> > Because B is not a Module Type, it is just an instance of A. What we
>> > would
>> > like is to define another Module TYPE B which is a subtype of A, just as
>> > in OO
>> > programming one can define subclasses of a superclass.
>> >
>> > To summarise, I have two suggestions:
>> >
>> > 1. Allow Module Sub-Typing i.e. inheritance.
>> > 2. Remove the enforcement of redefining all Parameters, and if they are
>> > not
>> > redefined, just carry them over as they are. (This is less crucial).
>> >
>> > Thoughts anyone?
>>
>