# Top 3 applications I mostly use

Here’s a list of items I spend most time of, daily (both work and non-work related):

1. Terminal – This should not come as a surprise. vim is my main tool for editing code, and I spend a lot of time on it. I also spend a lot of time using grep when searching for something, or running PHP/Coq/etc from command line to quick test some code. git is also there.
2. Chrome – After I write the code, I need to test it. Using the browser usually involves testing, but also stuff like social media, this blog, or reading something else interesting.
3. Notes – I don’t think about this application that much, but it’s a fact that I spend a lot of time using it (both mobile and desktop). You can write just anything in Notes, but I classify mine mostly to be:
1. TODOs
2. Schedules, appointments
3. Temporary information (what work I’ve done for the week, random thoughts, ideas (e.g. this post))
4. Personal information (card id, pin codes, bike codes)
5. Short Math proofs

There’s my list. What applications do you use on a daily basis? Feel free to put some in the comments section.

# Associativity of Elvis operator

I had written a piece of code in the format a ?: (b ?: c) and I was wondering if I could omit the brackets. That’s right, we need to figure if this operator is associative.

That is, we need to see if we can show that (a ?: b) ?: c = a ?: (b ?: c).

The definition of it is:
a ?: b = a (if a is not empty)
a ?: b = b (otherwise)

So that means we can consider these cases:

1. Suppose a is empty.
Now we are left with b ?: c = b ?: c, which is true by reflexivity.
2. Suppose a is not empty.
Then, (a ?: b) evaluates to a, so we have a ?: c on the LHS, and thus a ?: c = a ?: (b ?: c).

Since a is not empty, and by definition of this operator, we have that a = a, which is true by reflexivity.

Bonus: here’s the same proof in Coq:

(* Definition of data type for empty and value one *)
Inductive value {a : Type} : Type :=
| Value : a -> value
| Empty : value.

(* Definition of Elvis operator *)
Definition elvis {x : Type} (x1 : @value x) (x2 : @value x) : (@value x) :=
match x1 with
| Empty => x2
| Value _ => x1
end.

(* Fancy notation for Elvis operator *)
Notation "x ?: y" := (elvis x y) (at level 50).

Theorem elvis_assoc : forall (X : Type) (x1 : @value X) (x2 : @value X) (x3 : @value X),
x1 ?: (x2 ?: x3) = (x1 ?: x2) ?: x3.
Proof.
intros X x1 x2 x3.
case x1.
- (* x1 is not empty *) simpl. reflexivity.
- (* x1 is empty     *) simpl. reflexivity.
Qed.


Now that both considered cases are true, we’ve shown that ?: is associative and you can skip any brackets in your code 🙂

# Calculus of Constructions

As an additional extension to the hierarchy of logical systems we’ve discussed, we’ll consider type theory. In type theory, every “term” has a “type” and operations are restricted to terms of a certain type.

Type theory was created to avoid paradoxes in a variety of formal logics and rewrite systems. For example, Russell’s paradox is not applicable since every sentence has its own type.

The most powerful concept in Coq is not about Coq; it’s the calculus of constructions. Coq is just a lot of awesome automation machinery on top of that.

Calculus of Constructions is a type theory based on intuitionistic logic and simply typed lambda calculus. Together with Dependent Types, Inductive Types, Recursion, they provide a neat way to do proofs.

To demonstrate why they are powerful, let’s consider one of the inference rules as an example:
${\displaystyle {\Gamma ,x:A\vdash B:K\qquad \qquad \Gamma ,x:A\vdash N:B \over {\Gamma \vdash (\lambda x:A.N):(\forall x:A.B):K}}}$

What this means is that if above the line holds, then so does everything below the line.

In this case, K is either a Prop or a Type. For simplicity, assume K is Type. To translate it, it means that:
1. If we have a judgment x of type A, from which it follows that B : K (B is a Type)
and
2. If we have a judgment x of type A, from which it follows that N : B (N has type of B)
then we can deduce that
(\x : A . N) has type (\forall (x : A) . B), and the term (\forall (x : A) . B) has type Type.

In other words, this is the rule that ties together lambda abstraction and universal quantification. It also says that a universal quantification is a type.

This rule is the reason why this flows nicely:

(* Make sure you have enabled "Display all basic low-level contents" *)
Definition test (s : Set) : bool := true.

Check test.                 (* test : forall _ : Set, bool *)

Check forall _ : Set, bool. (* forall _ : Set, bool : Type *)


Other data types are encoded similarly as with Church Numerals.

The interesting thing about this system is that it has the strong normalization property, which means that every sequence of rewrites eventually terminates.

While this is not useful for IO, it is very useful for proofs.

In any case, we can take advantage of IO by extracting code to other languages as seen in Coq to Haskell.