A super brief introduction to Coq.

introduction.v

(* Welcome!
   This super brief tutorial will demonstrate a few basics ideas of what you
   can do with Coq and will point you to further documentation to learn more
   about it. *)

(* Anything between (* and *) is a comment. Comments can be nested. *)

(* Coq has a standard library and a small part of it is already loaded when
   you launch it. This part is called the prelude. It defines many very basic
   and useful construct, such as logic connectors, the natural numbers, etc. *)

(* You can ask Coq to print the type of a term with the Check command.
   Your IDE may also have a menu or a keyboard shortcurt for this operation. *)

(* For instance, 0 is a natural number. Evaluate your buffer until this point
   to have Coq print this information. (In CoqIDE, use the arrows in the tool
   bar. *)

Check 0.

(* You can compute with Coq. *)

Compute 1 + 1.

(* You can define new constants. *)

Definition my_sum := 1 + 1.

Print my_sum.

Compute my_sum.

(* You can define functions. *)

Definition add_two x := 2 + x.

Compute add_two my_sum.

(* The standard library also includes modules that you have to import
   explicitely. *)

Require List. (* Allow calling stuff in module List. *)
Import List.ListNotations. (* Load notations defined in specific sub-module. *)

(* You can define recursive functions. *)

Fixpoint length_nat_list (l : list nat) : nat :=
  match l with
  | nil => 0
  | cons _ l => 1 + length_nat_list l
  end.

(* You can define polymorphic functions. *)

Fixpoint length_poly_list {A : Type} (l : list A) : nat :=
  match l with
  | nil => 0
  | cons _ l => 1 + length_poly_list l
  end.

(* There are restrictions on the kind of recursive functions you can define
   because Coq must be able to see that they terminate. *)

Fail Fixpoint termination_not_obvious (n : nat) :=
  match n with
  | 0 => termination_not_obvious 1
  | _ => 0
  end.

(* You can state and prove theorems. *)

Lemma length_app :
  forall (A : Type) (l l' : list A),
    length_poly_list (l ++ l')%list = length_poly_list l + length_poly_list l'.
Proof.

  (* The proofs are built from tactics, which are macros that allow the user
     to progress in the proof and build a certificate at the same time.
     You may execute the proof step by step to see the evolution of what
     needs to be proved.
   *)

  intros A.
  induction l.

  (* This last tactic created two sub-goals that we are now going to prove
     one after the other. *)

  - reflexivity.

    (* This last tactic terminated the current sub-goal. *)

  - intros.
    simpl.
    f_equal.
    easy.

    (* This last tactic terminated the second and last sub-goal. The proof is
       over. You may display the certificate, but it's not very readable. *)

    Show Proof.

(* We are now going to save the proof and have it checked by Coq's proof
   checker. So far, the certificate has not been checked. The tactics are
   not guaranteed to be free of bugs but it's not necessary to trust them
   because the proof certificate is verified in the end. *)

Qed.

(* This introduction was just to give you a brief view, but there are many
   more things that you can do and have not been shown. To learn more, you
   will have to read a tutorial. *)

(* Several long tutorials (textbooks) are available:
   - the Coq'Art (Y.Bertot and P. Castéran)...
   - Software Foundations (B. Pierce et al)...
   - Certified Programming with Dependent Types (A. Chlipala) ...
   - Mathematical Components (A. Mahboubi and E. Tassi)...

  Several short tutorials are also available:
  - An interactive tutorial in a single Coq file (M. Nahas)...
  - Coq in a Hurry (Y. Bertot)...

  A more up-to-date list may be found at ... *)

(* There is also a reference manual at https://coq.inria.fr/refman/ and
   a documentation of the standard library at https://coq.inria.fr/stdlib/. *)

(* Other useful ressources are... *)

(l ++ l')%list

Is the %list needed here?

Please, intros x xs IHxs then simpl and then rewrite IHxs (hiding the application of the induction hypothesis is the first proof one does is not good IMO).

Maybe a banner "if you are not familiar with functional programming ,skip to the end"

And hence, I'd suggest skipping the monomorphic list example, let's assume you know caml/haskell

Termination is also a bit too much IMO, as well as show proof.

my2c

@Zimmi48: I like your micro-tutorial very very much. A few comments:

• Check 0 is still issuing a warning in CoqIDE, I'm in favor to remove this warning. It is so often that we want to write it. It is faster to write than using a menu; it is not faster than using the Check key binding, but to use the Check key binding, you need to type the expression you want to Check anyway, so, at the end, it is as easy to type the 5 letters of Check. If I get support for removing it, I can do it.
• I agree with @gares, the non-terminating example is too technical for this tuto-teaser.
• %listis indeed not needed; maybe tell in the comment above that ++ is concatenation of lists though.
• Show Proof: if it is to tell it is not readable, I agree it can better be removed. If the objective is otherwise to explain that proofs are like program expressions. It can be an interesting teaser inviting the reader to understand in which sense Coq is at the same time a logic and a programming language. So, it could be kept with a comment, say: "Coq exploits the famous proofs-as-programs correspondence and represents proofs in the same language the programs are written. The proof can be visualized with Show Proof (even if a bit difficult to read).". But maybe it is also too much. [In passing: it is actually difficult to read because of the list_ind. If we unfold the list_ind, it is pretty natural and only the complex return clause remains difficult to read.]
• Missing parenthesis after "tool bar".
• I would have a slight preferences towards keeping the two distinct non-polymorphic and polymorphic examples, seeing it as a teaser about the richness of the language.