44
$\begingroup$

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?

$\endgroup$
3
  • 5
    $\begingroup$ Why not an actual hello world? You can certainly do that with coq, cf. eg. coq-blog.clarus.me/tutorial-a-hello-world-in-coq.html $\endgroup$
    – Clément
    Feb 8, 2022 at 19:21
  • 6
    $\begingroup$ I can write a detailed answer promoting coq.io if you upvote this comment 5 times :-) $\endgroup$ Feb 13, 2022 at 18:55
  • 2
    $\begingroup$ Also I could add as separate answer about building Formal Web Site with Lean 4: lean4.dev on the same contract conditions. Btw lean4.dev has its own package manager bum.pm written also in Lean 4 (before official). Leonardo de Moura gave a like to us, give us yours! :-) $\endgroup$ Feb 13, 2022 at 22:01

9 Answers 9

28
$\begingroup$

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.
$\endgroup$
5
  • 2
    $\begingroup$ Would it be interesting to write a question asking for the proofs of commutativity of the natural numbers in different proof assistants, so one can compare them? $\endgroup$
    – Will Sawin
    Feb 8, 2022 at 18:52
  • 1
    $\begingroup$ @WillSawin That sounds like it could be a useful question, but I would recommend maybe to wait a bit for the site to cool-down a bit. $\endgroup$ Feb 8, 2022 at 18:56
  • $\begingroup$ Thanks for adding this answer. Please consider adding Require Import Coq.Arith.PeanoNat. (or another means of getting Nat in scope (?)) to the top of the proof to make it self-contained. I tried following along in this proof in ProofGeneral and wasn't sure where Nat.add_0_r lived. $\endgroup$ Feb 14, 2022 at 1:57
  • $\begingroup$ @Zimmi48, please see somment by Gregory Nisbet! $\endgroup$ Feb 14, 2022 at 4:55
  • $\begingroup$ Indeed, just Require Import Arith. or what Gregory wrote should work. $\endgroup$
    – Zimm i48
    Feb 14, 2022 at 20:47
19
$\begingroup$

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:

$\endgroup$
1
  • 7
    $\begingroup$ About the proof of the irrationality of the square root of 2: Freek Wiedijk wrote a book about the comparison of the various existing proof assistants (in the year 2007) referring exactly to this theorem. $\endgroup$
    – M. Lonardi
    Feb 10, 2022 at 1:33
17
$\begingroup$
  1. Defining lists, usually:
list A := Nil | Cons of A * list A
  1. Defining append for lists:
append Nil ys := ys
append (Cons x xs) ys := Cons x (append xs ys)
  1. 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.

$\endgroup$
16
$\begingroup$

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.

$\endgroup$
3
  • 4
    $\begingroup$ Maybe this, plus the definition of addition, then 2+2=4... $\endgroup$ Feb 8, 2022 at 20:35
  • $\begingroup$ This is not a proof of a theorem, is it? $\endgroup$
    – mario
    Mar 4, 2022 at 15:17
  • $\begingroup$ this wasn't stated as a requirement in the question, and I guess this proves things like nat.rec $\endgroup$ Mar 4, 2022 at 16:33
14
$\begingroup$

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.

$\endgroup$
10
$\begingroup$

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.

$\endgroup$
10
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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!"
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.