summaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorDivay Prakash <divayprakash@users.noreply.github.com>2020-01-24 20:30:55 +0530
committerGitHub <noreply@github.com>2020-01-24 20:30:55 +0530
commit471b05c51d2c783ab8d369b6ca8d305accbebd3e (patch)
tree5670f5e162fafcacf8f29b4227ccea2fbe221daa
parentce95d2763ed7a5804eb454a1e018baa16e443ef7 (diff)
parent672b3804f933a40df15db2e29d9a06030928194b (diff)
Merge pull request #3784 from sshine/coq-fix-code-width
[coq/en] Fix code width
-rw-r--r--coq.html.markdown208
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