mirror of
https://github.com/adambard/learnxinyminutes-docs.git
synced 2024-12-28 17:59:05 +03:00
Merge pull request #3784 from sshine/coq-fix-code-width
[coq/en] Fix code width
This commit is contained in:
Divay Prakash
GitHub
commit
471b05c51d
@ -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 containing definitions related to the integers Z *)
|
||||
Require Import ZArith.
|
||||
(* Imports the Zarith module holding definitions related to the integers Z *)
|
||||
|
||||
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
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user