Pour éviter que le patch soit signalé comme malveillant, je lui ai donné une extension `.txt`.
FWIW, j'ai encore pas eu de problèmes avec des attachments `text/x-diff` et/ou extensions `.diff` ou `.patch` :-)
Au début, je voulais nommer le type interval `I` mais le nom a déjà été pris par le combinateur I, donc j’ai fini par le nommer `Interval`.
Je pense que c'est mieux de renommer le combinateur `I`. En Haskell ça s'appelle `id`, donc on pourrait utiliser ça.
Je voulais également définir le type interval en Typer, mais j’avais du mal à référencer le type en OCaml de manière satisfaisante, j’ai fini donc par le définir dans `debruijn.ml`, peut-être que vous auriez une meilleure idée.
Pas sûr si c'est mieux, mais tu devrais pouvoir faire ce qu'on fait pour les booléens (via `predef_names` in `src/builtin.ml`).
Dans `samples/cubical.typer`, j’essayais de prouver que `(Eq_comm (Eq_comm p)) = p`. Je pensais que si le typechecker était capable de faire la réduction `Eq_uneq (Eq_eq f) i = f (_ := i)`, je pourrais donc compléter la preuve, mais encore faut-il que le typechecker puisse utiliser le lemme qui dit que `not (not i) = i`.
Le typechecker ne sait pas utiliser des lemmes, donc ça ne va probablement pas marcher "juste par réduction" :-(
%% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l
+Eq_eq : (l : TypeLevel) ≡> (t : Type_ l)
≡> (f : Interval ≡> t)-> Eq (f (_ := i0)) (f (_ := i1));+Eq_eq = ##Eq.eq;
Side note: il serait bon de vérifier qu'on peut définir la version "hétérogène":
Eq_eq' : (t : Interval ≡> Type) ≡> (f : (i : ?) ≡> t (_ := i)) -> Eq (f (_ := i0)) (f (_ := i1));
Et peut-être qu'il serait mieux d'utiliser la version hétérogène pour le "builtin" et définir la version homogène (pour laquelle l'inférence de types devrait mieux fonctionner) par dessus, plutôt que l'inverse.
Mais, pour ça, je pense qu'il faudra redéfinir `Eq`.
+Eq_uneq : (l : TypeLevel) ≡> (t : Type_ l)
≡> (x : t) => (y : t)=> Eq x y -> (Interval ≡> t);+Eq_uneq = ##Eq.uneq;
Même chose ici.
-Eq_refl : ((x : ?t) ≡> Eq x x); +Eq_refl : (l : TypeLevel) ≡> (t : Type_ l)
≡> (x : t) => Eq x x;
Hmm... on change ≡> en => ... Si je comprends bien c'est à cause du "->" dans le type de `Eq_eq`, mais je crois que ce "->" peut-être changé en "≡>" aussi (sinon, ça veut dire que nos preuves d'égalité portent vraiment de l'information et donc qu'elles ne sont pas effaçables).
-Eq_refl = ##Eq.refl; +Eq_refl = lambda (l : TypeLevel) ≡> lambda (t : Type_ l) ≡>
lambda (x : t) => Eq_eq (lambda _ ≡> x);
A.k.a
Eq_refl = lambda l ≡> lambda t ≡> lambda x => Eq_eq (lambda _ ≡> x);
[ Side note: autour de `Eq` il y a souvent besoin de passer explicitement des arguments effaçables, ce qui suggère qu'il serait utile de pouvoir définir certains arguments effaçable comme étant "effaçables mais pas implicites". ]
-Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x; +Eq_comm : (x : ?t) => (y : ?t) => Eq x y -> Eq y x;
🙁
-Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x)
%% FIXME: The code is incorrectly accepted even%% without this `(p := p)` because we just get a%% metavar which remains uninstantiated and then%% the definition gets ignored in the runtime%% environment (see Eval.from_lctx).(p := p)Eq_refl;+Eq_comm p = Eq_eq (lambda i ≡> Eq_uneq p (_ := Interval_not i));
🙂
+%% If `y=z` is taken to be unnecessary, this implies that we could define +%% Eq_broken_trans : Eq ?x ?y -> Eq ?x ?z; +Eq_trans : (x : ?t) => (y : ?t) => (z : ?t) => Eq x y -> Eq y z -> Eq x z; +Eq_trans x=y = lambda y=z -> Eq_cast (p := y=z) (f := lambda x' -> Eq x x') x=y;
Good.
+%% FIXME: The below code is accepted even in the absence of `p := y=z`.
!!!
+Eq_funext : (f : ? -> ?) => (g : ? -> ?) =>
((x : ?) -> Eq (f x) (g x)) ->Eq (lambda x -> f x) (lambda x -> g x);+Eq_funext p = Eq_eq (lambda i ≡> lambda x -> Eq_uneq (p x) (_ := i));
🙂
+%% FIXME: It'd be nice to be able to say `Eq f g` directly
En effet. Pour ça, il faut ajouter η dans `conv_p`. Ça devrait pas être trop difficile.
+++ b/samples/cubical.typer
Tu pourrais le mettre dans `HoTT.typer` :-)
+hello : String; +hello = Eq_cast (p := reflString) (f := lambda x -> x) "hello";
Je pense que pour l'instant on a pas de réductions sur `Eq_cast` dans `conv_p` mais il serait bon d'en ajouter pour qu'on puisse avoir
Eq_refl : Eq "hello" hello;
+%% FIXME: This should be provable, need to reduce `(Eq_comm (Eq_comm p))` to `p`. +%% It should be sufficient to add the following reduction: +%% Eq_uneq (Eq_eq f) i = f (_ := i)
Sounds good.
+%% and apply `notnot=id`. +%% Eq_comm_inv : (x : ?t) => (y : ?t) => (p : Eq x y) -> Eq (Eq_comm (Eq_comm p)) p; +%% Eq_comm_inv p = Eq_refl;
Je crois que `= Eq_refl;` est un peu optimiste vu que ça dépend de `notnot=id` et je ne vois pas de manière simple d'obtenir `notnot=id` de manière définitionnelle. En gros, ça nécessiterait de tester l'équivalence extensionnelle des fonctions passées aux deux `Eq_eq` et si on fait ça de manière définitionnelle, j'ai l'impression que ça donne l'axiome K, aka UIP.
--- a/src/debruijn.ml +++ b/src/debruijn.ml
J'me suis arrêté ici pour l'instant.
Stefan