A frequent use for refactoring in programming languages is to enable a semantic change. For example, the refactoring generalise definition introduces a new parameter to replace a selected subexpression. Consider the following function:
f :: int -> int
f x = x^2
The function can be generalised over the highlighted subexpression (2) to create a new function:
f :: int -> int -> int
f x n = x^n
Now, in order to preserve program behaviour, any calls to f must be instantiated with the generalised subexpression. We can see this is semantics preserving as λx. x^2 is refactored to λn. (λx. x^n) and any calls are applications and so (λn. (λx. x^n)) 2 will β-reduce to λx. x^2.
This refactoring also has a similar meaning in proof scripts with the added requirement that lemmas involving the definition must be ‘specialised’. I’m wondering if we can guarantee that all lemmas will still be proved after this operation; it seems feasible…
Consider the theorem: for all x in X 0 < f x implies 0 < Sum ( f x ^ n), where x is a real number, say and X a set of reals. A proof of this will go through fine, but in proving this, one also proves that 0 < (f x) ^n either implicitly or explicitly (using an Isar ‘have’).
What if you prove this theorem, perhaps as it’s an explicit requirement for another theorem you’re in the middle of,and then realise this fact? What you’d do is split them up! Another thing to note is that, for the sub-proof, the assumption ‘for all x in X…’ is not required just the fact that f x > 0.
This may seem a contrived example, but I actually did this! Not sure what it says about me however….
What we’d like therefore is an automatic refactoring where this subproof is extracted and minimal assumptions.
I’d be really interested if anyone has come across a more subtle example?
Hello and welcome to my blog!
I’m Iain Whiteside and this blog has been created to track my thoughts and ideas about Proof Engineering – the topic of my PhD!
I’m hopefully going to be communicating through this quite regularly so please visit often and comment!
Bye for now!
