Zimbabwe biggest bank CBZ “caught smuggling new notes and coins into black market”
by Staff ReporterThe Commercial Bank of Zimbabwe (CBZ Holdings) has been accused of smuggling notes and coins to the parallel market money.
The alleged scandal was disclosed by popular twitter who is also a ZANU PF crusader, @matigary who is believed to be Taurai Chinyamakobvu who said:
It’s not enough to demand an explanation to these @CBZHoldings seals on the coins.
It would be silly to imagine RBZ did not anticipate that bank notes would not be on the street. This has happened over and over when new notes are introduced. OVER & OVER.
The QN is why was it not anticipated & nipped in the bud. Controls nhai Mangudya?
These reports come after an image of new notes alleged to be on the parallel market has circulated on social media platforms suggesting that banks were feeding cash onto the parallel market.
The central bank, the Reserve Bank of Zimbabwe this Tuesday introduced $5 and $2 notes, as well as $2 coins and whilst banks, are still issuing limited amounts of money to account holders, currency dealers on the parallel markets seem to be in possession of huge amounts of these new notes already.
More: Mining Zimbabwe


Library CoqIntro
A streamlined interactive tutorial on fundamentals of Coq,
focusing on a minimal set of features needed for developing
programming language metatheory.
Mostly developed by Aaron Bohannon, with help from Benjamin Pierce, Dimitrios Vytiniotis, and Steve Zdancewic.
Mostly developed by Aaron Bohannon, with help from Benjamin Pierce, Dimitrios Vytiniotis, and Steve Zdancewic.
Contents
- Getting Started
- Definitions
- Proofs
- Working with Implication and Universal Quantification
- Working with Definitions
- Working with Conjunction and Disjunction
- Reasoning by Cases and Induction
- Working with Existential Quantification
- Working with Negation
- Working with Equality
- Reasoning by Inversion
- Additional Important Tactics
- Basic Automation
- Functions and Conversion
- Solutions to Exercises
To get started...
- Install Coq (from the Download page of the main Coq web site)
- Install an IDE: either CoqIDE (from the same page) or Proof General (use Google to find it).
- Which should you choose? Their command sets are similar,
so basically the trade-offs are simple:
- Proof General is an extension of Emacs (or XEmacs, if you prefer), while CoqIDE uses a simpler point-and-click model of editing.
- PG is pretty easy to install; CoqIDE is very easy to install if you can find a pre-built version for the OS you are running on but can be a little tricky to build from scratch because it has lots of dependencies.
- Familiarize yourself with the most important commands
-
- If you are using PG, try this:
- Open this file and check that the mode line says something like "coq Holes Scripting"
- Go down a few pages and do C-C C-return. Notice that the part of the file above the cursor changes color (and becomes read-only), indicating that it has been sent to Coq.
- Come back here and do C-C C-return again
- You now know all you really need to navigate in this file and send parts of it to Coq, but there are some other navigation commands that are sometimes more convenient. To see a couple more, do C-C C-n several times and observe the result; then do C-C C-u a couple of times and observe the result.
- If you are using PG, try this:
-
- If you are using CoqIDE, try this:
- Open this file.
- Scroll down a few pages.
- Hover the mouse over each the buttons at the top of the window; this will make the "tool tips" appear so you can see which is which.
- Press the "Go to cursor" button. Observe what happens.
- Press the forward and backward buttons a few times. Observe.
- Scroll back to here again and start reading.
- If you are using CoqIDE, try this:
- Open the Coq reference manual (from the Documentation page of the Coq web site) in a web browser. Spend 30 seconds looking over the table of contents to get an idea what's there. (There is no need to actually read anything now.)
In this file, we will be working with a very simple language
of expressions over natural numbers and booleans. First we
need to define the datatype of terms.
The Inductive keyword defines a new inductive type. We name our new type tm and declare that tm lives in the sort Set. Types in Set are datatypes, which can be used just like those in standard programming languages. After the inductive definition, the global environment contains the name of the newly defined type, along with the names of all of the constructors. Coq also automatically defines a few operators for eliminating values of the new type (tm_rec, tm_ind, etc.); we can ignore these for the time being, since we will not need to use them directly.
The Inductive keyword defines a new inductive type. We name our new type tm and declare that tm lives in the sort Set. Types in Set are datatypes, which can be used just like those in standard programming languages. After the inductive definition, the global environment contains the name of the newly defined type, along with the names of all of the constructors. Coq also automatically defines a few operators for eliminating values of the new type (tm_rec, tm_ind, etc.); we can ignore these for the time being, since we will not need to use them directly.
Inductive tm : Set :=
| tm_true : tm
| tm_false : tm
| tm_if : tm -> tm -> tm -> tm
| tm_zero : tm
| tm_succ : tm -> tm
| tm_pred : tm -> tm
| tm_iszero : tm -> tm.
Next, we want to designate some of our tm expressions as
"values" in our object language. Mathematically, the
property of being a value is a unary relation over tms.
The definition of the unary relation value will be built
from the definition of two auxiliary relations: bvalue for
the set of boolean values and nvalue for the set of
numerical values.
We define n-ary relations in Coq much as we do on paper -- by giving a set of inference rules that can be used to justify the membership of a tuple in the relation. The definition of such an inference system also uses the keyword Inductive. Although this is exactly the same device we used to build the set tm, in this case we want to do something slightly different: we will be using it to inductively defining the structures (derivation trees) that justify the membership of a tuple in a relation, rather than directly defining a set inductively. These derivation trees will need to be given a dependent type in order to ensure that only correct derivation trees can be built. It is possible to view their type as a datatype such as tm; however, it is more natural to interpret it as a proposition, so it will be declared to live in Prop instead of Set. Prop is parallel to Set in the sort hierarchy, but types in Prop can be thought of as logical propositions rather than datatypes. The inhabitants of types in Prop can be thought of as proofs rather than programs.
The unary relations bvalue and nvalue are defined by very simple inference systems, each having just two rules. After defining these inference systems, bvalue and nvalue will each be a family of types indexed by elements of tm. We can build inhabitants of some (but not all) of the types in these families with the constructors from our inductive definition. Semantically, we consider the proposition bvalue t to be true if it is inhabited and false if it is not. (It is worth noting at this point that, by default, Coq's logic is constructive and P \/ not P is provable for some P but not for others. However, it is sound to add the law of the excluded middle as an axiom, if desired.)
We define n-ary relations in Coq much as we do on paper -- by giving a set of inference rules that can be used to justify the membership of a tuple in the relation. The definition of such an inference system also uses the keyword Inductive. Although this is exactly the same device we used to build the set tm, in this case we want to do something slightly different: we will be using it to inductively defining the structures (derivation trees) that justify the membership of a tuple in a relation, rather than directly defining a set inductively. These derivation trees will need to be given a dependent type in order to ensure that only correct derivation trees can be built. It is possible to view their type as a datatype such as tm; however, it is more natural to interpret it as a proposition, so it will be declared to live in Prop instead of Set. Prop is parallel to Set in the sort hierarchy, but types in Prop can be thought of as logical propositions rather than datatypes. The inhabitants of types in Prop can be thought of as proofs rather than programs.
The unary relations bvalue and nvalue are defined by very simple inference systems, each having just two rules. After defining these inference systems, bvalue and nvalue will each be a family of types indexed by elements of tm. We can build inhabitants of some (but not all) of the types in these families with the constructors from our inductive definition. Semantically, we consider the proposition bvalue t to be true if it is inhabited and false if it is not. (It is worth noting at this point that, by default, Coq's logic is constructive and P \/ not P is provable for some P but not for others. However, it is sound to add the law of the excluded middle as an axiom, if desired.)
Inductive bvalue : tm -> Prop :=
| b_true : bvalue tm_true
| b_false : bvalue tm_false.
Inductive nvalue : tm -> Prop :=
| n_zero : nvalue tm_zero
| n_succ : forall t,
nvalue t ->
nvalue (tm_succ t).
The Definition keyword is used for defining non-recursive
functions (including 0-ary functions, i.e., constants).
Here we define the unary predicate value using disjunction
on propositions (written \/).
Note: It is not actually necessary to provide the types of the arguments nor the return type when they can easily be inferred; for example, the annotations : tm and : Prop are optional here.
Note: It is not actually necessary to provide the types of the arguments nor the return type when they can easily be inferred; for example, the annotations : tm and : Prop are optional here.
Having defined tms and values, we can define a
call-by-value operational semantics of our language by
giving a definition of the single-step evaluation of one
term to another. We give this as an inductively defined
binary relation.
Inductive eval : tm -> tm -> Prop :=
| e_iftrue : forall t2 t3,
eval (tm_if tm_true t2 t3) t2
| e_iffalse : forall t2 t3,
eval (tm_if tm_false t2 t3) t3
| e_if : forall t1 t1' t2 t3,
eval t1 t1' ->
eval (tm_if t1 t2 t3) (tm_if t1' t2 t3)
| e_succ : forall t t',
eval t t' ->
eval (tm_succ t) (tm_succ t')
| e_predzero :
eval (tm_pred tm_zero) tm_zero
| e_predsucc : forall t,
nvalue t ->
eval (tm_pred (tm_succ t)) t
| e_pred : forall t t',
eval t t' ->
eval (tm_pred t) (tm_pred t')
| e_iszerozero :
eval (tm_iszero tm_zero) tm_true
| e_iszerosucc : forall t,
nvalue t ->
eval (tm_iszero (tm_succ t)) tm_false
| e_iszero : forall t t',
eval t t' ->
eval (tm_iszero t) (tm_iszero t').
We define multi-step evaluation with the relation
eval_many. This relation includes all of the pairs of
terms that are connected by sequences of evaluation steps.
Inductive eval_many : tm -> tm -> Prop :=
| m_refl : forall t,
eval_many t t
| m_step : forall t t' u,
eval t t' ->
eval_many t' u ->
eval_many t u.
Exercise
Multi-step evaluation is often defined as the "reflexive, transitive closure" of single-step evaluation. Write an inductively defined relation eval_rtc that corresponds to that verbal description.In case you get stuck or need a hint, you can find solutions to all the exercises near the bottom of the file.
A term is a normal_form if there is no term to which it
can step. Note the concrete syntax for negation and
existential quantification in the definition below.
Exercise
Sometimes it is more convenient to use a big-step semantics for a language. Add the remaining constructors to finish the inductive definition full_eval for the big-step semantics that corresponds to the small-step semantics defined by eval. Build the inference rules so that full_eval t v logically implies both eval_many t v and value v. In order to do this, you may need to add the premise nvalue v to the appropriate cases.Hint: You should end up with a total of 8 cases.
Inductive full_eval : tm -> tm -> Prop := | f_value : forall v, value v -> full_eval v v | f_iftrue : forall t1 t2 t3 v, full_eval t1 tm_true -> full_eval t2 v -> full_eval (tm_if t1 t2 t3) v | f_succ : forall t v, nvalue v -> full_eval t v -> full_eval (tm_succ t) (tm_succ v).
Tip
If you want to see the type of an identifier x, you can use the command Check x. If you want to see the definition of an identifier x, you can use the command Print x.
A proposition and its proof are both represented as terms in
the calculus of inductive constructions, which is
syntactically very small.
Proof terms are most easily built interactively, using tactics to manipulate a proof state. A proof state consists of a set of goals (propositions or types for which you must produce an inhabitant), each with a context of hypotheses (inhabitants of propositions or types you are allowed to use). A proof state begins initially with one goal (the statement of the lemma you are tying to prove) and no hypotheses. A goal can be solved, and thereby eliminated, when it exactly matches one of hypotheses in the context. A proof is completed when all goals are solved.
Tactics can be used for forward reasoning (which, roughly speaking, means modifying the hypotheses of a context while leaving the goal unchanged) or backward reasoning (replacing the current goal with one or more new goals in simpler contexts). Given the level of detail required in a formal proof, it would be ridiculously impractical to complete a proof using forward reasoning alone. However it is usually both possible and practical to complete a proof using backward reasoning alone. Therefore, we focus almost exclusively on backward reasoning in this tutorial. Of course, most people naturally use a significant amount of forward reasoning in their thinking process, so it may take you a while to become accustomed to getting by without it.
We use the keyword Lemma to state a new proposition we wish to prove. (Theorem and Fact are exact synonyms for Lemma.) The keyword Proof, immediately following the statement of the proposition, indicates the beginning of a proof script. A proof script is a sequence of tactic expressions, each concluding with a ".". Once all of the goals are solved, we use the keyword Qed to record the completed proof. If the proof is incomplete, we may tell Coq to accept the lemma on faith by using Admitted instead of Qed.
We now proceed to introduce the specific proof tactics.
Proof terms are most easily built interactively, using tactics to manipulate a proof state. A proof state consists of a set of goals (propositions or types for which you must produce an inhabitant), each with a context of hypotheses (inhabitants of propositions or types you are allowed to use). A proof state begins initially with one goal (the statement of the lemma you are tying to prove) and no hypotheses. A goal can be solved, and thereby eliminated, when it exactly matches one of hypotheses in the context. A proof is completed when all goals are solved.
Tactics can be used for forward reasoning (which, roughly speaking, means modifying the hypotheses of a context while leaving the goal unchanged) or backward reasoning (replacing the current goal with one or more new goals in simpler contexts). Given the level of detail required in a formal proof, it would be ridiculously impractical to complete a proof using forward reasoning alone. However it is usually both possible and practical to complete a proof using backward reasoning alone. Therefore, we focus almost exclusively on backward reasoning in this tutorial. Of course, most people naturally use a significant amount of forward reasoning in their thinking process, so it may take you a while to become accustomed to getting by without it.
We use the keyword Lemma to state a new proposition we wish to prove. (Theorem and Fact are exact synonyms for Lemma.) The keyword Proof, immediately following the statement of the proposition, indicates the beginning of a proof script. A proof script is a sequence of tactic expressions, each concluding with a ".". Once all of the goals are solved, we use the keyword Qed to record the completed proof. If the proof is incomplete, we may tell Coq to accept the lemma on faith by using Admitted instead of Qed.
We now proceed to introduce the specific proof tactics.
Example
The tactic intros x1 ... xn moves antecedents and universally quantified variables from the goal into the context as hypotheses. The tactic apply is complementary to intros. If the conclusion (the part following the rightmost arrow) of a constructor, hypothesis, or lemma e matches our current goal, then apply e will replace the goal with a new goal for each premise/antecedent of e. If e has no premises, then the current goal is solved. Using apply allows us to build a proof tree from the bottom up. In the following example, our proof script will effectively build the following proof tree:nvalue t ---------------------------- (e_predsucc) eval (tm_pred (tm_succ t)) t ------------------------------------------------ (e_succ) eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)
Step through the proof to see how this tree is constructed. For each tactic, we give the corresponding statement in a written proof. (The uses of Check are inessential.)
Let t be a tm.
Assume that t is an nvalue (and let's call that
assumption Hn for future reference).
By e_succ, in order to prove our conclusion, it suffices
to prove that eval (tm_pred (tm_succ t)) t.
That, in turn, can be shown by e_predsucc, if we are
able to show that nvalue t.
But, in fact, we assumed nvalue t.
Qed.
Hint for PG users
If you place the cursor after Proof. and do C-c C-return, you'll notice that the window displaying Coq's responses is (annoyingly) empty, instead of showing what is to be proved. The reason for this is that, actually, a different buffer is being displayed! (To see this, do C-c C-n and C-c C-u a few times and notice that the buffer name in the mode line changes.) You can use C-c C-p to switch the display back from the *response* buffer to the *goals* buffer.Example
Now consider, for a moment, the rule m_step:eval t t' eval_many t' u ------------------------- (m_step) eval_many t u
If we have a goal such as eval_many e1 e2, we should be able to use apply m_step in order to replace it with the goals eval e1 t' and eval_many t' e2. But what exactly is t' here? When and how is it chosen? It stands to reason the conclusion is justified if we can come up with any t' for which the premises can be justified.
Now we note that, in the Coq syntax for the type of m_step, all three variables t, t', and u are universally quantified. The tactic apply m_step will use pattern matching between our goal and the conclusion of m_step to find the only possible instantiation of t and u. However, apply m_step will raise an error since it does not know how it should instantiate t'. In this case, the apply tactic takes a with clause that allows us to provide this instantiation. This is demonstrated in the proof below. (Note that the use of this feature means that our proof scripts are not invariant under alpha-equivalence on the types of our constructors and lemmas. If this is a concern, there are other means of achieving the same result in a way that is compatible with alpha-conversion. See the next example.)
Observe how this works in the proof script below. The proof tree here gives a visual representation of the proof term we are going to construct and the proof script has again been annotated with the steps in English.

Let t be a tm, and assume nvalue t.
By m_step, to show our conclusion, it suffices to find
some t' for which
eval (tm_succ (tm_pred (tm_succ t))) t'
and
eval t' (tm_succ t).
Let us choose t' to be tm_succ t.
By the lemma e_succ_pred_succ, to show
eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t),
it suffices to show nvalue t.
And, in fact, we assumed nvalue t.
Moreover, by the rule m_refl, we also may conclude
eval (tm_succ t) (tm_succ t).
Example
Coq is built around the Curry-Howard correspondence. Proofs of universally quantified propositions are functions that take the witness of the quantifier as an argument. Similarly, proofs of implications are functions that take one proof as an argument and return another proof. Observe the types of the following terms.Check (e_succ_pred_succ).
Check (e_succ_pred_succ tm_zero).
Check (n_zero).
Check (e_succ_pred_succ tm_zero n_zero).
Example
Any tactic like apply that takes the name of a constructor or lemma as an argument can just as easily be given a more complicated expression as an argument. Thus, we may use function application to construct proof objects on the fly in these cases. Observe how this technique can be used to rewrite the proof of the previous lemma.Although, we have eliminated one use of apply, this is not necessarily an improvement over the previous proof. However, there are cases where this technique is quite valuable.
Lemma m_succ_pred_succ_alt : forall t,
nvalue t ->
eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t).
Check m_step.
Check e_succ_pred_succ.
Check m_refl.
Qed.
Hint for PG users
By default, the "." key is "electric" -- it inserts a period _and_ causes the material up to the cursor to be sent to Coq. If you find this behavior annoying, it can be toggled by doing "C-c .".Exercise
Write a proof script to prove the following lemma, based upon the proof given in English.Note: The lemma and the next should be useful in later proofs.
Let t1 and t2 be terms, and assume eval t1 t2. We
may conclude eval_many t1 t2 by m_step if we can find
a term t' such that eval t1 t' and eval_many t' t2.
We will choose t' to be t2. Now we can show
eval t1 t2 by our assumption, and we can show
eval_many t2 t2 by m_refl.
Let t1, t2, and t3 be terms. Assume eval t1 t2
and eval t2 t3. By m_step, we may conclude that
eval_many t1 t3 if we can find a term t' such that
eval t1 t' and eval_many t' t3. Let's choose t' to
be t2. We know eval t1 t2 holds by assumption. In
the other case, by the lemma m_one, to show eval_many
t2 t3, it suffices to show eval t2 t3, which is one of
our assumptions.
Lemma m_iftrue_step : forall t t1 t2 u,
eval t tm_true ->
eval_many t1 u ->
eval_many (tm_if t t1 t2) u.
eval t tm_true ->
eval_many t1 u ->
eval_many (tm_if t t1 t2) u.
Let t, t1, t2, and u be terms. Assume that
eval t tm_true and eval_many t1 u. To show
eval_many (tm_if t t1 t2) u, by m_step, it suffices to
find a t' for which eval (tm_if t t1 t2) t' and
eval_many t' u. Let us choose t' to be
tm_if tm_true t1 t2. Now we can use e_if to show that
eval (tm_if t t1 t2) (tm_if tm_true t1 t2) if we can
show eval t tm_true, which is actually one of our
assumptions. Moreover, using m_step once more, we can
show eval_many (tm_if tm_true t1 t2) u where t' is
chosen to be t1. Doing so leaves us to show
eval (tm_if tm_true t1 t2) t1 and eval_many t1 u. The
former holds by e_iftrue and the latter holds by
assumption.
Example
There is a notion of equivalence on Coq terms that arises from the conversion rules of the underlying calculus of constructions. It is sometimes useful to be able to replace one term in a proof with an equivalent one. For instance, we may want to replace a defined name with its definition. This sort of replacement can be done the tactic unfold. This tactic can be used to manipulate the goal or the hypotheses.Definition strongly_diverges t :=
forall u, eval_many t u -> ~ normal_form u.
Lemma unfold_example : forall t t',
strongly_diverges t ->
eval t t' ->
strongly_diverges t'.
Exercise
In reality, many tactics will perform conversion automatically as necessary. Try removing the uses of unfold from the above proof to check which ones were necessary.Working with Conjunction and Disjunction
- split
- left
- right
- destruct (for conjunction and disjunction)
Example
If H is the name of a conjunctive hypothesis, then destruct H as p will replace the hypothesis H with its components using the names in the pattern p. Observe the pattern in the example below.Example
Patterns may be nested to break apart nested structures. Note that infix conjunction is right-associative, which is significant when trying to write nested patterns. We will later see how to use destruct on many different sorts of hypotheses.
Lemma m_three_conj : forall t t' t'' t''',
eval t t' /\ eval t' t'' /\ eval t'' t''' ->
eval_many t t'''.
eval t t' /\ eval t' t'' /\ eval t'' t''' ->
eval_many t t'''.
Lemma m_three : forall t t' t'' t''',
eval t t' ->
eval t' t'' ->
eval t'' t''' ->
eval_many t t'''.
eval t t' ->
eval t' t'' ->
eval t'' t''' ->
eval_many t t'''.

Example
If the goal is a disjunction, we can use the left or right tactics to solve it by proving the left or right side of the conclusion.Example
If we have a disjunction in the context, we can use destruct to reason by cases on the hypothesis. Note the syntax of the associated pattern.
Lemma e_if_true_or_false : forall t1 t2,
eval t1 tm_true \/ eval t1 tm_false ->
eval_many (tm_if t1 t2 t2) t2.
eval t1 tm_true \/ eval t1 tm_false ->
eval_many (tm_if t1 t2 t2) t2.
Lemma two_values : forall t u,
value t /\ value u ->
bvalue t \/
bvalue u \/
(nvalue t /\ nvalue u).
value t /\ value u ->
bvalue t \/
bvalue u \/
(nvalue t /\ nvalue u).
We know value t and value u, which means either
bvalue t or nvalue t, and either bvalue u or
nvalue u. Consider the case in which
bvalue t holds. Then one of the disjuncts of our
conclusion is proved. Next, consider the case in which
nvalue t holds. Now consider the subcase where
bvalue u holds. ...
Example
destruct can be used on propositions with implications. This will have the effect of performing destruct on the conclusion of the implication, while leaving the hypotheses of the implication as additional subgoals.
Lemma destruct_example : forall bv t t' t'',
bvalue bv ->
(value bv -> eval t t' /\ eval t' t'') ->
eval_many t t''.
bvalue bv ->
(value bv -> eval t t' /\ eval t' t'') ->
eval_many t t''.
Tip
After applying a tactic that introduces multiple subgoals, it is sometimes useful to see not only the subgoals themselves but also their hypotheses. Adding the command Show n. to your proof script to cause Coq to display the nth subgoal in full.Example
Use destruct to reason by cases on an inductively defined datatype or proposition.Note: It is possible to supply destruct with a pattern in these instances also. However, the patterns become increasingly complex for bigger inductive definitions; so it is often more practical to omit the pattern (thereby letting Coq choose the names of the terms and hypotheses in each case), in spite of the fact that this adds an element of fragility to the proof script (since the proof script will mention names that were system-generated).
Lemma e_iszero_nvalue : forall v,
nvalue v ->
eval (tm_iszero v) tm_true \/
eval (tm_iszero v) tm_false.
nvalue v ->
eval (tm_iszero v) tm_true \/
eval (tm_iszero v) tm_false.
Example
You can use induction to reason by induction on an inductively defined datatype or proposition. This is the same as destruct, except that it also introduces an induction hypothesis in the inductive cases.
We proceed by induction on the derivation of
eval_many t t'.
Case m_refl: Since t and t' must be the same, our
conclusion holds by assumption.
Case m_step: Now let's rename the t' from the lemma
statement to u0 (as Coq likely will) and observe that
there must be some t' (from above the line of the
m_step rule) such that eval t t' and
eval_many t' u0. Our conclusion follows from from
an application of m_step with our new t' and our
induction hypothesis, which allows us to piece together
eval_many t' u0 and eval_many u0 u to get
eval_many t' u.
Exercise
It is possible to use destruct not just on hypotheses but on any lemma we have proved. If we have a lemmalemma1 : P /\ Q
then we can use the tactic
destruct lemma1 as [ H1 H2 ].
to continue our proof with H1 : P and H2 : Q in our context. This works even if the lemma has antecedents (they become new subgoals); however it fail if the lemma has a universal quantifier, such as this:
lemma2 : forall x, P(x) /\ Q(x)
However, remember that we can build a proof of P(e) /\ Q(e) (which can be destructed) using the Coq expression lemma2 e. So we need to phrase our tactic as
destruct (lemma2 e) as [ H1 H2 ].
An example of this technique is below.
Lemma m_iszero_nvalue : forall t v,
nvalue v ->
eval_many t v ->
eval_many (tm_iszero t) tm_true \/
eval_many (tm_iszero t) tm_false.
nvalue v ->
eval_many t v ->
eval_many (tm_iszero t) tm_true \/
eval_many (tm_iszero t) tm_false.
Exercise
Prove the following lemma.Hint: You may be interested in some previously proved lemmas, such as m_one and m_trans.
Note: Even though this lemma is in a comment, its solution is also at the bottom. (Coq will give an error if we leave it uncommented since it mentions the eval_rtc relation, which was the solution to another exercise.)
Lemma eval_rtc_many : forall t u, eval_rtc t u -> eval_many t u.
Exercise
Prove the following lemma.Lemma eval_many_rtc : forall t u, eval_many t u -> eval_rtc t u.
Exercise
Prove the following lemma.Lemma full_eval_to_value : forall t v, full_eval t v -> value v.
Example
Tip: We can combine patterns that destruct existentials with patterns that destruct other logical connectives.Here is the same proof with just one use of destruct.
Example
Tip: We give patterns to the intros tactic to destruct hypotheses as we introduce them.Here is the same proof again without any uses of destruct.
Exercise
Tip: You should find the lemma m_iszero useful. Use Check m_iszero. if you've forgotten its statement.
Lemma exists_iszero_nvalue : forall t,
(exists nv, nvalue nv /\ eval_many t nv) ->
exists bv, eval_many (tm_iszero t) bv.
(exists nv, nvalue nv /\ eval_many t nv) ->
exists bv, eval_many (tm_iszero t) bv.
There exists some nv such that nvalue nv. Consider
the case where nv is tm_zero. Then choose bv to
be tm_true. By m_trans, we can show that
eval_many (tm_iszero t) tm_true by showing
eval_many (tm_iszero t) (tm_iszero tm_zero) and
eval_many (tm_iszero tm_zero) tm_true. The former
follows from m_iszero and our assumption. The latter
follows from m_one and the rule e_iszerozero. On the
other hand, in the case where nv is built from
tm_succ, we choose bv to be tm_false and the proof
follows similarly.
Example
The standard library defines an uninhabited type False and defines not P to stand for P -> False. Furthermore, Coq defines the notation ~ P to stand for not P. (Such notations only affect parsing and printing -- Coq views not P and ~ P as being syntactically equal.)The most basic way to work with negated statements is to unfold not and treat False just as any other proposition.
(Note how multiple definitions can be unfolded with one use of unfold. Also, as noted earlier, many uses of unfold are not strictly necessary. You can try deleting the uses from the proof below to check that the proof script still works.)
Example
If you happen to have False as a hypothesis, you may use destruct on that hypothesis to solve your goal.Example
Recalling that destruct can be used on propositions with antecedents and that negation is simply an abbreviation for an implication, using destruct on a negated hypothesis has the derived behavior of replacing our goal with the proposition that was negated in our context.Tip: We actually don't even need to do the unfolding below because destruct would have done it for us.
Lemma destruct_negation_example : forall t v,
value v ->
eval t tm_zero ->
(value v -> normal_form t) ->
eval tm_true tm_false.
value v ->
eval t tm_zero ->
(value v -> normal_form t) ->
eval tm_true tm_false.
Lemma negation_exercise : forall v1 v2,
~ (value v1 \/ value v2) ->
~ (~ bvalue v1 /\ ~ bvalue v2) ->
eval tm_true tm_false.
~ (value v1 \/ value v2) ->
~ (~ bvalue v1 /\ ~ bvalue v2) ->
eval tm_true tm_false.
Example
If you have an equality in your context, there are several ways to substitute one side of the equality for the other in your goal or in other hypotheses.If one side of the equality is a variable x, then the tactic subst x will replace all occurrences of x in the context and goal with the other side of the quality and will remove x from your context.
Use reflexivity to solve a goal of the form e = e.
Lemma equality_example_1 : forall t1 t2 t3 u1 u2,
t1 = tm_iszero u1 ->
t2 = tm_succ u2 ->
t3 = tm_succ t2 ->
tm_if t1 t2 t3 =
tm_if (tm_iszero u1) (tm_succ u2) (tm_succ (tm_succ u2)).
t1 = tm_iszero u1 ->
t2 = tm_succ u2 ->
t3 = tm_succ t2 ->
tm_if t1 t2 t3 =
tm_if (tm_iszero u1) (tm_succ u2) (tm_succ (tm_succ u2)).
Example
If neither side of the equality in your context is a variable (or if you don't want to discard the hypothesis), you can use the rewrite tactic to perform a substitution. The arrow after rewrite indicates the direction of the substitution. As demonstrated, you may perform rewriting in the goal or in a hypothesis.
Lemma equality_example_2a : forall t u v,
tm_succ t = tm_succ u ->
eval (tm_succ u) v ->
eval (tm_succ t) v.
Lemma equality_example_2b : forall t u v,
tm_succ t = tm_succ u ->
eval (tm_succ u) v ->
eval (tm_succ t) v.
tm_succ t = tm_succ u ->
eval (tm_succ u) v ->
eval (tm_succ t) v.
Lemma equality_example_2b : forall t u v,
tm_succ t = tm_succ u ->
eval (tm_succ u) v ->
eval (tm_succ t) v.
Example
We also note that, analogously with destruct, we may use rewrite even with a hypothesis (or lemma) that has antecedents.
Lemma equality_example_2c : forall t u v,
nvalue v ->
(nvalue v -> tm_succ t = tm_succ u) ->
eval (tm_succ u) v ->
eval (tm_succ t) v.
nvalue v ->
(nvalue v -> tm_succ t = tm_succ u) ->
eval (tm_succ u) v ->
eval (tm_succ t) v.
Example
If you need to derive additional equalities implied by an equality in your context (e.g., by the principle of constructor injectivity), you may use inversion. inversion is a powerful tactic that uses unification to introduce more equalities into your context. (You will observe that it also performs some substitutions in your goal.)
Lemma equality_exercise : forall t1 t2 t3 u1 u2 u3 u4,
tm_if t1 t2 t3 = tm_if u1 u2 u2 ->
tm_if t1 t2 t3 = tm_if u3 u3 u4 ->
t1 = u4.
tm_if t1 t2 t3 = tm_if u1 u2 u2 ->
tm_if t1 t2 t3 = tm_if u3 u3 u4 ->
t1 = u4.
Example
inversion will also solve a goal when unification fails on a hypothesis. (Internally, Coq can construct a proof of False from contradictory equalities.)Exercise
Note: e1 <> e2 is a notation for ~ e1 = e2, i.e., the two are treated as syntactically equal.Note: This is fairly trivial to prove if we have a size function on terms and some automation. With just the tools we have described so far, it requires just a little bit of work.
Hint: The proof requires induction on t. (This is the first example of induction on datatypes, but it is even more straightforward than induction on propositions.) In each case, unfold the negation, pull the equality into the context, and use inversion to eliminate contradictory equalities.
Example
The inversion tactic also allows you to reason by inversion on an inductively defined proposition as in paper proofs: we try to match some proposition with the conclusion of each inference rule and only consider the cases (possibly none) where there is a successful unification. In those cases, we may use the premises of the inference rule in our reasoning.Since inversion may generate many equalities between variables, it is useful to know that using subst without an argument will perform all possible substitutions for variables. It is a little difficult to predict which variables will be eliminated and which will be kept by this tactic, but this is a typical sort of trade-off when using powerful tactics.
(The use of subst in this proof is superfluous, but you can observe that it simplifies the context.)
By inversion on the eval_many relation, then conclusion
eval_many (tm_pred t) tm_zero must have been derived by
the rule m_step, which means there is some t' for
which eval (tm_pred t) t' and eval_many t' tm_zero.
Now, by inversion on the eval relation, there are only
three ways that eval (tm_pred t) t' could have been
derived:
By e_predzero, with t and t' both being equal to
tm_zero. Our conclusion follows from n_zero.By e_predsucc, with t being tm_succ t0 where we
have nvalue t0. In this case, our conclusion is provable with n_succ.By e_pred, with t taking an evaluation step. This
contradicts our assumption that t is a normal form (which can be shown by using destruct on that assumption).
Lemma contradictory_equalities_exercise :
(exists t, exists u, exists v,
value t /\
t = tm_succ u /\
u = tm_pred v) ->
eval tm_true tm_false.
(exists t, exists u, exists v,
value t /\
t = tm_succ u /\
u = tm_pred v) ->
eval tm_true tm_false.
Lemma eval_fact_exercise : forall t1 t2,
eval (tm_iszero (tm_pred t1)) t2 ->
eval t2 tm_false ->
exists u, t1 = tm_succ u.
eval (tm_iszero (tm_pred t1)) t2 ->
eval t2 tm_false ->
exists u, t1 = tm_succ u.
Lemma normal_form_if : forall t1 t2 t3,
normal_form (tm_if t1 t2 t3) ->
t1 <> tm_true /\ t1 <> tm_false /\ normal_form t1.
normal_form (tm_if t1 t2 t3) ->
t1 <> tm_true /\ t1 <> tm_false /\ normal_form t1.
Example
Sometimes we need to have a tactic that moves hypotheses from our context back into our goal. Often this is because we want to perform induction in the middle of a proof and will not get a sufficiently general induction hypothesis without a goal of the correct form. (To be specific, if we need to have an induction hypothesis with a forall quantifier in front, then we must make sure our goal has a forall quantifier in front at the time we invoke the induction tactic.) Observe how generalize dependent achieves this in the proof below, moving the variable t and all dependent hypotheses back into the goal. You may want to remove the use of generalize dependent to convince yourself that it is performing an essential role here.Exercise
Coq has many operations (called "tacticals") to combine smaller tactics into larger ones.If t1 and t2 are tactics, then t1; t2 is a tactic that executes t1, and then executes t2 on subgoals left by or newly generated by t1. This can help to eliminate repetitious use of tactics. Two idiomatic uses are performing subst after inversion and performing intros after induction. More opportunities to use this tactical can usually be discovered after writing a proof. (It is worth noting that some uses of this tactical can make proofs less readable or more difficult to maintain. Alternatively, some uses can make proofs more readable or easier to maintain. It is always good to think about your priorities when writing a proof script.)
Revise the proof for value_is_normal_form to include uses of the ; tactical.
Example
Sometimes it is helpful to be able to use forward reasoning in a proof. One form of forward reasoning can be done with the tactic assert. assert adds a new hypothesis to the context but asks us to first justify it.Example
assert can also be supplied with a tactic that proves the assertion. We rewrite the above proof using this form.Example
The proof below introduces two new, simple tactics. First, the tactic replace e1 with e2 performs a substitution in the goal and then requires that you prove e2 = e1 as a new subgoal. This often allows us to avoid more cumbersome forms of forward reasoning. Second, the clear tactic discards a hypothesis from the context. Of course, this tactic is never needed, but it can be nice to use when there are complicated, irrelevant hypotheses in the context.
Lemma single_step_to_multi_step_determinacy :
(forall t u1 u2, eval t u1 -> eval t u2 -> u1 = u2) ->
forall t v1 v2,
eval_many t v1 -> normal_form v1 ->
eval_many t v2 -> normal_form v2 ->
v1 = v2.
(forall t u1 u2, eval t u1 -> eval t u2 -> u1 = u2) ->
forall t v1 v2,
eval_many t v1 -> normal_form v1 ->
eval_many t v2 -> normal_form v2 ->
v1 = v2.
Exercise
This proof is lengthy and thus somewhat challenging. All of the techniques from this section will be useful; some will be essential. In particular, you will need to use generalize dependent at the beginning of the proof. You will find assert helpful in the cases where your assumptions are contradictory but none of them are in a negative form. In that situation, you can assert a negative statement that follows from your hypotheses (recall that normal_form is a negative statement). Finally, you will want to use the above lemma nvalue_is_normal_form. Good luck!Exercise
Prove the following lemmas. The last is quite long, and you may wish to wait until you know more about automation.Lemma full_eval_from_value : forall v w, value v -> full_eval v w -> v = w. Lemma eval_full_eval : forall t t' v, eval t t' -> full_eval t' v -> full_eval t v. Lemma full_eval_complete : forall t v, value v -> eval_many t v -> full_eval t v.
Example
You can use eapply e instead of apply e with (x := e1). This will generate subgoals containing unification variables that will get unified during subsequent uses of apply.Example
You can use esplit to turn an existentially quantified variable in your goal into a unification variable.Example
The auto tactic solves goals that are solvable by any combination of- intros
- apply (used on some local hypothesis)
- split, left, right
- reflexivity
If auto cannot solve the goal, it will leave the proof state completely unchanged (without generating any errors).
The lemma below is a proposition that has been contrived for the sake of demonstrating the scope of the auto tactic and does not say anything of practical interest. So instead of thinking about what it means, you should think about the operations that auto had to perform to solve the goal.
Note: It is important to remember that auto does not destruct hypotheses! There are more advanced forms of automation available that do destruct hypotheses in some specific ways.
Lemma auto_example : forall t t' t'',
eval t t' ->
eval t' t'' ->
(forall u, eval t t' -> eval t' u -> eval_many t u) ->
eval t' t \/ t = t /\ eval_many t t''.
eval t t' ->
eval t' t'' ->
(forall u, eval t t' -> eval t' u -> eval_many t u) ->
eval t' t \/ t = t /\ eval_many t t''.
Example
The eauto tactic solves goals that are solvable by some combination of- intros
- eapply (used on some local hypothesis)
- split, left, right
- esplit
- reflexivity
This lemma has two significantly differences from the previous one, both of which render auto useless.
Lemma eauto_example : forall t t' t'',
eval t t' ->
eval t' t'' ->
(forall u, eval t u -> eval u t'' -> eval_many t t'') ->
eval t' t \/ (exists u, t = u) /\ eval_many t t''.
eval t t' ->
eval t' t'' ->
(forall u, eval t u -> eval u t'' -> eval_many t t'') ->
eval t' t \/ (exists u, t = u) /\ eval_many t t''.
Example
You can enhance auto (or eauto) by appending using x_1, ..., x_n, where each x_i is the name of some constructor or lemma. Then auto will attempt to apply those constructors or lemmas in addition to the assumptions in the local context.
Lemma eauto_using_example : forall t t' t'',
eval t t' ->
eval t' t'' ->
eval t' t \/ t = t /\ eval_many t t''.
eval t t' ->
eval t' t'' ->
eval t' t \/ t = t /\ eval_many t t''.
Exercise
Go back and rewrite your proofs for m_one, m_two, and m_iftrue_step. You should be able to make them very succinct given what you know now.Exercise
See how short you can make these proofs.Note: This is an exercise. We are not making the claim that shorter proofs are necessarily better!
Hint: Remember that we can connect tactics in sequence with ;. However, as you can imagine, figuring out the best thing to write after a ; usually involves some trial and error.
Lemma pred_not_circular : forall t,
t <> tm_pred t.
Lemma m_succ : forall t u,
eval_many t u ->
eval_many (tm_succ t) (tm_succ u).
Lemma m_pred : forall t u,
eval_many t u ->
eval_many (tm_pred t) (tm_pred u).
t <> tm_pred t.
Lemma m_succ : forall t u,
eval_many t u ->
eval_many (tm_succ t) (tm_succ u).
Lemma m_pred : forall t u,
eval_many t u ->
eval_many (tm_pred t) (tm_pred u).
Exercise
Go back and rewrite your proofs for m_trans and two_values. Pulling together several tricks you've learned, you should be able to prove two_values in one (short) line.Note
Sometimes there are lemmas or constructors that are so frequently needed by auto that we don't want to have to add them to our using clause each time. Coq allows us to request that certain propositions that always be considered by auto and eauto.The following command adds four lemmas to the default search procedure of auto.
Constructors of inductively defined propositions are some of
the most frequently needed by auto. Instead of writing
we may simply write
Let's add all our constructors to auto.
Hint Resolve b_true b_false.
we may simply write
Hint Constructors bvalue.
Let's add all our constructors to auto.
Hint Constructors bvalue nvalue eval eval_many.
By default auto will never try to unfold definitions to
see if a lemma or constructor can be applied. With the
Hint Unfold command, we can instruct auto to try unfold
definitions in the goal as it is working.
There are a few more variants on the Hint command that can
be used to further customize auto. You can learn about
them in the Coq reference manual.
Functions and Conversion
- Fixpoint/struct
- match ... end
- if ... then ... else ...
- simpl
- remember
In this section we start to use Coq as a programming language and learn how to reason about programs defined within Coq.
Example
Coq defines many datatypes in its standard libraries. Have a quick look now through the library Datatypes to see some of the basic ones, in particular bool and nat. (Note that constructors of the datatype nat are the letter O and the letter S. However, Coq will parse and print nats using a standard decimal representation.)We define two more datatypes here that will be useful later.
Inductive bool_option : Set :=
| some_bool : bool -> bool_option
| no_bool : bool_option.
Inductive nat_option : Set :=
| some_nat : nat -> nat_option
| no_nat : nat_option.
| some_bool : bool -> bool_option
| no_bool : bool_option.
Inductive nat_option : Set :=
| some_nat : nat -> nat_option
| no_nat : nat_option.
Example
We can define simple (non-recursive) functions from one datatype to another using the Definition keyword. The match construct allows us to do case analysis on a datatype. The match expression has a first-match semantics and allows nested patterns; however, Coq's type checker demands that pattern-matching be exhaustive.We define functions below for converting between Coq bools and boolean values in our object language.
Definition tm_to_bool (t : tm) : bool_option :=
match t with
| tm_true => some_bool true
| tm_false => some_bool false
| _ => no_bool
end.
Definition bool_to_tm (b : bool) : tm :=
match b with
| true => tm_true
| false => tm_false
end.
match t with
| tm_true => some_bool true
| tm_false => some_bool false
| _ => no_bool
end.
Definition bool_to_tm (b : bool) : tm :=
match b with
| true => tm_true
| false => tm_false
end.
Example
Coq also has an if/then/else expression. It can be used, not just with the type bool but, in fact, with any datatype having exactly two constructors (the first constructor corresponding to the then branch and the second to the else branch). Thus, we can define a function is_bool as below.Example
To define a recursive function, use Fixpoint instead of Definition.The type system will only allow us to write functions that terminate. The annotation {struct t} here informs the type-checker that termination is guaranteed because the function is being defined by structural recursion on t.
Fixpoint tm_to_nat (t : tm) {struct t} : nat_option :=
match t with
| tm_zero => some_nat O
| tm_succ t1 =>
match tm_to_nat t1 with
| some_nat n => some_nat (S n)
| no_nat => no_nat
end
| _ => no_nat
end.
Fixpoint nat_to_tm (n : nat) {struct n} : tm :=
match n with
| O => tm_zero
| S m => tm_succ (nat_to_tm m)
end.
match t with
| tm_zero => some_nat O
| tm_succ t1 =>
match tm_to_nat t1 with
| some_nat n => some_nat (S n)
| no_nat => no_nat
end
| _ => no_nat
end.
Fixpoint nat_to_tm (n : nat) {struct n} : tm :=
match n with
| O => tm_zero
| S m => tm_succ (nat_to_tm m)
end.
Exercise
Write a function interp : tm -> tm that returns the normal form of its argument according to the small-step semantics given by eval.Hint: You will want to use tm_to_nat (or another auxiliary function) to prevent stuck terms from stepping in the cases e_predsucc and e_iszerosucc.
Example
The tactic simpl (recursively) reduces the application of a function defined by pattern-matching to an argument with a constructor at its head. You can supply simpl with a particular expression if you want to prevent it from simplifying elsewhere.
Lemma tm_to_bool_dom_includes_bvalue : forall bv,
bvalue bv -> exists b, tm_to_bool bv = some_bool b.
bvalue bv -> exists b, tm_to_bool bv = some_bool b.
Example
Not all uses of simpl are optional. Sometimes they are necessary so that we can use the rewrite tactic. Observe, also, how using rewrite can automatically trigger a reduction if it creates a redex.Example
Here's an example where it is necessary to use simpl on a hypothesis. To trigger a reduction of a match expression in a hypothesis, we use the destruct tactic on the expression being matched.Example
Using the tactic destruct (or induction) on a complex expression (i.e., one that is not simply a variable) may not leave you with enough information for you to finish the proof. The tactic remember can help in these cases. Its usage is demonstrated below. If you are curious, try to finish the proof without remember to see what goes wrong.
Lemma remember_example : forall v,
eval_many
(tm_pred (tm_succ v))
(match tm_to_nat v with
| some_nat _ => v
| no_nat => tm_pred (tm_succ v)
end).
eval_many
(tm_pred (tm_succ v))
(match tm_to_nat v with
| some_nat _ => v
| no_nat => tm_pred (tm_succ v)
end).
Exercise
Prove the following lemmas involving the function interp from a previous exercise:Lemma interp_reduces : forall t, eval_many t (interp t). Lemma interp_fully_reduces : forall t, normal_form (interp t).
Inductive eval_rtc : tm -> tm -> Prop :=
| r_eval : forall t t',
eval t t' ->
eval_rtc t t'
| r_refl : forall t,
eval_rtc t t
| r_trans : forall t u v,
eval_rtc t u ->
eval_rtc u v ->
eval_rtc t v.
Inductive full_eval : tm -> tm -> Prop :=
| f_value : forall v,
value v ->
full_eval v v
| f_iftrue : forall t1 t2 t3 v,
full_eval t1 tm_true ->
full_eval t2 v ->
full_eval (tm_if t1 t2 t3) v
| f_iffalse : forall t1 t2 t3 v,
full_eval t1 tm_false ->
full_eval t3 v ->
full_eval (tm_if t1 t2 t3) v
| f_succ : forall t v,
nvalue v ->
full_eval t v ->
full_eval (tm_succ t) (tm_succ v)
| f_predzero : forall t,
full_eval t tm_zero ->
full_eval (tm_pred t) tm_zero
| f_predsucc : forall t v,
nvalue v ->
full_eval t (tm_succ v) ->
full_eval (tm_pred t) v
| f_iszerozero : forall t,
full_eval t tm_zero ->
full_eval (tm_iszero t) tm_true
| f_iszerosucc : forall t v,
nvalue v ->
full_eval t (tm_succ v) ->
full_eval (tm_iszero t) tm_false.
Lemma m_one_sol : forall t t',
eval t t' ->
eval_many t t'.
Lemma m_two_sol : forall t t' t'',
eval t t' ->
eval t' t'' ->
eval_many t t''.
Lemma m_iftrue_step_sol : forall t t1 t2 u,
eval t tm_true ->
eval_many t1 u ->
eval_many (tm_if t t1 t2) u.
Lemma m_if_iszero_conj_sol : forall v t2 t2' t3 t3',
nvalue v /\ eval t2 t2' /\ eval t3 t3' ->
eval_many (tm_if (tm_iszero tm_zero) t2 t3) t2' /\
eval_many (tm_if (tm_iszero (tm_succ v)) t2 t3) t3'.
Lemma two_values_sol : forall t u,
value t /\ value u ->
bvalue t \/
bvalue u \/
(nvalue t /\ nvalue u).
Lemma m_trans_sol : forall t u v,
eval_many t u ->
eval_many u v ->
eval_many t v.
Lemma eval_rtc_many_sol : forall t u,
eval_rtc t u ->
eval_many t u.
Lemma eval_many_rtc_sol : forall t u,
eval_many t u ->
eval_rtc t u.
Lemma full_eval_to_value_sol : forall t v,
full_eval t v ->
value v.
Lemma value_can_expand_sol : forall v,
value v ->
exists u, eval u v.
Lemma exists_iszero_nvalue_sol : forall t,
(exists nv, nvalue nv /\ eval_many t nv) ->
exists bv, eval_many (tm_iszero t) bv.
Lemma normal_form_to_forall_sol : forall t,
normal_form t ->
forall u, ~ eval t u.
Lemma normal_form_from_forall_sol : forall t,
(forall u, ~ eval t u) ->
normal_form t.
Lemma negation_exercise_sol : forall v1 v2,
~ (value v1 \/ value v2) ->
~ (~ bvalue v1 /\ ~ bvalue v2) ->
eval tm_true tm_false.
Lemma equality_exercise_sol : forall t1 t2 t3 u1 u2 u3 u4,
tm_if t1 t2 t3 = tm_if u1 u2 u2 ->
tm_if t1 t2 t3 = tm_if u3 u3 u4 ->
t1 = u4.
Lemma succ_not_circular_sol : forall t,
t <> tm_succ t.
Lemma inversion_exercise_sol : forall t,
normal_form t ->
eval_many (tm_pred t) tm_zero ->
nvalue t.
Lemma contradictory_equalities_exercise_sol :
(exists t, exists u, exists v,
value t /\
t = tm_succ u /\
u = tm_pred v) ->
eval tm_true tm_false.
Lemma eval_fact_exercise_sol : forall t1 t2,
eval (tm_iszero (tm_pred t1)) t2 ->
eval t2 tm_false ->
exists u, t1 = tm_succ u.
Lemma normal_form_if_sol : forall t1 t2 t3,
normal_form (tm_if t1 t2 t3) ->
t1 <> tm_true /\ t1 <> tm_false /\ normal_form t1.
Lemma full_eval_from_value_sol : forall v w,
value v ->
full_eval v w ->
v = w.
Lemma value_is_normal_form_sol : forall v,
value v ->
normal_form v.
Theorem eval_deterministic_sol : forall t t' t'',
eval t t' ->
eval t t'' ->
t' = t''.
Lemma eval_full_eval_sol : forall t t' v,
eval t t' ->
full_eval t' v ->
full_eval t v.
Lemma full_eval_complete_sol : forall t v,
value v ->
eval_many t v ->
full_eval t v.
Lemma pred_not_circular_sol : forall t,
t <> tm_pred t.
Lemma m_succ_sol : forall t u,
eval_many t u ->
eval_many (tm_succ t) (tm_succ u).
Lemma m_pred_sol : forall t u,
eval_many t u ->
eval_many (tm_pred t) (tm_pred u).
Fixpoint interp (t : tm) {struct t} : tm :=
match t with
| tm_true => tm_true
| tm_false => tm_false
| tm_if t1 t2 t3 =>
match interp t1 with
| tm_true => interp t2
| tm_false => interp t3
| t4 => tm_if t4 t2 t3
end
| tm_zero => tm_zero
| tm_succ t1 => tm_succ (interp t1)
| tm_pred t1 =>
match interp t1 with
| tm_zero => tm_zero
| tm_succ t2 =>
match tm_to_nat t2 with
| some_nat _ => t2
| no_nat => tm_pred (tm_succ t2)
end
| t2 => tm_pred t2
end
| tm_iszero t1 =>
match interp t1 with
| tm_zero => tm_true
| tm_succ t2 =>
match tm_to_nat t2 with
| some_nat _ => tm_false
| no_nat => tm_iszero (tm_succ t2)
end
| t2 => tm_iszero t2
end
end.
Lemma tm_to_bool_dom_includes_bvalue_sol : forall bv,
bvalue bv -> exists b, tm_to_bool bv = some_bool b.
Lemma tm_to_bool_dom_only_bvalue_sol : forall bv b,
tm_to_bool bv = some_bool b -> bvalue bv.
Lemma tm_to_nat_dom_includes_nvalue_sol : forall v,
nvalue v -> exists n, tm_to_nat v = some_nat n.
Lemma tm_to_nat_dom_only_nvalue_sol : forall v n,
tm_to_nat v = some_nat n -> nvalue v.
Lemma interp_reduces_sol : forall t,
eval_many t (interp t).
Lemma interp_fully_reduces_sol : forall t,
normal_form (interp t).
This page has been generated by coqdoc


WWE fired Superstar for breaking wind during Baron Corbin promo
by Danny HartnZo (fka Enzo Amore) discussed a variety of WWE topics during his appearance on Chris Jericho’s Talk Is Jericho podcast, including the time that he was fired by the company for breaking wind during an NXT promo class.
The former Cruiserweight Champion revealed that he tried to lighten the mood after Baron Corbin cut a “terrible” promo in front of Dusty Rhodes, but his attempt to entertain everybody else in the room backfired.
“One time we had a promo class [with] Dusty Rhodes, Baron Corbin was up there cutting a terrible promo. Baron was trying to get help and Dusty was helping him, and I just raised my hand and everybody looked at me, and I just farted, loud as hell. They fined me two hundred and fifty dollars, fired me that night, and then I got back into work the next day and they rehired me.”
(If you use quotes from this article, please credit Talk Is Jericho and give a H/T to Sportskeeda for the transcription).
Enzo Amore’s WWE career highlights
After establishing themselves as one of the most popular acts in NXT, Enzo Amore and Big Cass moved to RAW in April 2016 after WrestleMania 32.
They worked with some of the biggest names in the company during their first year on the Red brand, including John Cena and Chris Jericho, before WWE decided to separate them by turning Cass heel in June 2017.
Amore has mentioned in past media interviews that one of his career highlights came at WrestleMania 33, where he teamed with Cass in a Fatal 4-Way ladder match against The Bar, The Club and the returning Hardy Boyz.
Before he was fired by WWE in January 2018, Amore had a four-month run as the main star in the cruiserweight division on RAW and 205 Live.
Now you can rate RAW, SmackDown and NXT matches on Sportskeeda !


The Multiple Master Menu
The MM Menu provides a few commands for manipulating Multiple Master or Apple distortable fonts. If the current font is a MM itself font the menu also includes a list of all font instances that make up this one. This menu is available in the font view and the outline glyph view.
The menu as it appears in the font view
- Create MM...
- MM Valid
- MM Info...

MM Valid
Checks that the current multiple master font can be saved. So each master design must match in:
- Contours
- There must be the same number of contours and
- each contour must have the same number of points and
- each spline on the contour must be the same type (ie it can't correspond to a straight line in one font and a curve in another)
- References
- There must be the same number of references and
- Each corresponding reference must refer to the same encoding
- Hints
- Same number of hints
- HintMasks (Counter masks are not supported here)
- HintMasks at corresponding points must specify a corresponding set of hints
- Kerning
- If a glyph kerns with another glyph in one font, then a corresponding kerning pair must exist in all designs
MM Info
Brings up the multiple master dialog and allows you to modify the current multiple master font.
Blend to New Font...
Allows you to create a blended version of the current multiple master font set as a stand alone font.
MM Change Default Weights
Allows you to change the default weights assigned to each master design used in blending the default instance of the font
<sub font name>
Clicking on a different sub font name in the menu will cause that sub-font to be displayed instead of the current one. The subfonts are the master designs and the default blended font.
The menu as it appears in the outline glyph view
-
-
<sub font names>
MM Reblend
Reblends the default version of the current glyph
View
A submenu which allows you to choose which of the designs of this glyph you want displayed in the background of the view
<sub font name>
Clicking on a different sub font name in the menu will cause the glyph from that sub-font to be displayed instead of the current one. The subfonts are the master designs and the default blended font.


--- title: Check out the new TRIPLE LBi website excerpt: 'Check out the new TRIPLE LBi website: http://www.triplelbi.com/' date: '2010-09-23 09:09:28 +0200' date_gmt: '2010-09-23 07:09:28 +0200' categories: - Webdev tags: - tweets - web - design - development ---
Check out the new TRIPLE LBi website: http://www.triplelbi.com/


Adds an actor to the party given the actor id.
Returns the agility of the unit.
Returns the living party members.
Returns all items within the party's posession. Items can be of equip item, or item type.
Returns the party's armor.
Returns the battle members in the party.
Returns true if the party can use the item.

Clears the unit's actions.
Clears the action results.
Has the party consume the given item.
Returns the dead party members.
Returns the party's equippable items.
Returns true if the game party exists.
Returns the actor faces for the save file.
Increases the party gold given a specified amount.
Returns party gold.
Returns true if the encounter rate is set to half.
Returns true if the encounter rate is set to none.
Returns true if the party has double gold in effect.
Returns true if the party has the given item; if includeEquip is set to true, this will also check party equipment.
Returns true if the party has an increased chance of preemptive strike.
Returns the highest level in the party.
Returns true if unit is in battle.
Increases the Int of steps the party has taken.
Initialize all party items.
Returns true if all members of the unit are dead.
Returns true if any party member has the specified equip item.
Returns true if the game party is empty.
Returns the last item selected by the game party.
Returns the leader of the party.
Decreases the party gold given a specified amount.
Creates the action's of the game unit.
Returns the maximum battle members in the party.
Returns maximum gold of the party.
Returns the maximum Int of items of the given item.
Returns all party members.
Returns the actor that will be used in the current menu; this is for menu scenes that target one actor.
Returns the movable members in the party.
Returns the Int of items in the possession of the party of the given item.
Handler for when battle has ended.
Handler for when battle is started.
Handler for when the player walks.
Performs escape motion for the entire party.
Performs victory motion for the entire party.
Returns a random dead target from the game unit.
Returns a random target from the game unit.
Removes an actor from the party given the actor id.
Remove battle states from all actors in the party.
Refreshes the motion on all actors in the party.
Revive the battle members of the party.
Selects a member of the unit given a battler.
Sets up a test battle with the party.
Sets up the battle test items.
Sets up the battle test members.
Sets up the starting party members.
Returns the size of the party.
Returns the Int of steps the party has taken.
Returns the weapons of the party.
Generated using TypeDoc
The game object for the party. Contains information such as gold and items.


These are builds for Framer. Keep in mind that most of these are beta and some of them might be broken.


--- layout: post authors: ["Raniere Silva"] title: "Solution for the Challenges" date: 2015-07-28 time: "14:00:00" tags: ["Lessons", "Community"] ---
One of the enhancement that we have in mind for the next release of our lessons is to provide the solution for the challenges. Having the solutions will help instructors speed up when preparing the lesson for workshops and learners reading the lessons. Before we start adding the solutions will be great to have one template for how it should be write. If you have some suggestions, please add it at this issue on GitHub.


I translate geek into English and I’m a problem solver driven by every day's challenge. Work happens to be my passion and, at the core, I am also an innovator that focuses on designing and building award winning technologies for the future, as it's closer than we think.
Pure CSS3 and HTML5 Only Game prototype! Play the game and share love.
marianzburlea/css3-html5-gameAngular Attack contest project. See Gymbo in action. Record your workouts and share results with friends.
rumblex/angularattack2016-gymboLorem ipsum dolor sit amet, consectetur adipisicing.
read moreAccusantium dolor dolorum est officia, placeat ullam?
read moreBeatae dignissimos ex id quibusdam ut! Consectetur!
read moreBlanditiis cumque sit ut. Dolorum eligendi, fugiat?
read moreAtque beatae dignissimos, distinctio illum necessitatibus neque.
read moreAutem enim fugiat impedit molestiae nemo quaerat?
read moreAssumenda consequatur dignissimos ea ex minus sit!
read moreCommodi deserunt, neque nihil nobis non voluptatibus.
read more


Hi there! This document lives here to give you some basic information about your WordPress site and how to update it. The first few sections are general to all Honey Agency WordPress installations, and the rest is specific to your site. Let's get started!
If you're somewhat familiar with WordPress, feel free to skip to the next section, it's not integral to understanding your new website. WordPress is a Content Management System (CMS) - at a basic level it performs the following functions:
At Honey Agency, we custom-build the backend so site-owners don't need to worry about code or formatting, there's a few fields that you fill out and we take care of formatting via code. We usually re-size images for you as well; so unless you see a note about image sizes when you are uploading them we're taking care of the size on the front-end.
WordPress breaks down content into pages
and posts
. A page
is the most general form of webpage content: you have some text, possibly an image, and you can access that content via a URL. A post
is similar to a page
, but it's hierarchy is based on the model of a blog: you generally have the text and image content that you'd have with a page
, but posts are displayed in series and usually have a date and an author.
These are generalizations, but are the basic grounds of how a lot of the web is built.
At Honey Agency, we try to separate content-types into custom versions of a post
to make the website hierarchy more simple and streamlined for clients. For example at honeyagency.com, we have a team page with individual team members so we have a custom post
that's called Team Member
. When you want to add a new team member you don't have to custom-format anything, you just click Add New Team Member on the backend; once you fill out all the content required the team member is automatically populated in different places on the site.
Depending on your site, you might have a few custom-posts that we'll go over in the sections below.
Logging in to your WordPress site is easy: just add /wp-login
to the end of your URL, use the Password and Username (or email) provided and you're on your way. Once you login you will see what's called the WordPress dashboard-from here you can get anywhere you need to update content. If you look at the homepage of your site while logged in, there will be a black-bar along the top of the page with links to various site functions.
One of the perks of having a site with a CMS is that you have a centralized location for any images you've added site-wide. So anytime you upload images, PDFs, audio, etc to a post, a page, or a custom post they'll be added to a folder similar to the Photos
or Pictures
folder on your computer.
To get to your Media Library, click the Media Library
navigation item in the left-hand side menu in the WordPress dashboard. You'll be presented with a gallery of all the images currently on your site.
To add a media item, click Add New
from the Media Library
. From here you can drag-and-drop however many images you like (note the Maximum upload file size, this is per-file) and they'll automatically be added and have URL's generated for them. Usually, you'll simply upload images or PDFs directly to a post or page, in which case they'll be added to this library.
In the WordPress overview, you heard that the page
is the most basic form of content in WordPress, this is how we'll add & edit those.
Once you're logged in you can add a new page from either:
+ New
and click Page
Add New
.You'll be taken to the backend of a page with no title or content, when you add a title the URL will automatically be generated for you. If you want to change that URL click the area of text you want to change and edit the text, WordPress will automatically convert your text to lower-case and will replace spaces with hyphens to be URL-compatible.
After you have your title and URL set, you can use the area below to add content. The large white text-box is called a WYSIWYG (What You See Is What You Get) and will operate similarly to Microsoft Word, Apple Pages, or Google Docs.
You'll see a bar on the right-hand side of the page with options for publishing the page. To publish (make the page go live) the page, click Publish
. If you don't want people to see the content, you can choose Save Draft
. If you want to schedule the page, you can change the date where you see Publish immediately. If you want to publish the page but only want people who are logged into the site to see it (other admins) you can choose Private
under the Visibility option.
To edit a page that is already created, you can either click Edit Page
in the black top-bar when you're looking at the page from the front-end, or you can find the page by clicking Pages
in the dashboard and clicking the blue title of the page you're looking for from the list of pages.
Featured images are used as the header image and the social media "share image" (the little preview-picture people see when you share a link on a social media platform) if there isn't a custom header image on your site. These are located on the right-hand side of the page when you're editing a page
, a post
, or any type of custom post
. Click Set Featured Image
and you'll see a pop-up that should be populated with your media library. You can select a previously uploaded image or click the Upload Files
tab at the top of this pop-up to upload an image.
Site options is the location, available in the left-hand menu within the dashboard, where you'll find places to update the following:
Social media URLs are simple to update, and when the links are left blank it will hide the icons on the front-end, making it easy to toggle on and off.
To add a link, click the pencil icon, a box with a place to add the link as well as a title will pop up, all you need to do is fill those in.
The email signup form is available to edit here, but this will rarely be changed.
Search Form Placeholder
This is the content that is grayed-out within the search field.
Search Form Button
This is the text in the search button.
Default Site Image
This is the image that's displayed for social media, link sharing, etc when the shared page has no image, it should be large, but you most likely won't need to update it.
404 Text
This is where you can edit the copy that is displayed on the 404 page.
You can update the footer from the dashboard, just below where you found site options. You’re able to control:
This link interface is where you can provide a link to the schedule.
This is a field that can contain multiple values, click “Add Row” to add a link.
This links to google maps
These are the links at the very bottom of the footer.


Write an expression that checks if given integer is odd or even.
Odd?
Problem 2. Divisible by 7 and 5
Write a boolean expression that checks for given integer if it can be divided (without remainder) by 7 and 5 in the same time.
Result:
Problem 3. Rectangle area
Write an expression that calculates rectangle’s area by given width and height.
Result:
Problem 4. Third digit
Write an expression that checks for given integer if its third digit (right-to-left) is 7.
Result:
Problem 5. Third bit
Write a boolean expression for finding if the bit #3 (counting from 0) of a given integer.
The bits are counted from right to left, starting from bit #0.
The result of the expression should be either 1 or 0.
Result:
Problem 6. Point in Circle
Write an expression that checks if given point P(x, y) is within a circle K({0,0}, 5). //{0,0} is the centre and 5 is the radius
Result:
Problem 7. Is prime
Write an expression that checks if given positive integer number n (n ≤ 100) is prime.
Prime?
Problem 8. Trapezoid area
Write an expression that calculates trapezoid's area by given sides a and b and height h.
Result:
Problem 9. Point in Circle and outside Rectangle
Write an expression that checks for given point P(x, y) if it is within the circle K( (1,1), 3) and out of the rectangle R(top=1, left=-1, width=6, height=2).


This Page needs JavaScript in order to work, please enable it.
Garthering traffic-data ...
Reading realtime-log ...
Adaption-logic
rate-based
buffer-based
Forwarding-strategy
best-route
broadcast
ncc
omccrf
saf


An implementation of the computational strategy for the comprehensive analysis of condition-dependent operon maps in prokaryotes proposed by Fortino et al. (2014) <doi:10.1186/1471-2105-15-145>. It uses RNA-seq transcriptome profiles to improve prokaryotic operon map inference.
| Version: | 1.0 |
| Depends: | R (≥ 3.0.1) |
| Imports: | stats, utils, mclust, earth, plyr, seqinr, randomForest, rminer, GenomicRanges, GenomeInfoDb, S4Vectors, IRanges |
| Published: | 2016-02-24 |
| Author: | Vittorio Fortino |
| Maintainer: | Vittorio Fortino <vittorio.fortino at ttl.fi> |
| License: | GPL-3 |
| NeedsCompilation: | no |
| CRAN checks: | CONDOP results |
| Reference manual: | CONDOP.pdf |
| Package source: | CONDOP_1.0.tar.gz |
| Windows binaries: | r-devel: CONDOP_1.0.zip, r-release: CONDOP_1.0.zip, r-oldrel: CONDOP_1.0.zip |
| OS X binaries: | r-release: CONDOP_1.0.tgz, r-oldrel: CONDOP_1.0.tgz |
Please use the canonical form https://CRAN.R-project.org/package=CONDOP to link to this page.


It is very common to update single attribute of a model instance (say update first name in user profile) and save it to db.
In [18]: u = User.objects.get(id=1) In [19]: u.first_name = u"kracekumar" In [20]: u.save() Very straight forward approach. How does django send the sql query to database ?
In [22]: from django.db import connection In [22]: connection.queries Out[22]: [... {u'sql': u'UPDATE "auth_user" SET "password" = \'pbkdf2_sha256$12000$vsHWOlo1ZhZg$DrC46wq+a2jEtEzxmUEw4vQw8oV/rxEK7zVi30QLGF4=\', "last_login" = \'2014-02-01 06:55:44.
[Read More]
how not to insult developer while hiring
In December I was looking for new job. I came across one and applied. After couple of rounds of interview, co founder informed me we will get back to you, but never happened. This sounds normal but it is not.
Interview First round of interview started with online pair programming with one of the co-founder X. After that I went to their office, met product manager, co founder X had discussion for an hour.
[Read More]
On leaving HasGeek
Today (31-12-2013) is my last working day at HasGeek. It was in July 2012, I joined HasGeek. It was fabulous journey for past 18 months, meeting lot of new people, being part of events, writing lot of code. I was part of large, medium, small conferences like Fifth elephant (2012, 2013), Cartonama (2012), JSFoo(2012, 2013), Droidcon (2012, 2013), Metarefresh (2013), various hacknight and geekup.
I will be joning Aplopio Technology Inc, flagship product recruiterbox on 16 January, 2014.
[Read More]
introduction to python
This is the material which I use for teaching python to beginners.
tld;dr: Very minimal explanation more code.
Python?
Interpreted language Multiparadigm Introduction
hasgeek@hasgeek-MacBook:~/codes/python/hacknight$ python Python 2.7.3 (default, Aug 1 2012, 05:14:39) [GCC 4.6.3] on linux2 Type "help", "copyright", "credits" or "license" for more information. >>> >>> print "Let's learn Python" Let's learn Python Numbers
>>> 23 + 43 66 >>> 23 - 45 -22 >>> 23 * 45 1035 >>> 23 ** 4 279841 >>> 23 / 4 5 >>> 23 / 4.
[Read More]
Deploying full fledged flask app in production
This article will focus on deploying flask app starting from scratch like creating separate linux user, installating database, web server. Web server will be nginx, database will be postgres, python 2.7 middleware will be uwsgi, server ubuntu 13.10 x64. Flask app name is fido. Demo is carried out in Digital ocean.
Step 1 - Installation Python header
root@fido:~# apt-get install -y build-essential python-dev Install uwsgi dependencies
root@fido:~# apt-get install -y libxml2-dev libxslt1-dev Nginx, uwsgi
[Read More]
ipynb2viewer - Afternoon hack
ipython nbconvert has lot of handy options to convert ipynb to markdown, html etc… But I wanted to upload ipynb to gist.github.com and create a link in nbviewer.ipython.org. Started with curl and soon realized, it is getting messy. So wrote a small python program ipynb2viewer, Source code.
Install pip install ipynb2viewer Usage Upload all ipynb files in the given path to gist.github.com and return nbviewer urls.
ipynb2viewer all <path> Upload mentioned file to gist.
[Read More]
Why you should use IPython
In December bangpypers meetup, I gave a talk on Why you should use IPython. Here is the link to nbviewer.
Autogenerate Dockerfile from ubuntu image
I was learning docker to use in one of my projects. I kept installing packages, finally created required Ubuntu image. Suddenly thought it would be cool if I can generate Dockerfile like pip freeze > requirements.txt.
sudo docker run ubuntu dpkg --get-selections | awk '{print $1}' > base.list && sudo docker run pyextra dpkg --get-selections | awk '{print $1}'> pyextra.list && sort base.list pyextra.list | uniq -u > op.list && python -c "f = open('Dockerfile', 'w');f.
[Read More]
easy_install broken in os x mavericks
I hardly use easy_install. Nowadays all the python requirements are installed via pip.
IPython is my primary python console. After installing mavericks, I installed IPython and fired IPython console. Following warning message appeared
➜ ~ ipython /Library/Python/2.7/site-packages/IPython/utils/rlineimpl.py:94: RuntimeWarning: ****************************************************************************** libedit detected - readline will not be well behaved, including but not limited to: * crashes on tab completion * incorrect history navigation * corrupting long-lines * failure to wrap or indent lines properly It is highly recommended that you install readline, which is easy_installable: easy_install readline Note that `pip install readline` generally DOES NOT WORK, because it installs to site-packages, which come *after* lib-dynload in sys.
[Read More]
Why programmers should love to read and write
Everyday as a programmer we solve problems and introduce new problems. Most of the time is spent in reading other people source code, library documentation, replying to developers email. Though communication is what programmers do all the time with computer and humans.
Programmers around the globe suggests books like SICP. I have never come across people who suggests books like on writing well for programmers. Though I haven’t read the book myself, the point is why aren’t people recommending books like how to write well.
[Read More]


Everyone knows by now that experiences, not things, make us happy. But what if you could pay your way into a simulated experience of limitless bliss?
Defining money is easy. Defining happiness? Not so much.
We've problematized modern money in this issue of MONTAG by trying to figure out what's next: credit, cryptocurrency, or capitalism's collapse. So for the purposes of this article, let's just call money "money," and assume the status quo: that money is necessary for survival, and can also be used to buy things purely for pleasurable purposes.
Most research into whether money can buy happiness says that once you've reached the point that the amount of money you have pays for your basic physiological and safety needs, the amount of happiness money can give plateaus.
Michael Norton, a professor at the Harvard Business School and co-author of Happy Money: The Science of Smart Spending, lists a few things you can spend money on that will actually correlate to increased happiness:
- buying experiences (instead of things, because memories are forever, while stuff is not)
- denying yourself or delaying consumption (and then splurging, instead of perpetually indulging, to trick yourself out of hedonic adaptation)
- buying time (paying others to do things you don't enjoy, increasing net happiness by decreasing unpleasurable tasks)
- and "investing in others" (giving to charity, or spending money on other people)
Researchers in 2006 measured the physiological response to charitable giving based on activity in a few areas of the brain: one of which is the orbitofrontal cortex, which has been linked to reward and hedonic pleasure (also known as happiness). The same area was monitored in a study of whether knowing wine is expensive increased consumers' enjoyment, and the answer was yes, people did have a stronger pleasure response to wine that they thought cost more money.
So if you were looking for the short answer to whether money can buy happiness, it's affirmative. But why stop there, when through trying to answer this question we've figured out which parts of the brain manufacture the sensation we call happiness? Why not use technology to press that button as often as possible?
The Experience Machine
The Experience Machine is a thought experiment by Robert Nozick that questions the limits of hedonism and asks exactly this question. In its simplest form, you can enter a simulation in which everything that can possibly make you happy happens. You choose the life you want to experience in a simulation while floating in a tank and unaware that you are living inside of the simulation, and there is no reason for you to exit it, except to potentially rotate the menu of experiences. Would you plug in?
Most people, including Wait But Why's Tim Urban, say they wouldn't, because of existential FOMO: "I thought about the real world going on all around me while I lay unconscious in a vat forever, missing everything."
Alan Watts tackles another aspect of this question in his Cosmic Drama: won't we get bored of everything in our simulated lives making us perfectly happy?
But there is an argument to be made for plugging in to the Experience Machine and embracing hedonism, as The Matrix's turncoat Cypher explains while enjoying juicy and delicious simulated steak. Even if you know it's simulated (which, in the thought experiment, you do not) there is no way not to enjoy it.
Life is but a game?
"Life is a dream for the wise, a game for the fool, a comedy for the rich, a tragedy for the poor" – Sholem Aleichem
Simulated realities in science fiction ask us to question whether we would change everything about our experience of life if we could through technology. And with technological advances like virtual and augmented reality allowing for every day more lifelike, realistic simulations at our fingertips, how long will it be until we're faced with the choice of living in a technologically-mediated more perfect reality 24/7?
The next logical step would be to connect the simulation directly to brain-computer interfaces where it can be launched at the press of a button without unwieldy headgear or screens. And at that point we might as well be in the vat.
To return to Michael Norton and others' assertions that experiences are the one thing you can buy that are guaranteed to give you happiness, why exclude simulated experiences that aren't fully immersive, just immersive enough – like video games?
Josh Taylor argues in "Why Robert Nozick Should Have Played More Video Games," that MMORPGs already allow users to participate in an Experience Machine of sorts, without the real-world FOMO or the lack of interpersonal interaction.
While many inhabitants of Second Life, which still has over half a million regular users, are also constructing and living alternative lives within the game that they can engineer for maximum satisfaction.
And technology will only get better – Linden Lab's VR portal Sansar is still in beta, but it's almost guaranteed that some people, if given the opportunity to live full time in a virtual world of their own creation, would choose it over living IRL.
Full immersion in a virtual world designed just for you isn't exactly possible yet, but when it is (not if), the Experience Machine will no longer be purely a thought experiment: it'll be the most happiness money can buy.


Lorem ipsum dolor sit amet, consectetur adipisicing elit. Possimus.
There are a couple of steps to complete the setup
Step 1:
Open the Google Authenticator App on your mobile and either enter the secret below or scan the QR code.
{{secretkey}}
Step 2:
Enter the current token which appears in the Google Authenticator App and click Submit
Token


| DOSE: |
1.5 hits |
oral |
LSD |
(blotter / tab) |
My experiences with hallucinogenic drugs have been a mixture of positive and negative. I have been experimenting with them for years; sometimes with friends, in search of a high, and others with a more spiritual purpose. Always in the back of my mind has been a deep respect for the power of the drugs. The first time I tried LSD, I knew that this was special, but far from a toy. The enlightening effects carry with them endless insight into life, but can also produce an equally negative effect, if taken in a careless manner.
My personality is such that I have, many times, gone the careless route. Most times I have gotten away with it, but it does come back to bite. It's like roulette.
The story I want to share, however, is a glimpse into hope rather than despair.
It wasn't the first time I had taken acid, but it was my fathers first. I had recently begun attending college, and had consequently been introduced to the world of acid. Always being comfortable with dad, I mentioned it to him. Surprisingly, he didn't offer any resistance. In fact, he had struck up a friendship with a well respected gentleman from town, who had been filling him with positive stories about his decades of experimentaion. In retrospect it nearly brings a tear to my eye to understand the way that it all played out. Like it had been written long before it happened.
We decided on Saturday. Mom would be at work, and we'd have the house to ourselves. With great anxiety I waited for him to arrive home from morning coffee with his 'well respected' friend. Finally, at around 10AM he pulled in the driveway.
 The session began with some small talk (relatively speaking) about the coffee conversation of the morning. As time slowly disappeared, it was replaced with an overwhelming feeling of love. Our converstation drifted toward the time when he and my mom were divorced (5 yrs. when I was 4-9 yrs old). He began telling me of the mess he had made of his life during that time. He had been living with his drug addict friend and his family for those years untill one day, for some reason, he took notice of his friends son sitting on his daddies lap.
I meanwhile am beginning to sense something very special, very near. An unspeakable and undeniable power was beginning to settle in the room. Dad continues his story explaining that he and mom decided to give it another whirl right after that.
At this point tears began streaming down my face as I recalled to him a memory which chronologically seemed to coincide, with his 'son on daddies lap' epiphany. I clearly remembered grabbing the top of a Yahtzee box and all over the underside of the box, drawing crying, sad faces with the words 'I miss my daddy' coming from the mouth. I showed the box to my mom and we both began to cry. Right after this they decided to 'give it another whirl.'
Now I am overtaken with a total release of any sense of despair and feel as if God himself had settled into the entire room, connecting my father and I in an otherwise unknowable way. For that short time I was fully aware of my connection to everything, but particularly to my father; interpretations of the word father are welcome.
If the word God is a turnoff to you feel free to replace it with whatever you see fit. I know of no other way to describe what I felt that day. Anyway, I don't know if this story will help anyone else, but it is the first time I have put it in writing and it is kind of healing to relive it. My Dad passed away a few years ago, but it is a comfort to have shared that experience with him. Thanks for reading.
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.


SMV infection miRNAs soybean genes Fig RNA response miRNA G-LRB data virus target isolates expression analysis using GLYMAG. targets miR Soybean downregulated protein gene DEGs Plant regulatory upregulated identified plant small Table). infection. G-L mosaic plants unique {border-style infections network px;} #ffffff;} additional change common different infection, involved degradome family mock-inoculated shown significantly Click DEMs LINK Table Wang differentially expressed file. predicted resistance viral cleavage defense including isolates. used associated control. factor fold infected total transcripts RT-qPCR following isolate libraries responses sequences soybean. transcription Biology Chen control enrichment induced networks responsive terms < (XLSX) Cell. G-L, million mock potential regulation roles transcriptional Arabidopsis Gene Life Rsv degradome-seq described interaction interactions likely microRNAs resulted role transcript translation two-fold Expression Log Methods. RNAs Regulatory Sciences changes compared enriched host indicate number plants. previously px; represented results targeted transcriptome viruses {font-family G-LRB, GLYMAG Infection List Target Zhang accumulation cell font-size global isolates, mapped molecular nodes novel respectively sequencing showed (DEGs) (FC) (G-L, ./journal.pone. ./tpc.. Analysis B). Canada GLYMAG, GLYMAg Genes Hill However, MicroRNAs Mol NGS RACE Res. Research SMV-infected Sci. analysis, biological comparison conserved corresponding double; genome highly internal library line metabolic miRNA-mRNA modifications negative, performed positive. reads stem-loop strains study suggesting (A) (B) (GO:) Crop Data Liu Meyers Molecular ONE. RLM-' RNA-seq SMV-responsive Sequencing Strand Virus abundance analysis. border-color border-width cellular complex constructed details detected differences distinct edges. experimental growth included initiation isolate. life mRNA map miR- miR-p microRNA modification normalized pathogens process proteins provide provided related represent revealed reverse sRNA-seq shared signal significant solid; specifically starch suggest synthesis tissues uniquely work {font-style {font-weight (DEMs) (GO:), ./--- A). AW. Argonaute BMC Buss DNA Factors Genome Jeong Library Mapping MicroRNA Nature Networks Nucleic Ontario, Science Science. Small Transcription Venn Viral Williams activated analyses antisense aspartic binding blue bold cDNA commonly connections cotton courier; dark defence defense-related derived development diagram differential dpi em; encode families function generated high identification immune infections, inoculation leaf mRNAs miR, miRNA-p miRNAs, miRNAs-p miRa model mutant obtained order perfectly play pt;} rRNA regulate regulating required resulting rice sciences site solid specific strain stress study, support systemic understand validated validation virulence


{% load staticfiles %}
Login | 2018 YTU Voting
Yangon Technological University
2018 SU Election
{% csrf_token %}
Admin Login
Username :
Password :
Unable to login!
Please Try Again.


Notebooks
Story: Sun and Moon story
Sun and Moon story
Title
Sun and Moon story
Collection
Summary
A continuation of the The Sun pierces the full Moon with his knife, in which the Moon asks the Sun to leave his /kuirri (piece of neck sinew) so that the children can still see him come. The Sun consents, letting go of him (putting his knife back into his bag).
Comments
1) This story is a continuation of The Sun pierces the full Moon with his knife, p.292, 2) Additions have been made by Dia!kwain on the verso pages of the story, 3) This story is found in Book II-4
Contributors
Date
18 September 1871 (started)
Categories
Celestial bodies and aeroscopy
Keywords
Moon (and children) , Moon (pierced by Sun) , Moon (his neck sinew or |kuirri) , Moon (gently goes) , Moon (sings) , Moon (Sun and Moon story) , Sun (consents to Moon) , Sun (pierces Moon with his knife) , Sun (his knife) , Sun (his bag) , Sun (and Moon story) , children (Sun and Moon story) , sinew (neck) , sinew (called |kuirri) , sinew (Moon's) , sinew (Sun and Moon story) , song (of Moon) , song (Sun and Moon story) , name (the Moon's neck sinew is called |kuirri)
Story Pages
478-481


{% extends 'layouts/layout-cookie-banner.html' %} {% extends 'layouts/layout.html' %} {% from 'button/macro.njk' import button %} {% from 'back-link/macro.njk' import backLink %} {% block pageTitle %} This link does not work {% endblock %} {% block content %}
This may be because you have already used the link to cancel changing your phone number.
You can check or change your phone number by visiting your NHS login settings.
Visit the NHS login help centre if you do not have access to the phone number on your NHS login.
Reference: CID3003


--- layout: page title : Narcotics Anonymous Meetings header : Narcotics Anonymous Meetings group: --- {% include JB/setup %}
You can locate other Narcotics Anonymous meetings here: https://www.nerna.org/meetings/search/zip
NA is a nonprofit fellowship or society of men and women for whom drugs had become a major problem. We are recovering addicts who meet regularly to help each other stay clean. This is a program of complete abstinence from all drugs. There is only one requirement for membership, the desire to stop using. We suggest that you keep an open mind and give yourself a break. Our program is a set of principles written so simply that we can follow them in our daily lives. The most important thing about them is that they work. There are no strings attached to NA. We are not affiliated with any other organizations. We have no initiation fees or dues, no pledges to sign, no promises to make to anyone. We are not connected with any political, religious, or law enforcement groups, and are under no surveillance at any time. Anyone may join us regardless of age, race, sexual identity, creed, religion, or lack of religion. We are not interested in what or how much you used or who your connections were, what you have done in the past, how much or how little you have, but only in what you want to do about your problem and how we can help. The newcomer is the most important person at any meeting, because we can only keep what we have by giving it away. We have learned from our group experience that those who