About
Go Walker displays API documentation for Go projects on Bitbucket, Github, Google Code, Launchpad and Git @ OSC.
The source code for Go Walker is available on Github(stable), Git @ OSC(beta).
Add a project to Go Walker
Go Walker generates API documentation from Go source code. The guidelines for writing documentation for the godoc tool apply to Go Walker and display object relationships between packages in your project.
It's important to write a good summary of the package in the first sentence of the package comment. Go Walker indexes the first sentence and displays the sentence in project lists.
To add a project to Go Walker, search for the peoject by import path. If Go Walker does not already have the documentation for the project, then Go Walker will fetch the source from the version control system on the fly and add the documentation. It may take up to 5 seconds because source code are contained in same page also.
Go Walker checks for package updates once per day. You can force Go Walker to refresh the documentation immediately by clicking the refresh link at the bottom of the package documentation page.
Remove a package from Go Walker
Go Walker automatically removes packages deleted from the version control system when Go Walker checks for updates to the package. You can force Go Walker to remove a deleted package immediately by clicking the refresh link at the bottom of the package documentation page, but be aware that this operation will not delete dependencies packages in case other packages use some of them.
If you do not want Go Walker to display documentation for your package, please open an issue with the import path of the path of the package that you want to remove.
Control panel
Go Walker has control panel for keyboard shortcuts for navigating package documentation pages. Type '?' on a package page for help. Thanks for chenwenli.
Add or remove labels for your project
Like we show the different categories in Labels page, you can also label your project by appending tags to URL or press g + t
to call control panel in documentation page. For example, Qbs is a ORM, so to lable it by typing github.com/coocood/qbs:tag=orm in the search box, or just visit gowalker.org/github.com/coocood/qbs:l=orm, and use :rl= to remove labels from your project.
Help translate site to your language
Go Walker supports multiple languages for site user interface. You can translate files under folder "views" to help Go Walker support your language.
Multiple language documentation
If your project directories contain readme(.md) files, Go Walker uses readme(.md) for English version, readme_[zh|cn](.md) for Chinese version. Go Walker shows them according to user language option.
Feedback
Send your ideas, feature requests and questions to joe2010xtmf#163.com. Report bugs using the Github Issue Tracker. Join the discussion at the Go Walker group.
Bookmarklet
The Go Walker bookmarklet navigates from pages on Bitbucket, Github Launchpad, Google code and Git @ OSC to the package documentation. To install the bookmarklet, click and drag the following link to your bookmark bar: Go Walker Bookmarklet.


PropPropositions and Evidence
(* $Date: 2012-07-23 16:26:25 -0400 (Mon, 23 Jul 2012) $ *)
Require Export Poly.
In previous chapters, we have seen many examples of factual
claims (propositions) and ways of presenting evidence of their
truth (proofs). In particular, we have worked extensively with
equality propositions of the form e1 = e2, with
implications (P → Q), and with quantified propositions
(∀ x, P).
In this chapter we take a deeper look at the way propositions are
expressed in Coq and at the structure of the logical evidence that
we construct when we carry out proofs.
Some of the concepts in this chapter may seem a bit abstract on a
first encounter. We've included a lot of exercises, most of
which should be quite approachable even if you're still working on
understanding the details of the text. Try to work as many of
them as you can, especially the one-starred exercises.
Inductively Defined Propositions
- Rule b_0: The number 0 is beautiful.
- Rule b_3: The number 3 is beautiful.
- Rule b_5: The number 5 is beautiful.
- Rule b_sum: If n and m are both beautiful, then so is their sum.
| (b_0) | |
| beautiful 0 |
| (b_3) | |
| beautiful 3 |
| (b_5) | |
| beautiful 5 |
| beautiful n beautiful m | (b_sum) |
| beautiful (n+m) |
----------- (b_3) ----------- (b_5)
beautiful 3 beautiful 5
------------------------------- (b_sum)
beautiful 8
Of course, there are other ways of using these rules to argue that
8 is beautiful — for instance:
beautiful 3 beautiful 5
------------------------------- (b_sum)
beautiful 8
----------- (b_5) ----------- (b_3)
beautiful 5 beautiful 3
------------------------------- (b_sum)
beautiful 8
beautiful 5 beautiful 3
------------------------------- (b_sum)
beautiful 8
Exercise: 1 star (varieties_of_beauty)
How many different ways are there to show that 8 is beautiful?(* FILL IN HERE *)
☐
In Coq, we can express the definition of beautiful as
follows:
Inductive beautiful : nat → Prop :=
b_0 : beautiful 0
| b_3 : beautiful 3
| b_5 : beautiful 5
| b_sum : ∀n m, beautiful n → beautiful m → beautiful (n+m).
The first line declares that beautiful is a proposition — or,
more formally, a family of propositions "indexed by" natural
numbers. (For each number n, the claim that "n is
beautiful" is a proposition.) Such a family of propositions is
often called a property of numbers.
Each of the remaining lines embodies one of the rules for
beautiful numbers.
We can use Coq's tactic scripting facility to assemble proofs that
particular numbers are beautiful.
Theorem three_is_beautiful: beautiful 3.
Proof.
(* This simply follows from the axiom b_3. *)
apply b_3.
Qed.
Theorem eight_is_beautiful: beautiful 8.
Proof.
(* First we use the rule b_sum, telling Coq how to
instantiate n and m. *)
apply b_sum with (n:=3) (m:=5).
(* To solve the subgoals generated by b_sum, we must provide
evidence of beautiful 3 and beautiful 5. Fortunately we
have axioms for both. *)
apply b_3.
apply b_5.
Qed.
Proof Objects
propositions ~ types evidence ~ dataMany useful things follow from this connection. To begin with, it gives us a natural interpretation of the b_sum constructor:
b_sum : ∀ n m,
beautiful n → beautiful m → beautiful (n+m).
If we read : as "has type," this says that b_sum is a data
constructor that takes four arguments: two numbers, n and m,
and two values of type beautiful n and beautiful m. That is,
b_sum can be viewed as a function that, given evidence for the
propositions beautiful n and beautiful m, gives us evidence
for the proposition that beautiful (n+m).
beautiful n → beautiful m → beautiful (n+m).
Check (b_sum 3 5 b_3 b_5).
The expression b_sum 3 5 b_3 b_5 can be thought of as
instantiating the parameterized constructor b_sum with the
specific arguments 3 5 and the corresponding proof objects for
its premises beautiful 3 and beautiful 5 (Coq is smart enough
to figure out that 3+5=8). Alternatively, we can think of b_sum
as a primitive "evidence constructor" that, when applied to two
particular numbers, wants to be further applied to evidence that
those two numbers are beautiful; its type,
[
∀ n m, beautiful n → beautiful m → beautiful (n+m),
]
expresses this functionality, in the same way that the polymorphic
type ∀ X, list X in the previous chapter expressed the fact
that the constructor nil can be thought of as a function from
types to empty lists with elements of that type.
This gives us an alternative way to write the proof that 8 is
beautiful:
Theorem eight_is_beautiful': beautiful 8.
Proof.
apply (b_sum 3 5 b_3 b_5).
Qed.
Notice that we're using apply here in a new way: instead of just
supplying the name of a hypothesis or previously proved theorem
whose type matches the current goal, we are supplying an
expression that directly builds evidence with the required
type.
Proof Scripts and Proof Objects
Theorem eight_is_beautiful'': beautiful 8.
Proof.
apply b_sum with (n:=3) (m:=5).
Show Proof.
apply b_3.
Show Proof.
apply b_5.
Show Proof.
Qed.
At any given moment, Coq has constructed a term with some
"holes" (indicated by ?1, ?2, and so on), and it knows what
type of evidence is needed at each hole. In the Show Proof
output, lines of the form ?1 → beautiful n record these
requirements. (The → here has nothing to do with either
implication or function types — it is just an unfortunate choice
of concrete syntax for the output!)
Each of the holes corresponds to a subgoal, and the proof is
finished when there are no more subgoals. At this point, the
Theorem command gives a name to the evidence we've built and
stores it in the global context.
Tactic proofs are useful and convenient because they avoid
building proof trees by hand, but they are not essential: in
principle, we can always construct the required evidence by hand.
Indeed, we don't even need the Theorem command: we can use
Definition instead, to directly give a global name to a piece of
evidence.
Definition eight_is_beautiful''' : beautiful 8 :=
b_sum 3 5 b_3 b_5.
All these different ways of building the proof lead to exactly the
same evidence being saved in the global environment.
Print eight_is_beautiful.
(* ===> eight_is_beautiful = b_sum 3 5 b_3 b_5 : beautiful 8 *)
Print eight_is_beautiful'.
(* ===> eight_is_beautiful' = b_sum 3 5 b_3 b_5 : beautiful 8 *)
Print eight_is_beautiful''.
(* ===> eight_is_beautiful'' = b_sum 3 5 b_3 b_5 : beautiful 8 *)
Print eight_is_beautiful'''.
(* ===> eight_is_beautiful''' = b_sum 3 5 b_3 b_5 : beautiful 8 *)
Exercise: 1 star (six_is_beautiful)
Give a tactic proof and a proof object showing that 6 is beautiful.Theorem six_is_beautiful :
beautiful 6.
Proof.
(* FILL IN HERE *) Admitted.
Definition six_is_beautiful' : beautiful 6 :=
(* FILL IN HERE *) admit.
☐
Exercise: 1 star (nine_is_beautiful)
Give a tactic proof and a proof object showing that 9 is beautiful.Theorem nine_is_beautiful :
beautiful 9.
Proof.
(* FILL IN HERE *) Admitted.
Definition nine_is_beautiful' : beautiful 9 :=
(* FILL IN HERE *) admit.
☐
Implications and Functions
Theorem b_plus3: ∀n, beautiful n → beautiful (3+n).
Proof.
intros n H.
apply b_sum.
apply b_3.
apply H.
Qed.
What is the proof object corresponding to b_plus3?
We've made a notational pun between → as implication and →
as the type of functions. If we take this pun seriously, then
what we're looking for is an expression whose type is
∀ n, beautiful n → beautiful (3+n) — that is, a
function that takes two arguments (one number and a piece of
evidence) and returns a piece of evidence!  Another equivalent way to write this definition is:
Definition b_plus3'' (n : nat) (H : beautiful n) : beautiful (3+n) :=
b_sum 3 n b_3 H.
Check b_plus3''.
(* ===> b_plus3'' : forall n, beautiful n -> beautiful (3+n) *)
Theorem b_times2: ∀n, beautiful n → beautiful (2*n).
Proof.
(* FILL IN HERE *) Admitted.
Proof.
(* FILL IN HERE *) Admitted.
Definition b_times2': ∀n, beautiful n → beautiful (2*n) :=
(* FILL IN HERE *) admit.
Theorem b_timesm: ∀n m, beautiful n → beautiful (m*n).
Proof.
(* FILL IN HERE *) Admitted.
Proof.
(* FILL IN HERE *) Admitted.
☐
Induction Over Proof Objects
Inductive gorgeous : nat → Prop :=
g_0 : gorgeous 0
| g_plus3 : ∀n, gorgeous n → gorgeous (3+n)
| g_plus5 : ∀n, gorgeous n → gorgeous (5+n).
Exercise: 1 star (gorgeous_tree)
Write out the definition of gorgeous numbers using the inference rule notation.☐
Theorem gorgeous__beautiful : ∀n,
gorgeous n → beautiful n.
Proof.
intros.
(* The argument proceeds by induction on the evidence H! *)
induction H as [|n'|n'].
Case "g_0".
apply b_0.
Case "g_plus3".
apply b_sum. apply b_3.
apply IHgorgeous.
Case "g_plus5".
apply b_sum. apply b_5. apply IHgorgeous.
Qed.
Let's see what happens if we try to prove this by induction on n
instead of induction on the evidence H.
Theorem gorgeous__beautiful_FAILED : ∀n,
gorgeous n → beautiful n.
Proof.
intros. induction n as [| n'].
Case "n = 0". apply b_0.
Case "n = S n'". (* We are stuck! *)
Admitted.
Theorem gorgeous_plus13: ∀n,
gorgeous n → gorgeous (13+n).
Proof.
(* FILL IN HERE *) Admitted.
gorgeous n → gorgeous (13+n).
Proof.
(* FILL IN HERE *) Admitted.
Definition gorgeous_plus13_po: ∀n, gorgeous n → gorgeous (13+n):=
(* FILL IN HERE *) admit.
Theorem gorgeous_sum : ∀n m,
gorgeous n → gorgeous m → gorgeous (n + m).
Proof.
(* FILL IN HERE *) Admitted.
gorgeous n → gorgeous m → gorgeous (n + m).
Proof.
(* FILL IN HERE *) Admitted.
Theorem beautiful__gorgeous : ∀n, beautiful n → gorgeous n.
Proof.
(* FILL IN HERE *) Admitted.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, optional (b_times2)
Prove the g_times2 theorem below without using gorgeous__beautiful. You might find the following helper lemma useful.Lemma helper_g_times2 : ∀x y z, x + (z + y)= z + x + y.
Proof.
(* FILL IN HERE *) Admitted.
Theorem g_times2: ∀n, gorgeous n → gorgeous (2*n).
Proof.
intros n H. simpl.
induction H.
(* FILL IN HERE *) Admitted.
☐
Evenness
Definition even (n:nat) : Prop :=
evenb n = true.
That is, we can define "n is even" to mean "the function
evenb returns true when applied to n."
Another alternative is to define the concept of evenness directly.
Instead of going via the evenb function ("a number is even if a
certain computation yields true"), we can say what the concept
of evenness means by giving two different ways of presenting
evidence that a number is even.
Inductive ev : nat → Prop :=
| ev_0 : ev O
| ev_SS : ∀n:nat, ev n → ev (S (S n)).
This definition says that there are two ways to give
evidence that a number m is even. First, 0 is even, and
ev_0 is evidence for this. Second, if m = S (S n) for some
n and we can give evidence e that n is even, then m is
also even, and ev_SS n e is the evidence.
Exercise: 1 star (double_even)
Construct a tactic proof of the following proposition.Theorem double_even : ∀n,
ev (double n).
Proof.
(* FILL IN HERE *) Admitted.
☐
We have seen that the proposition "some number is even" can
be phrased in two different ways — indirectly, via a boolean
testing function evenb, or directly, by inductively describing
what constitutes evidence for evenness. These two ways of
defining evenness are about equally easy to state and work with.
Which we choose is basically a question of taste.
However, for many other properties of interest, the direct
inductive definition is preferable, since writing a testing
function may be awkward or even impossible.
One such property is beautiful. This is a perfectly sensible
definition of a set of numbers, but we cannot translate its
definition directly as a Coq Fixpoint (or translate it directly
into a recursive function in any other programming language). We
might be able to find a clever way of testing this property using
a Fixpoint (indeed, it is not too hard to find one in this
case), but in general this could require arbitrarily deep
thinking. In fact, if the property we are interested in is
uncomputable, then we cannot define it as a Fixpoint no matter
how hard we try, because Coq requires that all Fixpoints
correspond to terminating computations.
On the other hand, writing an inductive definition of what it
means to give evidence for the property beautiful is
straightforward.
Exercise: 4 stars, optional (double_even_pfobj)
Try to predict what proof object is constructed by the above tactic proof. (Before checking your answer, you'll want to strip out any uses of Case, as these will make the proof object look a bit cluttered.) ☐Discussion: Computational vs. Inductive Definitions
Inverting Evidence
Theorem ev_minus2: ∀n,
ev n → ev (pred (pred n)).
Proof.
intros n E.
destruct E as [| n' E'].
Case "E = ev_0". simpl. apply ev_0.
Case "E = ev_SS n' E'". simpl. apply E'. Qed.
Exercise: 1 star, optional (ev_minus2_n)
What happens if we try to destruct on n instead of E? ☐Exercise: 1 star, recommended (ev__even)
Here is a proof that the inductive definition of evenness implies the computational one.Theorem ev__even : ∀n,
ev n → even n.
Proof.
intros n E. induction E as [| n' E'].
Case "E = ev_0".
unfold even. reflexivity.
Case "E = ev_SS n' E'".
unfold even. apply IHE'.
Qed.
Could this proof also be carried out by induction on n instead
of E? If not, why not?
(* FILL IN HERE *)
☐
The induction principle for inductively defined propositions does
not follow quite the same form as that of inductively defined
sets. For now, you can take the intuitive view that induction on
evidence ev n is similar to induction on n, but restricts our
attention to only those numbers for which evidence ev n could be
generated. We'll look at the induction principle of ev in more
depth below, to explain what's really going on.
(* FILL IN HERE *)
☐
Exercise: 1 star (l_fails)
The following proof attempt will not succeed.
Theorem l : ∀ n,
ev n.
Proof.
intros n. induction n.
Case "O". simpl. apply ev_0.
Case "S".
...
Briefly explain why.
ev n.
Proof.
intros n. induction n.
Case "O". simpl. apply ev_0.
Case "S".
...
☐
Exercise: 2 stars (ev_sum)
Here's another exercise requiring induction.Theorem ev_sum : ∀n m,
ev n → ev m → ev (n+m).
Proof.
(* FILL IN HERE *) Admitted.
☐
Here's another situation where we want to analyze evidence for
evenness: proving that if n+2 is even, then n is. Our first
idea might be to use destruct for this kind of case analysis:
Theorem SSev_ev_firsttry : ∀n,
ev (S (S n)) → ev n.
Proof.
intros n E.
destruct E as [| n' E'].
(* Stuck: destruct gives us un-provable subgoal here! *)
Admitted.
In the first sub-goal, we've lost the information that n is 0.
We could have used remember, but then we still need inversion
on both cases.
Theorem SSev_ev_secondtry : ∀n,
ev (S (S n)) → ev n.
Proof.
intros n E. remember (S (S n)) as n2.
destruct E as [| n' E'].
Case "n = 0". inversion Heqn2.
Case "n = S n'". inversion Heqn2. rewrite ← H0. apply E'.
Qed.
There is a much simpler way to this: we can use inversion directly
on the inductively defined proposition ev (S (S n)).
Theorem SSev__even : ∀n,
ev (S (S n)) → ev n.
Proof.
intros n E. inversion E as [| n' E']. apply E'. Qed.
(* Print SSev__even. *)
This use of inversion may seem a bit mysterious at first.
Until now, we've only used inversion on equality
propositions, to utilize injectivity of constructors or to
discriminate between different constructors. But we see here
that inversion can also be applied to analyzing evidence
for inductively defined propositions.
Here's how inversion works in general. Suppose the name
I refers to an assumption P in the current context, where
P has been defined by an Inductive declaration. Then,
for each of the constructors of P, inversion I generates
a subgoal in which I has been replaced by the exact,
specific conditions under which this constructor could have
been used to prove P. Some of these subgoals will be
self-contradictory; inversion throws these away. The ones
that are left represent the cases that must be proved to
establish the original goal.
In this particular case, the inversion analyzed the construction
ev (S (S n)), determined that this could only have been
constructed using ev_SS, and generated a new subgoal with the
arguments of that constructor as new hypotheses. (It also
produced an auxiliary equality, which happens to be useless here.)
We'll begin exploring this more general behavior of inversion in
what follows.
Exercise: 1 star (inversion_practice)
Theorem SSSSev__even : ∀n,
ev (S (S (S (S n)))) → ev n.
Proof.
(* FILL IN HERE *) Admitted.
ev (S (S (S (S n)))) → ev n.
Proof.
(* FILL IN HERE *) Admitted.
The inversion tactic can also be used to derive goals by showing
the absurdity of a hypothesis.
Theorem even5_nonsense :
ev 5 → 2 + 2 = 9.
Proof.
(* FILL IN HERE *) Admitted.
☐
We can generally use inversion on inductive propositions.
This illustrates that in general, we get one case for each
possible constructor. Again, we also get some auxiliary
equalities that are rewritten in the goal but not in the other
hypotheses.
Theorem ev_minus2': ∀n,
ev n → ev (pred (pred n)).
Proof.
intros n E. inversion E as [| n' E'].
Case "E = ev_0". simpl. apply ev_0.
Case "E = ev_SS n' E'". simpl. apply E'. Qed.
Exercise: 3 stars, recommended (ev_ev__ev)
Finding the appropriate thing to do induction on is a bit tricky here:Theorem ev_ev__ev : ∀n m,
ev (n+m) → ev n → ev m.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, optional (ev_plus_plus)
Here's an exercise that just requires applying existing lemmas. No induction or even case analysis is needed, but some of the rewriting may be tedious. You'll want the replace tactic used for plus_swap' in Basics.vTheorem ev_plus_plus : ∀n m p,
ev (n+m) → ev (n+p) → ev (m+p).
Proof.
(* FILL IN HERE *) Admitted.
☐
Programming with Propositions
Check (2 + 2 = 4).
(* ===> 2 + 2 = 4 : Prop *)
Check (ble_nat 3 2 = false).
(* ===> ble_nat 3 2 = false : Prop *)
Check (beautiful 8).
(* ===> beautiful 8 : Prop *)
Both provable and unprovable claims are perfectly good
propositions. Simply being a proposition is one thing; being
provable is something else!
Check (2 + 2 = 5).
(* ===> 2 + 2 = 5 : Prop *)
Check (beautiful 4).
(* ===> beautiful 4 : Prop *)
Both 2 + 2 = 4 and 2 + 2 = 5 are legal expressions
of type Prop.
We've seen one way that propositions can be used in Coq: in
Theorem (and Lemma and Example) declarations.
Theorem plus_2_2_is_4 :
2 + 2 = 4.
Proof. reflexivity. Qed.
But they can be used in many other ways. For example, we
can give a name to a proposition using a Definition, just as we
have given names to expressions of other sorts (numbers,
functions, types, type functions, ...).
Definition plus_fact : Prop := 2 + 2 = 4.
Check plus_fact.
(* ===> plus_fact : Prop *)
Now we can use this name in any situation where a proposition is
expected — for example, as the claim in a Theorem
declaration.
Theorem plus_fact_is_true :
plus_fact.
Proof. reflexivity. Qed.
There are many ways of constructing propositions. We can define a
new proposition primitively using Inductive, we can form an
equality proposition from two computational expressions, and we
can build up a new proposition from existing ones using
implication and quantification.
Definition strange_prop1 : Prop :=
(2 + 2 = 5) → (99 + 26 = 42).
Also, given a proposition P with a free variable n, we can
form the proposition ∀ n, P.
Definition strange_prop2 :=
∀n, (ble_nat n 17 = true) → (ble_nat n 99 = true).
We can also define parameterized propositions, such as
the property of being even.
Check even.
(* ===> even : nat -> Prop *)
Check (even 4).
(* ===> even 4 : Prop *)
Check (even 3).
(* ===> even 3 : Prop *)
The type of even, nat→Prop, can be pronounced in three
equivalent ways: (1) "even is a function from numbers to
propositions," (2) "even is a family of propositions, indexed
by a number n," or (3) "even is a property of numbers."
Propositions — including parameterized propositions — are
first-class citizens in Coq. For example, we can define them to
take multiple arguments...
Definition between (n m o: nat) : Prop :=
andb (ble_nat n o) (ble_nat o m) = true.
... and then partially apply them:
Definition teen : nat→Prop := between 13 19.
We can even pass propositions — including parameterized
propositions — as arguments to functions:
Definition true_for_zero (P:nat→Prop) : Prop :=
P 0.
Here are two more examples of passing parameterized propositions
as arguments to a function. The first takes a proposition P as
argument and builds the proposition that P is true for all
natural numbers. The second takes P and builds the proposition
that, if P is true for some natural number n', then it is also
true by the successor of n' — i.e. that P is preserved by
successor:
Definition true_for_all_numbers (P:nat→Prop) : Prop :=
∀n, P n.
Definition preserved_by_S (P:nat→Prop) : Prop :=
∀n', P n' → P (S n').
Induction Principles
Induction Principles for Inductively Defined Types
Check nat_ind.
(* ===> nat_ind :
forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n *)
The induction tactic is a straightforward wrapper that, at
its core, simply performs apply t_ind. To see this more
clearly, let's experiment a little with using apply nat_ind
directly, instead of the induction tactic, to carry out some
proofs. Here, for example, is an alternate proof of a theorem
that we saw in the Basics chapter.
Theorem mult_0_r' : ∀n:nat,
n * 0 = 0.
Proof.
apply nat_ind.
Case "O". reflexivity.
Case "S". simpl. intros n IHn. rewrite → IHn.
reflexivity. Qed.
This proof is basically the same as the earlier one, but a
few minor differences are worth noting. First, in the induction
step of the proof (the "S" case), we have to do a little
bookkeeping manually (the intros) that induction does
automatically.
Second, we do not introduce n into the context before applying
nat_ind — the conclusion of nat_ind is a quantified formula,
and apply needs this conclusion to exactly match the shape of
the goal state, including the quantifier. The induction tactic
works either with a variable in the context or a quantified
variable in the goal.
Third, the apply tactic automatically chooses variable names for
us (in the second subgoal, here), whereas induction lets us
specify (with the as... clause) what names should be used. The
automatic choice is actually a little unfortunate, since it
re-uses the name n for a variable that is different from the n
in the original theorem. This is why the Case annotation is
just S — if we tried to write it out in the more explicit form
that we've been using for most proofs, we'd have to write n = S
n, which doesn't make a lot of sense! All of these conveniences
make induction nicer to use in practice than applying induction
principles like nat_ind directly. But it is important to
realize that, modulo this little bit of bookkeeping, applying
nat_ind is what we are really doing.
Exercise: 2 stars, optional (plus_one_r')
Complete this proof as we did mult_0_r' above, without using the induction tactic.Theorem plus_one_r' : ∀n:nat,
n + 1 = S n.
Proof.
(* FILL IN HERE *) Admitted.
☐
The induction principles that Coq generates for other datatypes
defined with Inductive follow a similar pattern. If we define a
type t with constructors c1 ... cn, Coq generates a theorem
with this shape:
t_ind :
∀ P : t → Prop,
... case for c1 ... →
... case for c2 ... →
... →
... case for cn ... →
∀ n : t, P n
The specific shape of each case depends on the arguments to the
corresponding constructor. Before trying to write down a general
rule, let's look at some more examples. First, an example where
the constructors take no arguments:
∀ P : t → Prop,
... case for c1 ... →
... case for c2 ... →
... →
... case for cn ... →
∀ n : t, P n
Inductive yesno : Type :=
| yes : yesno
| no : yesno.
Check yesno_ind.
(* ===> yesno_ind : forall P : yesno -> Prop,
P yes ->
P no ->
forall y : yesno, P y *)
Exercise: 1 star (rgb)
Write out the induction principle that Coq will generate for the following datatype. Write down your answer on paper, and then compare it with what Coq prints.Inductive rgb : Type :=
| red : rgb
| green : rgb
| blue : rgb.
Check rgb_ind.
☐
Here's another example, this time with one of the constructors
taking some arguments.
Inductive natlist : Type :=
| nnil : natlist
| ncons : nat → natlist → natlist.
Check natlist_ind.
(* ===> (modulo a little tidying)
natlist_ind :
forall P : natlist -> Prop,
P nnil ->
(forall (n : nat) (l : natlist), P l -> P (ncons n l)) ->
forall n : natlist, P n *)
Inductive natlist1 : Type :=
| nnil1 : natlist1
| nsnoc1 : natlist1 → nat → natlist1.
Now what will the induction principle look like? ☐
From these examples, we can extract this general rule:
- The type declaration gives several constructors; each corresponds to one clause of the induction principle.
- Each constructor c takes argument types a1...an.
- Each ai can be either t (the datatype we are defining) or some other type s.
- The corresponding case of the induction principle
says (in English):
- "for all values x1...xn of types a1...an, if P holds for each of the xs of type t, then P holds for c x1 ... xn".
Exercise: 1 star (ex_set)
Here is an induction principle for an inductively defined set.
ExSet_ind :
∀ P : ExSet → Prop,
(∀ b : bool, P (con1 b)) →
(∀ (n : nat) (e : ExSet), P e → P (con2 n e)) →
∀ e : ExSet, P e
Give an Inductive definition of ExSet:
∀ P : ExSet → Prop,
(∀ b : bool, P (con1 b)) →
(∀ (n : nat) (e : ExSet), P e → P (con2 n e)) →
∀ e : ExSet, P e
Inductive ExSet : Type :=
(* FILL IN HERE *)
.
☐
What about polymorphic datatypes?
The inductive definition of polymorphic lists
Inductive list (X:Type) : Type :=
| nil : list X
| cons : X → list X → list X.
is very similar to that of natlist. The main difference is
that, here, the whole definition is parameterized on a set X:
that is, we are defining a family of inductive types list X,
one for each X. (Note that, wherever list appears in the body
of the declaration, it is always applied to the parameter X.)
The induction principle is likewise parameterized on X:
| nil : list X
| cons : X → list X → list X.
list_ind :
∀ (X : Type) (P : list X → Prop),
P [] →
(∀ (x : X) (l : list X), P l → P (x :: l)) →
∀ l : list X, P l
Note the wording here (and, accordingly, the form of list_ind):
The whole induction principle is parameterized on X. That is,
list_ind can be thought of as a polymorphic function that, when
applied to a type X, gives us back an induction principle
specialized to the type list X.
∀ (X : Type) (P : list X → Prop),
P [] →
(∀ (x : X) (l : list X), P l → P (x :: l)) →
∀ l : list X, P l
Exercise: 1 star (tree)
Write out the induction principle that Coq will generate for the following datatype. Compare your answer with what Coq prints.Inductive tree (X:Type) : Type :=
| leaf : X → tree X
| node : tree X → tree X → tree X.
Check tree_ind.
☐
Exercise: 1 star (mytype)
Find an inductive definition that gives rise to the following induction principle:
mytype_ind :
∀ (X : Type) (P : mytype X → Prop),
(∀ x : X, P (constr1 X x)) →
(∀ n : nat, P (constr2 X n)) →
(∀ m : mytype X, P m →
∀ n : nat, P (constr3 X m n)) →
∀ m : mytype X, P m
☐
∀ (X : Type) (P : mytype X → Prop),
(∀ x : X, P (constr1 X x)) →
(∀ n : nat, P (constr2 X n)) →
(∀ m : mytype X, P m →
∀ n : nat, P (constr3 X m n)) →
∀ m : mytype X, P m
Exercise: 1 star, optional (foo)
Find an inductive definition that gives rise to the following induction principle:
foo_ind :
∀ (X Y : Type) (P : foo X Y → Prop),
(∀ x : X, P (bar X Y x)) →
(∀ y : Y, P (baz X Y y)) →
(∀ f1 : nat → foo X Y,
(∀ n : nat, P (f1 n)) → P (quux X Y f1)) →
∀ f2 : foo X Y, P f2
☐
∀ (X Y : Type) (P : foo X Y → Prop),
(∀ x : X, P (bar X Y x)) →
(∀ y : Y, P (baz X Y y)) →
(∀ f1 : nat → foo X Y,
(∀ n : nat, P (f1 n)) → P (quux X Y f1)) →
∀ f2 : foo X Y, P f2
Exercise: 1 star, optional (foo')
Consider the following inductive definition:Inductive foo' (X:Type) : Type :=
| C1 : list X → foo' X → foo' X
| C2 : foo' X.
What induction principle will Coq generate for foo'? Fill
in the blanks, then check your answer with Coq.)
☐
foo'_ind :
∀ (X : Type) (P : foo' X → Prop),
(∀ (l : list X) (f : foo' X),
_______________________ →
_______________________ ) →
___________________________________________ →
∀ f : foo' X, ________________________
∀ (X : Type) (P : foo' X → Prop),
(∀ (l : list X) (f : foo' X),
_______________________ →
_______________________ ) →
___________________________________________ →
∀ f : foo' X, ________________________
Induction Hypotheses
∀ P : nat → Prop,
P 0 →
(∀ n : nat, P n → P (S n)) →
∀ n : nat, P n
is a generic statement that holds for all propositions
P (strictly speaking, for all families of propositions P
indexed by a number n). Each time we use this principle, we
are choosing P to be a particular expression of type
nat→Prop.
P 0 →
(∀ n : nat, P n → P (S n)) →
∀ n : nat, P n
Definition P_m0r (n:nat) : Prop :=
n * 0 = 0.
... or equivalently...
Definition P_m0r' : nat→Prop :=
fun n => n * 0 = 0.
Now when we do the proof it is easier to see where P_m0r
appears.
Theorem mult_0_r'' : ∀n:nat,
P_m0r n.
Proof.
apply nat_ind.
Case "n = O". reflexivity.
Case "n = S n'".
(* Note the proof state at this point! *)
unfold P_m0r. simpl. intros n' IHn'.
apply IHn'. Qed.
This extra naming step isn't something that we'll do in
normal proofs, but it is useful to do it explicitly for an example
or two, because it allows us to see exactly what the induction
hypothesis is. If we prove ∀ n, P_m0r n by induction on
n (using either induction or apply nat_ind), we see that the
first subgoal requires us to prove P_m0r 0 ("P holds for
zero"), while the second subgoal requires us to prove ∀ n',
P_m0r n' → P_m0r n' (S n') (that is "P holds of S n' if it
holds of n'" or, more elegantly, "P is preserved by S").
The induction hypothesis is the premise of this latter
implication — the assumption that P holds of n', which we are
allowed to use in proving that P holds for S n'.
Optional Material
Induction Principles in Prop
Inductive gorgeous : nat → Prop :=
g_0 : gorgeous 0
| g_plus3 : ∀ n, gorgeous n → gorgeous (3+m)
| g_plus5 : ∀ n, gorgeous n → gorgeous (5+m).
...to give rise to an induction principle that looks like this...
g_0 : gorgeous 0
| g_plus3 : ∀ n, gorgeous n → gorgeous (3+m)
| g_plus5 : ∀ n, gorgeous n → gorgeous (5+m).
gorgeous_ind_max :
∀ P : (∀ n : nat, gorgeous n → Prop),
P O g_0 →
(∀ (m : nat) (e : gorgeous m),
P m e → P (3+m) (g_plus3 m e) →
(∀ (m : nat) (e : gorgeous m),
P m e → P (5+m) (g_plus5 m e) →
∀ (n : nat) (e : gorgeous n), P n e
... because:
∀ P : (∀ n : nat, gorgeous n → Prop),
P O g_0 →
(∀ (m : nat) (e : gorgeous m),
P m e → P (3+m) (g_plus3 m e) →
(∀ (m : nat) (e : gorgeous m),
P m e → P (5+m) (g_plus5 m e) →
∀ (n : nat) (e : gorgeous n), P n e
- Since gorgeous is indexed by a number n (every gorgeous
object e is a piece of evidence that some particular number
n is gorgeous), the proposition P is parameterized by both
n and e — that is, the induction principle can be used to
prove assertions involving both a gorgeous number and the
evidence that it is gorgeous.
- Since there are three ways of giving evidence of gorgeousness
(gorgeous has three constructors), applying the induction
principle generates three subgoals:
- We must prove that P holds for O and b_0.
- We must prove that, whenever n is a gorgeous
number and e is an evidence of its gorgeousness,
if P holds of n and e,
then it also holds of 3+m and g_plus3 n e.
- We must prove that, whenever n is a gorgeous
number and e is an evidence of its gorgeousness,
if P holds of n and e,
then it also holds of 5+m and g_plus5 n e.
- We must prove that P holds for O and b_0.
- If these subgoals can be proved, then the induction principle tells us that P is true for all gorgeous numbers n and evidence e of their gorgeousness.
∀ P : nat → Prop,
... →
∀ n : nat, gorgeous n → P n
For this reason, Coq actually generates the following simplified
induction principle for gorgeous:
... →
∀ n : nat, gorgeous n → P n
Check gorgeous_ind.
(* ===> gorgeous_ind
: forall P : nat -> Prop,
P 0 ->
(forall n : nat, gorgeous n -> P n -> P (3 + n)) ->
(forall n : nat, gorgeous n -> P n -> P (5 + n)) ->
forall n : nat, gorgeous n -> P n *)
In particular, Coq has dropped the evidence term e as a
parameter of the the proposition P, and consequently has
rewritten the assumption ∀ (n : nat) (e: gorgeous n), ...
to be ∀ (n : nat), gorgeous n → ...; i.e., we no longer
require explicit evidence of the provability of gorgeous n.
In English, gorgeous_ind says:
We can apply gorgeous_ind directly instead of using induction.
- Suppose, P is a property of natural numbers (that is, P n is
a Prop for every n). To show that P n holds whenever n
is gorgeous, it suffices to show:
- P holds for 0,
- for any n, if n is gorgeous and P holds for
n, then P holds for 3+n,
- for any n, if n is gorgeous and P holds for n, then P holds for 5+n.
- P holds for 0,
Theorem gorgeous__beautiful' : ∀n, gorgeous n → beautiful n.
Proof.
intros.
apply gorgeous_ind.
Case "g_0".
apply b_0.
Case "g_plus3".
intros.
apply b_sum. apply b_3.
apply H1.
Case "g_plus5".
intros.
apply b_sum. apply b_5.
apply H1.
apply H.
Qed.
Module P.
Inductive p : (tree nat) → nat → Prop :=
| c1 : ∀n, p (leaf _ n) 1
| c2 : ∀t1 t2 n1 n2,
p t1 n1 → p t2 n2 → p (node _ t1 t2) (n1 + n2)
| c3 : ∀t n, p t n → p t (S n).
Describe, in English, the conditions under which the
proposition p t n is provable.
(* FILL IN HERE *)
☐
☐
End P.
More on the induction Tactic
- If P n is some proposition involving a natural number n, and
we want to show that P holds for all numbers n, we can
reason like this:
- show that P O holds
- show that, if P n' holds, then so does P (S n')
- conclude that P n holds for all n.
Theorem plus_assoc' : ∀n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
(* ...we first introduce all 3 variables into the context,
which amounts to saying "Consider an arbitrary n, m, and
p..." *)
intros n m p.
(* ...We now use the induction tactic to prove P n (that
is, n + (m + p) = (n + m) + p) for _all_ n,
and hence also for the particular n that is in the context
at the moment. *)
induction n as [| n'].
Case "n = O". reflexivity.
Case "n = S n'".
(* In the second subgoal generated by induction -- the
"inductive step" -- we must prove that P n' implies
P (S n') for all n'. The induction tactic
automatically introduces n' and P n' into the context
for us, leaving just P (S n') as the goal. *)
simpl. rewrite → IHn'. reflexivity. Qed.
It also works to apply induction to a variable that is
quantified in the goal.
Theorem plus_comm' : ∀n m : nat,
n + m = m + n.
Proof.
induction n as [| n'].
Case "n = O". intros m. rewrite → plus_0_r. reflexivity.
Case "n = S n'". intros m. simpl. rewrite → IHn'.
rewrite ← plus_n_Sm. reflexivity. Qed.
Note that induction n leaves m still bound in the goal —
i.e., what we are proving inductively is a statement beginning
with ∀ m.
If we do induction on a variable that is quantified in the goal
after some other quantifiers, the induction tactic will
automatically introduce the variables bound by these quantifiers
into the context.
Theorem plus_comm'' : ∀n m : nat,
n + m = m + n.
Proof.
(* Let's do induction on m this time, instead of n... *)
induction m as [| m'].
Case "m = O". simpl. rewrite → plus_0_r. reflexivity.
Case "m = S m'". simpl. rewrite ← IHm'.
rewrite ← plus_n_Sm. reflexivity. Qed.
Exercise: 1 star, optional (plus_explicit_prop)
Rewrite both plus_assoc' and plus_comm' and their proofs in the same style as mult_0_r'' above — that is, for each theorem, give an explicit Definition of the proposition being proved by induction, and state the theorem and proof in terms of this defined proposition.(* FILL IN HERE *)
☐
One more quick digression, for adventurous souls: if we can define
parameterized propositions using Definition, then can we also
define them using Fixpoint? Of course we can! However, this
kind of "recursive parameterization" doesn't correspond to
anything very familiar from everyday mathematics. The following
exercise gives a slightly contrived example.
Exercise: 4 stars, optional (true_upto_n__true_everywhere)
Define a recursive function true_upto_n__true_everywhere that makes true_upto_n_example work.(*
Fixpoint true_upto_n__true_everywhere
(* FILL IN HERE *)
Example true_upto_n_example :
(true_upto_n__true_everywhere 3 (fun n => even n))
= (even 3 -> even 2 -> even 1 -> forall m : nat, even m).
Proof. reflexivity. Qed.
*)
☐
Building Proof Objects Incrementally
Definition b_16_atmpt_1 : beautiful 16 := admit.
Maybe we can use b_sum to construct a term of type beautiful 16?
Recall that b_sum is of type
If we can demonstrate the beauty of 5 and 11, we should
be done.
∀ n m : nat, beautiful n → beautiful m → beautiful (n + m)
Definition b_16_atmpt_2 : beautiful 16 := b_sum 5 11 admit admit.
In the attempt above, we've omitted the proofs of the propositions
that 5 and 11 are beautiful. But the first of these is already
axiomatized in b_5:
Definition b_16_atmpt_3 : beautiful 16 := b_sum 5 11 b_5 admit.
What remains is to show that 11 is beautiful. We repeat the
procedure:
Definition b_16_atmpt_4 : beautiful 16 :=
b_sum 5 11 b_5 (b_sum 5 6 admit admit).
Definition b_16_atmpt_5 : beautiful 16 :=
b_sum 5 11 b_5 (b_sum 5 6 b_5 admit).
Definition b_16_atmpt_6 : beautiful 16 :=
b_sum 5 11 b_5 (b_sum 5 6 b_5 (b_sum 3 3 admit admit)).
And finally, we can complete the proof object:
Definition b_16 : beautiful 16 :=
b_sum 5 11 b_5 (b_sum 5 6 b_5 (b_sum 3 3 b_3 b_3)).
To recap, we've been guided by an informal proof that we have in
our minds, and we check the high level details before completing
the intricacies of the proof. The admit term allows us to do
this.
Additional Exercises
Exercise: 4 stars, recommended (palindromes)
A palindrome is a sequence that reads the same backwards as forwards.- Define an inductive proposition pal on list X that
captures what it means to be a palindrome. (Hint: You'll need
three cases. Your definition should be based on the structure
of the list; just having a single constructor
c : ∀ l, l = rev l → pal lmay seem obvious, but will not work very well.)
- Prove that
∀ l, pal (l ++ rev l).
- Prove that
∀ l, pal l → l = rev l.
(* FILL IN HERE *)
☐
Exercise: 5 stars, optional (palindrome_converse)
Using your definition of pal from the previous exercise, prove that
∀ l, l = rev l → pal l.
(* FILL IN HERE *)
☐
Exercise: 4 stars (subsequence)
A list is a subsequence of another list if all of the elements in the first list occur in the same order in the second list, possibly with some extra elements in between. For example,
[1,2,3]
is a subsequence of each of the lists
[1,2,3]
[1,1,1,2,2,3]
[1,2,7,3]
[5,6,1,9,9,2,7,3,8]
but it is not a subsequence of any of the lists
[1,1,1,2,2,3]
[1,2,7,3]
[5,6,1,9,9,2,7,3,8]
[1,2]
[1,3]
[5,6,2,1,7,3,8]
[1,3]
[5,6,2,1,7,3,8]
- Define an inductive proposition subseq on list nat that
captures what it means to be a subsequence. (Hint: You'll need
three cases.)
- Prove that subsequence is reflexive, that is, any list is a
subsequence of itself.
- Prove that for any lists l1, l2, and l3, if l1 is a
subsequence of l2, then l1 is also a subsequence of l2 ++
l3.
- (Optional, harder) Prove that subsequence is transitive — that is, if l1 is a subsequence of l2 and l2 is a subsequence of l3, then l1 is a subsequence of l3. Hint: choose your induction carefully!
(* FILL IN HERE *)
☐
☐
☐
☐
☐
Exercise: 2 stars, optional (foo_ind_principle)
Suppose we make the following inductive definition:
Inductive foo (X : Set) (Y : Set) : Set :=
| foo1 : X → foo X Y
| foo2 : Y → foo X Y
| foo3 : foo X Y → foo X Y.
Fill in the blanks to complete the induction principle that will be
generated by Coq.
| foo1 : X → foo X Y
| foo2 : Y → foo X Y
| foo3 : foo X Y → foo X Y.
foo_ind
: ∀ (X Y : Set) (P : foo X Y → Prop),
(∀ x : X, __________________________________) →
(∀ y : Y, __________________________________) →
(________________________________________________) →
________________________________________________
: ∀ (X Y : Set) (P : foo X Y → Prop),
(∀ x : X, __________________________________) →
(∀ y : Y, __________________________________) →
(________________________________________________) →
________________________________________________
Exercise: 2 stars, optional (bar_ind_principle)
Consider the following induction principle:
bar_ind
: ∀ P : bar → Prop,
(∀ n : nat, P (bar1 n)) →
(∀ b : bar, P b → P (bar2 b)) →
(∀ (b : bool) (b0 : bar), P b0 → P (bar3 b b0)) →
∀ b : bar, P b
Write out the corresponding inductive set definition.
: ∀ P : bar → Prop,
(∀ n : nat, P (bar1 n)) →
(∀ b : bar, P b → P (bar2 b)) →
(∀ (b : bool) (b0 : bar), P b0 → P (bar3 b b0)) →
∀ b : bar, P b
Inductive bar : Set :=
| bar1 : ________________________________________
| bar2 : ________________________________________
| bar3 : ________________________________________.
| bar1 : ________________________________________
| bar2 : ________________________________________
| bar3 : ________________________________________.
Exercise: 2 stars, optional (no_longer_than_ind)
Given the following inductively defined proposition:
Inductive no_longer_than (X : Set) : (list X) → nat → Prop :=
| nlt_nil : ∀ n, no_longer_than X [] n
| nlt_cons : ∀ x l n, no_longer_than X l n →
no_longer_than X (x::l) (S n)
| nlt_succ : ∀ l n, no_longer_than X l n →
no_longer_than X l (S n).
write the induction principle generated by Coq.
| nlt_nil : ∀ n, no_longer_than X [] n
| nlt_cons : ∀ x l n, no_longer_than X l n →
no_longer_than X (x::l) (S n)
| nlt_succ : ∀ l n, no_longer_than X l n →
no_longer_than X l (S n).
no_longer_than_ind
: ∀ (X : Set) (P : list X → nat → Prop),
(∀ n : nat, ____________________) →
(∀ (x : X) (l : list X) (n : nat),
no_longer_than X l n → ____________________ →
_____________________________ →
(∀ (l : list X) (n : nat),
no_longer_than X l n → ____________________ →
_____________________________ →
∀ (l : list X) (n : nat), no_longer_than X l n →
____________________
: ∀ (X : Set) (P : list X → nat → Prop),
(∀ n : nat, ____________________) →
(∀ (x : X) (l : list X) (n : nat),
no_longer_than X l n → ____________________ →
_____________________________ →
(∀ (l : list X) (n : nat),
no_longer_than X l n → ____________________ →
_____________________________ →
∀ (l : list X) (n : nat), no_longer_than X l n →
____________________
Exercise: 2 stars, optional (R_provability)
Suppose we give Coq the following definition:
Inductive R : nat → list nat → Prop :=
| c1 : R 0 []
| c2 : ∀ n l, R n l → R (S n) (n :: l)
| c3 : ∀ n l, R (S n) l → R n l.
Which of the following propositions are provable?
| c1 : R 0 []
| c2 : ∀ n l, R n l → R (S n) (n :: l)
| c3 : ∀ n l, R (S n) l → R n l.
- R 2 [1,0]
- R 1 [1,2,1,0]
- R 6 [3,2,1,0]


Finish support for packet construction and injection via libnet. All protocols
except UDP and ICMP are implemented, but need more testing.
Support more protocol types, such as DNS and IPv6.
Test on more architectures. Currently tested on Mac OS X/PPC and
Linux/x86.
Write full documentation for the module.
Come up with better system for documentation.
Make this work on Windows. I briefly struggled with compiling using VC7 under Win XP
using winpcap and LibnetNT. No luck, and was getting some rather interesting errors
about missing header files which appeared to be where they should be :-/.


Practical browser benchmark to guage performance across various browser environments. Chrome is by far the fastest browser environment for loki.
Close console (if visible) and press start. Results will display in page when done.
This may take a minute please wait...


Invert (0.0 to 1.0)
Brightness (0.0 to 4.0)
Contrast (0.0 to 4.0)
Saturate (0.0 to 4.0)
Hue Rotate ((violet) -180 to +180 (green))
Sepia (0.0 to 1.0)
Error while trying to enlight YT :((((.


go back to the other page
[???]
type the password here:
submit
button that may help
HB: where are there some things that are better than what you thought they would be?


See:
*Other components are available
Program hardware with plain ol'JS and your favourite editor
Expose Arduino functionality over the serialport
johnny-five ⇄ serialport ⇄ Firmata ⇄ Ardunio
Good luck with your test coverage


|
GLAC
1.0
|
A class for storing the observable data. More...
#include <observablestorer.h>
Public Member Functions | |
| ObservableStorer (unsigned long int NSize) | |
| ObservableStorer::ObservableStorer. More... | |
| ~ObservableStorer () | |
| double & | operator[] (unsigned long int iObs) |
| void | gatherResults () |
| ObservableStorer::gatherResults. More... | |
| void | runStatistics () |
| ObservableStorer::runStatistics. More... | |
| void | printStatistics () |
| void | writeObservableToFile (double acceptanceRatio) |
| ObservableStorer::writeObservableToFile. More... | |
| void | writeFlowObservableToFile (unsigned long int configNumber) |
| ObservableStorer::writeFlowObservableToFile. More... | |
| std::vector< double > | getObservableArray () |
| double | getObservable (unsigned long int iObs) |
| std::string | getObservableName () |
| void | setObservableName (std::string observableName) |
| void | setNormalizeObservableByProcessor (bool norm) |
| void | reset () |
| ObservableStorer::reset set all the members for observable storage to zero. More... | |
A class for storing the observable data.
Contains methods for printing statistics, writing to file, setting observables and reseting ect.
| ObservableStorer::ObservableStorer | ( | unsigned long int | NSize | ) |
ObservableStorer::ObservableStorer.
| NSize | the number of observables to allow storage for. |
Stores two arrays, one for observables, and one for observables squared.
| ObservableStorer::~ObservableStorer | ( | ) |
| void ObservableStorer::gatherResults | ( | ) |
ObservableStorer::gatherResults.
Performs a MPI reduce between all the data gathered and, if set - divides by the number of processors.
|
inline |
|
inline |
|
inline |
|
inline |
| void ObservableStorer::printStatistics | ( | ) |
| void ObservableStorer::reset | ( | ) |
ObservableStorer::reset set all the members for observable storage to zero.
| void ObservableStorer::runStatistics | ( | ) |
ObservableStorer::runStatistics.
Performs simple statistics such as mean, variance and standard deviation.
|
inline |
|
inline |
| void ObservableStorer::writeFlowObservableToFile | ( | unsigned long int | configNumber | ) |
ObservableStorer::writeFlowObservableToFile.
| configNumber | configuration number |
Writes to file using the IO::writeFlowObservableToFile method.
| void ObservableStorer::writeObservableToFile | ( | double | acceptanceRatio | ) |
ObservableStorer::writeObservableToFile.
| acceptanceRatio | from the Metropolis algorithm |
Writes to file using the IO::writeObservablesToFile method.


| ambarish.com Ambarish Goswami's Current Research |
|---|
| Home/ Current Research |
|
Current Research
|
|
Angular momentum and ground reference
points in biped robot balance control
Foot Rotation Indicator (FRI) point, Zero Moment Point (ZMP) or Center of Pressure (CoP), Centroidal Moment Pivot (CMP). We have studied the fundamental mechanics of rotational stability of multi-body systems with the goal to identify a general balance and stability criterion for humanoid robots. For this, our research focuses on the rate of change of centroidal angular momentum of a robot, which is the aggregate angular momentum computed at the robot's CoM. We propose humanoid robot balance control approaches using angular momentum rate change. Centroidal moment pivot (CMP) is the point on the foot/ground surface of a robot where the total ground reaction force would have to act such that its centroidal angular moementum stays constant. This new criterion generalizes earlier concepts such as GCoM, CoP, ZMP, and FRI point, and extends their applicability. |
|
Simple humanoid models for balance and control
If you could reduce the instantaneous inertia of the entire humanoid
robot to that of a single rigid body, what would it be?
We also introduce Inertia Shaping, a high-level approach to modify the kinodyanmic properties of a humanoid. |
|
Humanoid robot push recovery: Where to step?
Use of Capture Point (CaP) and angular momentum in biped robot push recovery.
Push recovery is difficult because humanoid dynamics are high dimensional, non-linear, and hybrid. Moreover, a humanoid robot is underactuated and makes friction-limited unilateral contacts with the ground. Despite these theoretical difficulties, animals and humans are very adept at push recovery. Although the humanoid literature contains several analysis and control techniques for external disturbance rejection, there is yet to emerge a principled approach towards ``when and where to step'' under a force disturbance. Collaboration with Jerry Pratt at the Institute of Human and Machine Cognition, Pensacola, Florida.
|
|
Active impedance based control of assistive exoskeletons
We propose a novel control method for lower-limb assist that produces a virtual modification of the mechanical impedance of the human limbs. This effect is accomplished by making the exoskeleton display active impedance properties. Active impedance control emphasizes control of the exoskeleton's dynamics and regulation of the transfer of energy between the exoskeleton and the user. It's goal is improving the dynamic response of the human limbs without sacrificing the user's control authority. The proposed method is an alternative to myoelectrical exoskeleton control, which is based on estimating muscle torques from electromyographical(EMG) activity. Implementation of an EMG-based controller is a complex task that involves modeling the user's musculoskeletal system and requires recalibration. In contrast, active impedance control is less dependent on estimation of the user's attempted motion, thereby avoiding conflicts resulting from inaccurate estimation.
We also introduce
a new form of human assist based on improving the kinematic response of the limbs.
Reduction of average muscle torques is a common goal of research in human assist.
However, less emphasis has been placed so far on improving the user's agility of motion.
We aim to use active impedance control to attain such effects as increasing the user's average
speed of motion, and improving their acceleration capabilities in order to compensate for perturbations
from the environment.
|
Ambarish Goswami
Last Revised March 05, 2008
Back to main page |


To capture the state of a form you are currently seeing follow these simple steps:
<form>
tags in the page and highlight them with an overlay
Click the overlay of the form you want to extract.
In case you want to extract a form (again) that you already have in your ruleset, please right-click a field inside that form and choose "Form-O-Fill: Save Form"


HOME
VIEW
DONATE
LOGOUT
Previous
Next
Charity organization1
DONATE
Charity organization2
DONATE
Charity organization3
DONATE
Contact
please give feedback
Drop a note.
India, Andhra Pradesh
Phone: +00<PHONE_NUMBER>
Email<EMAIL_ADDRESS>Send


The Format
structure provides printf
-style string formatting.
The syntax of format strings is a subset of that
supported by the C printf
function.
Synopsis
structure Format
Interface
datatype fmt_item
= ATOM of Atom.atom
| LINT of LargeInt.int
| INT of Int.int
| LWORD of LargeWord.word
| WORD of Word.word
| WORD8 of Word8.word
| BOOL of bool
| CHR of char
| STR of string
| REAL of Real.real
| LREAL of LargeReal.real
| LEFT of (int * fmt_item)
| RIGHT of (int * fmt_item)
exception BadFormat
exception BadFmtList
val format : string -> fmt_item list -> string
val formatf : string -> (string -> unit) -> fmt_item list -> unit
Description
datatype fmt_item = …
-
The
fmt_item
datatype is a union of the types that theformat
function supports. The constructors are interpreted as follows:ATOM atm
-
specifies an atom
atm
to convert (the conversion specifier must be “s”). LINT n
-
specifies a large integer value
n
to convert (the conversion specifier must be one of “d”, “o”, “x”, or “X”). INT n
-
specifies a default integer value
n
to convert (the conversion specifier must be one of “d”, “o”, “x”, or “X”). LWORD w
-
specifies a large word value
w
to convert (the conversion specifier must be one of “d”, “o”, “x”, or “X”). WORD w
-
specifies a default word value
w
to convert (the conversion specifier must be one of “d”, “o”, “x”, or “X”). WORD8 w
-
specifies an 8-bit word value
w
to convert (the conversion specifier must be one of “d”, “o”, “x”, or “X”). BOOL b
-
specifies a Boolean value
b
to convert (the conversion specifier must be “b”). CHR c
-
specifies a character value (the conversion specifier must be “c”).
STR s
-
specifies a string value
s
to convert (the conversion specifier must be “s”). The conversion is the identity; e.g.,STR "\n"
will produce a newline in the result string. REAL r
-
specifies a default real value
r
to convert (the conversion specifier must be one of “e”, “E”, “f”, “F”, “g”, or “G”).  LEFT(wid, item)
-
specifies a left-padded (right-justified) conversion, where the result of formatting
item
is padded on the left with spaces to the width specified bywid
. Note that the padding occurs afteritem
formatted, so it can be combined with width specifiers and zero padding. RIGHT(wid, item)
-
specifies a right-padded (left-justified) conversion, where the result of formatting
item
is padded on the right with spaces to the width specified bywid
. Note that the padding occurs afteritem
formatted, so it can be combined with width specifiers and zero padding.
exception BadFormat
-
This exception is raised when either
format
orformatf
is applied to an ill-formed format string. exception BadFmtList
-
This exception is raised when there is a mismatch in either number or type between the format string and the list of items.
val format : string -> fmt_item list -> string
-
format fmt
returns a function for formating a list of format items as a string by converting the list of items according to the format stringfmt
. If the format string is ill formed, theBadFormat
exception will be raised. Likewise, if there is a mismatch between the conversion specifiers in the format string and the list of items, then theBadFmtList
exception is raised. val formatf : string -> (string -> unit) -> fmt_item list -> unit
-
format fmt consumer items
is equivalent to the expressionconsumer (format fmt items)
Format Strings
The format and `formatf
functions take a format string and a list of
format items as arguments. The format string is composed of zero or more
directives, which are either ordinary characters (excluding %
), which are
copied to the result, or conversion specifiers, which are used to convert
the corresponding format items to strings that are then added to the result.
Conversion specifiers begin with the percent (%
) character followed by
the following in sequence:
-
Zero or more of the following single-character flags. Note that these only apply to the numeric conversion specifiers.
-
A " " (space), which means that a space character is used as the sign for positive numbers. This flag is incompatible with the “+” flag.
-
A “+”, which means that a
+
character is used as the sign for positive numbers. This flag is incompatible with the "` `" flag. -
A “~”, which means that the tilde character is used as the sign for negative numbers (i.e., SML syntax).
-
A “0”, which means that the zero character should be used to pad the number (on the left) to the requested width.
-
A “-”, which means that the minus character is used as the sign for negative numbers, which is the default behavior. Note that this interpretation of the “-” flag differs from the C
printf
function, where it is used to specify left justification; use theLEFT
constructor for that purpose. -
A “#”, which means that a base specifier should be prepended to the representation of the number.
-
-
an optional decimal number specifying a minimum field width. If the converted value has fewer characters than the field width, it will be padded on the left with spaces (or zeros, when zero-padding has been specified).
-
An optional precision, in the form of a period “.” followed by an optional decimal number. If the number is omitted, the precision is taken as zero. The precision specifies the the number of digits to appear after the decimal-point for “a”, “A”, “e”, “E”, “f”, and “F” conversions, the maximum number of significant digits for “g” and “G” conversions, and the maximum number of characters for the “s” conversion.
-
The conversion-specifier character, which must match the corresponding format item. The conversion character is one of the following:
-
A “d”, which specifies the conversion of an integer (
INT
orLINT
) or word (WORD
,LWORD
, orWORD8
) item to its decimal representation. -
An “o”, which specifies the conversion of an integer (
INT
orLINT
) or word (WORD
,LWORD
, orWORD8
) item to its octal representation. If the “#” flag was specifies, then a leading"0"
is prepended to the result. -
An “x” or “X”, which specifies the conversion of an integer (
INT
orLINT
) or word (WORD
,LWORD
, orWORD8
) item to its hexadecimal representation. The digits are lower-case for “x” and upper-case for “X”. If the “#” flag was specifies, then a leading “0x” (or “0X”) is prepended to the result. -
An “e” or “E”, which specifies the conversion of a real (
REAL
orLREAL
) item to the formats d . ddd e s dd
, where there is one digit before the decimal-point character and the number of digits after the decimal-point is equal to the precision. (The “`e” is replaced by “
E`” for the “E” conversion specifier.) If the precision is missing, it defaults to six and if the precision is zero, no decimal-point character appears. The signs (s
) of the number and exponent are displayed as specified by the flags. -
A “f” or “F”, which specifies the conversion of a real (
REAL
orLREAL
) item to the formats ddd . ddd
, where the number of digits after the decimal-point is equal to the precision specification (or six if not specified). -
A “g” or “G”, which specifies the conversion of a real (
REAL
orLREAL
) item to either the format specified by “e” or “f” (or “E” or “F” in the case of “G”). -
A “b”, which specifies the conversion of a boolean (
BOOL
) item, which will be displayed as either “true” or "`false`." -
A “c”, which specifies the identity conversion of a character (
CHAR
) item. -
A “s”, which specifies the identity conversion of a string (
STR
) or atom (ATOM
) item.
-


{% extends 'webapp/base.html' %}
{% block mainbody %}
Name
{{ starships.name }}
Starship Class
{{ starships.starship_class }}
Manufacturer
{{ starships.manufacturer }}
Cost in Credits
{{ starships.cost_in_credits }}
Length
{{ starships.length }}
Crew
{{ starships.crew }}
Passengers
{{ starships.passengers }}
Max Atmosphering Speed
{{ starships.max_atmosphering_speed }}
Hyperdrive Rating
{{ starships.hyperdrive_rating }}
MGLT
{{ starships.MGLT }}
Cargo Capacity
{{ starships.cargo_capacity }}
Consumables
{{ starships.consumables }}
Pilots
{{ starships.pilots }}
Films
{% endblock mainbody %}


In a normal playthrough, you need Grenade to melt ice and activate lanterns. But it is actually possible to do the same with sentry. For that, you simply need to use sentry near a lantern or ice. When the sentry runs out, it will explode and generate fire which will melt ice and activate lanterns.


Abstract
This note discusses numerical computation of guiding center orbits in tokamaks using cylindrical coordinates and several magnetic coordinates. Some subtle things involved in using a particular kind of magnetic coordinates called ﬁeld-line-following coordinates are discussed (I am using this kind of coordinates in developing a new module in GEM code). We assume a general tokamak magnetic ﬁeld speciﬁed numerically (provided by the EFIT G-ﬁle). This note is evolving, beginning with my ﬁrst try of computing guiding-center motion in Solovev analytical equilibrium using cylindrical coordinates, and then extending to general numerical magnetic ﬁeld, and later using magnetic coordinates.


This document describes how to install Apache Cordova and the Android SDK on a Linux machine. Instructions below are tested on Ubuntu 14.04, on a 32-bit installation. For other versions and Linux distributions, the procedure may differ.
Please provide your feedback so that we can keep this documentation up to date. You are welcome to ask for help at the Evothings Forum.
Follow these steps to install Cordova:
Install Node.js. Node.js may already be installed. To test the installation, open a terminal window and type:
nodejs --version
If the version number is displayed, Node.js is installed.
If Node.js is not installed, install with:
sudo apt-get install nodejs
Also add the alias "node" for nodejs, as this is needed by Cordova:
sudo ln -s /usr/bin/nodejs /usr/bin/node
Install Node Package Manager (npm). Test if npm is installed by typing:
npm --version
If npm is not installed, install with:
sudo apt-get install npm
Install Git. Git is a version control system, which is used by Cordova behind-the-scenes. Test if Git is installed by typing:
git --version
If Git is not installed, install with:
sudo apt-get install git
Install Cordova. Cordova is installed using the Node Package Manager (npm). Type the following to install:
sudo npm install -g cordova
Test the Cordova install by typing:
cordova --version
If you see the version number, you have successfully installed Apache Cordova!
The Android SDK needs the Java Development Kit (JDK) to be installed (minimum version 1.6). Note that the Java Runtime Environment (JRE) is not sufficient, you will need the JDK. To check if you have the JDK installed already, type this in a terminal window:
java -version javac -version
If version info is displayed, you have Java installed, but you may want to use the Oracle JDK, rather than the OpenJDK that comes with many Linux distributions. The Oracle JDK is needed for signing Android apps.
If you wish to install the Oracle JDK, proceed as follows (the steps below are based on a guide from wikiHow):
Start by removing the OpenJDK:
sudo apt-get purge openjdk-\* sudo apt-get autoremove
Find out if you have a 32-bit och 64-bit Linux version:
file /sbin/init
If you run 64-bit Linux, you should install 32-bit libraries (Android SDK will need this):
sudo apt-get install ia32-libs
Download the JDK (Java SE Development Kit). The download file ends with .tar.gz. For 32-bit systems get the "Linux x86" download, for 64-bit systems get the "Linux x64" download.
The downloaded file is typically saved to the folder "Download" in your home directory. The following steps create an installation directory and unpack the JDK files there. You can pick any directory for the install, we will use the directory "java" in the home folder. Replace "jdk-8u11-linux-i586.tar.gz" with the name of the file you just downloaded.
mkdir -p ~/java cd ~/Downloads mv jdk-8u11-linux-i586.tar.gz ~/java cd ~/java tar xvzf jdk-8u11-linux-i586.tar.gz rm jdk-8u11-linux-i586.tar.gz
Check the name of the JDK install directory with:
ls
The path to the JDK becomes "~/java/jdk1.8.0_11" where "jdk1.8.0_11" is the name displayed by the ls command.
Add the path to the JDK by editing .bashrc in your home directory. You can use for example nano or gedit for this:
nano ~/.bashrc
or:
gedit ~/.bashrc
Add the following to the end of the file (replace "jdk1.8.0_11" with the actual folder name!):
JAVA_HOME=~/java/jdk1.8.0_11 PATH=$PATH:~/java/jdk1.8.0_11/bin export JAVA_HOME export PATH
Edit the .bash_profile file to load .bashrc. Opening a terminal windows runs .bash_profile, and we want our path settings to be available in the terminal. If not already present, add the following lines to .bash_profile (se nano or gedit as above):
if [ -f ~/.bashrc ]; then source ~/.bashrc fi
Now you are ready to test the install. Close any open terminal windows, open a new terminal and type:
javac -version java -version
If version info is displayed you are done with the JDK install!
Apache Ant is a build system for Java, which is used by Cordova and the Android SDK. To install Ant, follow these steps:
Download Ant from here: ant.apache.org/bindownload.cgi. Get the zip download available at the page. Click the zip-file link for the most recent release, e.g. apache-ant-1.9.4-bin.zip, and save the file to your machine.
Unpack the zip file to the directory on your machine where you want Ant to be installed. You can pick any directory for the install, we will use the directory "ant" in the home folder. Here are the commands (make sure you use the actual name of the downloaded zip file):
mkdir -p ~/ant cd ~/ant unzip apache-ant-1.9.4-bin.zip rm apache-ant-1.9.4-bin.zip
To add Ant to the system path, edit .bashrc to contain the following lines at the end. Again, be careful to use the actual names of the files and folders on your system:
JAVA_HOME=~/java/jdk1.8.0_11 PATH=$PATH:~/java/jdk1.8.0_11/bin export JAVA_HOME ANT_HOME=~/ant/apache-ant-1.9.4 PATH=$PATH:~/ant/apache-ant-1.9.4/bin export ANT_HOME export PATH
Now test the install. Close the terminal window, open a new terminal (to make settings take effect) and type:
ant -versionIf you see a version number you have installed Ant successfully!
The SDK Tools for Android are used by Cordova to build Android apps. Follow these steps to install the SDK Tools:
Go to the page developer.android.com/sdk scroll down the page and click "VIEW ALL DOWNLOADS AND SIZES". Under "SDK Tools Only", click the windows installer file for Linux and download it (this file is named e.g. android-sdk_r23.0.2-linux.tgz).
When downloaded, unpack the files. Here are commands for unpacking the Android SDK folder into your home directory:
cd mv ~/Downloads/android-sdk_r23.0.2-linux.tgz . tar zxvf android-sdk_r23.0.2-linux.tgz rm android-sdk_r23.0.2-linux.tgz
The unpacked folder is named "android-sdk-linux" as of the release used in this example.
The Android SDK Tools need to be added to the system path. Edit .bashrc to contain the following lines at the end. Make sure you use the actual names of the files and folders on your system:
JAVA_HOME=~/java/jdk1.8.0_11 PATH=$PATH:~/java/jdk1.8.0_11/bin export JAVA_HOME ANT_HOME=~/ant/apache-ant-1.9.4 PATH=$PATH:~/ant/apache-ant-1.9.4/bin export ANT_HOME PATH=$PATH:~/android-sdk-linux/platform-tools PATH=$PATH:~/android-sdk-linux/tools export PATH
You need to have the specific Android SDK version used by Cordova. This is done by running the Android SDK Manager by typing the command:
android
This launches a window where you can select to install specific Android SDKs.
First time you launch the Android SDK Manager there will be preset selections. It is recommended to leave these untouched. Also select the entry "Android 4.4.2 (API 19)" is not installed already. This is the version used by the current Cordova 3.5 version. Note that the Android SDK required by Cordova will change in the future, as new versions of Cordova and Android are released. When this happens, open the Android SDK Manager again, and install the required API version(s).
To test the install, close the terminal window, open a new terminal and type:
adb versionThis should display version info for the Android Debug Bridge.
If you get stuck, consult the documentation at the respective web sites for Cordova, Java, Ant, and Android. The Cordova documentation has a platform guide for Android. You are also welcome to ask for help at the Evothings Forum.
One thing to do is to inspect all the environment variables. You can do this from a command window (note that you have to open a new command window after updating environment variables for updated values to be available). This displays the system PATH:
echo $PATH
Here is how to inspect the values of JAVA_HOME and ANT_HOME:
echo $JAVA_HOME echo $ANT_HOME
Next step is to create and build a Cordova project. Go to the Cordova Guide to learn more.
Evothings Studio makes it easy to develop Cordova apps. Check out how to use your Cordova project with the fast Evothings workflow.
It is easy and fun to get started with Evothings Studio. Download now and be up and running in 5 minutes!


| DOSE: T+ 0:00 |
3 hits |
oral |
LSA |
(blotter / tab) |
| T+ 3:00 |
1.25 tsp |
oral |
Syrian Rue |
(tea) |
INTRODUCTORY SUMMATION
The following report details my personal experimentation with what was purported to be ergot derived LSA by itself and in combination with the seeds of Peganum harmala (Syrian Rue).
SOURCE and ASSESMENT of the SUBSTANCE
A trusted friend had given me what was supposed to be ergot-derived LSA on small (about ¼” x ¼”) plain white squares of paper. Of course I have no way of saying what this stuff actually was. He assured me that his source was reliable and that this substance was an extraction of LSA from ergot and not a synthesis of LSD or anything else. I would go into further detail along these lines of reasoning but I have already done this in my experience report entitles “Lysergic Bioassay I – Visual and Auditory Phenomena” which the reader can look over.
The EXPERIENCE
As mentioned I took 3 tabs. Whereas I could barely feel “psychedelic” on 1 tab about 1 month earlier, 3 tabs was definitely a good strong dose, but not too much. Soon after taking the tabs I gently stretched, did a little yoga and so on. As I waited for the effects to sink in I listened to music, looked at art books and so on. Once I began to really feel it I put on a CD called “The Tibetan Tantric Choir” which is the chanting of the Gyoto Monks (Buddhist) of Tibet, a recording made by Mickey Hart.  By the very act of chanting along with this recording one does breathing exercises. It also seems to lower the brain waves if one relaxes into it. This usually seems to “tune me up” and it certainly did this time.
After some time I went outside to commune with Nature. The summer night dew on the grass felt amazing on my bare feet. I felt connected to Mother Earth. I gazed up at the starry sky and was dazzled by the twinkling brilliance. Many stars were blinking, streaking, flashing and slightly wandering. The longer I stared the more interstellar I felt. Whether it was illusion, perceptual enhancement or a little of both, I could see depth in the stars I never could before. In other words, rather than points of light on a relatively flat surface (how the human eye normally sees the night sky) it seemed obvious that some stars were further out than others. After some time of this I reminded myself that I was connected to the earth and looked down, touched the grass, touched the leaves of plants, etc. Then I would gaze at the stars again. Nature is divine. The world and the cosmos are our mother and grandmother as the sun is our father.
At some point before the peak effects I went back inside. I did my own version of what has been called “The Ritual of the Pentagram”, “The Banishing Ritual” etc. This is used in modern Wiccan and neo-pagan traditions. It has been used in different forms in various pagan traditions in Europe and certainly contains Gnostic and Hermetic elements.
One establishes a circle about oneself, resonates pentagrams in the air with hand motions and long intonations, a pentagram at each of the four directions. In my own version I then do long, slow intoning chants for each chakra, each with it’s own note and syllable. I will spare the reader the full explanation, but suffice to say that this ritual serves to center ones attention, clarify intention, to lower the “volume” of the everyday world so that one can open up to so much more – the inner and outer world.
I find this practice to be increasingly beneficial as I do it more and more. Without entheogens it works well. With entheogens it works very well. Once the circle is established and I open up to the influx of energy, I then meditate, do yoga, tai chi, or simply think about life and love and what not.
This time, having established this circle and having opened myself up, I did some yoga and tai chi. This was wonderful. I could feel myself opening up to more and more flow. Chi (as the Chinese call it) or prana (as yogins call it) was flowing through me. As I sometimes do, I began with formal moves from both traditions and then, once things were flowing, I moved spontaneously. The less I thought about what to do, the more I flowed. It was easier to maintain a meditative state of calmer thought (or no thought) and increased awareness.
I could feel more and more energy move through me. Here is where it get a bit challenging to explain. I could feel so much energy moving into me that I felt that I could harness this as power in some way. Thankfully, however, I had no intentions of harnessing this for myself. I let it flow back out of me. Consequently I could feel more energy flowing into me. I let this flow out. More flowed in. More flowed out. This whole time I was moving in pseudo tai chi motions. Many of us have done or have seen the flowing, fluid dance motions at raves and what not. Well, I suppose I must have looked as if I were doing such a dance but in slow motion. So much energy flowed through me but only in the beginning did I have linguistic thoughts like, “Wow! This is amazing!” or “I can really feel the chi!”.
For the most part I remained aware but did not have distinct thoughts with logistic meaning. The reader may have heard similar sayings, but it was as if I was like a flexible reed banding in the wind. If I had been rigid like a stiff tree I would have been broken in a sense. Or I was like a hollow tube, so much flowed through me that if I were plugged up at one end I would have been blown out in a bad way. Thankfully, I was able to let go and simply let it all flow.
This went on for what must have been 1 to 3 hours or so, slowly increasing in intensity and then slowly decreasing in intensity. At some point I slowed to a stop and finally had a distinct thought again. “Wow!” I thought, “I have been doing this for a couple of hours! That was so amazing! I can’t believe how wonderful that was!” or similar thoughts. It was truly an amazing experience.
The peak had passed. I made what I call Harmala tea from 1 ¼ teaspoons of coarsely ground seeds of Peganum harmala (Syrian Rue) and hot water from a kettle. This contains harmaline and harmine which are MAOIs.
[Erowid Note: Combining MAOIs with other psychoactive drugs carries serious medical risks and can result in extremely unpleasant side effects, overheating, nausea, confusion, heart problems, and even death. Please see Erowid's MAOI Vault]
I drank this tea and, as it had the first time I tried this combination (see my experience report “Lysergic Bioassay I – Visual and Auditory Phenomena”) I found it to be both grounding and more “psychedelic”. It was very enjoyable. I found myself writing love notes to my wonderful wife with little hearts, whimsical handwriting, images of faeries and tantric embraces, etc.
I then laid down for the night… OK, well it was actually morning by this time. Just as I had heard the first time I tried this LSA (or whatever it is) I was hearing a lot of tweaked digital droid bird-like techno sounds. Again these sort of swelled “up” slowly and then back “down” as I described in my “Lysergic Bioassay I” experience report. In the heart of the summer, there was a thick jungle of sounds from buzzing insects, clicking birds, and so on. I could swear that my breath and brain waves were in sink with the cycles of insect shrills surrounding the area that I could hear clearly through the open windows.
Overall it was a great, powerful and experientially mystical experience. I have tried some more tabs one time since this experiment occurred. This experience was very intense and I have submitted this report under the title “Lysergic Bioassay III – Cosmic transducer”.
Experience Reports are the writings and opinions of the individual authors who submit them.
Some of the activities described are dangerous and/or illegal and none are recommended by Erowid.