The Coq mailing list

["Igor Zhirkov" <igorjirkov AT gmail.com>]

                                        Jonathan, it does indeed.

Thanks, Pierre-Marie. However,  what the reference manual tells is:

Axiom: This command links term to the name ident as its specification in the global context. The fact asserted by term is thus assumed as a postulate.

Local axiom:  Such axioms are never made accessible through their unqualified name by Import and its variants (see 2.5.8). You have to explicitly give their fully qualified name to refer to them.

Honestly, this does not make things evident and local axiom seems to be created to hide axioms from other sections, whereas I declare no sections at all.

Is this a bug or such behaviour is expected?

--Igor

Sent from Mailbird

На 04.03.2016 17:26:31, Jonathan Leivent <jonikelee AT gmail.com> писал:

On 03/04/2016 11:14 AM, Igor Zhirkov wrote:
> Hi all,
>
> I was refreshing my memory on coercions lately and saw some strange behaviour of Variables declared outside sections. MWE in Coq 8.5 :
>
> Record mixin_of (T:Type) := Mixin { bogus: nat }.
> Structure pack_type: Type := Pack { type: Type ; _ : mixin_of type }.
> Coercion type: pack_type >-> Sortclass.
>
> Variable cT: pack_type.
>
> Check cT. (* prints cT: pack_type *)
>
> Definition my_struct : mixin_of cT :=
> match cT return mixin_of cT with
> | Pack _ c => c
> end.
>
> Now that gives an error:
>
> Toplevel input, characters 92-93:
> Error:
> In environment
> T : Type
> c : mixin_of T
> The term "c" has type "mixin_of T" while it is expected to have type
> "mixin_of cT".
>
>
> Looks strange to me because Check cT found it.
> It works however:
> * if the code above is inside a section;
> * if cT is added to the argument list manually;
>
> The Coq reference manual says that using Variable keyword is equivalent to Local Parameter, but I failed to find any explanation of the Local Parameter itself. (link: https://coq.inria.fr/refman/Reference-Manual003.html#hevea_default36 [https://coq.inria.fr/refman/Reference-Manual003.html#hevea_default36] ).
>
> So, what is actually going on here and why an information about such a variable is lost sometimes?
>
>
> --Igor
>

Note that this works:

Definition my_struct : mixin_of cT :=
let x := cT in
match x return (mixin_of x) with
| Pack _ c => c
end.

although that might just add to the mystery.

-- Jonathan