Syntax

Syntax of ask Proofs

Let's be more precise about the syntax of proofs.

〈proof〉 ::= 〈head〉 | 〈head〉 where 〈subproofs〉

A proof has a head, and it might have a where clause with subproofs. We say where is a "layout herald", meaning that it announces the arrival of a block of stuff, indented consistently and strictly more than the head. You can split the head over multiple lines as long as the later lines are indented more than the first: we know it's still the head until the where shows up.

〈subproofs〉 ::= | 〈indent〉 〈subproof〉 〈subproofs〉

The block of subproofs is either empty or it has at least one subproof. It's a bit tricky to give a formal grammar for consistent indentation, but I mean enough whitespace to get you to the same indented column each time.

〈head〉 ::= prove 〈proposition〉 〈method〉

Meanwhile, the head of a proof is the keyword prove followed by the goal (the proposition to prove) and the method (how to prove it). There are currently four available methods.

〈method〉 ::= ? | by 〈rule〉 | from 〈proposition〉 | given

The ? method indicates a stub: you are being asked to choose a more convincing method. Otherwise you can invoke a proof rule (using the keyword by), or you can unpack the reason for something that is proven (using the keyword from), or you can choose to record that what you are being asked to prove is given as a hypothesis. By design, ask allows you to omit proofs by the given method, as they are regarded as sufficiently obvious.

Meanwhile, subproofs are quite like proofs, but they might have extra hypotheses, introduced by keyword given

〈subproof〉 ::= 〈proof〉 | given 〈propositions〉 〈proof〉
〈propositions〉 ::= 〈proposition〉 | 〈proposition〉 , 〈propositions〉