- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

This shows you the differences between two versions of the page.

sav08:proofs_and_induction [2008/02/21 17:47] vkuncak |
sav08:proofs_and_induction [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 6: | Line 6: | ||

When proving a formula, we typically have a set of current //assumptions// and a goal. Moreover, we will consider the possibility of having multiple alternative goals, to explore multiple possible proofs at the same time. A state of our proof attempt is therefore given by a //sequent// of the form | When proving a formula, we typically have a set of current //assumptions// and a goal. Moreover, we will consider the possibility of having multiple alternative goals, to explore multiple possible proofs at the same time. A state of our proof attempt is therefore given by a //sequent// of the form | ||

- | \[ | + | \begin{equation*} |

A_1,\ldots,A_n \vdash G_1,\ldots,G_m | A_1,\ldots,A_n \vdash G_1,\ldots,G_m | ||

- | \] | + | \end{equation*} |

where $A_1,\ldots,A_n$ are assumptions and $G_1,\ldots,G_m$ are goals. The meaning of a sequent is the implication formula | where $A_1,\ldots,A_n$ are assumptions and $G_1,\ldots,G_m$ are goals. The meaning of a sequent is the implication formula | ||

- | \[ | + | \begin{equation*} |

A_1 \land \ldots \land A_n \rightarrow G_1 \lor \ldots \lor G_m | A_1 \land \ldots \land A_n \rightarrow G_1 \lor \ldots \lor G_m | ||

- | \] | + | \end{equation*} |

We admit the case of no assumptions ($n=0$) in which the left hand side is //true// and the case of no goals ($m=0$) in which case the right-hand side is considered to be //false//. (You can think of one of the assumptions always being the trivial assumption //true//, and one of the goals always being the trivially unprovable goal //false//.) | We admit the case of no assumptions ($n=0$) in which the left hand side is //true// and the case of no goals ($m=0$) in which case the right-hand side is considered to be //false//. (You can think of one of the assumptions always being the trivial assumption //true//, and one of the goals always being the trivially unprovable goal //false//.) | ||

The rules below will have the form | The rules below will have the form | ||

- | \[ | + | \begin{equation*} |

\frac{S_1\ ;\ ... \ ;\ S_K}{S_0} | \frac{S_1\ ;\ ... \ ;\ S_K}{S_0} | ||

- | \] | + | \end{equation*} |

where $S_0,S_1,\ldots,S_n$ are sequents. The meaning of each rule is that if we establish sequents $S_1,\ldots,S_K$ then we can derive sequent $S_0$. In other words, if we wish to prove sequent $S_0$, it suffices to prove sequents $S_1,\ldots,S_n$. The rules below allow us to eliminate propositional connectives in valid formulas until we obtain sequents of the form $P,A_2,\ldots,A_n \vdash P,G_2,\ldots,G_m$, which is a trivially valid sequent because one of its goals appears as an assumption. | where $S_0,S_1,\ldots,S_n$ are sequents. The meaning of each rule is that if we establish sequents $S_1,\ldots,S_K$ then we can derive sequent $S_0$. In other words, if we wish to prove sequent $S_0$, it suffices to prove sequents $S_1,\ldots,S_n$. The rules below allow us to eliminate propositional connectives in valid formulas until we obtain sequents of the form $P,A_2,\ldots,A_n \vdash P,G_2,\ldots,G_m$, which is a trivially valid sequent because one of its goals appears as an assumption. | ||

Line 28: | Line 28: | ||

If we can prove something from two assumptions, we can also prove it from their conjunction. | If we can prove something from two assumptions, we can also prove it from their conjunction. | ||

- | \[ | + | \begin{equation*} |

\frac{P,Q \vdash} | \frac{P,Q \vdash} | ||

{P\land Q \vdash} | {P\land Q \vdash} | ||

- | \] | + | \end{equation*} |

==== Conjunction-Right ==== | ==== Conjunction-Right ==== | ||

To prove a conjunction, prove each conjunct. | To prove a conjunction, prove each conjunct. | ||

- | \[ | + | \begin{equation*} |

\frac{\vdash P\ ;\ \vdash Q} | \frac{\vdash P\ ;\ \vdash Q} | ||

{\vdash P \land Q} | {\vdash P \land Q} | ||

- | \] | + | \end{equation*} |

==== Disjunction-Left ==== | ==== Disjunction-Left ==== | ||

To prove something from a disjunctive assumption, prove it by case analysis, one case for each disjunct. | To prove something from a disjunctive assumption, prove it by case analysis, one case for each disjunct. | ||

- | \[ | + | \begin{equation*} |

\frac{P \vdash \ ; \ Q \vdash} | \frac{P \vdash \ ; \ Q \vdash} | ||

{P\lor Q \vdash} | {P\lor Q \vdash} | ||

- | \] | + | \end{equation*} |

==== Disjunction-Right ==== | ==== Disjunction-Right ==== | ||

To prove a disjunction try to prove one of the disjuncts. | To prove a disjunction try to prove one of the disjuncts. | ||

- | \[ | + | \begin{equation*} |

\frac{\vdash P,Q} | \frac{\vdash P,Q} | ||

{\vdash P \lor Q} | {\vdash P \lor Q} | ||

- | \] | + | \end{equation*} |

==== Implication-Left ==== | ==== Implication-Left ==== | ||

To prove something from an implication, prove it from its conclusion and also prove the premise. | To prove something from an implication, prove it from its conclusion and also prove the premise. | ||

- | \[ | + | \begin{equation*} |

\frac{\vdash P\ ;\ Q \vdash} | \frac{\vdash P\ ;\ Q \vdash} | ||

{P \rightarrow Q \vdash} | {P \rightarrow Q \vdash} | ||

- | \] | + | \end{equation*} |

==== Implication-Right ==== | ==== Implication-Right ==== | ||

To prove an implication, assume its premise and prove its goal. | To prove an implication, assume its premise and prove its goal. | ||

- | \[ | + | \begin{equation*} |

\frac{P \vdash Q} | \frac{P \vdash Q} | ||

{\vdash P \rightarrow Q} | {\vdash P \rightarrow Q} | ||

- | \] | + | \end{equation*} |

==== Negation-Left ==== | ==== Negation-Left ==== | ||

Instead of proving a goal, you can assume its negation and prove any remaining goals (this generalizes proof by contradiction). | Instead of proving a goal, you can assume its negation and prove any remaining goals (this generalizes proof by contradiction). | ||

- | \[ | + | \begin{equation*} |

\frac{\lnot P \vdash} | \frac{\lnot P \vdash} | ||

{\vdash P} | {\vdash P} | ||

- | \] | + | \end{equation*} |

==== Negation-Right ==== | ==== Negation-Right ==== | ||

If you prove one of the goals, you can assume its negation and prove remaining goals. | If you prove one of the goals, you can assume its negation and prove remaining goals. | ||

- | \[ | + | \begin{equation*} |

\frac{\vdash P} | \frac{\vdash P} | ||

{\lnot P \vdash} | {\lnot P \vdash} | ||

- | \] | + | \end{equation*} |

==== Forall-Left ==== | ==== Forall-Left ==== | ||

If you have a universally quantified assumption, you can instantiate universal quantifier with any value, denoted by term //t// (this is what "for all" means). You keep the original quantified assumption in case you need to instantiate it multiple times. | If you have a universally quantified assumption, you can instantiate universal quantifier with any value, denoted by term //t// (this is what "for all" means). You keep the original quantified assumption in case you need to instantiate it multiple times. | ||

- | \[ | + | \begin{equation*} |

\frac{P(t), \forall x.P(x) \vdash} | \frac{P(t), \forall x.P(x) \vdash} | ||

{\forall x.P(x) \vdash} | {\forall x.P(x) \vdash} | ||

- | \] | + | \end{equation*} |

==== Forall-Right ==== | ==== Forall-Right ==== | ||

To prove a universally quantified goal, prove the goal for an arbitrary element, denoted by fresh variable $x_0$. Informally we would say "let $x_0$ be arbitrary...". | To prove a universally quantified goal, prove the goal for an arbitrary element, denoted by fresh variable $x_0$. Informally we would say "let $x_0$ be arbitrary...". | ||

- | \[ | + | \begin{equation*} |

\frac{\vdash P(x_0)} | \frac{\vdash P(x_0)} | ||

{\vdash \forall x.P(x)} | {\vdash \forall x.P(x)} | ||

- | \] | + | \end{equation*} |

==== Exists-Left ==== | ==== Exists-Left ==== | ||

When you have an existentially quantified assumption, you can pick a witness for existential statement and denote it by fresh variable "x_0". Informally we would say "let $x_0$ be such $x$". | When you have an existentially quantified assumption, you can pick a witness for existential statement and denote it by fresh variable "x_0". Informally we would say "let $x_0$ be such $x$". | ||

- | \[ | + | \begin{equation*} |

\frac{P(x_0) \vdash} | \frac{P(x_0) \vdash} | ||

{\exists x. P(x) \vdash} | {\exists x. P(x) \vdash} | ||

- | \] | + | \end{equation*} |

==== Exists-Right ==== | ==== Exists-Right ==== | ||

To prove an existentially quntified statement, supply a witness for the existential quantifier, given by value of some term //t//. Keep the original existential quantifier in case this was not the right instantiation. | To prove an existentially quntified statement, supply a witness for the existential quantifier, given by value of some term //t//. Keep the original existential quantifier in case this was not the right instantiation. | ||

- | \[ | + | \begin{equation*} |

\frac{\vdash P(t), \exists x.P(x)} | \frac{\vdash P(t), \exists x.P(x)} | ||

{\vdash \exists x. P(x)} | {\vdash \exists x. P(x)} | ||

- | \] | + | \end{equation*} |

===== Example ===== | ===== Example ===== | ||

Let us prove the following formula: | Let us prove the following formula: | ||

- | \[ | + | \begin{equation*} |

\exists x. \forall y. F(x,y) \vdash \forall u. \exists v. F(v,u) | \exists x. \forall y. F(x,y) \vdash \forall u. \exists v. F(v,u) | ||

- | \] | + | \end{equation*} |

===== Using Proof Rules in Isabelle ===== | ===== Using Proof Rules in Isabelle ===== | ||

Line 171: | Line 171: | ||

==== Stepwise Induction ==== | ==== Stepwise Induction ==== | ||

- | \[ | + | \begin{equation*} |

\frac{P(0)\ \ \land\ \ (\forall n\in \mathbb{N}. (P(n) \rightarrow P(n+1))} | \frac{P(0)\ \ \land\ \ (\forall n\in \mathbb{N}. (P(n) \rightarrow P(n+1))} | ||

{\forall n \in \mathbb{N}. P(n)} | {\forall n \in \mathbb{N}. P(n)} | ||

- | \] | + | \end{equation*} |

==== Total Induction ==== | ==== Total Induction ==== | ||

- | \[ | + | \begin{equation*} |

\frac{\forall n \in \mathbb{N}. ((\forall k < n. P(k)) \rightarrow P(n))} | \frac{\forall n \in \mathbb{N}. ((\forall k < n. P(k)) \rightarrow P(n))} | ||

{\forall n \in \mathbb{N}. P(n)} | {\forall n \in \mathbb{N}. P(n)} | ||

- | \] | + | \end{equation*} |

==== Structural Induction ===== | ==== Structural Induction ===== | ||

+ | |||

+ | Stepwise induction allows us to prove properties of natural numbers by proving that it holds for 0 and that it extends with each successor. Structural induction similarly allows us to prove that if property holds for basic structures and that if it holds for smaller structures then it also holds for larger structures. Examples of such structures are terms or expression trees. | ||

Consider a language $L$ of function symbols. Let $ar(f)$ denote the number of arguments (arity) of a function symbol $f \in L$. Let ${\it Terms}(L)$ denote the set of all terms in this language. To prove a property for all terms, we show that if the property holds for subterms, then it holds for the term built from these subterms. | Consider a language $L$ of function symbols. Let $ar(f)$ denote the number of arguments (arity) of a function symbol $f \in L$. Let ${\it Terms}(L)$ denote the set of all terms in this language. To prove a property for all terms, we show that if the property holds for subterms, then it holds for the term built from these subterms. | ||

- | \[ | + | \begin{equation*} |

\frac{\bigwedge_{f \in L} \forall t_1,\ldots,t_{ar(f)}.\ (\bigwedge_{i=1}^{ar(f)} P(t_i)) \rightarrow P(f(t_1,\ldots,t_n))} | \frac{\bigwedge_{f \in L} \forall t_1,\ldots,t_{ar(f)}.\ (\bigwedge_{i=1}^{ar(f)} P(t_i)) \rightarrow P(f(t_1,\ldots,t_n))} | ||

{\forall t \in {\it Terms}(L). P(t)} | {\forall t \in {\it Terms}(L). P(t)} | ||

- | \] | + | \end{equation*} |

+ | Note that if $c$ is a constant we assume $ar(c)=0$. Therefore, structural induction requires us to prove $P(c)$ for all constants $c \in L$. | ||

* [[Calculus of Computation Textbook]], Chapter 4 (some example refer to previous chapters, if you do not understand them, ignore them for now) | * [[Calculus of Computation Textbook]], Chapter 4 (some example refer to previous chapters, if you do not understand them, ignore them for now) |