August 2023 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][quotient-types] 7 commits: Implement `Quotient` formation
by James Tan Juan Whei (＠jamestjw) 24 Aug '23

24 Aug '23

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-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.

3 3

[Git][monnier/typer][main] 11 commits: Implement `Quotient` formation
by Stefan (＠monnier) 24 Aug '23

24 Aug '23

Stefan pushed to branch main at Stefan / Typer Commits: c88a9143 by James Tan at 2023-08-21T16:40:32-04:00 Implement `Quotient` formation - - - - - 98dd1f53 by James Tan at 2023-08-21T17:58:12-04:00 Implement `Quotient` introduction - - - - - 85c39685 by James Tan at 2023-08-21T18:58:26-04:00 Implement `Quotient` elimination - - - - - 89c93f93 by James Tan at 2023-08-21T18:58:29-04:00 Implement `Eq` constructor for `Quotient` - - - - - 69fdb2dd by James Tan at 2023-08-21T18:58:29-04:00 Improve unification scheme for SLlub (l1, l2) when l1 ≃ l2 - - - - - 7d9c88fc by James Tan at 2023-08-21T18:58:29-04:00 Implement `qcase` macro - Facilitates `Quotient` elimination - - - - - ee5361fa by James Tan at 2023-08-21T18:58:29-04:00 Write some proofs about quotient types - - - - - f84010df by James Tan at 2023-08-21T19:29:55-04:00 Add a proof that `Quotient` implies `funExt` - - - - - a445e1d0 by Stefan Monnier at 2023-08-24T19:33:22-04:00 Fix the annoying "Bug in the elaboration of a repeated metavar" There are still cases where it can happen, but they should hopefully be more "real" (i.e. cases where the two occurrences of the metavar are in different scopes). * src/debruijn.ml (builtin_axioms): Shorten accordingly. (meta_scope): Keep track of the scope level in the metavar map. * src/elab.ml (sform_identifier): Adjust accordingly. - - - - - 965b1d0d by Stefan Monnier at 2023-08-24T19:37:56-04:00 Make type constructors more like normal/executable Builtins * src/eval.ml (eval_call): When building closures for Builtins, build them one arg at a time, so it works even with very large values of `arity`. (quotient_type): Delete function. (type_constructor): New function. (register_builtin_functions): Use it for `IO/Ref/Array/Quotient`. * src/heap.ml (register_builtins): Use it for `Heap`. * src/debruijn.ml (builtin_axioms): Shorten accordingly. - - - - - 476b8241 by Stefan Monnier at 2023-08-24T19:38:30-04:00 Minor simplifications for Quotient code * btl/builtins.typer (Quotient_elim, Quotient_eq): Simplify the type annotation. (NormToQuotient): Make the base type implicit. * btl/qcase.typer (qcase_impl): Remove redundant `Integer->Int`. Remove leftover `TODO`. * samples/quotient.typer (Z): Adjust to new type of `NormToQuotient`. (q1=1): Simplify the type annotation. - - - - - 15 changed files: - btl/builtins.typer - btl/pervasive.typer - + btl/qcase.typer - samples/nat.typer - + samples/qcase_test.typer - + samples/quotient.typer - + samples/quotient_lib.typer - src/debruijn.ml - src/elab.ml - src/env.ml - src/eval.ml - src/heap.ml - src/opslexp.ml - src/unification.ml - tests/elab_test.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -531,4 +531,31 @@ 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"; + +Quotient_elim : (f : ?A -> ?B) + -> (p : (a : ?) -> (a' : ?) -> ?R a a' -> Eq (f a) (f a')) + ≡> (q : Quotient ?A ?R) -> ?B; +Quotient_elim = Built-in "Quotient.elim"; + +%% FIXME: We want to be able to say the following +%% Quotient_eq : (p : ?R ?a ?a') +%% ≡> Eq (Quotient_in (R := ?R) ?a) (Quotient_in (R := ?R) ?a'); +Quotient_eq : (R : ? -> ? -> ?) + ≡> R ?a ?a' + -> Eq (Quotient_in (R := R) ?a) (Quotient_in (R := R) ?a'); +Quotient_eq = Built-in "Quotient.eq"; + +%% Definition of a quotient type by using a normalisation function +%% NormToQuotient : (?A -> ?A) -> Type; +NormToQuotient f = Quotient ? (lambda a -> lambda a' -> Eq (f a) (f a')); + %%% 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,281 @@ +%% 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 bound in `e1`, and `a`, `a'`, `r` and `i` are +%% bound 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 0 body Sexp_error; + elim_fn_sexp = List_nth 1 body Sexp_error; + elim_compat_sexp = List_nth 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) 2) + then + let + e = List_nth 0 xs Sexp_error; + e_type = List_nth 1 xs Sexp_error; + extract_type sexp sexps = + if (is_sym sexp "_/_") + then + %% (_/_ A R ) + %% |___| |___| + %% | | + %% a r + let + a = List_nth 0 sexps Sexp_error; + r = List_nth 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) 2)) + then + let + %% (_=>_ (Quotient_in a) e1 ) + %% |_____________| |_________| + %% | | + %% qin fn_body + qin_sexp = List_nth 0 sexps Sexp_error; + fn_body_sexp = List_nth 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) + 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) + 2)) + then + let + %% (_=>_ (Quotient_eq a a' r i) p ) + %% |____________________| |__________| + %% | | + %% qeq proof_exp + qeq_sexp = List_nth 0 sexps Sexp_error; + proof_exp_sexp = List_nth 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 + %% 3 or 4 arguments, also ensure that identifier are symbols + if (and (is_sym sexp "Quotient_eq") + (and %% We allow the last parameter `i` to be omitted + (or (Int_eq (List_length sexps) 3) + (Int_eq (List_length sexps) 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) 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 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/nat.typer ===================================== @@ -14,6 +14,13 @@ plus = lambda (x : Nat) -> lambda (y : Nat) -> case x | zero => y | succ z => succ (plus z y); +minus : Nat -> Nat -> Nat; +minus = lambda (x : Nat) -> lambda (y : Nat) -> case x + | zero => zero + | succ m => case y + | zero => x + | succ n => minus m n; + one = succ zero; two = succ one; three = succ two; ===================================== 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,141 @@ +%%%% Definitions of `Nat` +nat-lib = load "samples/nat.typer"; +Nat = nat-lib.Nat; +zero = nat-lib.zero; +succ = nat-lib.succ; +Nat_- = nat-lib.minus; +NatToInt = nat-lib.to-num; + +NatPair = Pair Nat Nat; + +normaliseZ : NatPair -> NatPair; +normaliseZ np = case np + | pair m n => pair (Nat_- m n) (Nat_- n m); + +%% FIXME: Ideally, we shouldn't need to define this separately as this should +%% be taken care of by `NormToQuotient`. However, for now we still to +%% explicitly pass this as a value of R to most `Quotient` functions as it +%% cannot be inferred. +equalZ : NatPair -> NatPair -> Type; +equalZ x1 x2 = Eq (normaliseZ x1) (normaliseZ x2); + +Z = NormToQuotient normaliseZ; + +%% +%% Quotient.eq +%% +%% Proof that quotiented elements are equal when the base elements themselves +%% are related in the underlying type. + +q1-0 : Quotient NatPair equalZ; +q1-0 = Quotient_in (pair (succ zero) zero); + +q2-1 : Quotient NatPair equalZ; +q2-1 = Quotient_in (pair (succ (succ zero)) (succ zero)); + +q1=1 : Eq q1-0 q2-1; +q1=1 = 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. + +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 + +elim_β : (A : Type_ ?) ≡> (B : Type_ ?) + ≡> (R : A -> A -> Type_ ?) + ≡> (f : A -> B) + -> (p : (a : A) -> (a' : A) -> R a a' -> Eq (f a) (f a')) + -> (a : A) -> Eq (Quotient_elim (R := R) f + (p := p) (Quotient_in (R := R) a)) + (f a); +elim_β f p a = Eq_refl; + +%% +%% Proof that the existence of Quotient types implies functional extensionality +%% + +funext : (A : Type_ ?) -> (B : A -> Type_ ?) + -> (f1 : (a : A) -> B a) -> (f2 : (a : A) -> B a) + -> (h : (a : A) -> Eq (f1 a) (f2 a)) -> Eq f1 f2; +funext A B f1 f2 h = + let + fn_type = (a : A) -> B a; + %% This relation can be easily shown to be an equivalence relation + %% by leveraging the properties of the `Eq` type. + equiv_rel : (f1 : fn_type) -> (f1 : fn_type) -> Type_ ?; + equiv_rel f1 f2 = ((a : A) -> Eq (f1 a) (f2 a)); + extfun = Quotient fn_type equiv_rel; + extfun_app : (f : extfun) -> fn_type; + extfun_app f a = Quotient_elim (R := equiv_rel) + (f := lambda f -> f a) + (p := lambda f1 f2 r -> r a) f; + sound : Eq (Quotient_in (R := equiv_rel) f1) + (Quotient_in (R := equiv_rel) f2); + sound = Quotient_eq (R := equiv_rel) (a := f1) (a' := f2) h; + %% The two terms reduce to f1 and f2 respectively by + %% 1. Leveraging the fact that elim_β holds definitionally + %% 2. The η-equivalence of functions + res : Eq (extfun_app (Quotient_in (R := equiv_rel) f1)) + (extfun_app (Quotient_in (R := equiv_rel) f2)); + %% FIXME: Loading `samples/hott.typer` causes the following error + %% [X] Fatal :(internal) lub of two SLsucc + %% Hence, the definition of `Eq_cong` is inlined for now + res = Eq_eq (f := lambda i ≡> extfun_app (Eq_uneq (p := sound) (i := i))); + in + res; ===================================== samples/quotient_lib.typer ===================================== @@ -0,0 +1,123 @@ +%%%%% 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) -> 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) + -> 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? +%% This definition requires dependent elimination of `Quotient` +%% +%% 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,9 +145,9 @@ let type_eq_type = let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) let builtin_axioms = - ["Int"; "Elab_Context"; "IO"; "Ref"; "Sexp"; "Array"; "FileHandle"; - (* From `healp.ml`. *) - "Heap"; "DataconsLabel"] + ["Int"; "Elab_Context"; "Sexp"; "FileHandle"; + (* From `heap.ml`. *) + "DataconsLabel"] (* FIXME: Is this the best way to do this? Originally, I wanted to * define this in Typer and then reference it from OCaml code. @@ -183,7 +183,7 @@ type lctx_length = db_ridx type meta_scope = scope_level (* Integer identifying a level. *) * lctx_length (* Length of ctx when the scope is added. *) - * (meta_id SMap.t ref) (* Metavars already known in this scope. *) + * ((meta_id * scope_level) SMap.t ref) (* Metavars already known in this scope. *) type typeclass_ctx = (ltype * lctx_length) list (* the list of type classes *) ===================================== src/elab.ml ===================================== @@ -651,22 +651,15 @@ and sform_identifier ctx loc sargs ot = let subst = S.shift ctx_shift in let (_, _, rmmap) = ectx_get_scope ctx in if not (name = "") && SMap.mem name (!rmmap) then - let idx = SMap.find name (!rmmap) in - match (metavar_lookup idx) with - | MVar (sl',_,_) - -> if sl = sl' then - (mkMetavar (idx, subst, (loc, Some name)), Lazy) - else - (* FIXME: The variable is from another scope_level! It - means that `subst` is not the right substitution for - the metavar! *) - fatal ~loc:(Sexp.location loc) ("Bug in the elaboration of a metavar" - ^^ " repeated at a different scope level!") - | MVal _ - -> (* FIXME: We face the same problem as above, but here, - the situation is worse, we don't even know the scope - level! *) - fatal ~loc:(Sexp.location loc) "Bug in the elaboration of a repeated metavar!" + let (idx, sl') = SMap.find name (!rmmap) in + if sl = sl' then + (mkMetavar (idx, subst, (loc, Some name)), Lazy) + else + (* FIXME: The variable is from another scope_level! It + means that `subst` is not the right substitution for + the metavar! *) + fatal ~loc:(Sexp.location loc) ("Bug in the elaboration of a metavar" + ^^ " repeated at a different scope level!") else let t = match ot with | None -> newMetatype octx sl loc @@ -679,7 +672,7 @@ and sform_identifier ctx loc sargs ot = match lexp_lexp' mv with | Metavar (idx, _, _) -> idx | _ -> fatal ~loc:(Sexp.location loc) "newMetavar returned a non-Metavar" in - rmmap := SMap.add name idx (!rmmap)); + rmmap := SMap.add name (idx, sl) (!rmmap)); (mv, match ot with Some _ -> Checked | None -> Lazy) (* Normal identifier. *) ===================================== src/env.ml ===================================== @@ -184,6 +184,11 @@ let value_string_with_type v ltype ctx = (Lexp.to_string left) (Lexp.to_string right) (Lexp.to_string t) + | [_; _; (_, 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 ===================================== @@ -535,12 +535,8 @@ and eval_call loc unef i f args = if n >= 0 then (Var (vdummy, n))::buildargs (n - 1) else [] in - let rec buildbody n = - if n > 0 then - Lambda (vdummy, buildbody (n - 1)) - else Call (Builtin (dloc, name), buildargs (arity - 1)) in Closure (vdummy, - buildbody (arity - nargs - 1), + Call (Builtin (dloc, name), buildargs (List.length args)), buildctx args Myers.nil) with @@ -1027,6 +1023,17 @@ 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") +(* Dummy "implementation" of a type constructor. *) +let type_constructor loc _ _args = + error loc "No implementation of the construction of this type" + +let quotient_elim loc depth args = + let trace_dum = (Var ((epsilon (loc), None), -1)) in + match args with + | [f; q] -> + eval_call loc trace_dum depth f [q] + | _ -> error loc "Quotient.elim expects 2 arguments" + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -1048,6 +1055,7 @@ let register_builtin_functions () = ("Float->String" , float_to_string, 1); ("Int->String" , int_to_string, 1); ("Integer->String", integer_to_string, 1); + ("IO" , type_constructor, max_int); ("IO.bind" , io_bind, 2); ("IO.return" , io_return, 1); ("IO.run" , io_run, 2); @@ -1059,6 +1067,7 @@ let register_builtin_functions () = ("Eq.eq" , arity0_fun, 0); ("Eq.uneq" , eq_uneq, 2); ("Y" , y_operator, 1); + ("Ref" , type_constructor, max_int); ("Ref.make" , ref_make, 1); ("Ref.read" , ref_read, 1); ("Ref.write" , ref_write, 2); @@ -1070,6 +1079,7 @@ let register_builtin_functions () = ("Elab.is-arg-erasable", is_arg_erasable, 3); ("Elab.nth-arg" , nth_arg, 3); ("Elab.arg-pos" , arg_pos, 3); + ("Array" , type_constructor, max_int); ("Array.append" , array_append,2); ("Array.create" , array_create,2); ("Array.length" , array_length,1); @@ -1084,6 +1094,10 @@ let register_builtin_functions () = ("Test.false" , test_false,2); ("Test.eq" , test_eq,3); ("Test.neq" , test_neq,3); + ("Quotient" , type_constructor, max_int); + ("Quotient.in" , nop_fun, 1); + ("Quotient.eq" , nop_fun, 1); + ("Quotient.elim" , quotient_elim, 2); ] let _ = register_builtin_functions () ===================================== src/heap.ml ===================================== @@ -138,6 +138,7 @@ let heap_load_cell : builtin_function = | _ -> error ~loc "`Heap.store-cell` expects [Int; Int]" let register_builtins () = + add_builtin_function "Heap" Eval.type_constructor max_int; add_builtin_function "datacons-label<-string" datacons_label_of_string 1; add_builtin_function "Heap.alloc" heap_alloc 1; add_builtin_function "Heap.free" heap_alloc 1; ===================================== 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 @@ -319,12 +321,23 @@ and eq_uneq_whnf ctx args = else None | _ -> None +and quotient_elim_whnf ctx args = + match args with + | _l1 :: _l2 :: _l3 :: _A :: _R :: _P :: (_, f) :: (_, _p) :: (_, q) :: rest + -> (match lexp'_whnf q ctx with + | Call (_, qin, [_; _; _; _; (_, e)]) + when conv_builtin_p ctx qin "Quotient.in" + -> Some (mkCall (dsinfo, f, [Anormal, e]), rest) + | _ -> None) + | _ -> None + and register_reducible_builtins () = reducible_builtins := List.fold_right (fun (n, f) m -> SMap.add n f m) [ ("Eq.cast", eq_cast_whnf); - ("Eq.uneq", eq_uneq_whnf) + ("Eq.uneq", eq_uneq_whnf); + ("Quotient.elim", quotient_elim_whnf) ] !reducible_builtins (** A very naive implementation of sets of pairs of lexps. *) ===================================== 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,27 @@ 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/6ea6caae3d7a7e7619ade47cbc8fc58c… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6ea6caae3d7a7e7619ade47cbc8fc58c… You're receiving this email because of your account on gitlab.com.

1 0

Commit diffs par email
by Stefan Monnier 18 Aug '23

18 Aug '23

Pour info: j'ai changé la config de Gitlab pour n'envoyer les messages de "commit" que pour les changements sur la branche `main`. Donc si vous êtes intéressés par d'autres branches, il faudra soit les consulter manuellement de temps and temps, ou demander à leurs contributeurs de vous aviser quand y a des changements. Stefan

1 0

[Git][monnier/typer][quot-types/rational] 2 commits: Implement `Rational_-` and `Rational_*`
by James Tan Juan Whei (＠jamestjw) 05 Aug '23

05 Aug '23

James Tan Juan Whei pushed to branch quot-types/rational at Stefan / Typer Commits: f6bcc28b by James Tan at 2023-08-04T21:18:16-04:00 Implement `Rational_-` and `Rational_*` - - - - - 4f0b1096 by James Tan at 2023-08-04T22:13:11-04:00 Prove the commutativity of + and * of `Rational`s - - - - - 5 changed files: - btl/builtins.typer - btl/rational.typer - samples/hott.typer - samples/quotient_lib.typer - src/debruijn.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -628,6 +628,20 @@ Integer_isIntegral : (x : Integer) -> (y : Integer) -> Eq (Integer_* x y) 0 -> (Eq x 0 -> Void) -> Eq y 0; Integer_isIntegral = Built-in "Integer.isIntegral"; +%% +%% 1 · x ≡ x +%% +Integer_*Lid : (x : Integer) -> Eq (Integer_* 1 x) x; +Integer_*Lid = Built-in "Integer.*Lid"; + +%% +%% 0 · x ≡ 0 +%% FIXME: Might want to give this a more appropriate name, the intention +%% is to show that 0 is an absorbing element wrt multiplication. +%% +Integer_*Lzero : (x : Integer) -> Eq (Integer_* 0 x) 0; +Integer_*Lzero = Built-in "Integer.*Lzero"; + %%%% Integer theorems %% @@ -658,6 +672,12 @@ Integer_*DistR+ = lambda x -> lambda y -> lambda z -> (Eq_cong (lambda e -> Integer_+ (Integer_* x y) e) (Integer_*-comm z x)))); +Integer_*Rid : (x : Integer) -> Eq (Integer_* x 1) x; +Integer_*Rid x = Eq_trans (Integer_*-comm x 1) (Integer_*Lid x); + +Integer_*Rzero : (x : Integer) -> Eq (Integer_* x 0) 0; +Integer_*Rzero x = Eq_trans (Integer_*-comm x 0) (Integer_*Lzero x); + %% %% Quotient types %% ===================================== btl/rational.typer ===================================== @@ -5,6 +5,7 @@ quot_lib = load "samples/quotient_lib.typer"; Quotient_rec2 = quot_lib.rec2; +Quotient_elimProp2 = quot_lib.elimProp2; %% A hack to ensure that we have fully reduced expressions ℤ𝟘 = 0 : Integer; @@ -214,3 +215,101 @@ Rational_+ : Rational -> Rational -> Rational; Rational_+ a b = Quotient_rec2 (R := equalℚ) (S := equalℚ) Rational_isSet ℤ×ℤ+ ℚ+_feql ℚ+_feqr a b; + +Rational_+-Comm : (a : Rational) -> (b : Rational) -> + Eq (Rational_+ a b) (Rational_+ b a); +Rational_+-Comm a b = Quotient_elimProp2 (R := equalℚ) (S := equalℚ) + (P := lambda a b -> Eq (Rational_+ a b) + (Rational_+ b a)) + (lambda x y -> Rational_isSet (Rational_+ x y) + (Rational_+ y x)) + ℤ×ℤ+-Comm a b; + +ℤ×ℤ* : ℤ×ℤ≠𝟘 -> ℤ×ℤ≠𝟘 -> Rational; +ℤ×ℤ* a b = + let + x1 = fst a; y1 = snd a; p1 = not_zero_proof a; + x2 = fst b; y2 = snd b; p2 = not_zero_proof b; + in + Quotient_in (inR (x1 ℤ* x2) + (y1 ℤ* y2) + (Integer_0-product y1 y2 p1 p2)); + +ℤ×ℤ*-comm : (a : ℤ×ℤ≠𝟘) -> (b : ℤ×ℤ≠𝟘) -> Eq (ℤ×ℤ* a b) (ℤ×ℤ* b a); +ℤ×ℤ*-comm a b = + let + x1 = fst a; y1 = snd a; p1 = not_zero_proof a; + x2 = fst b; y2 = snd b; p2 = not_zero_proof b; + compat = + x1 ℤ* x2 ℤ* (y2 ℤ* y1) + ==< Eq_cong (lambda e -> x1 ℤ* x2 ℤ* e) (Integer_*-comm y2 y1) >== + x1 ℤ* x2 ℤ* (y1 ℤ* y2) + ==< Eq_cong (lambda e -> e ℤ* (y1 ℤ* y2)) (Integer_*-comm x1 x2) >== + x2 ℤ* x1 ℤ* (y1 ℤ* y2) + ==< Integer_*-comm (x2 ℤ* x1) (y1 ℤ* y2) >== + y1 ℤ* y2 ℤ* (x2 ℤ* x1) ∎; + in + Quotient_eq (R := equalℚ) + (a := inR (x1 ℤ* x2) (y1 ℤ* y2) (Integer_0-product y1 y2 p1 p2)) + (a' := inR (x2 ℤ* x1) (y2 ℤ* y1) (Integer_0-product y2 y1 p2 p1)) + compat; + +ℚ*_feql : (a : ℤ×ℤ≠𝟘) -> (a' : ℤ×ℤ≠𝟘) -> (b : ℤ×ℤ≠𝟘) -> equalℚ a a' + -> Eq (ℤ×ℤ* a b) (ℤ×ℤ* a' b); +ℚ*_feql a a' b p = + let + x1 = fst a ; y1 = snd a ; p1 = not_zero_proof a; + x1' = fst a'; y1' = snd a'; p1' = not_zero_proof a'; + x2 = fst b ; y2 = snd b ; p2 = not_zero_proof b; + compat = + x1 ℤ* x2 ℤ* (y1' ℤ* y2) + ==< Eq_cong (lambda e -> e ℤ* (y1' ℤ* y2)) (Integer_*-comm x1 x2) >== + x2 ℤ* x1 ℤ* (y1' ℤ* y2) + ==< (Integer_*-assoc (x2 ℤ* x1) y1' y2) >== + x2 ℤ* x1 ℤ* y1' ℤ* y2 + ==< Eq_cong (lambda e -> e ℤ* y2) (Eq_comm (Integer_*-assoc x2 x1 y1')) >== + x2 ℤ* (x1 ℤ* y1') ℤ* y2 + ==< Eq_cong (lambda e -> x2 ℤ* e ℤ* y2) p >== + x2 ℤ* (y1 ℤ* x1') ℤ* y2 + ==< Eq_cong (lambda e -> e ℤ* y2) (Integer_*-comm x2 (y1 ℤ* x1')) >== + y1 ℤ* x1' ℤ* x2 ℤ* y2 + ==< Eq_comm (Integer_*-assoc (y1 ℤ* x1') x2 y2) >== + y1 ℤ* x1' ℤ* (x2 ℤ* y2) + ==< Eq_cong (lambda e -> (y1 ℤ* x1') ℤ* e) (Integer_*-comm x2 y2) >== + y1 ℤ* x1' ℤ* (y2 ℤ* x2) + ==< (Integer_*-assoc (y1 ℤ* x1') y2 x2) >== + y1 ℤ* x1' ℤ* y2 ℤ* x2 + ==< Eq_cong (lambda e -> e ℤ* x2) (Eq_comm (Integer_*-assoc y1 x1' y2)) >== + y1 ℤ* (x1' ℤ* y2) ℤ* x2 + ==< Eq_cong (lambda e -> y1 ℤ* e ℤ* x2) (Integer_*-comm x1' y2) >== + y1 ℤ* (y2 ℤ* x1') ℤ* x2 + ==< Eq_cong (lambda e -> e ℤ* x2) (Integer_*-assoc y1 y2 x1') >== + y1 ℤ* y2 ℤ* x1' ℤ* x2 + ==< Eq_comm (Integer_*-assoc (y1 ℤ* y2) x1' x2) >== + y1 ℤ* y2 ℤ* (x1' ℤ* x2) ∎; + in + Quotient_eq (R := equalℚ) + (a := inR (x1 ℤ* x2) (y1 ℤ* y2) + (Integer_0-product y1 y2 p1 p2)) + (a' := inR (x1' ℤ* x2) (y1' ℤ* y2) + (Integer_0-product y1' y2 p1' p2)) + compat; + +ℚ*_feqr : (a : ℤ×ℤ≠𝟘) -> (b : ℤ×ℤ≠𝟘) -> (b' : ℤ×ℤ≠𝟘) -> equalℚ b b' + -> Eq (ℤ×ℤ* a b) (ℤ×ℤ* a b'); +ℚ*_feqr a b b' p = Eq_trans (ℤ×ℤ*-comm a b) + (Eq_trans (ℚ*_feql b b' a p) (ℤ×ℤ*-comm b' a)); + +Rational_* : Rational -> Rational -> Rational; +Rational_* a b = + Quotient_rec2 (R := equalℚ) (S := equalℚ) + Rational_isSet ℤ×ℤ* ℚ*_feql ℚ*_feqr a b; + +Rational_*-Comm : (a : Rational) -> (b : Rational) -> + Eq (Rational_* a b) (Rational_* b a); +Rational_*-Comm a b = Quotient_elimProp2 (R := equalℚ) (S := equalℚ) + (P := lambda a b -> Eq (Rational_* a b) + (Rational_* b a)) + (lambda x y -> Rational_isSet (Rational_* x y) + (Rational_* y x)) + ℤ×ℤ*-comm a b; ===================================== samples/hott.typer ===================================== @@ -182,6 +182,14 @@ HoTT_isContr = typecons (HoTT_isContr (l ::: TypeLevel) (isContr (a : A) ((a' : A) -> Eq a a')); isContr = datacons HoTT_isContr isContr; +isPropΠ : (A : Type_ ?) ≡> (B : A -> Type_ ?) ≡> + (h : (x : A) -> HoTT_isProp (B x)) -> + HoTT_isProp ((x : A) -> B x); +isPropΠ h f g = Eq_eq (f := lambda i ≡> + lambda (x : A) -> + Eq_uneq (p := h x (f x) (g x)) + (i := i)); + %% Provable without axioms: %% %% ¬¬¬A -> ¬A ===================================== samples/quotient_lib.typer ===================================== @@ -11,6 +11,8 @@ HoTT_isSet = HoTT_lib.HoTT_isSet; HoTT_isContr = HoTT_lib.HoTT_isContr; isContr = HoTT_lib.isContr; +isPropΠ = HoTT_lib.isPropΠ; + %%%%% Prelude END %%%%%% %% This function constructs the lid of this square: @@ -74,6 +76,19 @@ elimProp = lambda _ _ _ A R P ≡> lambda prop f -> in fa=fa'); +elimProp2 : (A : Type_ ?) ≡> (B : Type_ ?) ≡> + (R : A -> A -> Type_ ?) ≡> (S : B -> B -> Type_ ?) ≡> + (P : Quotient A R -> Quotient B S -> Type_ ?) ≡> + (prop : (x : Quotient A R) -> (y : Quotient B S) + -> HoTT_isProp (P x y)) -> + (f : (x : A) -> (y : B) -> P (Quotient_in x) (Quotient_in y)) -> + (x : Quotient A R) -> (y : Quotient B S) -> P x y; +elimProp2 = lambda _ _ _ _ _ A B R S P ≡> lambda prop f -> + elimProp (R := R) (P := lambda x -> (y : Quotient B S) -> P x y) + (lambda x -> isPropΠ (B := P x) (prop x)) + (lambda a -> elimProp (R := S) (P := P (Quotient_in a)) + (prop (Quotient_in a)) (f a)); + recProp : (A : Type_ ?) ≡> (B : Type_ ?) ≡> (R : A -> A -> Type_ ?) ≡> ===================================== src/debruijn.ml ===================================== @@ -155,7 +155,7 @@ let builtin_axioms = "Heap"; "DataconsLabel"; (* Integer axioms *) "Integer.1!=0"; "Integer.+-comm"; "Integer.*-comm"; "Integer.*-assoc"; - "Integer.*DistL+"; "Integer.isIntegral"] + "Integer.*DistL+"; "Integer.isIntegral"; "Integer.*Lid"; "Integer.*Lzero"] (* FIXME: Is this the best way to do this? Originally, I wanted to * define this in Typer and then reference it from OCaml code. View it on GitLab: https://gitlab.com/monnier/typer/-/compare/53990bc7a2ae6cde6df5cc093b16582e… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/53990bc7a2ae6cde6df5cc093b16582e… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][quot-types/rational] 22 commits: Implement heterogeneous equality `Heq`
by James Tan Juan Whei (＠jamestjw) 04 Aug '23

04 Aug '23

James Tan Juan Whei pushed to branch quot-types/rational at Stefan / Typer Commits: 1424c518 by James Tan at 2023-07-27T17:48:19-04:00 Implement heterogeneous equality `Heq` - - - - - 7932ef5b by James Tan at 2023-07-27T19:14:51-04:00 Implement `Quotient` formation - - - - - 8fc629ec by James Tan at 2023-07-27T19:14:52-04:00 Implement `Quotient` introduction - - - - - 54973f20 by James Tan at 2023-07-27T19:14:52-04:00 Implement `Quotient` elimination - - - - - d34d5a0a by James Tan at 2023-07-27T19:17:04-04:00 Implement `Eq` constructor for `Quotient` - - - - - e1f1f1f2 by James Tan at 2023-07-27T19:17:06-04:00 Improve unification scheme for SLlub (l1, l2) when l1 ≃ l2 - - - - - 798057a4 by James Tan at 2023-07-27T19:17:06-04:00 Implement `qcase` macro - Facilitates `Quotient` elimination - - - - - f47f1d40 by James Tan at 2023-07-27T19:17:06-04:00 Write some proofs about quotient types - - - - - 86a27d15 by James Tan at 2023-07-27T20:00:40-04:00 Implement dependent elimination of `Quotient` - Rename non-dependent elimination fn to `Quotient.rec` - Introduce new built-in function `Quotient.elim` - - - - - 1333d1f2 by James Tan at 2023-07-28T19:48:02-04:00 Write some hypothetical code to implement `elimProp` for `Quotient` - - - - - b2e99d9e by James Tan at 2023-07-28T21:58:13-04:00 Add the Interval `transp` function - - - - - 908d9e07 by James Tan at 2023-07-30T20:06:09-04:00 Implement `I.not` and `I.meet` as built-ins - - - - - 183f31b8 by James Tan at 2023-07-31T00:04:53-04:00 Make `toPathOver` and `elimProp` work - - - - - 90592ffc by James Tan at 2023-07-31T18:52:18-04:00 Make `rec2` work - Fix eta expansion of functions to work with not just variables - Add reduction rule of `Quotient.elim` - - - - - a457a490 by James Tan at 2023-07-31T18:52:20-04:00 Add note on propositional truncation - - - - - 3b967115 by James Tan at 2023-08-03T18:24:52-04:00 Provide a dummy runtime value for `Quotient` type - Allows the assignation of the type to a variable - - - - - 9db83957 by James Tan at 2023-08-03T18:24:54-04:00 Add preliminary code for `Rational` quotient - - - - - a3db35ad by James Tan at 2023-08-03T18:24:54-04:00 Implement equational reasoning - - - - - 8cfa0de9 by James Tan at 2023-08-03T18:24:55-04:00 Implement `Rational_negate` - Move `Eq_cong` to `builtins.typer` for better accessibility - - - - - c13a94b3 by James Tan at 2023-08-03T18:40:34-04:00 Implement set truncation of `Quotient` - - - - - 3bd07df7 by James Tan at 2023-08-03T20:02:25-04:00 Add 'fix' to make it possible to import `samples/hott.typer` in `samples/quotient_lib.typer` - - - - - 53990bc7 by James Tan at 2023-08-03T20:02:47-04:00 Implement `Rational_add` - - - - - 22 changed files: - btl/builtins.typer - btl/depelim.typer - btl/pervasive.typer - + btl/qcase.typer - + btl/rational.typer - + samples/equational_reasoning_test.typer - samples/hott.typer - + samples/qcase_test.typer - + samples/quotient.typer - + samples/quotient_lib.typer - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml - tests/elab_test.ml - tests/env_test.ml - tests/eval_test.ml - tests/instargs_test.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -49,36 +49,99 @@ Void = typecons Void; i0 = datacons I i0; i1 = datacons I i1; +%% Operations on the Interval are built-ins in order to enforce some +%% definitional equalities. I_not : I -> I; -I_not i = case i - | i0 => i1 - | i1 => i0; +I_not = Built-in "I.not"; + +I_meet : I -> I -> I; +I_meet = Built-in "I.meet"; + +%% Inspired by Cubical Agda, with the difference that we +%% return A r +%% The Cubical Agda definition: +%% transp : ∀ {ℓ} (A : I → Set ℓ) (r : I) (a : A i0) → A i1 +%% This way, we avoid the peculiarity of having to have +%% side conditions on `A` based on the value of `r`. +I_transp : (A : I ≡> Type_ ?) ≡> (r : I) ≡> + A (_ := i0) -> A (_ := I_not r); +I_transp = Built-in "I.transp"; %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l +%% Heq : (l : TypeLevel) ≡> (t1 : Type_ l) ≡> (t2 : Type_ l) +%% ≡> t1 -> t2 -> Type_ l + +Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l; +Eq = lambda _ ≡> lambda _ ≡> lambda x -> lambda y -> + Heq x y; + +Heq_eq : (l : TypeLevel) ≡> (t : I ≡> Type_ l) ≡> (f : (i : I) ≡> t (_ := i)) + ≡> Heq (f (_ := i0)) (f (_ := i1)); +Heq_eq = Built-in "Heq.eq"; + Eq_eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> (f : I ≡> t) - ≡> Eq (f (_ := i0)) (f (_ := i1)); -Eq_eq = Built-in "Eq.eq"; + ≡> Eq (t := t) (f (_ := i0)) (f (_ := i1)); +Eq_eq = lambda _ ≡> lambda t ≡> lambda f ≡> + Heq_eq (t := lambda _ ≡> t) (f := f); + +Heq_uneq : (l : TypeLevel) ≡> (t : I ≡> Type_ l) + ≡> (x : t (_ := i0)) => (y : t (_ := i1)) + => (p : Heq x y) ≡> (i : I) ≡> t (_ := i); +Heq_uneq = Built-in "Heq.uneq"; Eq_uneq : (l : TypeLevel) ≡> (t : Type_ l) ≡> (x : t) => (y : t) => (p : Eq x y) ≡> (i : I) ≡> t; -Eq_uneq = Built-in "Eq.uneq"; +Eq_uneq = lambda _ ≡> lambda t ≡> + lambda _ => lambda _ => + lambda p ≡> lambda i ≡> + Heq_uneq (t := lambda _ ≡> t) (p := p) (i := i); + +Heq_refl : (A : ?) ≡> (B : A -> ?) + ≡> (x : A) ≡> (y : B x) ≡> Heq y y; +Heq_refl = lambda _ ≡> lambda _ ≡> lambda A ≡> lambda B ≡> + lambda x ≡> lambda y ≡> + Heq_eq + (t := lambda _ ≡> B x) + (f := lambda _ ≡> y); Eq_refl : (l : TypeLevel) ≡> (t : Type_ l) - ≡> (x : t) ≡> Eq x x; -Eq_refl = lambda _ ≡> lambda _ ≡> lambda x - ≡> Eq_eq (f := lambda _ ≡> x); - -Eq_cast : (x : ?) ≡> (y : ?) - ≡> (p : Eq x y) - ≡> (f : ? -> ?) - ≡> f x -> f y; + ≡> (x : t) ≡> Eq x x; +Eq_refl = lambda _ ≡> lambda _ ≡> lambda x ≡> + Eq_eq (f := lambda _ ≡> x); +%% Note: This works too, but we use the simpler +%% definition. +%% Eq_refl = lambda _ ≡> lambda t ≡> lambda x ≡> +%% Heq_refl +%% (A := t) +%% (B := lambda _ -> t) +%% (x := x) (y := x); + +%% FIXME: Hmm the type of `f` implies that `x` and `y` are of the same type, +%% contrary to what is suggested by `Heq`. This implies that it is sufficient +%% to define Eq_cast +%% Heq_cast : (x : ?) ≡> (y : ?) +%% ≡> (p : Heq x y) +%% ≡> (f : I ≡> ? -> ?) +%% ≡> f (_ := i0) x -> f (_ := i1) y; +%% Heq_cast = Built-in "Heq.cast"; + %% FIXME: I'd like to just say: %% Eq_cast : Eq ?x ?y ≡> ?f ?x -> ?f ?y; -Eq_cast = Built-in "Eq.cast"; +Eq_cast : (x : ?) ≡> (y : ?) ≡> (p : Eq x y) ≡> (f : ? -> ?) + ≡> f x -> f y; +Eq_cast = lambda _ ≡> lambda _ ≡> %% Two level variables + lambda A ≡> %% Type of x and y + lambda x ≡> lambda y ≡> + lambda p ≡> lambda f ≡> + lambda fx -> + I_transp (A := lambda i ≡> f (Heq_uneq + (t := lambda _ ≡> A) + (p := p) (i := i))) + (r := i0) fx; %% Commutativity of equality! %% FIXME: I'd like to just say: @@ -92,6 +155,12 @@ Eq_comm p = Eq_eq (f := lambda i ≡> Eq_uneq (p := p) (i := I_not i)); 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; +Eq_cong : (x : ?A) => (y : ?A) => + (f : ?A -> ?) -> (p : Eq x y) + -> Eq (f x) (f y); +Eq_cong = lambda f -> lambda p -> + Eq_eq (f := lambda i ≡> f (Eq_uneq (p := p) (i := i))); + %% General recursion!! %% Whether this breaks consistency or not is a good question. %% The basic idea is the following: @@ -531,4 +600,125 @@ 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"; +%%%% Integer axioms +Integer_1≠0 = Built-in "Integer.1!=0" : Eq (t := Integer) 1 0 -> Void; + +Integer_+-comm : (x : Integer) -> (y : Integer) -> Eq (Integer_+ x y) (Integer_+ y x); +Integer_+-comm = Built-in "Integer.+-comm"; + +Integer_*-comm : (x : Integer) -> (y : Integer) -> Eq (Integer_* x y) (Integer_* y x); +Integer_*-comm = Built-in "Integer.*-comm"; + +Integer_*-assoc : (x : Integer) -> (y : Integer) -> (z : Integer) -> + Eq (Integer_* x (Integer_* y z)) (Integer_* (Integer_* x y) z); +Integer_*-assoc = Built-in "Integer.*-assoc"; + +%% +%% (x + y) · z ≡ x · z + y · z +%% +Integer_*DistL+ : (x : Integer) -> (y : Integer) -> (z : Integer) -> + Eq (Integer_* (Integer_+ x y) z) + (Integer_+ (Integer_* x z) (Integer_* y z)); +Integer_*DistL+ = Built-in "Integer.*DistL+"; + +%% +%% x · y ≡ 0 → ¬ x ≡ 0 → y ≡ 0 +%% +Integer_isIntegral : (x : Integer) -> (y : Integer) -> Eq (Integer_* x y) 0 -> + (Eq x 0 -> Void) -> Eq y 0; +Integer_isIntegral = Built-in "Integer.isIntegral"; + +%%%% Integer theorems + +%% +%% Zero-product property of integers +%% (¬ x ≡ 0) → (¬ y ≡ 0) -> (¬ x · y ≡ 0) +%% +Integer_0-product : (x : Integer) -> (y : Integer) -> (Eq x 0 -> Void) -> + (Eq y 0 -> Void) -> (Eq (Integer_* x y) 0 -> Void); +Integer_0-product = lambda x -> lambda y -> + lambda x≠0 -> lambda y≠0 -> lambda xy≠0 -> + y≠0 (Integer_isIntegral x y xy≠0 x≠0); + +%% +%% x · (y + z) ≡ x · y + x · z +%% +%% FIXME: It'd be much better to have some sort of operator to facilitate the +%% concatenation of equality proofs. +%% Also, the last 2 commutativity proofs could be combined if we had cong₂, +%% whose definition requires dependent paths. +Integer_*DistR+ : (x : Integer) -> (y : Integer) -> (z : Integer) -> + Eq (Integer_* x (Integer_+ y z)) + (Integer_+ (Integer_* x y) (Integer_* x z)); +Integer_*DistR+ = lambda x -> lambda y -> lambda z -> + Eq_trans (Integer_*-comm x (Integer_+ y z)) + (Eq_trans (Integer_*DistL+ y z x) + (Eq_trans (Eq_cong (lambda e -> Integer_+ e (Integer_* z x)) + (Integer_*-comm y x)) + (Eq_cong (lambda e -> Integer_+ (Integer_* x y) e) + (Integer_*-comm z x)))); + +%% +%% 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_rec : (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 : (A : ?) ≡> (R : A -> A -> ?) ≡> + (P : Quotient A R -> ?) ≡> + (f : (a : A) -> (P (Quotient_in a))) -> + (p : (a : A) -> (a' : A) -> R a a' -> Heq (f a) (f a')) ≡> + (q : Quotient A R) -> P q; +Quotient_elim = Built-in "Quotient.elim"; + +%% FIXME: If we eta expand this, i.e. if we write +%% ... lambda q -> Quotient_elim ... f (p := p) q +%% We get a Debruijn index error in while defining `rec2` in `quotient_lib.typer`, +%% this shouldn't happen and should be further investigated! +Quotient_rec : (A : ?) ≡> (B : ?) ≡> + (R : A -> A -> ?) ≡> + (f : A -> B) -> + (p : (a : A) -> (a' : A) -> R a a' -> Eq (f a) (f a')) ≡> + (q : Quotient A R) -> + B; +Quotient_rec = lambda _ ≡> lambda _ ≡> lambda _ ≡> + lambda A ≡> lambda B ≡> lambda R ≡> + lambda f -> lambda p ≡> + Quotient_elim (R := R) (P := lambda _ -> B) f (p := p); + +%% FIXME: This axiom is necessary if we want to eliminate 2 quotiented +%% expressions to produce another quotiented expression. For now, the +%% 'prop'-ness of `Quotient_eq` isn't verified during `Quotient` elimination, +%% because +%% 1. it makes `Quotient` elimination really troublesome, and +%% 2. I want to see if this changes/breaks anything. +Quotient_trunc : (A : ?) ≡> (R : A -> A -> ?) ≡> + (x : Quotient A R) ≡> (y : Quotient A R) ≡> + (p : Eq x y) -> (q : Eq x y) -> Eq p q; +Quotient_trunc = Built-in "Quotient.trunc"; + %%% builtins.typer ends here. ===================================== btl/depelim.typer ===================================== @@ -76,7 +76,7 @@ case_as_return_impl args = Sexp_node arrow_sexp (cons head_sexp - (cons (quote (##Eq\.cast + (cons (quote (Eq_cast (x := uquote head_sexp) (y := uquote target_sexp) (p := ##DeBruijn 0) ===================================== btl/pervasive.typer ===================================== @@ -690,6 +690,26 @@ 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; + +%%%% Equational reasoning +%% Function to do one step of equational reasoning +step-≡ : (x : ?A) -> (y : ?A) ≡> (z : ?A) ≡> Eq x y -> Eq y z -> Eq x z; +step-≡ _ p q = Eq_trans p q; + +%% Function to conclude equational reasoning +qed : (x : ?A) -> Eq x x; +qed x = Eq_refl; + +%% FIXME: Chosen somewhat arbitrarily for now +define-operator "==<" 45 40; +define-operator ">==" 40 42; +define-operator "∎" 43 (); + +_==<_>==_ = step-≡; +_∎ = qed; + %%%% 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_rec") + qelim_args; + in + IO_return qelim_sexp; +qcase_macro = macro qcase_impl; ===================================== btl/rational.typer ===================================== @@ -0,0 +1,216 @@ +%% +%% Prelude +%% + +quot_lib = load "samples/quotient_lib.typer"; + +Quotient_rec2 = quot_lib.rec2; + +%% A hack to ensure that we have fully reduced expressions +ℤ𝟘 = 0 : Integer; +ℤ𝟙 = 1 : Integer; +ℤ−𝟙 = -1 : Integer; + +%% This is defined to make the code in this module more readable. +%% Mirrors the precedence of the Int operators. +define-operator "ℤ+" 111 130; +define-operator "ℤ*" 142 155; + +_ℤ+_ = Integer_+; +_ℤ*_ = Integer_*; + +%% +%% Prelude END +%% + +%% Type that will serve as the underlying type +%% of the Rational quotient +type ℤ×ℤ≠𝟘 + | inR (z1 : Integer) (z2 : Integer) (Not (Eq z2 ℤ𝟘)); + +fst : ℤ×ℤ≠𝟘 -> Integer; +fst z + | inR z1 _ _ => z1; + +snd : ℤ×ℤ≠𝟘 -> Integer; +snd z + | inR _ z2 _ => z2; + +not_zero_proof : (z : ℤ×ℤ≠𝟘) -> Not (Eq (snd z) ℤ𝟘); +not_zero_proof z = + case z return (Not (Eq (snd z) ℤ𝟘)) + | inR z1 z2 p => p; + +%% Use functions to access individual components of the inductive type +%% to get better definitional equivalences. +equalℚ : ℤ×ℤ≠𝟘 -> ℤ×ℤ≠𝟘 -> Type_ ?; +equalℚ z1 z2 = Eq ((fst z1) ℤ* (snd z2)) ((snd z1) ℤ* (fst z2)); + +Rational : Type; +Rational = Quotient ℤ×ℤ≠𝟘 equalℚ; + +Rational_isSet : (x : Rational) -> (y : Rational) -> (p : Eq x y) -> (q : Eq x y) + -> Eq p q; +Rational_isSet x y p q = Quotient_trunc (R := equalℚ) p q; + +%% To construct an element of this quotient, we need to prove that some Integer != 0 +%% We could add the following axioms +%% +%% Integer_1!=0 : Eq (t := Integer) 1 0 -> False; +%% Integer_-1!=0 : Eq (t := Integer) -1 0 -> False; +%% Integer_succ!=0 : (x : Integer) -> Not (Eq x 0) -> Not (Eq (Integer_+ x 1) 0); +%% Integer_pred!=0 : (x : Integer) -> Not (Eq x 0) -> Not (Eq (Integer_- x 1) 0); + +%% While we are at it, these axioms seems good to have +%% Integer_x-1=x+-1 : (x : Integer) -> Eq (Integer_- x 1) (Integer_+ x -1); +%% Integer_x+1=x--1 : (x : Integer) -> Eq (Integer_+ x 1) (Integer_- x -1); + +Rational_1 : Rational; +Rational_1 = + %% FIXME: Small hack to make it work, if we put + %% the literal `1` as the second arg, this doesn't + %% type check + Quotient_in (inR ℤ𝟙 ℤ𝟙 Integer_1≠0); + +Rational_negate : Rational -> Rational; +Rational_negate x = + let + negate_fst : ℤ×ℤ≠𝟘 -> ℤ×ℤ≠𝟘; + negate_fst x = inR (ℤ−𝟙 ℤ* (fst x)) (snd x) (not_zero_proof x); + negate_compat : (a : ℤ×ℤ≠𝟘) -> (b : ℤ×ℤ≠𝟘) -> + equalℚ a b -> equalℚ (negate_fst a) (negate_fst b); + negate_compat a b r = + (ℤ−𝟙 ℤ* (fst a)) ℤ* (snd b) + ==< Eq_comm (Integer_*-assoc ℤ−𝟙 (fst a) (snd b)) >== + ℤ−𝟙 ℤ* ((fst a) ℤ* (snd b)) + ==< Eq_cong (lambda e -> ℤ−𝟙 ℤ* e) r >== + ℤ−𝟙 ℤ* ((snd a) ℤ* (fst b)) + ==< Integer_*-assoc ℤ−𝟙 (snd a) (fst b) >== + (ℤ−𝟙 ℤ* (snd a)) ℤ* (fst b) + ==< Eq_cong (lambda e -> e ℤ* (fst b)) + (Integer_*-comm ℤ−𝟙 (snd a)) >== + ((snd a) ℤ* ℤ−𝟙) ℤ* (fst b) + ==< Eq_comm (Integer_*-assoc (snd a) ℤ−𝟙 (fst b)) >== + (snd a) ℤ* (ℤ−𝟙 ℤ* (fst b)) ∎; + in + qcase (x : ℤ×ℤ≠𝟘 / equalℚ) + | Quotient_in a => Quotient_in (R := equalℚ) (negate_fst a) + | Quotient_eq a a' r => Quotient_eq (R := equalℚ) + (a := negate_fst a) + (a' := negate_fst a') + (negate_compat a a' r); + +ℤ×ℤ+ : ℤ×ℤ≠𝟘 -> ℤ×ℤ≠𝟘 -> Rational; +ℤ×ℤ+ a b = + let + x1 = fst a; y1 = snd a; p1 = not_zero_proof a; + x2 = fst b; y2 = snd b; p2 = not_zero_proof b; + in + Quotient_in (inR ((x1 ℤ* y2) ℤ+ (x2 ℤ* y1)) + (y1 ℤ* y2) + (Integer_0-product y1 y2 p1 p2)); + +ℤ×ℤ+-Comm : (a : ℤ×ℤ≠𝟘) -> (b : ℤ×ℤ≠𝟘) -> Eq (ℤ×ℤ+ a b) (ℤ×ℤ+ b a); +ℤ×ℤ+-Comm a b = + let + x1 = fst a; y1 = snd a; p1 = not_zero_proof a; + x2 = fst b; y2 = snd b; p2 = not_zero_proof b; + compat = + (x1 ℤ* y2 ℤ+ x2 ℤ* y1) ℤ* (y2 ℤ* y1) + ==< Eq_cong (lambda e -> (x1 ℤ* y2 ℤ+ x2 ℤ* y1) ℤ* e) + (Integer_*-comm y2 y1) >== + (x1 ℤ* y2 ℤ+ x2 ℤ* y1) ℤ* (y1 ℤ* y2) + ==< Integer_*-comm (x1 ℤ* y2 ℤ+ x2 ℤ* y1) (y1 ℤ* y2) >== + y1 ℤ* y2 ℤ* (x1 ℤ* y2 ℤ+ x2 ℤ* y1) + ==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* e) + (Integer_+-comm (x1 ℤ* y2) (x2 ℤ* y1)) >== + y1 ℤ* y2 ℤ* (x2 ℤ* y1 ℤ+ x1 ℤ* y2) ∎; + in + Quotient_eq (R := equalℚ) + (a := inR (x1 ℤ* y2 ℤ+ x2 ℤ* y1) + (y1 ℤ* y2) + (Integer_0-product y1 y2 p1 p2)) + (a' := inR (x2 ℤ* y1 ℤ+ x1 ℤ* y2) + (y2 ℤ* y1) + (Integer_0-product y2 y1 p2 p1)) + compat; + +%% FIXME: This proof begs to be simplified +ℚ+_feql : (a : ℤ×ℤ≠𝟘) -> (a' : ℤ×ℤ≠𝟘) -> (b : ℤ×ℤ≠𝟘) -> equalℚ a a' + -> Eq (ℤ×ℤ+ a b) (ℤ×ℤ+ a' b); +ℚ+_feql a a' b p = + let + x1 = fst a ; y1 = snd a ; p1 = not_zero_proof a; + x1' = fst a'; y1' = snd a'; p1' = not_zero_proof a'; + x2 = fst b ; y2 = snd b ; p2 = not_zero_proof b; + compat = + (x1 ℤ* y2 ℤ+ x2 ℤ* y1) ℤ* (y1' ℤ* y2) + ==< Integer_*DistL+ (x1 ℤ* y2) (x2 ℤ* y1) (y1' ℤ* y2) >== + (x1 ℤ* y2) ℤ* (y1' ℤ* y2) ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2) + ==< Eq_cong (lambda e -> e ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2)) + (Integer_*-assoc (x1 ℤ* y2) y1' y2) >== + (x1 ℤ* y2) ℤ* y1' ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2) + ==< Eq_cong (lambda e -> e ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2)) + (Eq_trans (Eq_comm (Integer_*-assoc x1 y2 y1')) + (Eq_trans (Eq_cong (lambda e -> x1 ℤ* e) + (Integer_*-comm y2 y1')) + (Integer_*-assoc x1 y1' y2))) >== + x1 ℤ* y1' ℤ* y2 ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2) + ==< Eq_cong (lambda e -> + e ℤ* y2 ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2)) + p >== + y1 ℤ* x1' ℤ* y2 ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2) + ==< Eq_cong (lambda e -> e ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2)) + (Eq_comm (Integer_*-assoc y1 x1' y2)) >== + y1 ℤ* (x1' ℤ* y2)ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2) + ==< Eq_cong (lambda e -> y1 ℤ* e ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2)) + (Integer_*-comm x1' y2) >== + y1 ℤ* (y2 ℤ* x1') ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2) + ==< Eq_cong (lambda e -> e ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2)) + (Integer_*-assoc y1 y2 x1') >== + y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ x2 ℤ* y1 ℤ* (y1' ℤ* y2) + ==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ e ℤ* (y1' ℤ* y2)) + (Integer_*-comm x2 y1) >== + y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* x2 ℤ* (y1' ℤ* y2) + ==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* x2 ℤ* e) + (Integer_*-comm y1' y2) >== + y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* x2 ℤ* (y2 ℤ* y1') + ==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ e) + (Integer_*-assoc (y1 ℤ* x2) y2 y1') >== + y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* x2 ℤ* y2 ℤ* y1' + ==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ e ℤ* y1') + (Eq_comm (Integer_*-assoc y1 x2 y2)) >== + y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* (x2 ℤ* y2) ℤ* y1' + ==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* e ℤ* y1') + (Integer_*-comm x2 y2) >== + y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* (y2 ℤ* x2) ℤ* y1' + ==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ e ℤ* y1') + (Integer_*-assoc y1 y2 x2) >== + y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* y2 ℤ* x2 ℤ* y1' + ==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ e) + (Eq_comm (Integer_*-assoc (y1 ℤ* y2) x2 y1')) >== + y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* y2 ℤ* (x2 ℤ* y1') + ==< Eq_cong (lambda e -> e ℤ+ y1 ℤ* y2 ℤ* (x2 ℤ* y1')) + (Eq_comm (Integer_*-assoc (y1 ℤ* y2) x1' y2)) >== + y1 ℤ* y2 ℤ* (x1' ℤ* y2) ℤ+ y1 ℤ* y2 ℤ* (x2 ℤ* y1') + ==< Eq_comm (Integer_*DistR+ (y1 ℤ* y2) (x1' ℤ* y2) (x2 ℤ* y1')) >== + y1 ℤ* y2 ℤ* (x1' ℤ* y2 ℤ+ x2 ℤ* y1') ∎; + in + Quotient_eq (R := equalℚ) + (a := inR (x1 ℤ* y2 ℤ+ x2 ℤ* y1) + (y1 ℤ* y2) + (Integer_0-product y1 y2 p1 p2)) + (a' := inR (x1' ℤ* y2 ℤ+ x2 ℤ* y1') + (y1' ℤ* y2) + (Integer_0-product y1' y2 p1' p2)) + compat; + +ℚ+_feqr : (a : ℤ×ℤ≠𝟘) -> (b : ℤ×ℤ≠𝟘) -> (b' : ℤ×ℤ≠𝟘) -> equalℚ b b' + -> Eq (ℤ×ℤ+ a b) (ℤ×ℤ+ a b'); +ℚ+_feqr a b b' p = Eq_trans (ℤ×ℤ+-Comm a b) + (Eq_trans (ℚ+_feql b b' a p) (ℤ×ℤ+-Comm b' a)); + +Rational_+ : Rational -> Rational -> Rational; +Rational_+ a b = + Quotient_rec2 (R := equalℚ) (S := equalℚ) + Rational_isSet ℤ×ℤ+ ℚ+_feql ℚ+_feqr a b; ===================================== samples/equational_reasoning_test.typer ===================================== @@ -0,0 +1,12 @@ +short : (x : ?A) -> (y : ?A) -> (p : Eq x y) -> Eq x y; +short x y p = + x ==< p >== + y ∎; + +long : (x : ?A) -> (y : ?A) -> (z : ?A) -> (w : ?A) -> + (p : Eq x y) -> (q : Eq y z) -> (r : Eq z w) -> Eq x w; +long x y z w p q r = + x ==< p >== + y ==< q >== + z ==< r >== + w ∎; ===================================== samples/hott.typer ===================================== @@ -101,12 +101,6 @@ Eq_funext : (f : ? -> ?) => (g : ? -> ?) => Eq f g; Eq_funext p = Eq_eq (f := lambda i ≡> lambda x -> Eq_uneq (p := p x) (i := i)); -%% Properties of the equality type -Eq_cong : (x : ?A) => (y : ?A) => - (f : ?A -> ?) -> (p : Eq x y) - -> Eq (f x) (f y); -Eq_cong f p = Eq_eq (f := lambda i ≡> f (Eq_uneq (p := p) (i := i))); - %% This is necessary to prove Eq_comm_inv notnot=id : (i : I) -> Eq i (I_not (I_not i)); notnot=id i = case i return (Eq i (I_not (I_not i))) @@ -183,6 +177,11 @@ HoTT_isSet A = (x : A) -> (y : A) -> (p : Eq x y) -> (q : Eq x y) -> Eq p q; %% encoding of classical `or` in type-theory, then it preserves `isProp`! HoTT_isProp P = (x : P) -> (y : P) -> 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; + %% Provable without axioms: %% %% ¬¬¬A -> ¬A @@ -202,9 +201,16 @@ Weak_double_negation nnna a = nnna (lambda na -> na a); %% Propositional truncation: ||A|| is equivalent to A but is a mere proposition. %% One way to approximate could be: -Propositional_truncation A = (P : ?) ≡> HoTT_isProp P ≡> (A -> P) -> P; -propositional_truncation : ?A -> Propositional_truncation ?A; -propositional_truncation a f = f a; +%% FIXME: The below definition makes the importation of this module fail! +%% Field type (ℓ : ##TypeLevel +%% => (ℓ : ##TypeLevel +%% ≡> (A : (##Type_ ℓ) +%% -> (##Type_ +%% (##TypeLevel.∪ (##TypeLevel.succ ℓ) +%% (##TypeLevel.∪ ℓ ℓ)))))) is not a Type! (##Type_ω) +%% Propositional_truncation A = (P : ?) ≡> HoTT_isProp P ≡> (A -> P) -> P; +%% propositional_truncation : ?A -> Propositional_truncation ?A; +%% propositional_truncation a f = f a; ===================================== 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" +ℤ = Quotient NatPair equalZ; + +%% +%% Quotient.eq +%% +%% Proof that quotiented elements are equal when +%% the base elements themselves are related in +%% the underlying type. +𝟙-𝟘 : ℤ; +𝟙-𝟘 = Quotient_in (pair (succ zero) zero); + +𝟚-𝟙 : ℤ; +𝟚-𝟙 = Quotient_in (pair (succ (succ zero)) (succ zero)); + +𝟙=𝟙 : Eq 𝟙-𝟘 𝟚-𝟙; +𝟙=𝟙 = 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 : ℤ -> Int; +Z_To_Int q = Quotient_rec (R := equalZ) NatPairToInt (p := NatPairToIntCompat) q; + +neg2_Z : ℤ; +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' : ℤ -> 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'' : ℤ -> 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 ℤ ≃ Int ===================================== samples/quotient_lib.typer ===================================== @@ -0,0 +1,194 @@ +%%%%% Prelude %%%%%% + +HoTT_lib = load "samples/hott.typer"; + +Eq_funext = HoTT_lib.Eq_funext; + +HoTT_isProp = HoTT_lib.HoTT_isProp; + +HoTT_isSet = HoTT_lib.HoTT_isSet; + +HoTT_isContr = HoTT_lib.HoTT_isContr; +isContr = HoTT_lib.isContr; + +%%%%% Prelude END %%%%%% + +%% This function constructs the lid of this square: +%% +%% x y +%% -------------- +%% | | +%% | | +%% | | p +%% | | +%% | | +%% -------------- +%% x l transp_x +%% +%% We first produce a path that corresponds to the base of this square (named `l` +%% in the code). Then by doing what we would normally do to 'concatenate' `l` and +%% `p`, i.e. the same way we traditionally prove transitivity, we obtain the lid +%% of this square. +toPathOver : (A : I ≡> Type_ ?) ≡> (x : A (_ := i0)) => (y : A (_ := i1)) => + %% Proof that transporting `x` from `A i0` to `A i1` + %% is equal to `y` + Eq (Eq_cast (p := Eq_eq (f := A)) + (f := id) x) y -> + Heq x y; +toPathOver = lambda _ A ≡> lambda x y => lambda p -> + %% We want a function that will return `x` when passed `i0` + %% and `y` when passed `i1`. + let + l : Heq x (Eq_cast (p := Eq_eq (f := A)) (f := id) x); + %% Making use of the funny definition of `transp`! + l = Heq_eq (t := A) + (f := lambda i ≡> + I_transp (A := (lambda j ≡> A (_ := I_meet i j))) + (r := I_not i) x); + in + Eq_cast + (x := (Eq_cast (p := Eq_eq (f := A)) (f := id) x)) + (y := y) + (p := p) (f := lambda y' -> Heq x y') l; + +elimProp : (A : Type_ ?) ≡> + (R : A -> A -> Type_ ?) ≡> + (P : Quotient A R -> Type_ ?) ≡> + (prop : (x : Quotient A R) -> HoTT_isProp (P x)) -> + (f : (x : A) -> P (Quotient_in x)) -> + (x : Quotient A R) -> P x; +elimProp = lambda _ _ _ A R P ≡> lambda prop f -> + Quotient_elim + (R := R) (P := P) f + (p := lambda a a' r -> + %% Want to return f a = f a' + let + a=a' : Eq (t := Quotient A R) (Quotient_in a) (Quotient_in a'); + a=a' = Quotient_eq (R := R) (a := a) (a' := a') r; + fa=fa' : Heq (f a) (f a'); + fa=fa' = toPathOver + (A := lambda i ≡> P (Eq_uneq (p := a=a') (i := i))) + (prop (Quotient_in a') + (Eq_cast (p := a=a') (f := P) (f a)) + (f a')); + in + fa=fa'); + +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_rec (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_rec (R := R) + (lambda _ -> a) + (p := lambda a a' r -> Eq_refl) + x; + +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_rec (R := R) + (lambda a -> lambda b -> + Quotient_rec (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; + p : (x : Quotient B S) -> + HoTT_isProp (Eq (Quotient_rec (R := S) (f a) (p := feqr a) x) + (Quotient_rec (R := S) (f a') (p := feqr a') x)); + p x = C_isSet (Quotient_rec (R := S) (f a) (p := feqr a) x) + (Quotient_rec (R := S) (f a') (p := feqr a') x); + compat : (x : Quotient B S) -> + (Eq (Quotient_rec (R := S) (f a) (p := feqr a) x) + (Quotient_rec (R := S) (f a') (p := feqr a') x)); + compat x = elimProp (R := S) + (P := lambda x -> + (Eq (Quotient_rec (R := S) (f a) (p := feqr a) x) + (Quotient_rec (R := S) (f a') (p := feqr a') x))) + p eqf x; + in + Eq_funext (f := Quotient_rec (R := S) (f a) (p := feqr a)) + (g := Quotient_rec (R := S) (f a') (p := feqr a')) + compat); + +%% Model propositional truncation using a quotient type! +%% We are essentially defining a relation where every element +%% of P is related to every other element of P. +%% FIXME: Unification errors occur when we make this universe polymorphic!? +PropTrunc : (P : Type) -> Type; +PropTrunc P = Quotient P (lambda p1 p2 -> Unit); + +%% FIXME: Hmm I think we won't be able to do this unless equality +%% between `Quotient`s is a `Prop` +%% squash : (x : PropTrunc ?P) -> (y : PropTrunc ?P) -> Eq x y; +%% squash x y = ?; + +%% Lemma 6.10.2 in HoTT book, to prove this we need to +%% apply propositional truncation on SurjectiveQuotientProof. +%% FIXME: Why is the unification of the levels not working? +%% type SurjectiveQuotientProof (l1 ::: TypeLevel) +%% (l2 ::: TypeLevel) +%% (A : Type_ l1) (R : A -> A -> Type_ l2) +%% (x : Quotient A R) : Type_ ? +%% | surjectiveQuotientProof (a : A) (Eq (Quotient_in (R := R) a) x); + +SurjectiveQuotientProof = typecons (SurjectiveQuotientProof (l1 ::: TypeLevel) + (l2 ::: TypeLevel) + (A : Type_ l1) + (R : A -> A -> Type_ l2) + (x : Quotient A R)) + (surjectiveQuotientProof (a : A) (Eq (Quotient_in (R := R) a) x)); +surjectiveQuotientProof = datacons SurjectiveQuotientProof surjectiveQuotientProof; + +%% FIXME: This should be made universe polymorphic, but this is contingent upon the +%% truncation type itself being polymorphic. We need to implement `squash` to complete +%% this proof. +%% Quotient_in_surjective : (A : Type) -> (R : A -> A -> Type) -> (x : Quotient A R) +%% -> PropTrunc (SurjectiveQuotientProof A R x); +%% Quotient_in_surjective = ? + +%% 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_rec (R := R) + (lambda a -> Quotient_in (op a)) + (p := opPreservesQuotient) + x; ===================================== src/builtin.ml ===================================== @@ -145,7 +145,7 @@ let register_builtin_csts () = OL.add_builtin_cst "Integer" DB.type_integer; OL.add_builtin_cst "Float" DB.type_float; OL.add_builtin_cst "String" DB.type_string; - OL.add_builtin_cst "Eq" DB.type_eq; + OL.add_builtin_cst "Heq" DB.type_heq; OL.add_builtin_cst "I" DB.type_interval let _ = register_builtin_csts () ===================================== src/debruijn.ml ===================================== @@ -130,24 +130,32 @@ let type_string = mkBuiltin ((dloc, "String"), type0) (* FIXME: This definition of `Eq` should preferably be in `builtins.typer`, * but we need `type_eq` when to hande `Case` expressions in * elab/conv_p/check! :-( *) -let type_eq_type = +let type_heq_type = let lv = (dsinfo, Some "l") in - let tv = (dsinfo, Some "t") in + let tv1 = (dsinfo, Some "t1") in + let tv2 = (dsinfo, Some "t2") in mkArrow (dsinfo, Aerasable, lv, type_level, - mkArrow (dsinfo, Aerasable, tv, + mkArrow (dsinfo, Aerasable, tv1, mkSort (dsinfo, Stype (mkVar (lv, 0))), - mkArrow (dsinfo, Anormal, (dsinfo, None), - mkVar (tv, 0), - mkArrow (dsinfo, Anormal, (dsinfo, None), - mkVar (tv, 1), - mkSort (dsinfo, Stype (mkVar (lv, 3))))))) -let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) + mkArrow (dsinfo, Aerasable, tv2, + mkSort (dsinfo, Stype (mkVar (lv, 1))), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv1, 1), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv2, 1), + mkSort (dsinfo, + Stype (mkVar (lv, 4)))))))) + +let type_heq = mkBuiltin ((dloc, "Heq"), type_heq_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"] + "Heap"; "DataconsLabel"; + (* Integer axioms *) + "Integer.1!=0"; "Integer.+-comm"; "Integer.*-comm"; "Integer.*-assoc"; + "Integer.*DistL+"; "Integer.isIntegral"] (* FIXME: Is this the best way to do this? Originally, I wanted to * define this in Typer and then reference it from OCaml code. ===================================== src/elab.ml ===================================== @@ -868,9 +868,9 @@ and unify_or_error lctx lxp ?lxp_name expect actual = | ((ck, _ctx, t1, t2)::_) -> lexp_error (Lexp.location lxp) lxp - ({|Type mismatch%s! Context expected:\n%s|} - ^^ {|\nbut %s has type:\n %s\n|} - ^^ {|can't unify:\n %s\nwith:\n %s|}) + ("Type mismatch%s! Context expected:\n%s" + ^^ "\nbut %s has type:\n %s\n" + ^^ "can't unify:\n %s\nwith:\n %s") (match ck with | Unif.CKimpossible -> "" | Unif.CKresidual -> " (residue)") @@ -979,8 +979,9 @@ and check_case rtype (loc, target, ppatterns) ctx = let tlxp' = shift_to_extended_ctx nctx tlxp in let tltp' = shift_to_extended_ctx nctx tltp in let tlvl' = shift_to_extended_ctx nctx tlvl in - let eqty = mkCall (loc, DB.type_eq, + let eqty = mkCall (loc, DB.type_heq, [(Aerasable, tlvl'); (* Typelevel *) + (Aerasable, tltp'); (* Inductive type *) (Aerasable, tltp'); (* Inductive type *) (Anormal, head_lexp); (* Lexp of the branch head *) (Anormal, tlxp')]) (* Target lexp *) ===================================== src/env.ml ===================================== @@ -178,13 +178,19 @@ let value_string_with_type v ltype ctx = let e' = OL.lexp_whnf e ctx in (match args with (* Pretty print identity types *) - | [_l; (_, t); (_, left); (_, right)] - when OL.conv_builtin_p ctx e' "Eq" + | [_l; (_, t); (_, _t2); (_, left); (_, right)] + when OL.conv_builtin_p ctx e' "Heq" -> sprintf "%s = %s [ %s ]" + (* TODO: Print something different when t1 != t2? *) (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 ===================================== @@ -766,9 +766,9 @@ let y_operator loc _depth args = let arity0_fun loc _ _ = error loc "Called a 0-arity function!?" -let eq_uneq loc _ vs = match vs with +let heq_uneq loc _ vs = match vs with | [x; _y] -> x - | _ -> error loc "Eq_uneq takes 2 arguments" + | _ -> error loc "Heq_uneq takes 2 arguments" let nop_fun loc _ vs = match vs with | [v] -> v @@ -1027,6 +1027,46 @@ 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_type loc _ args = + match args with + | [_; _] -> Vundefined + | _ -> error loc "Quotient expects 2 arguments" + +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 quotient_trunc loc _ args = + match args with + | [_; _] -> Vundefined + | _ -> error loc "Quotient.trunc expects 1 argument" + +let interval_meet loc _ args = + match args with + | [Vcons (sym1, _) as x; Vcons (sym2, _) as y] -> + (match (Sym.name sym1, Sym.name sym2) with + | "i0", _ -> x + | "i1", _ -> y + | _ -> error loc "Unexpected arguments passed to I.meet") + | _ -> error loc "I.meet expects 2 arguments" + +let interval_not loc _ args = + match args with + | [Vcons (sym, _)] -> + (match Sym.name sym with + | "i0" -> Vcons ((dloc, "i1"), []) + | "i1" -> Vcons ((dloc, "i0"), []) + | _ -> error loc "Unexpected argument passed to I.not") + | _ -> error loc "I.not expects 1 argument" + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -1055,9 +1095,9 @@ let register_builtin_functions () = ("File.open" , file_open, 2); ("File.read" , file_read, 2); ("File.write" , file_write, 2); - ("Eq.cast" , nop_fun, 1); - ("Eq.eq" , arity0_fun, 0); - ("Eq.uneq" , eq_uneq, 2); + ("Heq.cast" , nop_fun, 1); + ("Heq.eq" , arity0_fun, 0); + ("Heq.uneq" , heq_uneq, 2); ("Y" , y_operator, 1); ("Ref.make" , ref_make, 1); ("Ref.read" , ref_read, 1); @@ -1084,6 +1124,14 @@ let register_builtin_functions () = ("Test.false" , test_false,2); ("Test.eq" , test_eq,3); ("Test.neq" , test_neq,3); + ("Quotient" , quotient_type, 2); + ("Quotient.in" , nop_fun, 1); + ("Quotient.eq" , quotient_eq, 1); + ("Quotient.trunc", quotient_trunc, 2); + ("Quotient.elim" , quotient_elim, 2); + ("I.transp" , nop_fun, 1); + ("I.meet" , interval_meet, 2); + ("I.not" , interval_not, 1); ] let _ = register_builtin_functions () ===================================== src/lexp.ml ===================================== @@ -347,8 +347,8 @@ let mkSLlub' (e1, e2) = | (SortLevel SLz, SortLevel l) | (SortLevel l, SortLevel SLz) -> l | (SortLevel SLz, e) | (e, SortLevel SLz) -> Log.log_fatal ~section:"internal" "lub of SLz with %S" (lexp_head (hc e)) - | (SortLevel (SLsucc _), SortLevel (SLsucc _)) - -> Log.log_fatal ~section:"internal" "lub of two SLsucc" + | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) + -> SLsucc (mkSortLevel (SLlub (e1, e2))) | ((SortLevel _ | Var _ | Metavar _ | Susp _), (SortLevel _ | Var _ | Metavar _ | Susp _)) -> SLlub (e1, e2) ===================================== src/opslexp.ml ===================================== @@ -300,16 +300,7 @@ and conv_builtin_p ctx e name = | Builtin ((_, name'), _) -> name = name' | _ -> false -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" - -> Some (fx, rest) - | _ -> None) - | _ -> None - -and eq_uneq_whnf ctx args = +and heq_uneq_whnf ctx args = match args with | _l :: _t :: (_, x) :: (_, y) :: _p :: (_, i) :: rest -> if conv_p ctx i DB.interval_i0 @@ -319,12 +310,72 @@ and eq_uneq_whnf ctx args = else None | _ -> None +and interval_transp_whnf _ctx args = + match args with + | _l :: _a :: _r :: (_, a_i0) :: rest + -> Some (a_i0, rest) + | _ -> None + +and interval_meet_whnf ctx args = + match args with + | (_, x) :: (_, y) :: rest + -> + (* i0 ∧ x = i0 *) + if conv_p ctx x DB.interval_i0 + then Some (DB.interval_i0, rest) + (* i1 ∧ y = y *) + else if conv_p ctx x DB.interval_i1 + then Some (y, rest) + (* y ∧ i0 = i0 *) + else if conv_p ctx y DB.interval_i0 + then Some (DB.interval_i0, rest) + (* x ∧ i1 = x *) + else if conv_p ctx y DB.interval_i1 + then Some (x, rest) + (* x ∧ x = x *) + else if conv_p ctx x y + then Some(x, rest) + else None + | _ -> None + +and interval_not_whnf ctx args = + match args with + | (_, x) :: rest + -> + (* ~ i0 ≡ i1 *) + if conv_p ctx x DB.interval_i0 + then Some (DB.interval_i1, rest) + (* ~ i1 ≡ i0 *) + else if conv_p ctx x DB.interval_i1 + then Some (DB.interval_i0, rest) + else + (* ~ (~ i) ≡ i*) + (match lexp'_whnf x ctx with + | Call (_, fn, [_, y]) + when conv_builtin_p ctx fn "I.not" + -> Some (y, rest) + | _ -> None) + | _ -> None + +and quotient_elim_whnf ctx args = + match args with + | _l1 :: _l2 :: _l3 :: _A :: _R :: _P :: (_, f) :: (_, _p) :: (_, q) :: rest + -> (match lexp'_whnf q ctx with + | Call (_, qin, [_; _; _; _; (_, e)]) + when conv_builtin_p ctx qin "Quotient.in" + -> Some (mkCall (dsinfo, f, [Anormal, e]), rest) + | _ -> None) + | _ -> None + and register_reducible_builtins () = reducible_builtins := List.fold_right (fun (n, f) m -> SMap.add n f m) [ - ("Eq.cast", eq_cast_whnf); - ("Eq.uneq", eq_uneq_whnf) + ("Heq.uneq", heq_uneq_whnf); + ("I.transp", interval_transp_whnf); + ("I.meet", interval_meet_whnf); + ("I.not", interval_not_whnf); + ("Quotient.elim", quotient_elim_whnf) ] !reducible_builtins (** A very naive implementation of sets of pairs of lexps. *) @@ -484,8 +535,9 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let tlxp = mkSusp target subst in let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in - let eqty = mkCall (dsinfo, DB.type_eq, + let eqty = mkCall (dsinfo, DB.type_heq, [(Pexp.Aerasable, tlvl); (* Typelevel *) + (Pexp.Aerasable, tltp); (* Inductive type *) (Pexp.Aerasable, tltp); (* Inductive type *) (Pexp.Anormal, hlxp); (* Lexp of the branch head *) (Pexp.Anormal, tlxp)]) in (* Target lexp *) @@ -559,12 +611,12 @@ and mk_eq_witness sinfo e ctx = let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in - (* FIXME: Doesn't `e` need a "shift" here? *) - let fn = mkLambda (Pexp.Aerasable, (sinfo, None), etype, e) in - mkCall (sinfo, get_builtin "Eq.eq", - [Pexp.Aerasable, elevel; - Pexp.Aerasable, etype; - Pexp.Anormal, fn]) + let t = mkLambda (Pexp.Aerasable, (dsinfo, None), DB.type_interval, etype) in + let fn = mkLambda (Pexp.Aerasable, (dsinfo, None), DB.type_interval, e) in + mkCall (sinfo, get_builtin "Heq.eq", + [Pexp.Aerasable, elevel; + Pexp.Aerasable, t; + Pexp.Anormal, fn]) (********* Testing if a lexp is properly typed *********) @@ -907,8 +959,9 @@ and check'' erased ctx e = let tlxp = mkSusp e subst in let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in - let eqty = mkCall (l, DB.type_eq, + let eqty = mkCall (l, DB.type_heq, [(Pexp.Aerasable, tlvl); (* Typelevel *) + (Pexp.Aerasable, tltp); (* Inductive type *) (Pexp.Aerasable, tltp); (* Inductive type *) (Pexp.Anormal, hlxp); (* Lexp of the branch head *) (Pexp.Anormal, tlxp)]) in (* Target lexp *) ===================================== src/unification.ml ===================================== @@ -249,13 +249,11 @@ and unify' (e1: lexp) (e2: lexp) might become redexes; 3. Case expressions, for the same reason. *) - (* FIXME: Does the order of these branches matter? If we can place - the Lambda branches above the Var branches, we can avoid - having to explicitly name the Lambda * Var pair for the - η expansion of Lambdas. *) - | (Lambda _, Var _) -> unify_lambda msl e1' e2' ctx vs' + (* Do lambdas first in case eta expansion helps unification. *) + | (Lambda _, _) -> unify_lambda msl e1' e2' ctx vs' + | (_, Lambda _) -> unify_lambda msl e2' e1' ctx vs' + | (_, Var _) -> unify_var e2' e1' ctx - | (Var _, Lambda _) -> unify_lambda msl e2' e1' ctx vs' | (Var _, _) -> unify_var e1' e2' ctx | (_, Call _) -> unify_call msl e2' e1' ctx vs' | (Call _, _) -> unify_call msl e1' e2' ctx vs' @@ -266,8 +264,6 @@ and unify' (e1: lexp) (e2: lexp) constraints. *) | (_, Arrow _) -> unify_arrow msl e2' e1' ctx vs' | (Arrow _, _) -> unify_arrow msl e1' e2' ctx vs' - | (_, Lambda _) -> unify_lambda msl e2' e1' ctx vs' - | (Lambda _, _) -> unify_lambda msl e1' e2' ctx vs' | (_, Sort _) -> unify_sort msl e2' e1' ctx vs' | (Sort _, _) -> unify_sort msl e1' e2' ctx vs' | (_, SortLevel _) -> unify_sortlvl msl e2' e1' ctx vs' @@ -561,6 +557,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 ===================================== @@ -154,7 +154,7 @@ unify = lambda sxps -> do {vname <- gensym (); IO_return - (quote ((uquote vname) : (uquote (Sexp_node (Sexp_symbol "##Eq") sxps)); + (quote ((uquote vname) : (uquote (Sexp_node (Sexp_symbol "Eq") sxps)); (uquote vname) = Eq_refl; )); }); @@ -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" {| ===================================== tests/env_test.ml ===================================== @@ -73,9 +73,10 @@ let _ = (add_test "ENV" "Value Printer" (fun () -> (mkArrow (dsinfo, Aerasable, (dsinfo, Some "l"), DB.type_interval, DB.type_integer)), "(lambda _ ≡> 42)"); - ((Vbuiltin "Eq.eq"), - (mkCall (dsinfo, DB.type_eq, + ((Vbuiltin "Heq.eq"), + (mkCall (dsinfo, DB.type_heq, [Aerasable, mkVar ((dsinfo, None), 2); + Aerasable, DB.type_integer; Aerasable, DB.type_integer; Anormal, mkVar ((dsinfo, Some "x"), 0); Anormal, mkVar ((dsinfo, Some "y"), 0)])), ===================================== tests/eval_test.ml ===================================== @@ -493,7 +493,7 @@ implicitly = ?; exfalso (f : False) = ##case_ f; Not p = (contra : p) ≡> False; -typeclass Eq; +typeclass Heq; head : (ls : List ?τ) -> (p : Not (Eq nil ls)) -> ?τ; head ls p = @@ -513,7 +513,7 @@ Eq_unerase = Eq_cast (p := p) (f := Eq x) Eq_refl; exfalso (f : False) = ##case_ f; Not p = (contra : p) ≡> False; -typeclass Eq; +typeclass Heq; f : (b : Bool) -> (p : Not (Eq false b)) -> Eq true b; f b p = ===================================== tests/instargs_test.ml ===================================== @@ -53,6 +53,7 @@ eq : Eq a (1 : Int); eq = Eq_refl; typeclass Eq; +typeclass Heq; |} in let ctx = snd (E.eval_decl_str vars_str default_ectx default_rctx) in (List.map (fun (tstr, b) -> @@ -61,8 +62,25 @@ typeclass Eq; expect_equal_bool (I.is_typeclass ctx t) b ) ) [ + (* FIXME: In the case of `decltype a` + Head of Eq is (lambda (<anon> : TypeLevel) ≡> + (lambda (<anon> : (##Type_ <anon>)) ≡> + (lambda (x : <anon>) -> + (lambda (y : <anon>) -> + (Heq <anon> <anon> <anon> x y))))) + + BUT! + + Head of (Eq ##TypeLevel.z ##Int (a ##Int IntFromInteger) + (fromInteger ##Int IntFromInteger 1)) is Heq + + Temporary solution is to make both `Heq` AND `Eq` typeclasses. + In practice, this should be fine, i.e. when an Eq proof + needs to be found, the fact that Heq is a typeclass makes + it findable. *) ("Int", false); ("Eq", true); + ("Heq", true); ("decltype a", false); ("decltype eq", true); ]) View it on GitLab: https://gitlab.com/monnier/typer/-/compare/218b2e7183963adffad99d8515b7b479… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/218b2e7183963adffad99d8515b7b479… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch quot-types/rational
by James Tan Juan Whei (＠jamestjw) 02 Aug '23

02 Aug '23

James Tan Juan Whei pushed new branch quot-types/rational at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/quot-types/rational You're receiving this email because of your account on gitlab.com.

1 0