89 lines
2.7 KiB
Org Mode
89 lines
2.7 KiB
Org Mode
|
* Calculational Proofs
|
||
|
|
|
||
|
|
|
||
|
|
A calculational proof is just a chain of intermediate results that are
|
||
|
|
meant to be composed by basic principles such as the transitivity of
|
||
|
|
===. In Lean, a calculation proof starts with the keyword =calc=, and has
|
||
|
|
the following syntax
|
||
|
|
|
||
|
|
#+BEGIN_SRC
|
||
|
|
calc <expr>_0 'op_1' <expr>_1 ':' <proof>_1
|
||
|
|
'...' 'op_2' <expr>_2 ':' <proof>_2
|
||
|
|
...
|
||
|
|
'...' 'op_n' <expr>_n ':' <proof>_n
|
||
|
|
#+END_SRC
|
||
|
|
|
||
|
|
Each =<proof>_i= is a proof for =<expr>_{i-1} op_i <expr>_i=.
|
||
|
|
Recall that proofs are also expressions in Lean. The =<proof>_i=
|
||
|
|
may also be of the form ={ <pr> }=, where =<pr>= is a proof
|
||
|
|
for some equality =a = b=. The form ={ <pr> }= is just syntax sugar
|
||
|
|
for =subst <pr> (refl <expr>_{i-1})=
|
||
|
|
|
||
|
|
That is, we are claiming we can obtain =<expr>_i= by replacing =a= with =b=
|
||
|
|
in =<expr>_{i-1}=.
|
||
|
|
|
||
|
|
Here is an example
|
||
|
|
|
||
|
|
#+BEGIN_SRC lean
|
||
|
|
import nat
|
||
|
|
using nat
|
||
|
|
variables a b c d e : nat.
|
||
|
|
axiom Ax1 : a = b.
|
||
|
|
axiom Ax2 : b = c + 1.
|
||
|
|
axiom Ax3 : c = d.
|
||
|
|
axiom Ax4 : e = 1 + d.
|
||
|
|
|
||
|
|
theorem T : a = e
|
||
|
|
:= calc a = b : Ax1
|
||
|
|
... = c + 1 : Ax2
|
||
|
|
... = d + 1 : { Ax3 }
|
||
|
|
... = 1 + d : add_comm d 1
|
||
|
|
... = e : symm Ax4.
|
||
|
|
|
||
|
|
#+END_SRC
|
||
|
|
|
||
|
|
The proof expressions =<proof>_i= do not need to be explicitly provided.
|
||
|
|
We can use =by <tactic>= or =by <solver>= to (try to) automatically construct the
|
||
|
|
proof expression using the given tactic or solver.
|
||
|
|
|
||
|
|
Even when tactics and solvers are not used, we can still use the elaboration engine to fill
|
||
|
|
gaps in our calculational proofs. In the previous examples, we can use =_= as arguments for the
|
||
|
|
=add_comm= theorem. The Lean elaboration engine will infer =d= and =1= for us.
|
||
|
|
Here is the same example using placeholders.
|
||
|
|
|
||
|
|
#+BEGIN_SRC lean
|
||
|
|
import nat
|
||
|
|
using nat
|
||
|
|
variables a b c d e : nat.
|
||
|
|
axiom Ax1 : a = b.
|
||
|
|
axiom Ax2 : b = c + 1.
|
||
|
|
axiom Ax3 : c = d.
|
||
|
|
axiom Ax4 : e = 1 + d.
|
||
|
|
|
||
|
|
theorem T : a = e
|
||
|
|
:= calc a = b : Ax1
|
||
|
|
... = c + 1 : Ax2
|
||
|
|
... = d + 1 : { Ax3 }
|
||
|
|
... = 1 + d : add_comm _ _
|
||
|
|
... = e : symm Ax4.
|
||
|
|
|
||
|
|
#+END_SRC
|
||
|
|
|
||
|
|
The =calc= command can be configured for any relation that supports
|
||
|
|
some form of transitivity. It can even combine different relations.
|
||
|
|
|
||
|
|
#+BEGIN_SRC lean
|
||
|
|
import nat
|
||
|
|
using nat
|
||
|
|
|
||
|
|
theorem T2 (a b c : nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0
|
||
|
|
:= calc a = b : H1
|
||
|
|
... = c + 1 : H2
|
||
|
|
... = succ c : add_one _
|
||
|
|
... ≠ 0 : succ_ne_zero _
|
||
|
|
#+END_SRC
|
||
|
|
|
||
|
|
The Lean simplifier can be used to reduce the size of calculational proofs.
|
||
|
|
In the following example, we create a rewrite rule set with basic theorems from the Natural number library, and some of the axioms
|
||
|
|
declared above.
|