James Tan Juan Whei pushed to branch quotient-types at Stefan / Typer
Commits:
61d01f99 by James Tan at 2023-07-19T22:16:16-04:00
Implement `Quotient` formation
- - - - -
1282e0ba by James Tan at 2023-07-19T22:16:16-04:00
Implement `Quotient` introduction
- - - - -
00341dfd by James Tan at 2023-07-19T22:16:17-04:00
Implement `Quotient` elimination
- - - - -
55c38d85 by James Tan at 2023-07-19T22:16:17-04:00
Implement `Eq` constructor for `Quotient`
- - - - -
aa04cc68 by James Tan at 2023-…
[View More]07-19T22:16:17-04:00
Improve unification scheme for SLlub (l1, l2) when l1 ≃ l2
- - - - -
d00058fa by James Tan at 2023-07-26T19:34:39-04:00
Implement `qcase` macro
- Facilitates `Quotient` elimination
- - - - -
48982943 by James Tan at 2023-07-26T19:34:40-04:00
Write some proofs about quotient types
- - - - -
12 changed files:
- btl/builtins.typer
- btl/pervasive.typer
- + btl/qcase.typer
- + samples/qcase_test.typer
- + samples/quotient.typer
- + samples/quotient_lib.typer
- src/debruijn.ml
- src/env.ml
- src/eval.ml
- src/opslexp.ml
- src/unification.ml
- tests/elab_test.ml
Changes:
=====================================
btl/builtins.typer
=====================================
@@ -531,4 +531,42 @@ Heap_unsafe-store-cell = Built-in "Heap.store-cell";
Heap_unsafe-load-cell : Int -> Int -> Heap ?t;
Heap_unsafe-load-cell = Built-in "Heap.load-cell";
+%%
+%% Quotient types
+%%
+Quotient = Built-in "Quotient" : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡>
+ (A : Type_ l1) -> (R : A -> A -> Type_ l2) ->
+ Type_ (_∪_ l1 l2);
+
+Quotient_in : ?A -> Quotient ?A ?R;
+Quotient_in = Built-in "Quotient.in";
+
+%% FIXME: We want to be able to say the following
+%% Quotient_eq : (a : ?) ≡> (a' : ?) ≡> (p : ?R a a') ≡>
+%% Eq (Quotient_in (R := R?) a)
+%% (Quotient_in (R := R?) a');
+%% But we running into the following issue for now:
+%% "Bug in the elaboration of a repeated metavar!"
+Quotient_eq : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡>
+ (R : A -> A -> Type_ l2) ≡>
+ (a : A) ≡> (a' : A) ≡> (p : R a a') ->
+ Eq (Quotient_in (R := R) a)
+ (Quotient_in (R := R) a');
+Quotient_eq = Built-in "Quotient.eq";
+
+%% FIXME: We want to be able to say the following
+%% Quotient_elim : (f : ?A -> ?B) ->
+%% (p : (a : ?) -> (a' : ?) -> ?R a a' -> Eq (f a) (f a')) ≡>
+%% (q : Quotient ?A ?R) ->
+%% ?B;
+%% Same issue as above
+Quotient_elim : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (l3 : TypeLevel) ≡>
+ (A : Type_ l1) ≡> (B : Type_ l2) ≡>
+ (R : A -> A -> Type_ l3) ≡>
+ (f : A -> B) ->
+ (p : (a : A) -> (a' : A) -> R a a' -> Eq (f a) (f a')) ≡>
+ (q : Quotient A R) ->
+ B;
+Quotient_elim = Built-in "Quotient.elim";
+
%%% builtins.typer ends here.
=====================================
btl/pervasive.typer
=====================================
@@ -690,6 +690,9 @@ depelim = load "btl/depelim.typer";
case_as_return_ = depelim.case_as_return_;
case_return_ = depelim.case_return_;
+define-operator "qcase" () 42;
+qcase_ = let lib = load "btl/qcase.typer" in lib.qcase_macro;
+
%%%% Unit tests function for doing file
%% It's hard to do a primitive which execute test file
=====================================
btl/qcase.typer
=====================================
@@ -0,0 +1,284 @@
+%% Qcase macro
+%% Make the syntax cleaner for quotient eliminations
+%%
+%% qcase (e : A / R)
+%% | Quotient_in a => e1
+%% | Quotient_eq a a' r i => e2
+%%
+%% `a` is bounded in `e1`, and `a`, `a'`, `r` and `i` are
+%% bounded in `e2`. `i` can only be used in an erasable manner.
+%%
+%% TODO: The annotation is necessary for now, as we need the `R`
+%% However, we should make it optional.
+is_sym : Sexp -> String -> Bool;
+is_sym sexp s =
+ let
+ kfalse = K false;
+ in
+ Sexp_dispatch sexp
+ (lambda _ _ -> false) % Nodes
+ (String_eq s) % Symbol
+ kfalse % String
+ kfalse % Integer
+ kfalse % Float
+ kfalse; % List of Sexp
+%% (build_explicit_arg "name" sexp) yields a
+%% (name := sexp) Sexp
+build_explicit_arg : String -> Sexp -> Sexp;
+build_explicit_arg s sexp = Sexp_node (Sexp_symbol "_:=_")
+ (cons (Sexp_symbol s)
+ (cons sexp nil));
+qcase_impl = lambda (sexps : List Sexp) ->
+ %% For the same example that was given above, we expect
+ %% `sexps` to represent the following:
+ %% (_|_ (_:_ e (_/_ A R))
+ %% (_=>_ (Quotient_in a) e1)
+ %% (_=>_ (Quotient_eq a a' r i) e2))
+ %% Node : [(_|_ (_:_ e (_/_ A R)) (_=>_ (Qin a) e1) (_=>_ (Qeq a a' r i) e2))]
+ let
+ %% (_|_ (_:_ e (_/_ A R)) (_=>_ (Qin a) e1) (_=>_ (Qeq a a' r i) e2))
+ head = List_head Sexp_error sexps;
+ knil = K nil;
+ kerr = K Sexp_error;
+ get-list : Sexp -> List Sexp;
+ get-list node = Sexp_dispatch node
+ (lambda op lst -> lst) % Nodes
+ knil % Symbol
+ knil % String
+ knil % Integer
+ knil % Float
+ knil; % List of Sexp
+ %% List of:
+ %% (_:_ e (_/_ A R))
+ %% (_=>_ (Qin a) e1)
+ %% (_=>_ (Qeq a a' r i) e2)
+ body = get-list head;
+ elim_targ_sexp = List_nth (Integer->Int 0) body Sexp_error;
+ elim_fn_sexp = List_nth (Integer->Int 1) body Sexp_error;
+ elim_compat_sexp = List_nth (Integer->Int 2) body Sexp_error;
+ %% Triple of the expression to eliminate, the underlying type A
+ %% and the relation R
+ %% A and R are optional
+ elim_expr_details : Triplet Sexp (Option Sexp) (Option Sexp);
+ elim_expr_details =
+ let
+ kerr = K (triplet Sexp_error none none);
+ extract_from_annotated_e : Sexp -> List Sexp ->
+ Triplet Sexp (Option Sexp) (Option Sexp);
+ extract_from_annotated_e _ xs =
+ if (Int_eq (List_length xs) (Integer->Int 2))
+ then
+ let
+ e = List_nth (Integer->Int 0) xs Sexp_error;
+ e_type = List_nth (Integer->Int 1) xs Sexp_error;
+ extract_type sexp sexps =
+ if (is_sym sexp "_/_")
+ then
+ %% (_/_ A R )
+ %% |___| |___|
+ %% | |
+ %% a r
+ let
+ a = List_nth (Integer->Int 0) sexps Sexp_error;
+ r = List_nth (Integer->Int 1) sexps Sexp_error;
+ in
+ triplet e (some a) (some r)
+ else
+ triplet e (some Sexp_error) (some Sexp_error);
+ kerr' = K (triplet e (some Sexp_error) (some Sexp_error));
+ in
+ Sexp_dispatch e_type
+ extract_type % Nodes
+ kerr' % Symbol
+ kerr' % String
+ kerr' % Integer
+ kerr' % Float
+ kerr' % List of Sexp
+ else
+ triplet Sexp_error none none;
+ extract_targ_from_node : Sexp -> List Sexp ->
+ Triplet Sexp (Option Sexp) (Option Sexp);
+ extract_targ_from_node x xs =
+ %% Check if annotation is present
+ if (is_sym x "_:_")
+ then
+ %% Dissect the sexp to extract, the e, A and R
+ extract_from_annotated_e x xs
+ else
+ %% No annotation was given, return the entire
+ %% expresson as the elimination target
+ triplet x none none;
+ in
+ Sexp_dispatch elim_targ_sexp
+ extract_targ_from_node % Nodes
+ (lambda _ -> triplet elim_targ_sexp
+ none none) % Symbol
+ kerr % String
+ kerr % Integer
+ kerr % Float
+ kerr; % List of Sexp
+ %% The function (`f`) argument
+ elim_fn : Sexp;
+ elim_fn =
+ let
+ extract_fn : Sexp -> List Sexp -> Sexp;
+ extract_fn sexp sexps =
+ %% Check that branch is well formed
+ if (and (is_sym sexp "_=>_") (Int_eq (List_length sexps) (Integer->Int 2)))
+ then
+ let
+ %% (_=>_ (Quotient_in a) e1 )
+ %% |_____________| |_________|
+ %% | |
+ %% qin fn_body
+ qin_sexp = List_nth (Integer->Int 0) sexps Sexp_error;
+ fn_body_sexp = List_nth (Integer->Int 1) sexps Sexp_error;
+ bound_var : Sexp;
+ bound_var =
+ let
+ extract_var head args = if (and (is_sym head "Quotient_in")
+ (Int_eq (List_length args)
+ (Integer->Int 1)))
+ then
+ List_head Sexp_error args
+ else
+ %% FIXME: Might be good to have
+ %% a better way to report this
+ Sexp_error;
+ in
+ Sexp_dispatch qin_sexp
+ extract_var % Nodes
+ kerr % Symbol
+ kerr % String
+ kerr % Integer
+ kerr % Float
+ kerr; % List of Sexp
+ in
+ Sexp_node (Sexp_symbol "lambda_->_")
+ (cons bound_var
+ (cons fn_body_sexp nil))
+ else Sexp_error;
+ in
+ Sexp_dispatch elim_fn_sexp
+ extract_fn % Nodes
+ kerr % Symbol
+ kerr % String
+ kerr % Integer
+ kerr % Float
+ kerr; % List of Sexp
+ %% The proof (`p`) argument
+ elim_compat : Sexp;
+ elim_compat =
+ let
+ extract_proof : Sexp -> List Sexp -> Sexp;
+ extract_proof sexp sexps =
+ %% Check that branch is well formed
+ if (and (is_sym sexp "_=>_") (Int_eq (List_length sexps)
+ (Integer->Int 2)))
+ then
+ let
+ %% (_=>_ (Quotient_eq a a' r i) p )
+ %% |____________________| |__________|
+ %% | |
+ %% qeq proof_exp
+ qeq_sexp = List_nth (Integer->Int 0) sexps Sexp_error;
+ proof_exp_sexp = List_nth (Integer->Int 1) sexps Sexp_error;
+ is_symbol : Sexp -> Bool;
+ is_symbol sexp =
+ let
+ ktrue = K true;
+ kfalse = K false;
+ in
+ Sexp_dispatch sexp
+ (K kfalse) % Nodes
+ ktrue % Symbol
+ kfalse % String
+ kfalse % Integer
+ kfalse % Float
+ kfalse; % List of Sexp
+ build_proof : Sexp -> List Sexp -> Sexp;
+ build_proof sexp sexps =
+ %% Check that the right identifier is used with exactly
+ %% 4 arguments, also ensure that identifier are symbols
+ %% TODO: Make it possible to omit the `i`, in which case
+ %% we expect p to be an equality proof.
+ if (and (is_sym sexp "Quotient_eq")
+ (and %% We allow the last parameter `i` to be omitted
+ (or (Int_eq (List_length sexps) (Integer->Int 3))
+ (Int_eq (List_length sexps) (Integer->Int 4)))
+ (List_foldl (lambda acc sexp ->
+ and acc (is_symbol sexp))
+ true sexps)))
+ then
+ let
+ mklambda : Sexp -> Sexp -> Sexp;
+ mklambda param body =
+ Sexp_node (Sexp_symbol "lambda_->_")
+ (cons param (cons body nil));
+ proof_fn =
+ if (Int_eq (List_length sexps) (Integer->Int 3))
+ then
+ %% `i` is absent, i.e. we expect to be provided
+ %% with an equality proof.
+ %% We want to convert Quotient_eq a a' r => e
+ %% to (lambda a a' r -> e)
+ quote (uquote (List_foldr mklambda
+ sexps proof_exp_sexp))
+ else
+ %% Handle the case where `i` is present
+ %% We have to construct an equality proof
+ %% from what was given
+ %% We want to convert Quotient_eq a a' r i => e
+ %% to (lambda a a' r -> Eq_eq (f := lambda i ≡> e))
+ let
+ erasable_param = List_nth (Integer->Int 3)
+ sexps Sexp_error;
+ proof_fn_params =
+ List_reverse (List_tail (List_reverse sexps nil))
+ nil;
+ eq = quote (Eq_eq (f :=
+ lambda (uquote erasable_param) ≡>
+ (uquote proof_exp_sexp)));
+ in
+ quote (uquote (List_foldr mklambda
+ proof_fn_params eq));
+ in
+ build_explicit_arg "p" proof_fn
+ else
+ Sexp_error;
+ in
+ Sexp_dispatch qeq_sexp
+ build_proof % Nodes
+ kerr % Symbol
+ kerr % String
+ kerr % Integer
+ kerr % Float
+ kerr % List of Sexp
+ else
+ Sexp_error;
+ in
+ Sexp_dispatch elim_compat_sexp
+ extract_proof % Nodes
+ kerr % Symbol
+ kerr % String
+ kerr % Integer
+ kerr % Float
+ kerr; % List of Sexp
+ qelim_args : List Sexp;
+ qelim_args = case elim_expr_details
+ | triplet e a r =>
+ let
+ res = (cons elim_fn
+ (cons elim_compat
+ (cons e nil)));
+ res' = (case r
+ | none => res
+ | some r' =>
+ (cons (build_explicit_arg "R" r') res));
+ in
+ res';
+ qelim_sexp = Sexp_node (Sexp_symbol "Quotient_elim")
+ qelim_args;
+ in
+ IO_return qelim_sexp;
+qcase_macro = macro qcase_impl;
=====================================
samples/qcase_test.typer
=====================================
@@ -0,0 +1,50 @@
+%% Defining a total relation on Unit
+R : Unit -> Unit -> Type;
+R u1 u2 = Unit;
+
+inQ : Quotient Unit R;
+inQ = Quotient_in ();
+
+e1 : Unit;
+e1 = qcase (inQ : Unit / R)
+ | Quotient_in a => ()
+ | Quotient_eq a a' r i => ();
+
+e2 : Unit;
+e2 = qcase (inQ : Unit / R)
+ | Quotient_in a => ()
+ | Quotient_eq a a' r => Eq_refl;
+
+e3 : Unit;
+e3 = qcase inQ
+ | Quotient_in a => ()
+ | Quotient_eq a a' r i => ();
+
+e4 : Unit;
+e4 = qcase inQ
+ | Quotient_in a => ()
+ | Quotient_eq a a' r => Eq_refl;
+
+test-elim-to-unit = do {
+ Test_info "QCASE" "elimination to Unit";
+
+ r0 <- Test_eq "annotated elim to `Unit` with explicit `I`" e1 ();
+ r1 <- Test_eq "annotated elim to `Unit` without `I`" e2 ();
+ r2 <- Test_eq "unannotated elim to `Unit` with explicit `I`" e3 ();
+ r3 <- Test_eq "unannotated elim to `Unit` without `I`" e4 ();
+
+ success <- IO_return (and (and (and r0 r1) r2) r3);
+
+ if success then
+ (Test_info "QCASE" "elimination to Unit succeeded")
+ else
+ (Test_warning "QCASE" "elimination to Unit failed");
+
+ IO_return success;
+};
+
+exec-test = do {
+ b1 <- test-elim-to-unit;
+
+ IO_return b1;
+};
=====================================
samples/quotient.typer
=====================================
@@ -0,0 +1,116 @@
+Nat : Type;
+
+type Nat
+ | zero
+ | succ Nat;
+
+_-_ : Nat -> Nat -> Nat;
+_-_ x y = case x
+ | zero => zero
+ | succ m => case y
+ | zero => x
+ | succ n => m - n;
+
+NatPair = Pair Nat Nat;
+
+fst p = case p
+ | pair m _ => m;
+
+snd p = case p
+ | pair _ n => n;
+
+normaliseZ : NatPair -> NatPair;
+normaliseZ np = case np
+ | pair m n => pair (m - n) (n - m);
+
+equalZ : NatPair -> NatPair -> Type;
+equalZ x1 x2 = Eq (normaliseZ x1) (normaliseZ x2);
+
+%%
+%% See definitions of `Quotient` in `builtins.typer`
+%%
+
+%% FIXME: We shouldn't get this error
+%% "Requested Built-in \"Quotient\" does not exist"
+%% Z = Quotient NatPair equalZ;
+
+%%
+%% Quotient.eq
+%%
+%% Proof that quotiented elements are equal when
+%% the base elements themselves are related in
+%% the underlying type.
+𝟙-𝟘 : Quotient NatPair equalZ;
+𝟙-𝟘 = Quotient_in (pair (succ zero) zero);
+
+𝟚-𝟙 : Quotient NatPair equalZ;
+𝟚-𝟙 = Quotient_in (pair (succ (succ zero)) (succ zero));
+
+𝟙=𝟙 : Eq (t := Quotient NatPair equalZ) 𝟙-𝟘 𝟚-𝟙;
+𝟙=𝟙 = Quotient_eq
+ (R := equalZ)
+ (a := pair (succ zero) zero)
+ (a' := pair (succ (succ zero)) (succ zero))
+ Eq_refl;
+
+%%
+%% Quotient.elim
+%%
+%% Elimination of quotients requires a proof that
+%% the equality between quotients is respected
+NatToInt : Nat -> Int;
+NatToInt n = case n
+ | zero => 0
+ | succ n' => 1 + NatToInt n';
+
+NatPairToInt' : NatPair -> Int;
+NatPairToInt' np = case np
+ | pair x y =>
+ (case x
+ | zero => (NatToInt y) * -1
+ | succ _ => NatToInt x);
+
+NatPairToInt : NatPair -> Int;
+NatPairToInt np = NatPairToInt' (normaliseZ np);
+
+%% Proof that NatPairToInt respects the quotient Z
+NatPairToIntCompat : (a : NatPair) -> (a' : NatPair) ->
+ (p : equalZ a a') ->
+ Eq (NatPairToInt a) (NatPairToInt a');
+NatPairToIntCompat _ _ p = Eq_eq (f := lambda i ≡>
+ NatPairToInt' (Eq_uneq (p := p) (i := i)));
+
+%% FIXME: Explicitly providing a value for R should unnecessary,
+%% this should be inferred based on the type of `q`. This is
+%% because we do not handle residuals during unification for now.
+Z_To_Int : Quotient NatPair equalZ -> Int;
+Z_To_Int q = Quotient_elim (R := equalZ) NatPairToInt (p := NatPairToIntCompat) q;
+
+neg2_Z : Quotient NatPair equalZ;
+neg2_Z = Quotient_in (pair (succ zero) (succ (succ (succ zero))));
+
+neg2_Int : Int;
+neg2_Int = Z_To_Int neg2_Z;
+
+%% FIXME: This could work if we add a reduction rule
+%% neg2_refl : Eq neg2_Int (-2 : Int);
+%% neg2_refl = Eq_refl;
+
+%% `qcase` macro to facilitate elimination
+Z_To_Int' : Quotient NatPair equalZ -> Int;
+Z_To_Int' q =
+ %% The annotation is optional, but is necessary in
+ %% this case, since the propagation of type
+ %% information is insufficient the way things are now.
+ qcase (q : NatPair / equalZ)
+ | Quotient_in a => NatPairToInt a
+ | Quotient_eq a a' r i => NatPairToInt' (Eq_uneq (p := r) (i := i));
+
+%% Omitting the `i` parameter by providing an equality proof on the RHS
+Z_To_Int'' : Quotient NatPair equalZ -> Int;
+Z_To_Int'' q =
+ qcase (q : NatPair / equalZ)
+ | Quotient_in a => NatPairToInt a
+ | Quotient_eq a a' r => NatPairToIntCompat a a' r;
+
+%% TODO: Define Quotient NatPair equalZ ≃ Int
=====================================
samples/quotient_lib.typer
=====================================
@@ -0,0 +1,129 @@
+%%%%% Prelude %%%%%%
+
+%% FIXME : Loading hott.typer doesn't work for some reason
+%% due to "[X] Fatal :(internal) lub of two SLsucc"
+%% Some definitions will be duplicated for now
+
+Eq_funext : (f : ? -> ?) => (g : ? -> ?) =>
+ ((x : ?) -> Eq (f x) (g x)) ->
+ Eq f g;
+Eq_funext p = Eq_eq (f := lambda i ≡> lambda x -> Eq_uneq (p := p x) (i := i));
+
+HoTT_isProp P = (x : P) -> (y : P) -> Eq x y;
+
+HoTT_isSet A = (x : A) -> (y : A) -> HoTT_isProp (Eq x y);
+
+HoTT_isContr = typecons (HoTT_isContr (l ::: TypeLevel)
+ (A : Type_ l))
+ (isContr (a : A) ((a' : A) -> Eq a a'));
+isContr = datacons HoTT_isContr isContr;
+
+%%%%% Prelude END %%%%%%
+
+%% TODO: Prove dependent version of this after we introduce
+%% dependent elim, which will be more interesting and more
+%% worthwhile
+recProp : (A : Type_ ?) ≡>
+ (B : Type_ ?) ≡>
+ (R : A -> A -> Type_ ?) ≡>
+ (p : HoTT_isProp B) ->
+ (f : A -> B) ->
+ (x : Quotient A R) -> B;
+recProp = lambda _ _ _ _ _ R ≡>
+ lambda p f x ->
+ Quotient_elim (R := R) f (p := lambda a a' r -> p (f a) (f a')) x;
+
+%% Again, this is not very interesting, unlike its dependent
+%% counterpart.
+recContr : (A : Type_ ?) ≡>
+ (B : Type_ ?) ≡>
+ (R : A -> A -> Type_ ?) ≡>
+ (p : HoTT_isContr B) ->
+ (x : Quotient A R) -> B;
+recContr = lambda _ _ _ _ _ R ≡>
+ lambda p x -> case p
+ | isContr a f => Quotient_elim (R := R)
+ (lambda _ -> a)
+ (p := lambda a a' r -> Eq_refl)
+ x;
+
+%% FIXME: Quotient_elim should be named Quotient_rec?
+%% rec2 : (A : Type_ ?) ≡>
+%% (B : Type_ ?) ≡>
+%% (C : Type_ ?) ≡>
+%% (R : A -> A -> Type_ ?) ≡>
+%% (S : B -> B -> Type_ ?) ≡>
+%% (C_isSet : HoTT_isSet C) ->
+%% (f : A -> B -> C) ->
+%% ((a : A) -> (b : A) -> (c : B) -> R a b -> Eq (f a c) (f b c)) ->
+%% ((a : A) -> (b : B) -> (c : B) -> S b c -> Eq (f a b) (f a c)) ->
+%% Quotient A R -> Quotient B S -> C;
+%% rec2 = lambda _ _ _ _ _ A B C R S ≡>
+%% lambda C_isSet f feql feqr ->
+%% Quotient_elim (R := R)
+%% (lambda a ->
+%% lambda b -> Quotient_elim (R := S) (f a)
+%% (p := feqr a) b)
+%% (p := lambda a a' r ->
+%% let
+%% eqf : (b : B) -> Eq (f a b) (f a' b);
+%% eqf b = feql a a' b r;
+%% eqf' : Eq (f a) (f a');
+%% eqf' = Eq_funext (f := f a) (g := f a') eqf;
+%% p : (x : Quotient B S) ->
+%% HoTT_isProp (Eq (Quotient_elim (R := S) (f a)
+%% (p := feqr a) x)
+%% (Quotient_elim (R := S) (f a')
+%% (p := feqr a') x));
+%% p x = C_isSet (Quotient_elim (R := S) (f a)
+%% (p := feqr a) x)
+%% (Quotient_elim (R := S) (f a')
+%% (p := feqr a') x);
+%% res : (x : Quotient B S) ->
+%% (Eq (Quotient_elim (R := S) (f a)
+%% (p := feqr a) x)
+%% (Quotient_elim (R := S) (f a')
+%% (p := feqr a') x));
+%% res x = Quotient_elim (A := B)
+%% %% FIXME: We need depelim here
+%% (B := Eq (f a b) (f a' b))
+%% (R := S)
+%% eqf
+%% (p := lambda u v s ->
+%% Eq_eq (f := lambda i ≡>
+%% p (Eq_uneq (p := Quotient_eq (R := S) s) (i := i))
+%% (eqf u) (eqf v)))
+%% x;
+%% in
+%% Eq_funext (f := Quotient_elim (R := S) (f a)
+%% (p := feqr a))
+%% (g := Quotient_elim (R := S) (f a')
+%% (p := feqr a'))
+%% res);
+
+%% Lemma 6.10.2 in HoTT book, to prove this we need to
+%% apply propositional truncation on SurjectiveQuotientProof.
+%% type SurjectiveQuotientProof (A : ?) (x : Quotient A ?R)
+%% | surjectiveQuotientProof (a : A) (Eq (Quotient_in a) x);
+%% Quotient_in_surjective : (x : Quotient ?A ?R) -> ||SurjectiveQuotientProof ?A ?R x||₁;
+
+%% Given a proof that a unary operation preserves the underlying
+%% relation, we can apply the operation to the quotiented type.
+quotUnaryOp : (A : Type_ ?) ≡>
+ (R : A -> A -> Type_ ?) ≡>
+ (op : A -> A) ->
+ ((a : A) -> (a' : A) -> R a a' -> R (op a) (op a')) ->
+ Quotient A R -> Quotient A R;
+quotUnaryOp = lambda _ _ A R ≡>
+ lambda op h x ->
+ let
+ opPreservesQuotient : (a : A) -> (a' : A) -> R a a' ->
+ Eq (t := Quotient A R)
+ (Quotient_in (op a))
+ (Quotient_in (op a'));
+ opPreservesQuotient a a' r = Quotient_eq (R := R) (h a a' r);
+ in
+ Quotient_elim (R := R)
+ (lambda a -> Quotient_in (op a))
+ (p := opPreservesQuotient)
+ x;
=====================================
src/debruijn.ml
=====================================
@@ -145,7 +145,7 @@ let type_eq_type =
let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type)
let builtin_axioms =
- ["Int"; "Elab_Context"; "IO"; "Ref"; "Sexp"; "Array"; "FileHandle";
+ ["Int"; "Elab_Context"; "IO"; "Ref"; "Sexp"; "Array"; "FileHandle"; "Quotient";
(* From `healp.ml`. *)
"Heap"; "DataconsLabel"]
=====================================
src/env.ml
=====================================
@@ -184,7 +184,12 @@ let value_string_with_type v ltype ctx =
(Lexp.to_string left)
(Lexp.to_string right)
(Lexp.to_string t)
- | _ -> value_string v)
+ | [_; _; (_, t); (_, r)]
+ when OL.conv_builtin_p ctx e' "Quotient"
+ -> sprintf "(Quotient.in %s %s)"
+ (Lexp.to_string t)
+ (Lexp.to_string r)
+ | _ -> value_string v)
| _ -> value_string v
in get_string ltype ctx
=====================================
src/eval.ml
=====================================
@@ -1027,6 +1027,18 @@ let typelevel_lub loc (_depth : eval_debug_info) (args_val: value_type list) =
| [Vint v1; Vint v2] -> Vint(max v1 v2)
| _ -> error loc ("`Typlevel.⊔` expects 2 TypeLevel argument2")
+let quotient_elim loc depth args =
+ let trace_dum = (Var ((epsilon (loc), None), -1)) in
+ match args with
+ | [(Closure _) as f; q] ->
+ eval_call loc trace_dum depth f [q]
+ | _ -> error loc "Quotient.elim expects 2 arguments"
+
+let quotient_eq loc _ args =
+ match args with
+ | [_] -> Vundefined
+ | _ -> error loc "Quotient.eq expects 1 argument"
+
let register_builtin_functions () =
List.iter (fun (name, f, arity) -> add_builtin_function name f arity)
[
@@ -1084,6 +1096,9 @@ let register_builtin_functions () =
("Test.false" , test_false,2);
("Test.eq" , test_eq,3);
("Test.neq" , test_neq,3);
+ ("Quotient.in" , nop_fun, 1);
+ ("Quotient.eq" , quotient_eq, 1);
+ ("Quotient.elim" , quotient_elim, 2);
]
let _ = register_builtin_functions ()
=====================================
src/opslexp.ml
=====================================
@@ -304,7 +304,9 @@ and eq_cast_whnf ctx args =
match args with
| _l1 :: _l2 :: _t :: _x :: _y :: (_, p) :: _f :: (_, fx) :: rest
-> (match lexp'_whnf p ctx with
- | Call (_, eq, _) when conv_builtin_p ctx eq "Eq.eq"
+ | Call (_, eq, _)
+ when conv_builtin_p ctx eq "Eq.eq" ||
+ conv_builtin_p ctx eq "Quotient.eq"
-> Some (fx, rest)
| _ -> None)
| _ -> None
=====================================
src/unification.ml
=====================================
@@ -561,6 +561,10 @@ and unify_sortlvl (matching : scope_level option)
-> (* FIXME: This SLlub representation needs to be
* more "canonicalized" otherwise it's too restrictive! *)
(unify' l11 l21 ctx vs matching)@(unify' l12 l22 ctx vs matching)
+ | SLlub (l1, l2), other | other, SLlub (l1, l2)
+ when OL.conv_p ctx l1 l2
+ (* Arbitrarily selected `l1` over `l2` *)
+ -> unify' l1 (mkSortLevel other) ctx vs matching
| _, _ -> [(CKimpossible, ctx, sortlvl, lxp)])
| _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]
=====================================
tests/elab_test.ml
=====================================
@@ -180,7 +180,7 @@ unify (f Z (S Z)) (f (S Z) Z);
|}
let _ = add_elab_test_decl
- "WHNF of Eq.cast"
+ "WHNF of Eq.cast (applied to Eq.eq)"
{|
x = (4 : Int);
y = x;
@@ -192,6 +192,28 @@ test : Eq (Eq_cast (p := p) (f := lambda _ -> Unit) ()) ();
test = Eq_refl;
|}
+let _ = add_elab_test_decl
+ "WHNF of Eq.cast (applied to Quotient.eq)"
+ {|
+totalRel : Unit -> Unit -> Type;
+totalRel u1 u2 = Unit;
+
+unitQ : Quotient Unit totalRel;
+unitQ = Quotient_in unit;
+
+unitQ' = unitQ;
+
+unitQ=unitQ' : Eq (t := Quotient Unit totalRel) unitQ unitQ';
+unitQ=unitQ' = Quotient_eq
+ (R := totalRel)
+ (a := unit)
+ (a' := unit)
+ unit;
+
+test : Eq (Eq_cast (p := unitQ=unitQ') (f := lambda _ -> Unit) ()) ();
+test = Eq_refl;
+ |}
+
let _ = add_elab_test_decl
"Decidable at the type level"
{|
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/bfbff550912f1de9c0b1d61e494c2ac7…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/bfbff550912f1de9c0b1d61e494c2ac7…
You're receiving this email because of your account on gitlab.com.
[View Less]
Salut,
Je vous montre le problème lié aux types inductifs que j’ai mentionné hier.
On définit d’abord le type `Sigma`
Sigma = typecons
(Sigma (l1 ::: TypeLevel)
(l2 ::: TypeLevel)
(A : Type_ l1) (B : A -> Type_ l2))
(sigma (fst : A) (snd : B fst));
sigma = datacons Sigma sigma;
Mais quand il s’agit de construire une expression de ce type, on se retrouve dans l’obligation
de fournir la valeur de `B` explicitement lors …
[View More]de la construction même si l’information se trouve
déjà dans l’annotation de type.
up : Sigma Unit (lambda _ -> Unit);;
up = sigma (B := lambda _ -> Unit) unit unit; %% ça ne marche plus si on enlève l’argument B
Si on enlève le B, on obtient l’erreur "Context expected: (?B↑0 unit) but expression has type: Unit”.
J’ai investigué un tout petit peu, mais malheureusement j’ai pas pu trouver la source de ce problème.
J’ai rencontré un autre problème avec les indices de Debruijn quand j’écrivais cette preuve
HoTT_isContr A = Sigma A (lambda (x : A) -> ((y : A) -> Eq x y));
isContrΠ : (A : Type_ ?) ≡> (B : A -> Type_ ?) ≡>
(h : (x : A) -> HoTT_isContr (B x)) -> HoTT_isContr ((x : A) -> B x);
isContrΠ h =
sigma (A := (x : A) -> B x)
(B := (lambda (x : ((x : A) -> B x)) ->
((y : ((x : A) -> B x)) -> Eq x y)))
(lambda x -> case (h x) | sigma bx p => bx)
(lambda f -> Eq_eq (f := lambda i ≡>
lambda x ->
case (h x)
| sigma bx p => Eq_uneq (p := p (f x))
(i := i)));
qui donnait l’erreur
[X] Fatal :(DEBRUIJN) DeBruijn index 2 refers to wrong name. Expected: " %gensym% no 42 “
got " %gensym% no 39 “
On rencontre ce problème quand on est dans la branche du 2e `case` dans le code. Mon hypothèse est que
le `bx` n’est pas égal à l’autre `bx` dans le 1er `case`, et puisque ce que renvoit le 2e `case` dépend de ce
qui est renvoyé dans l’autre, ça devient un problème. La bonne nouvelle c’est que j’ai réussi à contourner le
problème en remplaçant les deux `case ` par des appels à des fonctions auxiliaires.
pr1 : Sigma ?A ?B -> ?A;
pr1 s = case s
| sigma a _ => a;
pr2 : (s : Sigma ?A ?B) -> ?B (pr1 s);
pr2 = lambda _ _ A B ≡> lambda s ->
case s
| sigma a b =>
let
branch=s : Eq (sigma (A := A) (B := B) a b) s;
branch=s = ##DeBruijn 0;
res : B (pr1 s);
res = Eq_cast (p := branch=s)
(f := lambda x -> B (pr1 x))
b;
in res;
isContrΠ : (A : Type_ ?) ≡> (B : A -> Type_ ?) ≡>
(h : (x : A) -> HoTT_isContr (B x)) -> HoTT_isContr ((x : A) -> B x);
isContrΠ = lambda _ _ A B ≡> lambda h ->
sigma (A := (x : A) -> B x)
(B := (lambda (x : ((x : A) -> B x)) ->
((y : ((x : A) -> B x)) -> Eq x y)))
(lambda x -> pr1 (h x))
(lambda g -> Eq_eq (f := lambda i ≡>
lambda x ->
Eq_uneq (p := (pr2 (h x))
(g x))
(i := i)));
A première vue, c’est peut-être lié à un problème similaire dans `hurkens.typer` (regardez la ligne 87).
Pour faciliter la reproduction de ces bugs, j’ai attaché en pièce jointe un fichier qui contient tout le code
que j’ai montré ci-dessus.
James
[View Less]
> Désolé pour le retard je l’avais complètement oublié, je viens de
> créer une branche qui s’appelle `cubical-equality`.
Merci. Je l'ai divisé en quelques commit plus ou moins indépendants et
je l'ai poussé sur `main`.
Stefan
Stefan pushed to branch main at Stefan / Typer
Commits:
6ea6caae by Stefan Monnier at 2023-07-18T20:03:41-04:00
test/env_tests.ml: Adjust to last change
- - - - -
1 changed file:
- tests/env_test.ml
Changes:
=====================================
tests/env_test.ml
=====================================
@@ -42,11 +42,11 @@ let _ = (add_test "ENV" "Set Variables" (fun () ->
if 10 <= (!global_verbose_lvl) then (
let var = [
- ((dsinfo, Some "a"), DB.type_int,…
[View More] (make_val "a"));
- ((dsinfo, Some "b"), DB.type_int, (make_val "b"));
- ((dsinfo, Some "c"), DB.type_int, (make_val "c"));
- ((dsinfo, Some "d"), DB.type_int, (make_val "d"));
- ((dsinfo, Some "e"), DB.type_int, (make_val "e"));
+ ((dsinfo, Some "a"), DB.type_integer, (make_val "a"));
+ ((dsinfo, Some "b"), DB.type_integer, (make_val "b"));
+ ((dsinfo, Some "c"), DB.type_integer, (make_val "c"));
+ ((dsinfo, Some "d"), DB.type_integer, (make_val "d"));
+ ((dsinfo, Some "e"), DB.type_integer, (make_val "e"));
] in
let n = (List.length var) - 1 in
@@ -71,15 +71,15 @@ let _ = (add_test "ENV" "Value Printer" (fun () ->
let open Lexp in
let exps = [((Vint 42),
(mkArrow (dsinfo, Aerasable, (dsinfo, Some "l"),
- DB.type_interval, DB.type_int)),
+ DB.type_interval, DB.type_integer)),
"(lambda _ ≡> 42)");
((Vbuiltin "Eq.eq"),
(mkCall (dsinfo, DB.type_eq,
[Aerasable, mkVar ((dsinfo, None), 2);
- Aerasable, DB.type_int;
+ Aerasable, DB.type_integer;
Anormal, mkVar ((dsinfo, Some "x"), 0);
Anormal, mkVar ((dsinfo, Some "y"), 0)])),
- "x = y [ ##Int ]")] in
+ "x = y [ ##Integer ]")] in
(* This test assumes that success = 0 and failure = -1 *)
List.fold_left
(fun res (v, ltype, expected)
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6ea6caae3d7a7e7619ade47cbc8fc58c1…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6ea6caae3d7a7e7619ade47cbc8fc58c1…
You're receiving this email because of your account on gitlab.com.
[View Less]
> Dans cette branche, j'escape les symboles et les noms de variable.
>
> https://gitlab.com/monnier/typer/-/compare/main...simon--escape-symbols
>
> Dites-moi si ça vous convient.
LGTM, please push. sauf:
c <> ' '
devrait être
c > ' '
vu que Typer considère tous les charactères <= 32 comme du whitespace.
Stefan