Merge remote-tracking branch 'upstream/master'

1 files changed, 120 insertions, 88 deletions

diff --git a/coq.html.markdown b/coq.html.markdown
index 115d9ff8..4c1ad690 100644
--- a/coq.html.markdown
+++ b/coq.html.markdown
@@ -25,19 +25,20 @@ Inside Proof General `Ctrl+C Ctrl+<Enter>` will evaluate up to your cursor.
 
 (*** Variables and functions ***)
 
-(* The Coq proof assistant can be controlled and queried by a command language called 
-   the vernacular. Vernacular keywords are capitalized and the commands end with a period.
-   Variable and function declarations are formed with the Definition vernacular. *)
+(* The Coq proof assistant can be controlled and queried by a command
+   language called the vernacular. Vernacular keywords are capitalized and
+   the commands end with a period.  Variable and function declarations are
+   formed with the Definition vernacular. *)
 
 Definition x := 10.
 
-(* Coq can sometimes infer the types of arguments, but it is common practice to annotate
-   with types. *)
+(* Coq can sometimes infer the types of arguments, but it is common practice
+   to annotate with types. *)
 
 Definition inc_nat (x : nat) : nat := x + 1.
 
-(* There exists a large number of vernacular commands for querying information. 
-   These can be very useful. *)
+(* There exists a large number of vernacular commands for querying
+   information.  These can be very useful. *)
 
 Compute (1 + 1). (* 2 : nat *) (* Compute a result. *)
 
@@ -46,48 +47,50 @@ Check tt. (* tt : unit *) (* Check the type of an expressions *)
 About plus. (* Prints information about an object *)
 
 (* Print information including the definition *)
-Print true. (* Inductive bool : Set := true : Bool | false : Bool *)  
+Print true. (* Inductive bool : Set := true : Bool | false : Bool *)
 
 Search nat. (* Returns a large list of nat related values *)
 Search "_ + _". (* You can also search on patterns *)
 Search (?a -> ?a -> bool). (* Patterns can have named parameters  *)
 Search (?a * ?a).
 
-(* Locate tells you where notation is coming from. Very helpful when you encounter
-   new notation. *)
-Locate "+". 
+(* Locate tells you where notation is coming from. Very helpful when you
+   encounter new notation. *)
 
-(* Calling a function with insufficient number of arguments
-   does not cause an error, it produces a new function. *)
+Locate "+".
+
+(* Calling a function with insufficient number of arguments does not cause
+   an error, it produces a new function. *)
 Definition make_inc x y := x + y. (* make_inc is int -> int -> int *)
 Definition inc_2 := make_inc 2.   (* inc_2 is int -> int *)
 Compute inc_2 3. (* Evaluates to 5 *)
 
-(* Definitions can be chained with "let ... in" construct.
-   This is roughly the same to assigning values to multiple
-   variables before using them in expressions in imperative
-   languages. *)
+
+(* Definitions can be chained with "let ... in" construct.  This is roughly
+   the same to assigning values to multiple variables before using them in
+   expressions in imperative languages. *)
+
 Definition add_xy : nat := let x := 10 in
                            let y := 20 in
                            x + y.
 
-
 (* Pattern matching is somewhat similar to switch statement in imperative
    languages, but offers a lot more expressive power. *)
+
 Definition is_zero (x : nat) :=
     match x with
     | 0 => true
     | _ => false  (* The "_" pattern means "anything else". *)
     end.
 
+(* You can define recursive function definition using the Fixpoint
+   vernacular.*)
 
-(* You can define recursive function definition using the Fixpoint vernacular.*)
 Fixpoint factorial n := match n with
                         | 0 => 1
                         | (S n') => n * factorial n'
                         end.
 
-
 (* Function application usually doesn't need parentheses around arguments *)
 Compute factorial 5. (* 120 : nat *)
 
@@ -104,11 +107,12 @@ end with
   | (S n) => is_even n
               end.
 
-(* As Coq is a total programming language, it will only accept programs when it can
-   understand they terminate. It can be most easily seen when the recursive call is
-   on a pattern matched out subpiece of the input, as then the input is always decreasing
-   in size. Getting Coq to understand that functions terminate is not always easy. See the
-   references at the end of the article for more on this topic. *)
+(* As Coq is a total programming language, it will only accept programs when
+   it can understand they terminate. It can be most easily seen when the
+   recursive call is on a pattern matched out subpiece of the input, as then
+   the input is always decreasing in size. Getting Coq to understand that
+   functions terminate is not always easy. See the references at the end of
+   the article for more on this topic. *)
 
 (* Anonymous functions use the following syntax: *)
 
@@ -119,16 +123,18 @@ Definition my_id2 : forall A : Type, A -> A := fun A x => x.
 Compute my_id nat 3. (* 3 : nat *)
 
 (* You can ask Coq to infer terms with an underscore *)
-Compute my_id _ 3. 
+Compute my_id _ 3.
 
-(* An implicit argument of a function is an argument which can be inferred from contextual
-   knowledge. Parameters enclosed in {} are implicit by default *)
+(* An implicit argument of a function is an argument which can be inferred
+   from contextual knowledge. Parameters enclosed in {} are implicit by
+   default *)
 
 Definition my_id3 {A : Type} (x : A) : A := x.
 Compute my_id3 3. (* 3 : nat *)
 
-(* Sometimes it may be necessary to turn this off. You can make all arguments explicit
-   again with @ *)
+(* Sometimes it may be necessary to turn this off. You can make all
+   arguments explicit again with @ *)
+
 Compute @my_id3 nat 3.
 
 (* Or give arguments by name *)
@@ -168,17 +174,19 @@ let rec factorial n = match n with
 
 (*** Notation ***)
 
-(* Coq has a very powerful Notation system that can be used to write expressions in more
-   natural forms. *)
+(* Coq has a very powerful Notation system that can be used to write
+   expressions in more natural forms. *)
+
 Compute Nat.add 3 4. (* 7 : nat *)
 Compute 3 + 4. (* 7 : nat *)
 
-(* Notation is a syntactic transformation applied to the text of the program before being
-   evaluated. Notation is organized into notation scopes. Using different notation scopes
-   allows for a weak notion of overloading. *)
+(* Notation is a syntactic transformation applied to the text of the program
+   before being evaluated. Notation is organized into notation scopes. Using
+   different notation scopes allows for a weak notion of overloading. *)
+
+(* Imports the Zarith module holding definitions related to the integers Z *)
 
-(* Imports the Zarith module containing definitions related to the integers Z *)
-Require Import ZArith. 
+Require Import ZArith.
 
 (* Notation scopes can be opened *)
 Open Scope Z_scope.
@@ -187,7 +195,7 @@ Open Scope Z_scope.
 Compute 1 + 7. (* 8 : Z *)
 
 (* Integer equality checking *)
-Compute 1 =? 2. (* false : bool *) 
+Compute 1 =? 2. (* false : bool *)
 
 (* Locate is useful for finding the origin and definition of notations *)
 Locate "_ =? _". (* Z.eqb x y : Z_scope *)
@@ -199,10 +207,10 @@ Compute 1 + 7. (* 8 : nat *)
 (* Scopes can also be opened inline with the shorthand % *)
 Compute (3 * -7)%Z. (* -21%Z : Z *)
 
-(* Coq declares by default the following interpretation scopes: core_scope, type_scope, 
-   function_scope, nat_scope, bool_scope, list_scope, int_scope, uint_scope. You may also
-   want the numerical scopes Z_scope (integers) and Q_scope (fractions) held in the ZArith
-   and QArith module respectively. *)
+(* Coq declares by default the following interpretation scopes: core_scope,
+   type_scope, function_scope, nat_scope, bool_scope, list_scope, int_scope,
+   uint_scope. You may also want the numerical scopes Z_scope (integers) and
+   Q_scope (fractions) held in the ZArith and QArith module respectively. *)
 
 (* You can print the contents of scopes *)
 Print Scope nat_scope.
@@ -230,17 +238,19 @@ Bound to classes nat Nat.t
 "x * y" := Init.Nat.mul x y
 *)
 
-(* Coq has exact fractions available as the type Q in the QArith module. 
-   Floating point numbers and real numbers are also available but are a more advanced
-   topic, as proving properties about them is rather tricky. *)
+(* Coq has exact fractions available as the type Q in the QArith module.
+   Floating point numbers and real numbers are also available but are a more
+   advanced topic, as proving properties about them is rather tricky. *)
 
 Require Import QArith.
 
 Open Scope Q_scope.
 Compute 1. (* 1 : Q *)
-Compute 2. (* 2 : nat *) (* only 1 and 0 are interpreted as fractions by Q_scope *) 
+
+(* Only 1 and 0 are interpreted as fractions by Q_scope *)
+Compute 2. (* 2 : nat *)
 Compute (2 # 3). (* The fraction 2/3 *)
-Compute (1 # 3) ?= (2 # 6). (* Eq : comparison *) 
+Compute (1 # 3) ?= (2 # 6). (* Eq : comparison *)
 Close Scope Q_scope.
 
 Compute ( (2 # 3) / (1 # 5) )%Q. (* 10 # 3 : Q *)
@@ -279,40 +289,43 @@ Definition my_fst2 {A B : Type} (x : A * B) : A := let (a,b) := x in
 
 (*** Lists ***)
 
-(* Lists are built by using cons and nil or by using notation available in list_scope. *)
+(* Lists are built by using cons and nil or by using notation available in
+   list_scope. *)
 Compute cons 1 (cons 2 (cons 3 nil)). (*  (1 :: 2 :: 3 :: nil)%list : list nat *)
-Compute (1 :: 2 :: 3 :: nil)%list. 
+Compute (1 :: 2 :: 3 :: nil)%list.
 
 (* There is also list notation available in the ListNotations modules *)
 Require Import List.
-Import ListNotations. 
+Import ListNotations.
 Compute [1 ; 2 ; 3]. (* [1; 2; 3] : list nat *)
 
 
-(*
-There are a large number of list manipulation functions available, including:
+(* There is a large number of list manipulation functions available,
+   including:
 
 • length
-• head : first element (with default) 
+• head : first element (with default)
 • tail : all but first element
 • app : appending
 • rev : reverse
 • nth : accessing n-th element (with default)
 • map : applying a function
-• flat_map : applying a function returning lists 
+• flat_map : applying a function returning lists
 • fold_left : iterator (from head to tail)
-• fold_right : iterator (from tail to head) 
+• fold_right : iterator (from tail to head)
 
  *)
 
 Definition my_list : list nat := [47; 18; 34].
 
 Compute List.length my_list. (* 3 : nat *)
+
 (* All functions in coq must be total, so indexing requires a default value *)
-Compute List.nth 1 my_list 0. (* 18 : nat *) 
+Compute List.nth 1 my_list 0. (* 18 : nat *)
 Compute List.map (fun x => x * 2) my_list. (* [94; 36; 68] : list nat *)
-Compute List.filter (fun x => Nat.eqb (Nat.modulo x 2) 0) my_list. (*  [18; 34] : list nat *)
-Compute (my_list ++ my_list)%list. (*  [47; 18; 34; 47; 18; 34] : list nat *)
+Compute List.filter (fun x => Nat.eqb (Nat.modulo x 2) 0) my_list.
+                                               (* [18; 34] : list nat *)
+Compute (my_list ++ my_list)%list. (* [47; 18; 34; 47; 18; 34] : list nat *)
 
 (*** Strings ***)
 
@@ -342,16 +355,19 @@ Close Scope string_scope.
 • PArith : Basic positive integer arithmetic
 • NArith : Basic binary natural number arithmetic
 • ZArith : Basic relative integer arithmetic
-• Numbers : Various approaches to natural, integer and cyclic numbers (currently 
-            axiomatically and on top of 2^31 binary words)
+
+• Numbers : Various approaches to natural, integer and cyclic numbers
+            (currently axiomatically and on top of 2^31 binary words)
 • Bool : Booleans (basic functions and results)
+
 • Lists : Monomorphic and polymorphic lists (basic functions and results),
           Streams (infinite sequences defined with co-inductive types)
 • Sets : Sets (classical, constructive, finite, infinite, power set, etc.)
-• FSets : Specification and implementations of finite sets and finite maps 
+• FSets : Specification and implementations of finite sets and finite maps
           (by lists and by AVL trees)
-• Reals : Axiomatization of real numbers (classical, basic functions, integer part, 
-          fractional part, limit, derivative, Cauchy series, power series and results,...)
+• Reals : Axiomatization of real numbers (classical, basic functions,
+          integer part, fractional part, limit, derivative, Cauchy series,
+          power series and results,...)
 • Relations : Relations (definitions and basic results)
 • Sorting : Sorted list (basic definitions and heapsort correctness)
 • Strings : 8-bits characters and strings
@@ -360,18 +376,20 @@ Close Scope string_scope.
 
 (*** User-defined data types ***)
 
-(* Because Coq is dependently typed, defining type aliases is no different than defining
-   an alias for a value. *)
+(* Because Coq is dependently typed, defining type aliases is no different
+   than defining an alias for a value. *)
 
 Definition my_three : nat := 3.
 Definition my_nat : Type := nat.
 
-(* More interesting types can be defined using the Inductive vernacular. Simple enumeration
-   can be defined like so *)
+(* More interesting types can be defined using the Inductive vernacular.
+   Simple enumeration can be defined like so *)
+
 Inductive ml := OCaml | StandardML | Coq.
 Definition lang := Coq.  (* Has type "ml". *)
 
-(* For more complicated types, you will need to specify the types of the constructors. *)
+(* For more complicated types, you will need to specify the types of the
+   constructors. *)
 
 (* Type constructors don't need to be empty. *)
 Inductive my_number := plus_infinity
@@ -379,23 +397,28 @@ Inductive my_number := plus_infinity
 Compute nat_value 3. (* nat_value 3 : my_number *)
 
 
-(* Record syntax is sugar for tuple-like types. It defines named accessor functions for
-   the components. Record types are defined with the notation {...} *)
+(* Record syntax is sugar for tuple-like types. It defines named accessor
+   functions for the components. Record types are defined with the notation
+   {...} *)
+
 Record Point2d (A : Set) := mkPoint2d { x2 : A ; y2 : A }.
 (* Record values are constructed with the notation {|...|} *)
 Definition mypoint : Point2d nat :=  {| x2 := 2 ; y2 := 3 |}.
 Compute x2 nat mypoint. (* 2 : nat *)
-Compute mypoint.(x2 nat). (* 2 : nat *) 
+Compute mypoint.(x2 nat). (* 2 : nat *)
+
+(* Types can be parameterized, like in this type for "list of lists of
+   anything". 'a can be substituted with any type. *)
 
-(* Types can be parameterized, like in this type for "list of lists
-   of anything". 'a can be substituted with any type. *)
 Definition list_of_lists a := list (list a).
 Definition list_list_nat := list_of_lists nat.
 
 (* Types can also be recursive. Like in this type analogous to
    built-in list of naturals. *)
 
-Inductive my_nat_list := EmptyList | NatList : nat -> my_nat_list -> my_nat_list.
+Inductive my_nat_list :=
+  EmptyList | NatList : nat -> my_nat_list -> my_nat_list.
+
 Compute NatList 1 EmptyList. (*  NatList 1 EmptyList : my_nat_list *)
 
 (** Matching type constructors **)
@@ -427,31 +450,38 @@ Compute sum_list [1; 2; 3]. (* Evaluates to 6 *)
 
 (*** A Taste of Proving ***)
 
-(* Explaining the proof language is out of scope for this tutorial, but here is a taste to
-   whet your appetite. Check the resources below for more. *)
+(* Explaining the proof language is out of scope for this tutorial, but here
+   is a taste to whet your appetite. Check the resources below for more. *)
+
+(* A fascinating feature of dependently type based theorem provers is that
+   the same primitive constructs underly the proof language as the
+   programming features.  For example, we can write and prove the
+   proposition A and B implies A in raw Gallina *)
 
-(* A fascinating feature of dependently type based theorem provers is that the same
-  primitive constructs underly the proof language as the programming features.
-  For example, we can write and prove the proposition A and B implies A in raw Gallina *)
+Definition my_theorem : forall A B, A /\ B -> A :=
+  fun A B ab => match ab with
+                  | (conj a b) => a
+                end.
 
-Definition my_theorem : forall A B, A /\ B -> A := fun A B ab => match ab with
-                                                                 | (conj a b) => a
-                                                                 end.
+(* Or we can prove it using tactics. Tactics are a macro language to help
+   build proof terms in a more natural style and automate away some
+   drudgery. *)
 
-(* Or we can prove it using tactics. Tactics are a macro language to help build proof terms
-   in a more natural style and automate away some drudgery. *)
 Theorem my_theorem2 : forall A B, A /\ B -> A.
 Proof.
   intros A B ab.  destruct ab as [ a b ]. apply a.
 Qed.
 
-(* We can prove easily prove simple polynomial equalities using the automated tactic ring. *)
+(* We can prove easily prove simple polynomial equalities using the
+   automated tactic ring. *)
+
 Require Import Ring.
 Require Import Arith.
 Theorem simple_poly : forall (x : nat), (x + 1) * (x + 2) = x * x + 3 * x + 2.
   Proof. intros. ring. Qed.
 
-(* Here we prove the closed form for the sum of all numbers 1 to n using induction *)
+(* Here we prove the closed form for the sum of all numbers 1 to n using
+   induction *)
 
 Fixpoint sumn (n : nat) : nat :=
   match n with
@@ -465,8 +495,10 @@ Proof. intros n. induction n.
        - simpl. ring [IHn]. (* induction step *)
 Qed.
 ```
-                                
-With this we have only scratched the surface of Coq. It is a massive ecosystem with many interesting and peculiar topics leading all the way up to modern research.
+
+With this we have only scratched the surface of Coq. It is a massive
+ecosystem with many interesting and peculiar topics leading all the way up
+to modern research.
 
 ## Further reading