Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Août 2023
- 3 participants
- 6 discussions
[Git][monnier/typer][quotient-types] 7 commits: Implement `Quotient` formation
by James Tan Juan Whei (@jamestjw) 24 Aoû '23
by James Tan Juan Whei (@jamestjw) 24 Aoû '23
24 Aoû '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 Aoû '23
by Stefan (@monnier) 24 Aoû '23
24 Aoû '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
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) 04 Aoû '23
by James Tan Juan Whei (@jamestjw) 04 Aoû '23
04 Aoû '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) 03 Aoû '23
by James Tan Juan Whei (@jamestjw) 03 Aoû '23
03 Aoû '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 Aoû '23
by James Tan Juan Whei (@jamestjw) 02 Aoû '23
02 Aoû '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