[coq/en] Fix code width

Many lines exceed the 80 character limit that makes the code wrap around
on the website.  This mainly addresses comments. The comment style has
been preserved.  For the code lines that exceeded 80 characters, I have
not adhered to any style.

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 Coq proof assistant can be controlled and queried by a command
-   the vernacular. Vernacular keywords are capitalized and the commands end with a period.
+   language called the vernacular. Vernacular keywords are capitalized and
-   Variable and function declarations are formed with the Definition vernacular. *)
+   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
+(* Coq can sometimes infer the types of arguments, but it is common practice
-   with types. *)
+   to annotate with types. *)
 
 Definition inc_nat (x : nat) : nat := x + 1.
 
-(* There exists a large number of vernacular commands for querying information. 
+(* There exists a large number of vernacular commands for querying
-   These can be very useful. *)
+   information.  These can be very useful. *)
 
 Compute (1 + 1). (* 2 : nat *) (* Compute a result. *)
 
@@ -53,41 +54,43 @@ 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
+(* Locate tells you where notation is coming from. Very helpful when you
-   new notation. *)
+   encounter new notation. *)
+
 Locate "+".
 
-(* Calling a function with insufficient number of arguments
+(* Calling a function with insufficient number of arguments does not cause
-   does not cause an error, it produces a new function. *)
+   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
+(* Definitions can be chained with "let ... in" construct.  This is roughly
-   variables before using them in expressions in imperative
+   the same to assigning values to multiple variables before using them in
-   languages. *)
+   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
+(* As Coq is a total programming language, it will only accept programs when
-   understand they terminate. It can be most easily seen when the recursive call is
+   it can understand they terminate. It can be most easily seen when the
-   on a pattern matched out subpiece of the input, as then the input is always decreasing
+   recursive call is on a pattern matched out subpiece of the input, as then
-   in size. Getting Coq to understand that functions terminate is not always easy. See the
+   the input is always decreasing in size. Getting Coq to understand that
-   references at the end of the article for more on this topic. *)
+   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: *)
 
@@ -121,14 +125,16 @@ Compute my_id nat 3. (* 3 : nat *)
 (* You can ask Coq to infer terms with an underscore *)
 Compute my_id _ 3.
 
-(* An implicit argument of a function is an argument which can be inferred from contextual
+(* An implicit argument of a function is an argument which can be inferred
-   knowledge. Parameters enclosed in {} are implicit by default *)
+   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
+(* Sometimes it may be necessary to turn this off. You can make all
-   again with @ *)
+   arguments explicit again with @ *)
+
 Compute @my_id3 nat 3.
 
 (* Or give arguments by name *)
@@ -168,16 +174,18 @@ let rec factorial n = match n with
 
 (*** Notation ***)
 
-(* Coq has a very powerful Notation system that can be used to write expressions in more
+(* Coq has a very powerful Notation system that can be used to write
-   natural forms. *)
+   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
+(* Notation is a syntactic transformation applied to the text of the program
-   evaluated. Notation is organized into notation scopes. Using different notation scopes
+   before being evaluated. Notation is organized into notation scopes. Using
-   allows for a weak notion of overloading. *)
+   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.
 
 (* Notation scopes can be opened *)
@@ -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, 
+(* Coq declares by default the following interpretation scopes: core_scope,
-   function_scope, nat_scope, bool_scope, list_scope, int_scope, uint_scope. You may also
+   type_scope, function_scope, nat_scope, bool_scope, list_scope, int_scope,
-   want the numerical scopes Z_scope (integers) and Q_scope (fractions) held in the ZArith
+   uint_scope. You may also want the numerical scopes Z_scope (integers) and
-   and QArith module respectively. *)
+   Q_scope (fractions) held in the ZArith and QArith module respectively. *)
 
 (* You can print the contents of scopes *)
 Print Scope nat_scope.
@@ -231,14 +239,16 @@ Bound to classes nat Nat.t
 *)
 
 (* 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
+   Floating point numbers and real numbers are also available but are a more
-   topic, as proving properties about them is rather tricky. *)
+   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 *)
 Close Scope Q_scope.
@@ -279,7 +289,8 @@ 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.
 
@@ -289,8 +300,8 @@ Import ListNotations.
 Compute [1 ; 2 ; 3]. (* [1; 2; 3] : list nat *)
 
 
-(*
+(* There is a large number of list manipulation functions available,
-There are a large number of list manipulation functions available, including:
+   including:
 
 • length
 • head : first element (with default)
@@ -308,10 +319,12 @@ There are a large number of list manipulation functions available, including:
 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.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 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
           (by lists and by AVL trees)
-• Reals : Axiomatization of real numbers (classical, basic functions, integer part, 
+• Reals : Axiomatization of real numbers (classical, basic functions,
-          fractional part, limit, derivative, Cauchy series, power series and results,...)
+          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
+(* Because Coq is dependently typed, defining type aliases is no different
-   an alias for a value. *)
+   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
+(* More interesting types can be defined using the Inductive vernacular.
-   can be defined like so *)
+   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
+(* Record syntax is sugar for tuple-like types. It defines named accessor
-   the components. Record types are defined with the notation {...} *)
+   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 *)
 
-(* Types can be parameterized, like in this type for "list of lists
+(* Types can be parameterized, like in this type for "list of lists of
-   of anything". 'a can be substituted with any type. *)
+   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
+(* Explaining the proof language is out of scope for this tutorial, but here
-   whet your appetite. Check the resources below for more. *)
+   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
+(* A fascinating feature of dependently type based theorem provers is that
-  primitive constructs underly the proof language as the programming features.
+   the same primitive constructs underly the proof language as the
-  For example, we can write and prove the proposition A and B implies A in raw Gallina *)
+   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
+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
+(* Or we can prove it using tactics. Tactics are a macro language to help
-   in a more natural style and automate away some drudgery. *)
+   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
@@ -466,7 +496,9 @@ Proof. intros n. induction n.
 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