docs: Add section on how to express "FOR ALL" in Rego

This is a common question that comes up. Until we have a keyword that
lets users express "FOR ALL" we should have docs we can point to.

Fixes open-policy-agent#1307

Signed-off-by: Torin Sandall <torinsandall@gmail.com>

docs/content/how-do-i-write-policies.md

@@ -1053,6 +1053,98 @@ The result:
 +-----------+------------------------+
 ```
 
+## Universal Quantification (FOR ALL)
+
+Like SQL, Rego does not have a direct way to express _universal quantification_
+("FOR ALL"). However, like SQL, you can use other language primitives (e.g.,
+[Negation](#negation)) to express FOR ALL. For example, imagine you want to
+express a policy that says (in English):
+
+```
+There must be no apps named "bitcoin-miner".
+```
+
+A common mistake is to try encoding the policy with a rule named
+`no_bitcoin_miners` like so:
+
+```ruby
+no_bitcoin_miners {
+    app := apps[_]
+    app.name != "bitcoin-miner"  # THIS IS NOT CORRECT.
+}
+```
+
+It becomes clear that this is incorrect when you use the [`some`](#some-keyword)
+keyword, because the rule is true whenever there is SOME app that is not a
+bitcoin-miner:
+
+```ruby
+no_bitcoin_miners {
+    some i
+    app := apps[i]
+    app.name != "bitcoin-miner"
+}
+```
+
+You can confirm this by testing the rule inside the REPL:
+
+```ruby
+> no_bitcoin_miners with apps as [{"name": "bitcoin-miner"}, {"name": "web"}]
+true
+```
+
+The reason the rule is incorrect is that variables in Rego are _existentially
+quantified_. This means that rule bodies and queries express FOR ANY and not FOR
+ALL. To express FOR ALL in Rego complement the logic in the rule body (e.g.,
+`!=` becomes `==`) and then complement the check using negation (e.g.,
+`no_bitcoin_miners` becomes `not any_bitcoin_miners`).
+
+For this policy, you define a rule that finds if there exists a bitcoin-mining
+app (which is easy using the `some` keyword). And then you use negation to check
+that there is NO bitcoin-mining app. Technically, you're using 2 negations and
+an existential quantifier, which is logically the same as a universal
+quantifier.
+
+For example:
+
+```ruby
+no_bitcoin_miners_using_negation {
+    not any_bitcoin_miners
+}
+
+any_bitcoin_miners {
+    some i
+    app := apps[i]
+    app.name == "bitcoin-miner"
+}
+```
+
+```ruby
+> no_bitcoin_miners_using_negation with apps as [{"name": "web"}]
+true
+> no_bitcoin_miners_using_negation with apps as [{"name": "bitcoin-miner"}, {"name": "web"}]
+undefined
+```
+
+> The `undefined` result above is expected because we did not define a default
+> value for `no_bitcoin_miners_using_negation`. Since the body of the rule fails
+> to match, there is no value generated.
+
+Alternatively, we can implement the same kind of logic inside a single rule
+using [Comprehensions](#comprehensions).
+
+```ruby
+no_bitcoin_miners_using_comprehension {
+    bitcoin_miners := {app | app := apps[_]; app.name == "bitcoin-miner"}
+    count(bitcoin_miners) == 0
+}
+```
+
+> Whether you use negation or comprehensions to express FOR ALL is up to you.
+> The comprehension version is more concise and does not require a helper rule
+> while the negation version is more verbose but a bit simpler and allows for
+> more complex ORs.
+
 ## Modules
 
 In Rego, policies are defined inside *modules*. Modules consist of:

docs/content/language-cheatsheet.md

@@ -74,6 +74,9 @@ not obj.foo.bar.bar
 # check if "foo" belongs to the set
 a_set["foo"]
 
+# check if "foo" DOES NOT belong to the set
+not a_set["foo"]
+
 # check if the array ["a", "b", "c"] belongs to the set
 a_set[["a", "b", "c"]]
 
@@ -132,6 +135,34 @@ foo[k1] == foo[k2]; k1 != k2
 foo[k].bar.baz[i] == 7; foo[k].qux > 3
 ```
 
+#### For All
+
+```ruby
+# assert no values in set match predicate
+count({x | set[x]; f(x)}) == 0
+
+# assert all values in set make function f true
+count({x | set[x]; f(x)}) == count(set)
+
+# assert no values in set make function f true (using negation and helper rule)
+not any_match
+
+# assert all values in set make function f true (using negation and helper rule)
+not any_not_match
+```
+
+```ruby
+any_match {
+    set[x]
+    f(x)
+}
+
+any_not_match {
+    set[x]
+    not f(x)
+}
+```
+
 ## Rules
 
 In the examples below `...` represents one or more conditions.