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...
Afficher les réponses par date