Simon Génier pushed to branch eq-cong-eq-trans at Stefan / Typer Commits: 2a2018c3 by Simon Génier at 2020-09-09T17:07:58-04:00 Add a few logic functions. - - - - - 1 changed file: - btl/pervasive.typer Changes: ===================================== btl/pervasive.typer ===================================== @@ -452,6 +452,10 @@ in List_map mf xs; False = Void; True = Unit; +%% Prove anything from a contradiction. +unvoid : Void -> ?t; +unvoid v = case v; + Not prop = prop -> False; %% Commutativity of equality! @@ -466,6 +470,20 @@ Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) (p := p) Eq_refl; +%% Congruence of equality. You can "inject" a (pure) function on both sides of an +%% equality and it will remain true. +Eq_cong + : (x : ?t) + ≡> (y : ?t) + ≡> (p : Eq x y) + ≡> (f : ?t -> ?r) + -> Eq (f x) (f y); +Eq_cong f = Eq_cast (f := lambda xy -> Eq (f x) (f xy)) (p := p) Eq_refl; + +%% Transitivity of equality. +Eq_trans : (x : ?t) ≡> (y : ?t) ≡> (z : ?t) ≡> Eq x y -> Eq y z -> Eq x z; +Eq_trans p q = Eq_cast (f := lambda yz -> Eq x yz) (p := q) p; + %% Like Bool, except that it additionally carries the meaning of its value. %% We don't use the `type` macro here because it would make these `true` %% and `false` constructors override `Bool`'s, and we currently don't View it on GitLab: https://gitlab.com/monnier/typer/-/commit/2a2018c3a45c0723060ab178cae7b958a0... -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/2a2018c3a45c0723060ab178cae7b958a0... You're receiving this email because of your account on gitlab.com.