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/53990bc7a2ae6cde6df5cc093b16582e2...