I proved False! about coq

[coqbot]

Les variables de sections ont des noms courts a l'interieur du noyaux
et des nom longs a l'exterieur. D'ou la possibilite de contourner la
verification de noms doubles et de faire une preuve suivante:

Section S1.
Local a:=Set.
Definition z:a:=nat.
Section S2.
Local a:=False.
Lemma f:False.
Exact z.
Save.
End S2.
End S1.
Check f.

Je l'ai passe dans la V7 distribuee...

Jacek

[coqbot]

Hugo Herbelin <herbelin@ pauillac.inria.fr>
Bonjour,

Les variables de sections ont des noms courts a l'interieur du noyaux
et des nom longs a l'exterieur. D'ou la possibilite de contourner la
verification de noms doubles et de faire une preuve [de False].

Oui, j'avais adopté le principe que les variables de section étaient
des objets globaux, car partagées pour la durée de vie de la section,
susceptibles d'avoir des implicites, d'être déclarées comme coercions
ou comme hints, et, d'une certaine manière (discutable et discutée)
persistant au delà de la fermeture de la section dans le sens où elles
font partie de la structure du document mathématique rédigé par
l'utilisateur.

Dans la foulée, j'avais rompu avec l'unicité du nom court pour
autoriser des variables de section qualifiées, c'est-à-dire pouvant
partager le même nom court si définies à des niveaux de section
différents. Cette modification est a posteriori indépendante du souci
d'expliciter la différence entre les 2 notions (notamment donc de
pouvoir ou pas avoir des implicites, et être déclarable ou pas comme
coercion ou comme hint).

Pour caractériser ce qui relevait des déclarations "globales",
j'avais introduit le type suivant

type global_reference =
| VarRef of section_path
| ConstRef of constant_path
| IndRef of inductive_path
| ConstructRef of constructor_path

qui s'est avéré être pratique pour typer les fonctions s'appliquant
aux "globaux".

Ce type est avantageusement utilisé dans rawconstr et pattern où il
simplifie le code, et mon intention était de l'introduire dans constr
aussi.

Sous prétexte que la gestion des références dans constr allait de
toutes façons changer à l'occasion de l'introduction des modules (et
aussi que ce fichu vecteur de variables passé aux const, ind et cstr,
allait peut-être servir un jour...), cette modif a toujours été
repoussée. D'où le "trou de sécurité" exploité par Jacek.

En résumé, mon opinion est que

• dans la version actuelle (sans modules), l'abstraction
  "global_reference" est pertinente vis à vis de l'utilisation comparée
  que l'on fait des variables de section et des variables de but.

• ou bien on accentue cette différence en distinguant bien dans la
  syntaxe vars de sec et vars de but, ou bien on tend à les fusionner,
  c'est-à-dire à autoriser les vars de but à être coercion, hint, avec
  implicites, ce qui veut dire que les preuves n'ont pas seulement leur
  propre environnement de constructions, mais aussi leur propre
  environnement d'objets non purement logiques (hints and co).

• le choix d'avoir des noms longs ou courts (et de l'assumer jusque
  bout avec des tests de non redéfinition appropriés) pour les variables
  de section (et de but après tout) reste un choix indépendant des
  points précédents.

                                            Hugo
  

[coqbot]

Résolu: le choix fait est d'interdire les variables de section d'avoir le même
nom (court).