11. Inductive Proof Flashcards
What is the proof pattern for induction on a list?
What is a well-founded ordering?
An ordering of a set such that (for all x) there are no infinite downward chains
What is a noetherian ordering?
An ordering of a set such that (for all x) there are no infinite downward chains
What is cut elimination?
In the L-system, the cut rule is unnecessary
What is the sub-formula property?
Every cut-free proof only contains formulas which are sub-formulas of the original goal
What does the cut elimination and sub-formula propertys allow us to do?
Complete (possible non-terminating) proof search
What happens when we add the induction rule to L-systems?
Cut elimination and sub-formula fails
What are the two stratergys when you get stuck during induction?
- Generalisation
- Lemma speculation
What is generalisation?
Generalizing in order to prove
reverse (append (reverse xs) (Cons x Nil)) = Cons x (reverse (reverse xs))
reverse (append ys (Cons x Nil)) = Cons x (reverse xs)
What is lemma speculation?
Introduce a new lemma to prove the inductive step
The new lemma must also be proved
What is distinctness (datatype)?
What is injectivity (datatype)?
What is the general form of a datatype?
What propertys of datatypes does isabelle provide automatically?
distinctness, injectivity
What is the induction rule of inference?
fv(Gamma, P) means the set of free variables in Gamma and P
What does this do?
Ignore assumptions
What does this do?
Use assumptions, but do not rewrite them
What does this do?
Rewrite assumps, don’t use them
