qnighy/Sample.v

## Sample.v
(* *
 * * Vernacular Commands
 * *)


(*
 * Chapter 1 The Gallina specification language
 *)

(* 1.3.1 Assumptions *)
Axiom foo : Bar.
Parameter foo : Bar.
Parameter foo1 foo2 foo3 : Bar.
Parameter (foo1 foo2 foo3 : Bar) (foo4 foo5 foo6 : Baz).
Conjecture foo : Bar.
Parameters foo : Bar.

Variable foo : Bar.
Variable foo1 foo2 foo3 : Bar.
Variable (foo1 foo2 foo3 : Bar) (foo4 foo5 foo6 : Baz).
Hypothesis foo : Bar.
Variables foo : Bar.
Hypotheses foo : Bar.

(* 1.3.2 Definitions *)
Definition foo := baz.
Definition foo : Bar := baz.
Definition foo x y z : Bar := baz.
Definition foo (x y z : X) (a b c : A) : Bar := baz.
Example foo := baz.
Example foo : Bar := baz.
Example foo x y z : Bar := baz.
Example foo (x y z : X) (a b c : A) : Bar := baz.

Let foo := baz.
Let foo : Bar := baz.

(* 1.3.3 Inductive Definitions *)
Inductive Bar : Set :=
    foo1 : Bar
  | foo2 : Bar -> Bar.
CoInductive Bar : Set :=
    foo1 : Bar
  | foo2 : Bar -> Bar.

Inductive Bar := foo1 | foo2 (_:Bar).
CoInductive Bar := foo1 | foo2 (_:Bar).

Inductive Bar : nat -> Prop :=
  | foo1 : Bar O
  | foo2 : forall n:nat, Bar n -> Bar (S (S n)).
CoInductive Bar : nat -> Prop :=
  | foo1 : Bar O
  | foo2 : forall n:nat, Bar n -> Bar (S (S n)).

Inductive Bar(A:Set) : Set := foo : A -> Bar A.
Inductive Bar(A:Set) : Set := foo (_:A).
CoInductive Bar(A:Set) : Set := foo : A -> Bar A.
CoInductive Bar(A:Set) : Set := foo (_:A).

Inductive Bar1 : nat -> Prop :=
  | foo1 : Bar1 O
  | foo2 n : Bar2 n -> Bar1 (S n)
with Bar2 : nat -> Prop :=
  | foo3 n : Bar1 n -> Bar2 (S n).
CoInductive Bar1 : nat -> Prop :=
  | foo1 : Bar1 O
  | foo2 n : Bar2 n -> Bar1 (S n)
with Bar2 : nat -> Prop :=
  | foo3 n : Bar1 n -> Bar2 (S n).


(* 1.3.4 Definition of recursive functions *)
Fixpoint foo n := baz.
Fixpoint foo (n m:nat) : Bar := baz.
Fixpoint foo n m {struct n} : Bar := baz.
CoFixpoint foo n := baz.
CoFixpoint foo (n m:nat) : Bar := baz.
CoFixpoint foo n m {struct n} : Bar := baz.

Fixpoint foo1 n := baz
with foo2 n := bazbaz.
CoFixpoint foo1 n := baz
with foo2 n := bazbaz.

(* 1.3.5 Assertions and proofs *)
Theorem foo a b c : Bar. Qed.
Lemma foo (a b c: A) : Bar. Qed.
Remark foo : Bar. Qed.
Fact foo : Bar. Qed.
Corollary foo : Bar. Qed.
Proposition foo : Bar. Qed.

Theorem foo1 n: Bar n with foo2 n: Baz n. Qed.

Definition foo (a b c: A) : Bar. Qed.
Example foo a b c : Bar. Qed.
Let foo : Bar. Qed.

Theorem foo : Bar. Proof. Qed.
Theorem foo : Bar. Proof. Defined.
Theorem foo : Bar. Proof. Admitted.
Theorem foo : Bar. Proof. Admitted.


(*
 * Chapter 2 Extensions of Gallina
 *)

(* 2.2.1 Record types *)
Record Bar : Type := { foo1 : nat; foo2 : foo1 = O }.
Structure Bar : Type := { foo1 : nat; foo2 : foo1 = O }.
Inductive Bar : Type := { foo1 : nat; foo2 : foo1 = O }.
CoInductive Bar : Type := { foo1 : nat; foo2 : foo1 = O }.

Record Bar : Type := makeBar { foo1 : nat; foo2 : foo1 = O }.
CoInductive Bar : Type := makeBar { foo1 : nat; foo2 : foo1 = O }.

Set Printing Projections.
Unset Printing Projections.
Test Printing Projections.

(* 2.2.4 Controlling pretty-printing of match exptessions *)

Set Printing Matching.
Unset Printing Matching.
Test Printing Matching.

Set Printing Wildcard.
Unset Printing Wildcard.
Test Printing Wildcard.

Set Printing Synth.
Unset Printing Synth.
Test Printing Synth.

Add Printing Let foo.
(* Remove Printing Let foo. *)
(* Test Printing Let for foo. *)
Print Table Printing Let.

Add Printing If foo.
(* Remove Printing If foo. *)
(* Test Printing If for foo. *)
Print Table Printing If.


(* 2.3 Advanced recursive functions *)

Function foo a b c {struct a} : Bar := baz.
Function foo a b c : Bar := baz.
Function foo (a b c: A) {measure a} : Bar := baz.
Function foo (a b c: A) {wf a} : Bar := baz.

(* 2.4 Section Mechanism *)
Section HogeSection.
End HogeSection.

(* 2.5 Module System *)

Module HogeModule.
End HogeModule.

Module HogeModule(X Y Z : PiyoModule). End HogeModule.
Module HogeModule(X Y Z : !PiyoModule). End HogeModule.
Module HogeModule : FugaModuleType. End HogeModule.
Module HogeModule(X Y Z : PiyoModule) : FugaModuleType. End HogeModule.
Module HogeModule(X Y Z : PiyoModule) : !FugaModuleType. End HogeModule.
Module HogeModule <: FugaModuleType1 <: FugaModuleType2. End HogeModule.
Module HogeModule(X Y Z : PiyoModule) <: FugaModuleType1 <: FugaModuleType2. End HogeModule.
Module Import HogeModule. End HogeModule.
Module Import HogeModule(X Y Z : PiyoModule). End HogeModule.
Module Import HogeModule : FugaModuleType. End HogeModule.
Module Import HogeModule(X Y Z : PiyoModule) : FugaModuleType. End HogeModule.
Module Import HogeModule <: FugaModuleType1 <: FugaModuleType2. End HogeModule.
Module Import HogeModule(X Y Z : PiyoModule) <: FugaModuleType1 <: FugaModuleType2. End HogeModule.
Module Export HogeModule. End HogeModule.
Module Export HogeModule(X Y Z : PiyoModule). End HogeModule.
Module Export HogeModule : FugaModuleType. End HogeModule.
Module Export HogeModule(X Y Z : PiyoModule) : FugaModuleType. End HogeModule.
Module Export HogeModule <: FugaModuleType1 <: FugaModuleType2. End HogeModule.
Module Export HogeModule(X Y Z : PiyoModule) <: FugaModuleType1 <: FugaModuleType2. End HogeModule.

Module HogeModule.
  Include FugaModule.
  Include FugaModule1 <+ FugaModule2 <+ FugaModule3.
End HogeModule.

Module HogeModule := FugaModule.
Module HogeModule := PiyoFunctor FugaModule1 FugaModule2.
Module HogeModule(X Y Z : PiyoModule) : FugaModuleType := PiyoFunctor FugaModule1.
Module HogeModule(X Y Z : PiyoModule) <: FugaModuleType1 <: FugaModuleType2 := PiyoFunctor FugaModule1.
Module HogeModule(X Y Z : PiyoModule) := FugaModule3 <+ PiyoFunctor FugaModule1 FugaModule2 <+ FugaModule4.

Module Type HogeModuleType.
End HogeModuleType.

Module Type HogeModuleType(X Y Z : PiyoModule). End HogeModuleType.

Module Type HogeModuleType.
  Include FugaModule.
  Include FugaModule1 <+ FugaModule2 <+ FugaModule3.
  Axiom Inline foo : Bar.
  Conjecture Inline foo : Bar.
  Parameter Inline foo : Bar.
  Parameters Inline foo : Bar.
  Variable Inline foo : Bar.
  Variables Inline foo : Bar.
  Hypothesis Inline foo : Bar.
  Hypotheses Inline foo : Bar.

  Declare Module PiyoModule : HogeraSig.
  Declare Module PiyoFunctor (X Y:CogeraModuleType) : HogeraSig.
End HogeModuleType.

Import HogeModule.
Export HogeModule Foo.

Module HogeModule : FugaModuleType with Definition foo := (foo1 + foo2) with Module PiyoModule := CogeraModule.

Print Module HogeModule.
Print Module Type HogeModule.
Locate Module HogeModule.

(* 2.7 Implicit arguments *)

Definition foo {a : A} (b : B) : Bar := baz _.

Inductive foo {A : Type} : Set := .

Arguments foo [x] y _ [a] b c.
Local Arguments foo [x] y _ [a] b c.
Global Arguments foo [x] y _ [a] b c.
Arguments foo [x y z a b c], [x y z a b] c, [x] y [z a b] c, x y [z a b] c, x y [z] a [b] c, x y z a b c.
Local Arguments foo [x y z a b c], [x y z a b] c, [x] y [z a b] c, x y [z a b] c, x y [z] a [b] c, x y z a b c.
Global Arguments foo [x y z a b c], [x y z a b] c, [x] y [z a b] c, x y [z a b] c, x y [z] a [b] c, x y z a b c.

Arguments foo : default implicits.
Local Arguments foo : default implicits.
Global Arguments foo : default implicits.

Set Implicit Arguments.
Unset Implicit Arguments.
Test Implicit Arguments.
Set Strict Implicit.
Unset Strict Implicit.
Test Strict Implicit.
Set Strongly Strict Implicit.
Unset Strongly Strict Implicit.
Test Strongly Strict Implicit.
Set Contextual Implicit.
Unset Contextual Implicit.
Test Contextual Implicit.
Set Reversible Pattern Implicit.
Unset Reversible Pattern Implicit.
Test Reversible Pattern Implicit.
Set Maximal Implicit Insersion.
Unset Maximal Implicit Insersion.
Test Maximal Implicit Insersion.

Arguments foo [x] y _ [a] b c : rename.
Local Arguments foo [x] y _ [a] b c : rename.
Global Arguments foo [x] y _ [a] b c : rename.

Print Implicit foo.

Set Printing Implicit.
Unset Printing Implicit.
Test Printing Implicit.
Set Printing Implicit Defensive.
Unset Printing Implicit Defensive.
Test Printing Implicit Defensive.

Set Parsing Explicit.
Unset Parsing Explicit.
Test Parsing Explicit.

(* 2.7.18 Canonical structures *)
Canonical Structure foo.
Canonical Structure foo : Bar := baz.
Canonical Structure foo(x y z : X) : Bar := baz.

Print Canonical Projections.

(* 2.7.19 Implicit types of variables *)
Implicit Types foo1 foo2 foo3 : Bar.
Implicit Type foo1 : Bar.
Implicit Types (foo1 foo2 foo3 : Bar) (foo4 foo5 foo6 : Baz).

(* 2.7.20 Implicit generalization *)
Generalizable All Variables.
Generalizable No Variables.
Generalizable Variables foo1 foo2 foo3.
Generalizable Variable foo1 foo2 foo3.
Global Generalizable All Variables.
Global Generalizable No Variables.
Global Generalizable Variables foo1 foo2 foo3.
Global Generalizable Variable foo1 foo2 foo3.

(* 2.8 Coercions *)
Coercion foo : Bar >-> Sortclass.
Coercion foo : Bar >-> Funclass.

(* 2.9 Printing constructions in full *)
Set Printing All.
Unset Printing All.
Test Printing All.

(* 2.10 Printing Universes *)
Set Printing Universes.
Unset Printing Universes.
Test Printing Universes.
Print Universes.
Print Sorted Universes.
Print Universes "foo.dot".
Print Sorted Universes "foo.dot".

(* 2.11 Existential variables *)
Set Printing Existential Variables.
Unset Printing Existential Variables.
Test Printing Existential Variables.


(*
 * Chapter 6 Vernacular commands
 *)

(* 6.1 Displaying *)
Print foo.
Print Term foo.
About foo.

Print All.
Inspect 1.
Print Section HogeSection.

(* 6.2 Options and Flags *)
Set Implicit Arguments.
Unset Implicit Arguments.
Local Set Implicit Arguments.
Local Set Implicit Arguments.
Global Unset Implicit Arguments.
Global Unset Implicit Arguments.
Test Implicit Arguments.
(* vice versa *)

(* 6.3 Requests to the environment *)
Check (foo1 + foo2).
Eval lazy in (foo1 + foo2).
Compute (foo1 + foo2).
Extraction (foo1 + foo2).
Recursive Extraction foo1, foo2, foo3.

Print Assumptions foo1.
Print Opaque Dependencies foo1.

Search (foo1 + foo2).
SearchAbout foo.
SearchAbout "_ + _".
SearchAbout "_ + _"%type.
SearchAbout (_ + _).
SearchAbout "_ + _" -S inside Peano.
SearchAbout "_ + _" -S outside Datatypes.
SearchPattern (_ + _ = _ + _).
SearchPattern (_ + _ = _ + _) inside Peano.
SearchPattern (_ + _ = _ + _) outside Datatypes.
SearchRewrite (_ + _ + _).
SearchRewrite (_ + _ + _) inside Peano.
SearchRewrite (_ + _ + _) outside Datatypes.

Locate foo.

Set Whelp Server "http://example.com:8000/".
Set Whelp Getter "http://example.com:8000/".
Whelp Locate ".*".
Whelp Match (_ + _).
Whelp Instance (_ + _).
Whelp Elim foo.
Whelp Hint (foo1 + foo2).

(* 6.4 Loading files *)
Load HogeFile.
Load "HogeFile.v".
Load "HogeFile".
Load Verbose HogeFile.
Load Verbose "HogeFile.v".

(* 6.5 Compiled files *)
Require HogeModule.
Require Import HogeModule.
Require Export HogeModule.
Require HogeModule FugaModule PiyoModule.
Require Import HogeModule FugaModule PiyoModule.
Require Export HogeModule FugaModule PiyoModule.
Require "HogeModule".
Require Import "HogeModule".
Require Export "HogeModule".

Print Libraries.

Declare ML Module "foo" "bar" "baz".
Local Declare ML Module "foo" "bar" "baz".
Print ML Modules.

(* 6.6 Loadpath *)
Pwd.
Cd.
Cd "..".

Add LoadPath "/usr" as foo.bar.
Add LoadPath "/usr".
Add Rec LoadPath "/usr" as foo.bar.
Add Rec LoadPath "/usr".
Remove LoadPath "/usr".
Print LoadPath.

Add ML Path "/usr".
Add Rec ML Path "/usr".
Print ML Path.
Locate File "foo".
Locate Library foo.bar.

(* 6.7 Backtracking *)
Reset foo.
Reset Initial.

Back.
Back 2.
BackTo 10.

(* 6.8 State files *)
Write State "foo.coq".
Write State foo.
Restore State "foo.coq".
Restore State foo.

(* 6.9 Quitting and debugging *)
Quit.
Drop.

Time Print All.
Timeout 1 Print All.
Set Default Timeout 10.
Unset Default Timeout.
Test Default Timeout.

(* 6.10 Controlling display *)
Set Silent.
Unset Silent.
Set Printing Width 78.
Unset Printing Width.
Test Printing Width.
Set Printing Depth 50.
Unset Printing Depth.
Test Printing Depth.

(* 6.11 Controlling the reduction strategies and the conversion algorithm *)
Opaque foo1 foo2 foo3.
Transparent foo1 foo2 foo3.
Strategy opaque [foo1 foo2 foo3].
Strategy 5 [foo1 foo2 foo3].
Strategy 0 [foo1 foo2 foo3].
Strategy expand [foo1 foo2 foo3].

Declare Reduction foo := simpl; idtac.

Set Virtual Machine.
Unset Virtual Machine.
Test Virtual Machine.

(* 6.12 Controlling the locality of commands *)
Local Set Implicit Arguments.
Global Set Implicit Arguments.
(* as such *)


(*
 * Chapter 7 Proof handling
 *)

(* 7.1 Switching on/off the proof editing mode *)
Goal True.
Qed.

Goal True. Save foo.
Goal True. Save Theorem foo.
Goal True. Save Lemma foo.
Goal True. Save Remark foo.
Goal True. Save Fact foo.
Goal True. Save Corollary foo.
Goal True. Save Proposition foo.

Goal True.
Proof.
Qed.

Section HogeSection.
  Variable x y z : Bar.
  Goal True.
  Proof using x z.
  Admitted.
End HogeSection.

Goal True.
Abort.

Goal True. Abort foo.
Goal True. Abort All.

Existential 153 := (foo1 + foo2).
Grab Existential Variables.

(* 7.2 Navigation in the proof tree *)
Goal True.
  Undo.
  Undo 3.
  Restart.

  Focus.
  Focus 1.
  Unfocus.
  Unfocused.
  {
  }
  split.
  - assumption.
  - split.
    + assumption.
    + split.
      * assumption.
      * assumption.
Qed.

(* 7.3 Requesting Information *)
Goal True.
  Show.
  Show 1.
  Show Implicits.
  Show Implicits 1.
  Show Script.
  Show Tree.
  Show Proof.
  Show Conjectures.
  Show Intro.
  Show Intros.
  Show Existentials.

  Guarded.
Qed.

(* 7.4 Controlling the effect of proof editing commands *)
Set Hyps Limit 10.
Unset Hyps Limit.
Set Automatic Introduction.
Unset Automatic Introduction.


(*
 * Chapter 8 Tactics
 *)

(* 8.6 Rewriting expressions *)

Declare Left Step (foo1 foo2).
Declare Right Step (foo1 foo2).

(* 8.7 Performing computations *)
Arguments foo x y : simpl never.
Arguments foo {A B C} x y / z w.
Arguments foo x y : simpl nomatch.

(* 8.9 Controlling automation *)
Create HintDb bazdb.
Create HintDb bazdb discriminated.

Hint Resolve (foo1 foo2) : bazdb1 bazdb2.
Hint Resolve (foo1 foo2) foo3 foo4 : bazdb1 bazdb2.
Hint Immediate (foo1 foo2) foo3 foo4 : bazdb1 bazdb2.
Hint Constructors foo1 foo2 : bazdb1 bazdb2.
Hint Unfold foo1 foo2 : bazdb1 bazdb2.
Hint Transparent foo1 foo2 : bazdb1 bazdb2.
Hint Opaque foo1 foo2 : bazdb1 bazdb2.
Hint Extern 10 (~(_ = foo ?X)) => idtac X : bazdb1 bazdb2.

Local Hint Resolve (foo1 foo2) : bazdb1 bazdb2.
Local Hint Resolve (foo1 foo2).

Hint Resolve foo : core arith zarith bool datatypes sets typeclass_instances.

Print Hint foo.
Print Hint *.
Print HintDb bazdb.

Hint Rewrite (foo1 foo2) foo3 foo4 : bazdb1 bazdb2.
Hint Rewrite -> (foo1 foo2) foo3 foo4 : bazdb1 bazdb2.
Hint Rewrite <- (foo1 foo2) foo3 foo4 : bazdb1 bazdb2.
Hint Rewrite (foo1 foo2) foo3 foo4 using idtac : bazdb1 bazdb2.
Print Rewrite HintDb bazdb.

Goal True.
Proof with (simpl; auto).
  intros...
Qed.

Section HogeSection.
  Variable x y z : X.
  Goal True. Proof with (simpl; auto) using x z. intros... Qed.
  Goal True. Proof using x z with (simpl; auto). intros... Qed.
End HogeSection.

Declare Implicit Tactic idtac.

(* 8.10 Decision procedures *)
Set Firstorder Depth 5.


(*
 * Chapter 9 The tactic language
 *)

Ltac foo foo1 foo2 foo3 := idtac.
Ltac foo := fun foo1 foo2 foo3 => idtac.

Ltac foo1 a b c := idtac
with foo2 a b c := idtac
with foo3 a b c := idtac.

Ltac foo foo1 foo2 foo3 ::= idtac. (* redefinition *)

Print Ltac foo.

Set Ltac Debug.
Unset Ltac Debug.


(*
 * Chapter 12 Syntax extensions and interpretation scopes
 *)

(* 12.1 Notations *)
Notation "A <----------> B" := (foo B A).

Notation "'This' A 'is' 'more' B" := (this_is_more A B) (at level 0, B at level 70).

Print Grammar constr.
Print Grammar pattern.
Print Grammar tactic.

Infix "<---------->" := (flip foo) (at level 80, right associativity).

Notation "A <----------> B <----------> C" := (foo B A /\ foo C B) (at level 80, B at next level).

Notation "A <----------> B" := (foo B A) (format "'[hv' A '/' <----------> '//' B ']'").

Reserved Notation "A <----------> B".

Inductive foo x y z := bar
where "A <----------> B" := baz.
CoInductive foo x y z := bar
where "A <----------> B" := baz.
Fixpoint foo x y := bar
where "A <----------> B" := baz
and "A >----------< B" := bazbaz.

Set Printing Notations.
Unset Printing Notations.

Locate "+".

Notation "'foo'" := bar (at level 70, a at level 80, b at next level, left associativity, right associativity, no associativity, x ident, P binder, Q closed binder, G global, X bigint, only parsing, format "").

(* 12.2 Interpretation scopes *)

Open Scope foo_scope.
Close Scope foo_scope.
Local Open Scope foo_scope.
Local Close Scope foo_scope.
Global Open Scope foo_scope.
Global Close Scope foo_scope.

Delimit Scope foo_scope with foo.

Arguments foo x%bar y%baz.
Arguments foo : clear scopes.

Bind Scope foo_scope with SomeSet.
Bind Scope foo_scope with Funclass.
Bind Scope foo_scope with Sortclass.

Definition foo := a%type a%nat a%N a%Z a%positive a%Q a%Qc a%real a%bool a%list a%core a%string a%char.

Print Visibility.
Print Visibility foo_scope.

Print Scope foo_scope.
Print Scopes.

(* 12.3 Abbreviations *)
Notation abbr := (foo bar _ baz).
Local Notation abbr y z := (foo z y) (only parsing).

(* 12.4 Tactic Notations *)

Tactic Notation "foo" := idtac.
Tactic Notation (at level 100) "bar" ident(a) simple_intropattern(a) reference(a) hyp(a) hyp_list(a) ne_hyp_list(a) constr(a) constr_list(a) ne_constr_list(a) integer(a) integer_list(a) ne_integer_list(a) int_or_var(a) int_or_var_list(a) ne_int_or_var_list(a) tactic(a) tactic0(a) tactic1(a) tactic2(a) tactic3(a) tactic4(a) tactic5(a) "baz" := idtac.
	(* *
	* * Vernacular Commands
	* *)


	(*
	* Chapter 1 The Gallina specification language
	*)

	(* 1.3.1 Assumptions *)
	Axiom foo : Bar.
	Parameter foo : Bar.
	Parameter foo1 foo2 foo3 : Bar.
	Parameter (foo1 foo2 foo3 : Bar) (foo4 foo5 foo6 : Baz).
	Conjecture foo : Bar.
	Parameters foo : Bar.

	Variable foo : Bar.
	Variable foo1 foo2 foo3 : Bar.
	Variable (foo1 foo2 foo3 : Bar) (foo4 foo5 foo6 : Baz).
	Hypothesis foo : Bar.
	Variables foo : Bar.
	Hypotheses foo : Bar.

	(* 1.3.2 Definitions *)
	Definition foo := baz.
	Definition foo : Bar := baz.
	Definition foo x y z : Bar := baz.
	Definition foo (x y z : X) (a b c : A) : Bar := baz.
	Example foo := baz.
	Example foo : Bar := baz.
	Example foo x y z : Bar := baz.
	Example foo (x y z : X) (a b c : A) : Bar := baz.

	Let foo := baz.
	Let foo : Bar := baz.

	(* 1.3.3 Inductive Definitions *)
	Inductive Bar : Set :=
	foo1 : Bar
	\| foo2 : Bar -> Bar.
	CoInductive Bar : Set :=
	foo1 : Bar
	\| foo2 : Bar -> Bar.

	Inductive Bar := foo1 \| foo2 (_:Bar).
	CoInductive Bar := foo1 \| foo2 (_:Bar).

	Inductive Bar : nat -> Prop :=
	\| foo1 : Bar O
	\| foo2 : forall n:nat, Bar n -> Bar (S (S n)).
	CoInductive Bar : nat -> Prop :=
	\| foo1 : Bar O
	\| foo2 : forall n:nat, Bar n -> Bar (S (S n)).

	Inductive Bar(A:Set) : Set := foo : A -> Bar A.
	Inductive Bar(A:Set) : Set := foo (_:A).
	CoInductive Bar(A:Set) : Set := foo : A -> Bar A.
	CoInductive Bar(A:Set) : Set := foo (_:A).

	Inductive Bar1 : nat -> Prop :=
	\| foo1 : Bar1 O
	\| foo2 n : Bar2 n -> Bar1 (S n)
	with Bar2 : nat -> Prop :=
	\| foo3 n : Bar1 n -> Bar2 (S n).
	CoInductive Bar1 : nat -> Prop :=
	\| foo1 : Bar1 O
	\| foo2 n : Bar2 n -> Bar1 (S n)
	with Bar2 : nat -> Prop :=
	\| foo3 n : Bar1 n -> Bar2 (S n).


	(* 1.3.4 Definition of recursive functions *)
	Fixpoint foo n := baz.
	Fixpoint foo (n m:nat) : Bar := baz.
	Fixpoint foo n m {struct n} : Bar := baz.
	CoFixpoint foo n := baz.
	CoFixpoint foo (n m:nat) : Bar := baz.
	CoFixpoint foo n m {struct n} : Bar := baz.

	Fixpoint foo1 n := baz
	with foo2 n := bazbaz.
	CoFixpoint foo1 n := baz
	with foo2 n := bazbaz.

	(* 1.3.5 Assertions and proofs *)
	Theorem foo a b c : Bar. Qed.
	Lemma foo (a b c: A) : Bar. Qed.
	Remark foo : Bar. Qed.
	Fact foo : Bar. Qed.
	Corollary foo : Bar. Qed.
	Proposition foo : Bar. Qed.

	Theorem foo1 n: Bar n with foo2 n: Baz n. Qed.

	Definition foo (a b c: A) : Bar. Qed.
	Example foo a b c : Bar. Qed.
	Let foo : Bar. Qed.

	Theorem foo : Bar. Proof. Qed.
	Theorem foo : Bar. Proof. Defined.
	Theorem foo : Bar. Proof. Admitted.
	Theorem foo : Bar. Proof. Admitted.



	(*
	* Chapter 2 Extensions of Gallina
	*)

	(* 2.2.1 Record types *)
	Record Bar : Type := { foo1 : nat; foo2 : foo1 = O }.
	Structure Bar : Type := { foo1 : nat; foo2 : foo1 = O }.
	Inductive Bar : Type := { foo1 : nat; foo2 : foo1 = O }.
	CoInductive Bar : Type := { foo1 : nat; foo2 : foo1 = O }.

	Record Bar : Type := makeBar { foo1 : nat; foo2 : foo1 = O }.
	CoInductive Bar : Type := makeBar { foo1 : nat; foo2 : foo1 = O }.

	Set Printing Projections.
	Unset Printing Projections.
	Test Printing Projections.

	(* 2.2.4 Controlling pretty-printing of match exptessions *)

	Set Printing Matching.
	Unset Printing Matching.
	Test Printing Matching.

	Set Printing Wildcard.
	Unset Printing Wildcard.
	Test Printing Wildcard.

	Set Printing Synth.
	Unset Printing Synth.
	Test Printing Synth.

	Add Printing Let foo.
	(* Remove Printing Let foo. *)
	(* Test Printing Let for foo. *)
	Print Table Printing Let.

	Add Printing If foo.
	(* Remove Printing If foo. *)
	(* Test Printing If for foo. *)
	Print Table Printing If.


	(* 2.3 Advanced recursive functions *)

	Function foo a b c {struct a} : Bar := baz.
	Function foo a b c : Bar := baz.
	Function foo (a b c: A) {measure a} : Bar := baz.
	Function foo (a b c: A) {wf a} : Bar := baz.

	(* 2.4 Section Mechanism *)
	Section HogeSection.
	End HogeSection.

	(* 2.5 Module System *)

	Module HogeModule.
	End HogeModule.

	Module HogeModule(X Y Z : PiyoModule). End HogeModule.
	Module HogeModule(X Y Z : !PiyoModule). End HogeModule.
	Module HogeModule : FugaModuleType. End HogeModule.
	Module HogeModule(X Y Z : PiyoModule) : FugaModuleType. End HogeModule.
	Module HogeModule(X Y Z : PiyoModule) : !FugaModuleType. End HogeModule.
	Module HogeModule <: FugaModuleType1 <: FugaModuleType2. End HogeModule.
	Module HogeModule(X Y Z : PiyoModule) <: FugaModuleType1 <: FugaModuleType2. End HogeModule.
	Module Import HogeModule. End HogeModule.
	Module Import HogeModule(X Y Z : PiyoModule). End HogeModule.
	Module Import HogeModule : FugaModuleType. End HogeModule.
	Module Import HogeModule(X Y Z : PiyoModule) : FugaModuleType. End HogeModule.
	Module Import HogeModule <: FugaModuleType1 <: FugaModuleType2. End HogeModule.
	Module Import HogeModule(X Y Z : PiyoModule) <: FugaModuleType1 <: FugaModuleType2. End HogeModule.
	Module Export HogeModule. End HogeModule.
	Module Export HogeModule(X Y Z : PiyoModule). End HogeModule.
	Module Export HogeModule : FugaModuleType. End HogeModule.
	Module Export HogeModule(X Y Z : PiyoModule) : FugaModuleType. End HogeModule.
	Module Export HogeModule <: FugaModuleType1 <: FugaModuleType2. End HogeModule.
	Module Export HogeModule(X Y Z : PiyoModule) <: FugaModuleType1 <: FugaModuleType2. End HogeModule.

	Module HogeModule.
	Include FugaModule.
	Include FugaModule1 <+ FugaModule2 <+ FugaModule3.
	End HogeModule.

	Module HogeModule := FugaModule.
	Module HogeModule := PiyoFunctor FugaModule1 FugaModule2.
	Module HogeModule(X Y Z : PiyoModule) : FugaModuleType := PiyoFunctor FugaModule1.
	Module HogeModule(X Y Z : PiyoModule) <: FugaModuleType1 <: FugaModuleType2 := PiyoFunctor FugaModule1.
	Module HogeModule(X Y Z : PiyoModule) := FugaModule3 <+ PiyoFunctor FugaModule1 FugaModule2 <+ FugaModule4.

	Module Type HogeModuleType.
	End HogeModuleType.

	Module Type HogeModuleType(X Y Z : PiyoModule). End HogeModuleType.

	Module Type HogeModuleType.
	Include FugaModule.
	Include FugaModule1 <+ FugaModule2 <+ FugaModule3.
	Axiom Inline foo : Bar.
	Conjecture Inline foo : Bar.
	Parameter Inline foo : Bar.
	Parameters Inline foo : Bar.
	Variable Inline foo : Bar.
	Variables Inline foo : Bar.
	Hypothesis Inline foo : Bar.
	Hypotheses Inline foo : Bar.

	Declare Module PiyoModule : HogeraSig.
	Declare Module PiyoFunctor (X Y:CogeraModuleType) : HogeraSig.
	End HogeModuleType.

	Import HogeModule.
	Export HogeModule Foo.

	Module HogeModule : FugaModuleType with Definition foo := (foo1 + foo2) with Module PiyoModule := CogeraModule.

	Print Module HogeModule.
	Print Module Type HogeModule.
	Locate Module HogeModule.

	(* 2.7 Implicit arguments *)

	Definition foo {a : A} (b : B) : Bar := baz _.

	Inductive foo {A : Type} : Set := .

	Arguments foo [x] y _ [a] b c.
	Local Arguments foo [x] y _ [a] b c.
	Global Arguments foo [x] y _ [a] b c.
	Arguments foo [x y z a b c], [x y z a b] c, [x] y [z a b] c, x y [z a b] c, x y [z] a [b] c, x y z a b c.
	Local Arguments foo [x y z a b c], [x y z a b] c, [x] y [z a b] c, x y [z a b] c, x y [z] a [b] c, x y z a b c.
	Global Arguments foo [x y z a b c], [x y z a b] c, [x] y [z a b] c, x y [z a b] c, x y [z] a [b] c, x y z a b c.

	Arguments foo : default implicits.
	Local Arguments foo : default implicits.
	Global Arguments foo : default implicits.

	Set Implicit Arguments.
	Unset Implicit Arguments.
	Test Implicit Arguments.
	Set Strict Implicit.
	Unset Strict Implicit.
	Test Strict Implicit.
	Set Strongly Strict Implicit.
	Unset Strongly Strict Implicit.
	Test Strongly Strict Implicit.
	Set Contextual Implicit.
	Unset Contextual Implicit.
	Test Contextual Implicit.
	Set Reversible Pattern Implicit.
	Unset Reversible Pattern Implicit.
	Test Reversible Pattern Implicit.
	Set Maximal Implicit Insersion.
	Unset Maximal Implicit Insersion.
	Test Maximal Implicit Insersion.

	Arguments foo [x] y _ [a] b c : rename.
	Local Arguments foo [x] y _ [a] b c : rename.
	Global Arguments foo [x] y _ [a] b c : rename.

	Print Implicit foo.

	Set Printing Implicit.
	Unset Printing Implicit.
	Test Printing Implicit.
	Set Printing Implicit Defensive.
	Unset Printing Implicit Defensive.
	Test Printing Implicit Defensive.

	Set Parsing Explicit.
	Unset Parsing Explicit.
	Test Parsing Explicit.

	(* 2.7.18 Canonical structures *)
	Canonical Structure foo.
	Canonical Structure foo : Bar := baz.
	Canonical Structure foo(x y z : X) : Bar := baz.

	Print Canonical Projections.

	(* 2.7.19 Implicit types of variables *)
	Implicit Types foo1 foo2 foo3 : Bar.
	Implicit Type foo1 : Bar.
	Implicit Types (foo1 foo2 foo3 : Bar) (foo4 foo5 foo6 : Baz).

	(* 2.7.20 Implicit generalization *)
	Generalizable All Variables.
	Generalizable No Variables.
	Generalizable Variables foo1 foo2 foo3.
	Generalizable Variable foo1 foo2 foo3.
	Global Generalizable All Variables.
	Global Generalizable No Variables.
	Global Generalizable Variables foo1 foo2 foo3.
	Global Generalizable Variable foo1 foo2 foo3.

	(* 2.8 Coercions *)
	Coercion foo : Bar >-> Sortclass.
	Coercion foo : Bar >-> Funclass.

	(* 2.9 Printing constructions in full *)
	Set Printing All.
	Unset Printing All.
	Test Printing All.

	(* 2.10 Printing Universes *)
	Set Printing Universes.
	Unset Printing Universes.
	Test Printing Universes.
	Print Universes.
	Print Sorted Universes.
	Print Universes "foo.dot".
	Print Sorted Universes "foo.dot".

	(* 2.11 Existential variables *)
	Set Printing Existential Variables.
	Unset Printing Existential Variables.
	Test Printing Existential Variables.



	(*
	* Chapter 6 Vernacular commands
	*)

	(* 6.1 Displaying *)
	Print foo.
	Print Term foo.
	About foo.

	Print All.
	Inspect 1.
	Print Section HogeSection.

	(* 6.2 Options and Flags *)
	Set Implicit Arguments.
	Unset Implicit Arguments.
	Local Set Implicit Arguments.
	Local Set Implicit Arguments.
	Global Unset Implicit Arguments.
	Global Unset Implicit Arguments.
	Test Implicit Arguments.
	(* vice versa *)

	(* 6.3 Requests to the environment *)
	Check (foo1 + foo2).
	Eval lazy in (foo1 + foo2).
	Compute (foo1 + foo2).
	Extraction (foo1 + foo2).
	Recursive Extraction foo1, foo2, foo3.

	Print Assumptions foo1.
	Print Opaque Dependencies foo1.

	Search (foo1 + foo2).
	SearchAbout foo.
	SearchAbout "_ + _".
	SearchAbout "_ + _"%type.
	SearchAbout (_ + _).
	SearchAbout "_ + _" -S inside Peano.
	SearchAbout "_ + _" -S outside Datatypes.
	SearchPattern (_ + _ = _ + _).
	SearchPattern (_ + _ = _ + _) inside Peano.
	SearchPattern (_ + _ = _ + _) outside Datatypes.
	SearchRewrite (_ + _ + _).
	SearchRewrite (_ + _ + _) inside Peano.
	SearchRewrite (_ + _ + _) outside Datatypes.

	Locate foo.

	Set Whelp Server "http://example.com:8000/".
	Set Whelp Getter "http://example.com:8000/".
	Whelp Locate ".*".
	Whelp Match (_ + _).
	Whelp Instance (_ + _).
	Whelp Elim foo.
	Whelp Hint (foo1 + foo2).

	(* 6.4 Loading files *)
	Load HogeFile.
	Load "HogeFile.v".
	Load "HogeFile".
	Load Verbose HogeFile.
	Load Verbose "HogeFile.v".

	(* 6.5 Compiled files *)
	Require HogeModule.
	Require Import HogeModule.
	Require Export HogeModule.
	Require HogeModule FugaModule PiyoModule.
	Require Import HogeModule FugaModule PiyoModule.
	Require Export HogeModule FugaModule PiyoModule.
	Require "HogeModule".
	Require Import "HogeModule".
	Require Export "HogeModule".

	Print Libraries.

	Declare ML Module "foo" "bar" "baz".
	Local Declare ML Module "foo" "bar" "baz".
	Print ML Modules.

	(* 6.6 Loadpath *)
	Pwd.
	Cd.
	Cd "..".

	Add LoadPath "/usr" as foo.bar.
	Add LoadPath "/usr".
	Add Rec LoadPath "/usr" as foo.bar.
	Add Rec LoadPath "/usr".
	Remove LoadPath "/usr".
	Print LoadPath.

	Add ML Path "/usr".
	Add Rec ML Path "/usr".
	Print ML Path.
	Locate File "foo".
	Locate Library foo.bar.

	(* 6.7 Backtracking *)
	Reset foo.
	Reset Initial.

	Back.
	Back 2.
	BackTo 10.

	(* 6.8 State files *)
	Write State "foo.coq".
	Write State foo.
	Restore State "foo.coq".
	Restore State foo.

	(* 6.9 Quitting and debugging *)
	Quit.
	Drop.

	Time Print All.
	Timeout 1 Print All.
	Set Default Timeout 10.
	Unset Default Timeout.
	Test Default Timeout.

	(* 6.10 Controlling display *)
	Set Silent.
	Unset Silent.
	Set Printing Width 78.
	Unset Printing Width.
	Test Printing Width.
	Set Printing Depth 50.
	Unset Printing Depth.
	Test Printing Depth.

	(* 6.11 Controlling the reduction strategies and the conversion algorithm *)
	Opaque foo1 foo2 foo3.
	Transparent foo1 foo2 foo3.
	Strategy opaque [foo1 foo2 foo3].
	Strategy 5 [foo1 foo2 foo3].
	Strategy 0 [foo1 foo2 foo3].
	Strategy expand [foo1 foo2 foo3].

	Declare Reduction foo := simpl; idtac.

	Set Virtual Machine.
	Unset Virtual Machine.
	Test Virtual Machine.

	(* 6.12 Controlling the locality of commands *)
	Local Set Implicit Arguments.
	Global Set Implicit Arguments.
	(* as such *)



	(*
	* Chapter 7 Proof handling
	*)

	(* 7.1 Switching on/off the proof editing mode *)
	Goal True.
	Qed.

	Goal True. Save foo.
	Goal True. Save Theorem foo.
	Goal True. Save Lemma foo.
	Goal True. Save Remark foo.
	Goal True. Save Fact foo.
	Goal True. Save Corollary foo.
	Goal True. Save Proposition foo.

	Goal True.
	Proof.
	Qed.

	Section HogeSection.
	Variable x y z : Bar.
	Goal True.
	Proof using x z.
	Admitted.
	End HogeSection.

	Goal True.
	Abort.

	Goal True. Abort foo.
	Goal True. Abort All.

	Existential 153 := (foo1 + foo2).
	Grab Existential Variables.

	(* 7.2 Navigation in the proof tree *)
	Goal True.
	Undo.
	Undo 3.
	Restart.

	Focus.
	Focus 1.
	Unfocus.
	Unfocused.
	{
	}
	split.
	- assumption.
	- split.
	+ assumption.
	+ split.
	* assumption.
	* assumption.
	Qed.

	(* 7.3 Requesting Information *)
	Goal True.
	Show.
	Show 1.
	Show Implicits.
	Show Implicits 1.
	Show Script.
	Show Tree.
	Show Proof.
	Show Conjectures.
	Show Intro.
	Show Intros.
	Show Existentials.

	Guarded.
	Qed.

	(* 7.4 Controlling the effect of proof editing commands *)
	Set Hyps Limit 10.
	Unset Hyps Limit.
	Set Automatic Introduction.
	Unset Automatic Introduction.



	(*
	* Chapter 8 Tactics
	*)

	(* 8.6 Rewriting expressions *)

	Declare Left Step (foo1 foo2).
	Declare Right Step (foo1 foo2).

	(* 8.7 Performing computations *)
	Arguments foo x y : simpl never.
	Arguments foo {A B C} x y / z w.
	Arguments foo x y : simpl nomatch.

	(* 8.9 Controlling automation *)
	Create HintDb bazdb.
	Create HintDb bazdb discriminated.

	Hint Resolve (foo1 foo2) : bazdb1 bazdb2.
	Hint Resolve (foo1 foo2) foo3 foo4 : bazdb1 bazdb2.
	Hint Immediate (foo1 foo2) foo3 foo4 : bazdb1 bazdb2.
	Hint Constructors foo1 foo2 : bazdb1 bazdb2.
	Hint Unfold foo1 foo2 : bazdb1 bazdb2.
	Hint Transparent foo1 foo2 : bazdb1 bazdb2.
	Hint Opaque foo1 foo2 : bazdb1 bazdb2.
	Hint Extern 10 (~(_ = foo ?X)) => idtac X : bazdb1 bazdb2.

	Local Hint Resolve (foo1 foo2) : bazdb1 bazdb2.
	Local Hint Resolve (foo1 foo2).

	Hint Resolve foo : core arith zarith bool datatypes sets typeclass_instances.

	Print Hint foo.
	Print Hint *.
	Print HintDb bazdb.

	Hint Rewrite (foo1 foo2) foo3 foo4 : bazdb1 bazdb2.
	Hint Rewrite -> (foo1 foo2) foo3 foo4 : bazdb1 bazdb2.
	Hint Rewrite <- (foo1 foo2) foo3 foo4 : bazdb1 bazdb2.
	Hint Rewrite (foo1 foo2) foo3 foo4 using idtac : bazdb1 bazdb2.
	Print Rewrite HintDb bazdb.

	Goal True.
	Proof with (simpl; auto).
	intros...
	Qed.

	Section HogeSection.
	Variable x y z : X.
	Goal True. Proof with (simpl; auto) using x z. intros... Qed.
	Goal True. Proof using x z with (simpl; auto). intros... Qed.
	End HogeSection.

	Declare Implicit Tactic idtac.

	(* 8.10 Decision procedures *)
	Set Firstorder Depth 5.



	(*
	* Chapter 9 The tactic language
	*)

	Ltac foo foo1 foo2 foo3 := idtac.
	Ltac foo := fun foo1 foo2 foo3 => idtac.

	Ltac foo1 a b c := idtac
	with foo2 a b c := idtac
	with foo3 a b c := idtac.

	Ltac foo foo1 foo2 foo3 ::= idtac. (* redefinition *)

	Print Ltac foo.

	Set Ltac Debug.
	Unset Ltac Debug.



	(*
	* Chapter 12 Syntax extensions and interpretation scopes
	*)

	(* 12.1 Notations *)
	Notation "A <----------> B" := (foo B A).

	Notation "'This' A 'is' 'more' B" := (this_is_more A B) (at level 0, B at level 70).

	Print Grammar constr.
	Print Grammar pattern.
	Print Grammar tactic.

	Infix "<---------->" := (flip foo) (at level 80, right associativity).

	Notation "A <----------> B <----------> C" := (foo B A /\ foo C B) (at level 80, B at next level).

	Notation "A <----------> B" := (foo B A) (format "'[hv' A '/' <----------> '//' B ']'").

	Reserved Notation "A <----------> B".

	Inductive foo x y z := bar
	where "A <----------> B" := baz.
	CoInductive foo x y z := bar
	where "A <----------> B" := baz.
	Fixpoint foo x y := bar
	where "A <----------> B" := baz
	and "A >----------< B" := bazbaz.

	Set Printing Notations.
	Unset Printing Notations.

	Locate "+".

	Notation "'foo'" := bar (at level 70, a at level 80, b at next level, left associativity, right associativity, no associativity, x ident, P binder, Q closed binder, G global, X bigint, only parsing, format "").

	(* 12.2 Interpretation scopes *)

	Open Scope foo_scope.
	Close Scope foo_scope.
	Local Open Scope foo_scope.
	Local Close Scope foo_scope.
	Global Open Scope foo_scope.
	Global Close Scope foo_scope.

	Delimit Scope foo_scope with foo.

	Arguments foo x%bar y%baz.
	Arguments foo : clear scopes.

	Bind Scope foo_scope with SomeSet.
	Bind Scope foo_scope with Funclass.
	Bind Scope foo_scope with Sortclass.

	Definition foo := a%type a%nat a%N a%Z a%positive a%Q a%Qc a%real a%bool a%list a%core a%string a%char.

	Print Visibility.
	Print Visibility foo_scope.

	Print Scope foo_scope.
	Print Scopes.

	(* 12.3 Abbreviations *)
	Notation abbr := (foo bar _ baz).
	Local Notation abbr y z := (foo z y) (only parsing).

	(* 12.4 Tactic Notations *)

	Tactic Notation "foo" := idtac.
	Tactic Notation (at level 100) "bar" ident(a) simple_intropattern(a) reference(a) hyp(a) hyp_list(a) ne_hyp_list(a) constr(a) constr_list(a) ne_constr_list(a) integer(a) integer_list(a) ne_integer_list(a) int_or_var(a) int_or_var_list(a) ne_int_or_var_list(a) tactic(a) tactic0(a) tactic1(a) tactic2(a) tactic3(a) tactic4(a) tactic5(a) "baz" := idtac.