What's the "Hello, World!" for proof assistants?

Question

Many programming language tutorials start with a simple program which just outputs "Hello, World!" to the console or another output. For the various proof assistants, is there some widely-known equivalent for this? Maybe a simple proof by induction?

Answer 1

The proof of commutativity for addition of natural numbers has been used as a simple pedagogical example in some places, including the Wikipedia page for Coq. It is a bit longer than just "Hello World" but it is an example that is about as simple as one can imagine for a proof, while still remaining non-trivial. This is what the proof term (quoted from the Wikipedia page) would look like for Coq:

plus_comm =
fun n m : nat =>
nat_ind (fun n0 : nat => n0 + m = m + n0)
  (plus_n_0 m)
  (fun (y : nat) (H : y + m = m + y) =>
   eq_ind (S (m + y))
     (fun n0 : nat => S (y + m) = n0)
     (f_equal S H)
     (m + S y)
     (plus_n_Sm m y)) n
     : forall n m : nat, n + m = m + n

However, Coq users rarely write such proof terms directly. Rather, they prove theorems with tactics. Here is a tactic-based proof of the same theorem (leading to a slightly different proof term):

Lemma plus_comm : forall n m, n + m = m + n.
  intros; induction n.
  - simpl.
    symmetry.
    apply Nat.add_0_r.
  - simpl.
    rewrite Nat.add_succ_r.
    f_equal.
    apply IHn.
Qed.

Answer 2

These might be somewhat advanced for an honest "Hello, world!" but I think that the irrationality of $\sqrt 2$ and the infinitude of primes are two very common get-the-feet-wet projects for people looking at the mathematical side of proof assistants.

The infinitude of primes in different languages:

• Agda
• Coq
• Lean
• Metamath

Answer 3

1. Defining lists, usually:

list A := Nil | Cons of A * list A

2. Defining append for lists:

append Nil ys := ys
append (Cons x xs) ys := Cons x (append xs ys)

3. Showing that append is associative, usually:

**left as an exercise**

Of course this would look different for a proof assistant which is not based on inductive types.

Answer 4

Another example could be the definition of natural numbers (for type-theoretic assistants):

inductive nat : Type
| zero : nat
| succ : nat → nat

This also shows off the induction principle for naturals being automatically generated, which can be quite surprising.

Answer 5

A "Hello, World!" of proof assistants should be available in as many languages as possible. As pointed out by Clément in his answer to a different question, there are around twenty provably-correct implementations of the "leftpad" function at the lets-prove-leftpad repository. Quoting from that repository:

Leftpad is a function that takes a character, a length, and a string, and pads the string to that length. It pads it by adding the character to the left. So it's adding padding on the left. Leftpad.

>> leftpad('!', 5, "foo")
!!foo
>> leftpad('!', 0, "foo")
foo

This is more relevant if you are interested in software verification than mathematical proofs, as it has a rather different flavours than the examples of natural numbers or lists that showcase the use of inductive types.

Answer 6

Many proof assistants based on an intensional type theory equipped with inductive types may choose the commutativity (or simpler, associativity) of addition as the "Hello world".

This shows two important things:

• The proof assistant is able to recognize the natural numbers as a legitimate definition, and to generate the appropriate induction/recursion principle for it.
• The proof assistant is able to handle equality and quantifiers. This shows that it has basic functionalities in logic and reasoning, without which it may no longer be regarded as a proof assistant.

However it is also a little bit away from the "day-to-day math". But considering that a "Hello world" program is also quite far from industrial programs, it's totally acceptable.

Answer 7

Proving some elementary results on propositions but using the language of types could be a good option for languages where that makes sense, since it makes clear some of the motivation behind the "propositions as types" paradigm. Here are what two of these results could look like in Agda:

data ∅ : Set where
    
double-negation : {P : Set} → P → ((P → ∅) → ∅)
double-negation p f = f p

triple-negation : {P : Set} → (((P → ∅) → ∅) → ∅) → (P → ∅)
triple-negation f p = f λ g → g p

Beginners could also ponder about how to simplify the proof of the second result using the first.

Answer 8

For a "Hello World" for proof assistants I personally use the fact that reversing a list is an involution:

theorem rev_rev {l : List α} : l.reverse.reverse = l

Usually, the proof showcases induction, using lemmas (manually or automatically), rewriting and working with equality. The equality might not be that straightforward in, say, cubical provers.

Answer 9

Most answers seem to be metaphorical, but a literal answer also seems warranted as many proof assistants are programming languages too. In Lean:

def main : IO Unit := IO.println "Hello, world!"