-
Notifications
You must be signed in to change notification settings - Fork 1
Ask syntax tutorial
ask is a programming language as well as a programming environment in which you can write programs and proofs. This is a short text-based tutorial that explains the syntax of ask. The goal of this document is to be a reference for the next time you ask yourself "how do I achieve that in ask?" or "I've seen this being used but what does it mean really?".
Let us get started with proofs.
ask allows you to prove formulas, proofs are started by the keyword prove and are followed by a formula which you will then need to prove:
┌ Keyword to start proofs
│
│ ┌ The goal
│ │
│ │ ┌ The proof, nothing for now
╭─┴─╮ ╭──┴─╮ ▼
prove p -> p ?
Here I've used ? to indicate that the proof isn't finished yet. You can use ? as a placeholder for things you haven't gotten to yet, and ask will place them for you whenever it generates the next step in your proof.
Such a formula is easy to prove: p -> p (read p implies p) can be proven by using the ImpI rule:
proven p -> p by ImpI
And the proof is proven! In reality, many things happened behind the scene, but first lets recap the syntax:
┌ Keyword changed to `proven` means we're done
│
│ ┌ Indicates that we are using a rule
│ │
│ │ ┌ The rule we used
╭──┴─╮ ▼ ╭─┴─╮
proven p -> p by ImpI
in general proofs in ask follow this structure:
given *assumptions* prove *formula* by *rule*
The previous proof has no given but by ImpI does a lot of work behind the scenes, we can explicitly state the steps of by ImpI:
proven p -> b by ImpI
given p prove p given
╰─┬─╯ ▲ ▲
│ │ └ The new goal
│ │
│ └ `p` is now part of our assumptions.
│
└ Tells what formulas we know are true
The second line introduces a new assumption and changes our goal to p instead of p -> p, the last statement given tells ask that the formula to prove is accessible immediately in the assumption list.
ImpI is not the only rule, we also have AndI, OrIL, OrIR, NotI and Contradiction. Let's see what they do:
ImpI changes a goal x -> y to y and adds x to your givens:
proof x -> y by ImpI
given x prove y ?
AndI will prove a goal of the shape x & y by asking you to prove x and y separately in two difference branches:
prove x & y by AndI
prove x ?
prove y ?
OrIL proves a goal of the shape x | y by asking you to prove x, the left part of the or.
prove x | y by OrIL
prove x ?
OrIR proves a goal of the shape x | y by asking you to prove y, the right part of the or:
prove x | y by OrIR
prove y ?
NotI allows to prove a statement of the shape Not x by asking you to prove False when given x in your assumptions. It states that if x were to be true, then it would lead to a contradiction, indicating that Not x must be true:
prove Not x by NotI
given x prove False ?
Contradiction allows to prove any statement, by proving that the opposite leads to a contradiction:
prove p by Contradiction
given Not p prove False ?
And that is all for the rules, you will notice that for the last two we are asked to prove False and that will be the topic of the next section.
In ask there is no way to prove False, so what does it mean when we are faced with prove False ?
It means that somewhere in our proofs we are faced with a contradiction, a contradiction occurs when you are given both a formula and its negation:
given a, Not a prove False by FalseI
Here I've used by FalseI which is a rule that we have not seen but is applied implicitly whenever a contradiction is visible in the list of assumptions given to you.
This is the crux of proof by contradiction whenever you have faced with
given Not p prove False
Your goal should be to bring into scope a p such that it can cancel out with the Not p and prove False. Additionally, if you cannot bring a p into your givens, you can try bringing Not (Not p) which is the negation of Not p. Both of which cancel out to produce a False.
Until now, we have seen proofs that use by in order to modify the goal of a proof:
In the following proof, we use by to change our goal (a & b) -> a to a. But except for Contradiction, there are no rules which apply to a:
prove (a & b) -> a by ImpI
given a & b prove a ? -- what do we do? there are no rules to apply to `a` here
This is a case where we need to use from. from is a statement that you use instead of by and that will analyse the formula that you give it.
prove (a & b) -> a by ImpI
given a & b prove a from a & b
╰┬─╯ ╰─┬─╯
│ └ The formula to inspect
│
└ Indicates that we want to inspect a formula
As you can see, if you give it a & b it will add to your assumptions the formula a and the formula b. The goal, however, will not change. from will do as much work as it can in order to reach the goal, so if you give it an implication which has its hypothesis in your given, it will prove the formula without any additional work:
proven (a -> b) -> a -> b by ImpI
given (a -> b) proven a -> b by ImpI
╰───┬──╯
└ We have `a -> b` in our givens
given a proven b from a -> b -- DONE!
▲
└ We also have `a` in our givens
In here we are given a, and we are saying "please inspect a -> b" ask will then attempt to prove successively a -> b and then a and then the goal b. Since both a and a -> b are in the givens, and b proves the goal, there is no additional steps! Let's see what from can do for us:
Inspecting a ->b will do a lot of work for us, ask will attempt to prove successfully a -> b, a and b:
prove goal from a -> b
prove a -> b ?
prove a ?
given b prove goal ?
Interestingly enough, if a -> b and a are already given, and b is the goal, the following is a valid proof:
given a -> b, a prove b from a -> b -- DONE!
This is because every step is trivially proven by ask, writing down all the steps gives us:
given a -> b, a prove b from a -> b
proven a -> b given
proven a given
given b proven b given
And those cases are eluded by ask, this is a feature we will see a lot in the following examples.
Inspecting a & b allows to introduce a and b into our assumptions. So in the next line they are added to our given.
prove goal from a & b
prove a & b ?
given a, b prove goal ?
If goal is one of your branches in the & formula, using from a & b will trivially prove your statement:
given a & b proven b from a & b - DONE!
Inspecting an or formula will ask us to prove the goal using the left part of the formula and the right part of the formula, as well as the formula itself. If any of the branches are already proven ask will elude them for you.
prove goal from a | b
prove a | b ?
given a prove goal ?
given b prove goal ?
When decomposing Not a, ask will attempt to prove both a and Not a, if either of those is unavailable in your assumptions, you will be asked to prove it.
given x prove goal from Not x
prove Not x
given Not x prove goal from Not x
prove x
prove goal from Not y
prove Not y
prove y
In all those example you can see that using from Not x allows us to change the goal entierly since it does not appear in either of the branches that ask asks us to prove! This is particularly handy when proving something by Contradiction.
ask is also a programming language which allows defining types and values for those types as well as functions. First, let's see how we define new values and their types:
Values and their types are defined with data declarations:
┌ The keyword saying we are declaring a new type and its values
│
│ ┌ The type name
│ │
│ │ ┌ The values we can construct
╭─┴╮ ╭─┴╮ ╭────┴─────╮
data Bool = True | False
▲
└ The pipe separates the different values
data is followed by the name of the type, then an = sign and finally the values that will be in this type. Here we have declared the values True and False and have given them the type name Bool. This mean everywhere we are dealing with the type Bool we can expect it to be either one of two values, either False or True. We say that True and False inhabit the type Bool.
Each values that inhabit your type are built using constructors when you write True | False you say that Bool has two constructors named True and False. Each constructor can itself take values in argument in order to build itself. For example, in the following, Either has two constructors which each take 1 value in argument:
┌ The type parameters
│ ┌ Right takes values of type `b`
╭┴╮ ▼
data Either a b = Left a | Right b
▲
└ Left takes a values of type `a`
Constructors have to be declared with a capital letter (like True instead of true). Variables are declared using a lower-case letter (like a).
Here are more examples of data declarations:
data Unit = Unit
The following type is interesting for academic purposes, you can declare it, but you cannot construct values of this type, since it has no constructors.
data Impossible =
We can use multiple constructors to declare linked lists by saying either our list is empty, or it contains a Bool and another list, which itself could be either empty or contain more elements.
data BoolList = Empty | Cons Bool BoolList
nb: The word Cons comes from Lisp
In the previous example, we declared lists of Bool, now we would like to describe lists which contain any arbitrary other type. We do this by giving List a type parameter a and using it for the Cons constructor. Effectively saying Cons takes an a and another list of as.
data List a = Empty | Cons a (List a)
Note that we can give name to the arguments of constructors, like so:
data List a = Empty | Cons (head :: a) (tail :: List a)
We don't have to have multiple constructors, we can declare type with only 1 constructor. Additionally, this constructor can have multiple arguments, here we are giving two arguments to the constructor MkPair.
data Nat = Z | S Nat
data NatPair = MkPair Nat Nat
In the previous example pairs could only contain Nat, here they can contain anything and we are indicating this property by giving the type Pair two type parameters, a and b
data Pair a b = MkPair (fst :: a) (snd :: b)
data Triple a b c = MkTriple (fst :: a) (snd :: b) (trd :: c)
A fun brain teaser is trying to figure out how this is almost the same as
Pair a (Pair b c)
You can do this by implementing the two functions:
TripleToPairs :: Triple a b c -> Pair a (Pair b c)
PairsToTriple :: Pair a (Pair b c) -> Triple a b c
Here our constructor takes two arguments but of the same type a.
data Same a = MkSame a a
Functions in ask are defined in two parts, first the type signature, and second the definition, which needs to fit the type signature. For example, the following function inverts a boolean value:
not :: Bool -> Bool
defined not x from x
defined not True = False
defined not False = True
We declare a function and its type by giving its name and then giving its type separated with a double colon, ::. Then we start a new definition with the keyword define followed by the name of the function we are defining and the arguments to use.
data Bool = True | false
┌ The name of the function
│
│ ┌ Separates the name from the type signature
│ │
│ │ ┌ The type signature
╭┴╮ ▼ ╭────┴─────╮
not :: Bool -> Bool
define not x ?
╰──┬─╯ ╰┬╯ ▲
│ │ └ The argument, here of type `Bool`
│ │
│ └ Recall the name of the function
│
└ Declare the fact that we are defining a function
In the actual implementation we re-use from in order to analyse the possible values that x can have. Given x is a Bool, it can have either of two values: True or False. This is why asking ask about define not x from x returns us an incomplete definition with two branches, one where x is True and one where x is False:
define not x from x
define not True ?
define not False ?
The final step is to actually implement this function by telling ask which values this function must return depending on the value of x by using the = sign. So for True we return False and for False we return True .
defined not x from x
defined not True = False
defined not False = True
Once we are done, the define turn into defined indicating that ask is happy about the information you have given it.
Definitions use multiple arguments, typically in the following function we have two values to inspect:
┌ The two arguments of the function
╭────┴─────╮
xor :: Bool -> Bool -> Bool
┌ We refer to them as `x` and `y` in the definition
╭┴╮
define xor x y from x
define xor True y from y
define xor True True = False
define xor True False = True
define xor False y from y
define xor False True = True
define xor False False = False
More generally the syntax can be summarised as
define *function name* *arguments* *implementation*
Where the *implementation* can be a from, a return value using =, or it can be inductively as we will see in the next section.
data declarations can be recursive, for example the definition of natural number makes use of itself in its own definition
┌ Definition of `Natural`
│ ┌ Reference to itself
╭──┴──╮ ╭──┴──╮
data Natural = Zero | Successor Natural
In order to process those definitions, we are going to use functions that use their own definitions in order to completely process a recursive data structure such as Natural.
For example, in the next function we are going to double a Natural by doing nothing when we are looking at Zero and by adding one extra layer of Successor when we are looking at a Successor and then call the double function recursively
double :: Natural -> Natural
┌ Here we advertise our plan to make a recursive call
╭────┴────╮
define double x inductively x -- inductive definition on `x`
define double x from x -- inspect `x`
define double Zero = Zero -- in case of `Zero` return `Zero`
define double (Successor n) = Successor (Successor (double n))
╰─────────┬────────╯ ╰──┬──╯
We add an extra `Successor` ┘ │
│
We make a recursive call to `double` ┘
inductively x tells ask that we are interested in looking at the value x, and we expect to make recursive calls on x given one of its constructors.
Now that we know how to write proofs and how to write programs it is time to see how to write proofs about programs. As before, proofs are declared with the keyword prove and the keyword switches to proven once you’ve proven it
In the upcoming sections we are going to assume that we are given the following definitions:
- A definition for natural numbers
data N = Z | S N - A definition for
+on natural numbers(+) :: N -> N -> N define a + b inductively a where define a + b from a where define Z + b = b define (S a) + b = S (a + b)
The following proves that adding Z to a number does not change it. It depends on the implementation of the function +.
┌ Start the proof with the `prove` keyword
│
│ ┌ Write the equation to prove
╭─┴─╮ ╭───┴───╮
prove n + Z = n ?
▲
└ Use our gadgets to carry out the proof
Proving things about programs is very similar to proving statements on propositions, the difference is that now you have to pay careful attention to the implementation of the program in order to make progress. With that in mind proving statements about programs allows us to make use of two new tools: test and under.
When working on proofs you might find yourself in a position where the goal is not written in the smallest, most irreducible form. Fortunately, ask can reduce terms by evaluating them using the keyword test. In the following, we want to prove that adding n to Z gives us n back unchanged:
prove Z + n = n ?
We can prove it if we evaluate the left side of the equation, to evaluate we will send the following to ask:
prove Z + n = n test
And it comes back proven:
proven Z + n = n tested
This is thanks to the implementation of (+) . We can tell that if we evaluate the expression on the left, we get the expression on the right because the line define Z + b = b in the definition of (+) says that whenever the first argument is Z, the function returns its second argument.
As an example of the opposite, let us take this statement:
prove n + Z = n ?
Using test, you will see that ask will not be able to evaluate the left side of the equation, because nowhere in the implementation is explained what to do when the second argument is Z. In order to prove this statement we are going to use from and inductively as explained in the next section.
In the case we want to prove n + Z = n we will need to inspect n, the first argument of (+), just like its implementation is doing. Similarly to implementing functions, or inspecting propositions, we can use from to decompose a variable into its possible constructors:
prove n + Z = n from n where
given n = Z prove Z + Z = Z ?
given n = S n' prove (S n') + Z = (S n') ?
In this case n has two possible constructors Z and S n, this is why we are now asked to prove our statement for each possible cases: the case where n = Z and the case where n = S n'. Each case appear in your context as a given and the goal of each proof is rewritten to take this new fact into account.
The first case can be proven using test since we know from the implementation of (+) that Z + n = n
prove n + Z = n from n where
given n = Z prove Z + Z = Z tested
given n = S n' prove (S n') + Z = (S n') ?
The second case can be proven by noticing that (S n') + Z = S n' is exactly the statement we want to prove, except n has been replaced by S n'. Since n' is smaller than n this is a situation where you can use proof by induction. You do this the same way you do inductive definitions, by using the keyword inductively followed by the variable that is getting smaller, in this case n:
prove n + Z = n inductively n where
prove n + Z = n from n where
prove n = Z prove Z = Z = Z tested
prove n = S n' prove S n' + Z = S n' tested
This proof gadget is not strictly reserved to proofs about programs, it works with propositions too. What is says is that if you are given a proof that a = b and b = c then you have a proof of a = c.
Another way to see this is that if you want to prove a = c it is enough to prove a = b and b = c. If you pick your b value smartly the proof might become very easy! Let us see that in action:
prove a = b -> b = c -> a = c by ImpI where
given a = b prove b = c -> a = c by ImpI where
given b = c prove a = c by Route b where
prove a = b given
prove b = c given
Using by Route b tells ask to generate two branches for our proof, one for each side of our equality. In practice, it is common that ask is able to deduce automatically one of those branches, and will only show you the branch that it was not able to prove by itself.
Another way to see this property is graphically:
╭──► B ───╮
│ │
│ ▼
A ───?──► CIf you cannot go directly from a to c you might be able to take a detour through b. Creating a route between a and c going through b.
This proof technique is also useful when you want ask to compute some part of the equation but stop evaluating at a particular step that makes the proof easy for you.
We have seen that ask can deduce that equality proofs hold if both side if the equality sign use the same constructor. Similarly, ask can prove a statement if both side of the equality are using the same outermost function, and each corresponding argument can be proven equal.
prove f a b = f c d under (f) where
prove a = c
prove b = d
The outermost function might also by an operator, if you are proving things about addition (+) or concatenation (++) you might need to use under with the operator's symbol, for example using (+):
prove a + b = c + d under (+) where
prove a = c
prove b = d
Be mindful of the way operators bracket, in this instance, the + operator brackets to the left, which means a + b + c is equal to (a + b) + c. If you are not careful about this you might attempt to use under in a situation that will not help you:
prove a + b + c = a + (b + c) under (+) where
prove a + b = a ?
prove c = b + c ?
In this case you might have expected to be able to use under (+) in order to get to the proofs that a = a and b + c = b + c, however, because of the bracketing rules, the statement is handled like this:
┌───────┬─ Outermost function is (+)
▼ ▼
(a + b) + c = a + (b + c)
╰──┬──╯ ▲ ▲ ╰──┬──╯
╰────┬─│───╯ │
│ ╰─────┬────╯
│ └ c = b + c
│
└ a + b = a
Where the first argument of + on the left side has to match the first argument of + on the right side. Which means a + b must be equal to b, and similarly for the second argument of +, which means c must be equal to b + c.
At the beginning of this documents we've seen how to use AndI OrIL OrIR ImpI NotI and Contradiction in order to manipulate the goal of a proposition. In ask you can also define your own custom propositions on user-defined data types. For this we use the work prop followed by the name of our proposition and followed by the types involved in the proposition. For example in the following we define a type for the three move of the game “rock paper scissors” and the rules of the game as a prop:
data Move = Rock | Paper | Scissors
prop Move ! Move where
prove Rock ! Scissors by Blunting
prove Scissors ! Paper by Cutting
prove Paper ! Rock by Wrapping
The symbol ! is the name of the proposition and works as an infix operators between two moves. We could have given it a name using letter, starting with a capital:
prop Beats Move Move where
prove Beats Rock Scissors by Blunting
prove Beats Scissors Paper by Cutting
prove Beats Paper Rock by Wrapping
But the proofs now read a bit more awkwardly. If you read ! as “beats” Rock ! Scissors reads “Rock beats scissors” which is much more natural. I is your judgement call if you want your prop to use a symbol or a name to describe it.
props can also have custom subgoals such that when you use a rule, you are required to prove something different that makes progress toward the proof. For example in the following, we are going to says that in order to prove that a number is smaller or equal to another, it is enough to prove that the Left side is Z or that, if both sides are S, then the numbers under the S are themselves following the “smaller or equal” relation:
-- the prop is called `LTE` for "Less Than or Equal"
prop LTE N N where
-- Either `Z` is on the left
prove LTE Z a by LeZ
-- Or we have `S a = S b` and
-- `a` and `b` have to be `<=` themselves
prove LTE (S a) (S b) by LeSS where
prove LTE a b
The general syntax is this:
┌ The keyword `prop`
│
│ ┌ The name of the prop, must be capitalised
│ │
│ │ ┌ The types the prop is about
╭─┴─╮╭┴╮ ╭┴╮
prop LTE N N where
┌ The keyword `prove`
╭─┴─╮
prove LTE Z a by LeZ
▲ ▲ ╰┬╯
│ │ └ The name of the rule, must be capitalised
│ │
│ └ The `by` keyword
│
└ The constructor for which this rule applies
prove LTE (S a) (S b) by LeSS where
prove LTE a b ◀︎ The additional proofs you need to supply
After using this rule
In some situation you might need to use from on a prop that appears in your givens. This operation makes ask create one branch for each proof that could have proven the prop you are giving in argument. ask will only use valid proofs and ignore the invalid ones. In the following example we are reusing LTE in order to showcase what happens when you use from (LTE a b)
prove LTE a b -> LTE c d by ImpI where
This is a `prop` about `LTE` ┐
╭───┴───╮
given LTE a b prove LTE c d from (LTE a b)
-- This is the case we need to prove when our prop has been
-- proven with `LeZ`
given a = Z prove LTE c d
-- This is the case we need to prove when our prop has been
-- proven with LeSS
given a = S a', b = S b', LTE a' b' prove LTE c d
As you can see, ask generates one branch for each possible proof of LTE, the LeZ case tells us that a must be Z. This is because LeZ is only usable when the first argument is Z (LTE Z b) , since a is our first argument, it must be that a = Z.
In the second case ask generates a series of assumptions that are the consequence of proving a = b with LeSS. When proving with LeSS three things must be true:
- The first argument
ahas a predecessora'such thata = S a' - The second argument
bhas a predecessorb'such thatb = S b' - Each predecessors are related by
LTE:LTE a' b'
Since those facts must be true in order to prove a = b using LeSS ask puts them in our list of givens.
One final use for from is to substitute variables which have been proven equal. In the following example we use from a = S n in order to replace a by S n making the proof substantially easier to prove:
prove a = S n -> LTE n a by ImpI where
given a = S n prove LTE n a from a = S n where
prove LTE n (S n) ?
As you can see the original statement was about two variables, a and n and they do not seem related so ask cannot do anything to prove this. However, using the hypothesis that a = S n we can replace occurrence of a on the right by S n, which turns our goal into LTE n (S n), something that we can deal with much more easily.