R – How to write ∀x ( P(x) and Q(x) ) in Coq

You can do it more quickly by just applying H, but this script should be more clear.

Lemma foo : forall (A:Type) (P Q: A-> Prop), (forall x, P x /\ Q x) -> (forall x, P x).
intros.
destruct (H x). 
exact H0.
Qed.

Incrementing / Decrementing Operators

++ increment operator

-- decrement operator

Example    Name              Effect
---------------------------------------------------------------------
++$a       Pre-increment     Increments $a by one, then returns $a.
$a++       Post-increment    Returns $a, then increments $a by one.
--$a       Pre-decrement     Decrements $a by one, then returns $a.
$a--       Post-decrement    Returns $a, then decrements $a by one.

These can go before or after the variable.

If put before the variable, the increment/decrement operation is done to the variable first then the result is returned. If put after the variable, the variable is first returned, then the increment/decrement operation is done.

For example:

$apples = 10;
for ($i = 0; $i < 10; ++$i) {
    echo 'I have ' . $apples-- . " apples. I just ate one.\n";
}

Live example

In the case above ++$i is used, since it is faster. $i++ would have the same results.

Pre-increment is a little bit faster because it really increments the variable and after that 'returns' the result. Post-increment creates a special variable, copies there the value of the first variable and only after the first variable is used, replaces its value with second's.

However, you must use $apples--, since first, you want to display the current number of apples, and then you want to subtract one from it.

You can also increment letters in PHP:

$i = "a";
while ($i < "c") {
    echo $i++;
}

Once z is reached aa is next, and so on.

Note that character variables can be incremented but not decremented and even so only plain ASCII characters (a-z and A-Z) are supported.

Stack Overflow Posts:

• Understanding Incrementing