Bonjour Stefan,

La normalisation de l’expression lors de l’elimination est en effet nécessaire pour préserver la subject reduction, on peut se référer aux sections 2.3 et 2.4 du travail de Pierre Courtieu sur les normalised types. Par exemple, pour faire marcher l'égalité définitionnelle, son éliminateur dépendant a le type suivant:

Qrec: (t : ?A/?F) → (f : (a : ?A) → ?P (Qin a)) → ?P (Norm t);

L’éliminateur renvoie un terme de type `?P (Norm t)` au lieu de quelque chose de type `?P t` où `Norm t` est la version normalisée de `t` justement pour éviter de casser la subject reduction. Courtieu n’a pas fourni une explication détaillée de la raison pour laquelle il a dû faire ça, mais j’imagine qu’il a conçu son système comme il l'a fait justement à cause du problème que vous avez mentionné.

James

Le 2 mai 2024 à 11:13, Stefan Monnier monnier@iro.umontreal.ca a écrit :

Salut James,

T'avais raison de rester avec une égalité propositionnelle pour tes types quotient: renforcer l'égalité définitionnelle pour les types quotients pose des problèmes.

Soit le type quotient A/F où A est le type de base et F est une fonction qui prend un argument de type A et renvoie la classe d'équivalence à laquel il appartient.

Soit une élimination comme:

Qrec: ?A/?F → (f : ?A → ?t) → (P : ∀ x,y . ?F x = ?F y → f x = f y) → ?t;

qui dit que tu peux appliquer `f` au "contenu" d'un quotient ?A/?F pour autant que tu prouves avec `P` que `f` traite tous les éléments d'une même classe de la même manière.

Le problème est que l'élimination ne garanti que l'égalité propositionnelle du résultat. Donc si tu permets à deux valeurs différentes de type A/F d'être définitionnellement égales, t'as un problème, parce que tu casses le principe que

e₁ ≃ e₂ => E[e₁] ≃ E[e₂]

Plus concrètement, disons que le constructeur des quotients est Qin, si tu as

e₁ ≄ e₂ ∧ Qin e₁ ≃ Qin e₂

tu peux montrer que

E[Qin e₁] = E[Qin e₂]

parce que ton `Qrec` te donne cette `=` (i.e. égalité propositionnelle), mais tu ne peux pas montrer que cette égalité est vraie définitionnellement (`≃`), et en effet elle n'est pas vraie définitionnellement si le `f` de l'éliminateur est la fonction identité (qui est un cas possible si le contexte nous fournit la preuve `P`).

Donc à moins de faire attention que `Qrec` renvoie toujours une valeur "normalisée", on perd la propriété de "subject reduction". 🙁

Étonnement, je n'ai encore pas vu une telle explication dans mes lectures. Toi?

Stefan