# Felix Tutorial ## Definitions Definitions are given within a normal `definition` environment. ```tex \begin{definition}\label{ordinal} $\alpha$ is an ordinal iff $\alpha$ is \in-transitive and every element of $\alpha$ is \in-transitive. \end{definition} ``` The vocabulary you define is automatically extracted as a pattern and added to the grammar of Felix. Each pattern can consist of multiple words and also include variables as parameters. You can define the following: Kind | Pattern | Example ---- | ---- | ---- Nouns | ` is a iff ` | `$k$ is a divisor of $n$ iff ...` Adjectives | ` is iff ` | `$n$ is divisible by $k$ iff ...` Verbs | ` iff ` | `$k$ divides $n$ iff ...` Operators | `$ = $` | `$n + k = ...$` Relators | `$ $ iff ` | `$n < k$ iff ...` Predicates | `$\{}...{} iff ` | `$\Cong{a}{b}{c}{d}$ iff ...` Source fixity declarations are line-leading pragmas such as `%! infixl 4`. User declarations may use literal levels 0 through 7; the two higher internal levels are reserved. Verification keeps compact proof-independent theorem authority separate from exact proof/declaration validation. Its authorization summary lists only direct source axioms and syntactic `Omitted` sites, not facts that merely inherit their safety. ## Abbreviations Abbreviationas are definitions that are always automatically expanded by Felix. ## Proof vernacular Proof checking in Felix relies on automated theorem provers like Vampire. This means that reasoning can be quite loosely structured and many small details are taken care of automatically. However, reasoning steps that require deep and complex reasoning may require more detailed proofs. Within proofs, we distinguish between *global facts*, which are all preceding theorems that have been successfully proved, and *local assumptions*, which are the assumptions of the theorem statement (e.g. `Suppose ...`) or of individual proof steps (`Assume ...`) and *intermediate claims* that are established throughout the proof. At the start of a proof, the *sufficiency* or *proof goal* corresponds to the conclusion of the theorem statement. Some proof steps may change this sufficiency. ### Proof via intermediate claims The simplest way to prove a statement is to make intermediate claims, relying on the proof automation to put everything together. Unless an explicit justification is given, all global facts are available to the proof automation. In the following example, establishing the local fact that a restricted relation is a subset of itself, is enough for the proof automation to find the rest of the proof. As no explicit justification is given, all global facts can be used to establish that `$R$ is injective` and `$\restrl{R}{A}\subseteq R$` imply `$\restrl{R}{A}$ is injective`. ```tex \begin{proposition}\label{restrl_injective} Suppose $R$ is injective. Then $\restrl{R}{A}$ is injective. \end{proposition} \begin{proof} $\restrl{R}{A}\subseteq R$. \end{proof} ``` If an explicit justification by reference given, then the available global facts are restricted to only those explicitly listed. However, local assumptions and intermediate claims are always available. Explicitly justified proof steps are the best option in terms of stability and perfomance, since they minimize the search space for the proof automation. ```tex \begin{proposition}\label{inters_of_family_of_equivalences_is_equivalence} Let $F$ be a family of relations. Suppose every element of $F$ is an equivalence. Then $\inters{F}$ is an equivalence. \end{proposition} \begin{proof} $\inters{F}$ is quasireflexive by \cref{quasireflexive,inters_destr,inters_iff_forall}. $\inters{F}$ is symmetric by \cref{symmetric,inters_iff_forall,inters_destr}. $\inters{F}$ is transitive by \cref{transitive,inters_iff_forall,inters_destr}. \end{proof} ``` ### Proof finishing steps If no explicit proof-finishing step is given, the implicit last step is to establish the conclusion from everything that came before, including all global facts. Alternatively, we can again restrict the of global facts available with an explicit reference using the syntax `Follows by \cref{}`. ```tex \begin{proposition}\label{function_apply_default} Suppose $x\notin\dom{f}$. Then $f(x) = \emptyset$. \end{proposition} \begin{proof} $\img{f}{\{x\}} = \emptyset$ by \cref{setext,emptyset,img_singleton_iff,dom_intro}. Follows by \cref{apply,unions_emptyset}. \end{proof} ``` There is also a built-in tactic that applies set extensionality, replacing a sufficiency of the form `A = B` with two sufficiencies `A\subseteq B` and `B\subseteq A`. This can be useful when you have to prove that two sets are equal. ```tex \begin{proposition}\label{dom_circ_exact} Let $f, g$ be functions. Suppose $\ran{f} = \dom{g}$. $\dom{g\circ f} = \dom{f}$. \end{proposition} \begin{proof} Every element of $\dom{g\circ f}$ is an element of $\dom{f}$. Follows by set extensionality. \end{proof} ``` ### Assumption steps If the suffiency is syntactically of the form `$\phi$ implies $\psi$` or similar, then we can locally assume `\phi` and are left with `\psi` as the sufficieny. Here is a simple artificial example. ```tex \begin{proposition}\label{assumption_example} If $x\in y$ and $a\in b$, then $x\in y$. \end{proposition} \begin{proof} Assume $a\in b$. % Sufficiency is now "If $a\in b$, then $x\in y$." Assume $x\in y$. % Sufficiency is now "$x\in y$." Follows by assumption. % Finishing proof steps, which uses only local assumptions and intermediate claims (no global facts). \end{proof} ``` We can also make an assumption step against sufficiencies of the form `$\phi$ or $\psi$`, which changes the goal to the negation of `\psiw`. ## Proof by contradiction You can start a proof by negation (or, if the sufficiency is negative, a proof of a negation) with `Suppose not`. Below is a proof of a negative statement ("It is not the case that there exists..."). ```tex \begin{theorem}[Cantor]\label{cantor} There exists no surjection from $A$ to $\pow{A}$. \end{theorem} \begin{proof} Suppose not. Consider a surjection $f$ from $A$ to $\pow{A}$. Let $B = \{a \in A \mid a\notin f(a)\}$. Then $B\in\pow{A}$. Take an element $a'$ of $A$ such that $f(a') = B$ by \cref{surj}. Now $a' \in B$ iff $a' \notin f(a') = B$. Contradiction. \end{proof} ``` `Suppose not` should only be used when necessary. It disables checking for contradictions within axioms and can lead lower quality error messages. `Contradiction` ends the current proof or explicit subproof, so no further proof step may follow it in the same scope. ## Case splits You can case split on any number on cases, as long as the proof automation is able to prove the disjunction of all the cases. Within each case, there is a local assumption that the case holds. ```tex \begin{proposition}\label{ordinal_preceq_implies_subseteq} Let $\alpha,\beta$ be ordinals. Suppose $\alpha\precedeseq\beta$. Then $\alpha\subseteq\beta$. \end{proposition} \begin{proof} \begin{byCase} \caseOf{$\alpha = \beta$.} Trivial. \caseOf{$\alpha\precedes\beta$.} $\alpha\subset\beta$. \end{byCase} \end{proof} ``` ## Consider We can obtain a witness of an existential statement as a local constant with `Consider`. For example, `Consider $p$ such that $p$ is a prime factor of $n$` requires the prover to show that such a `$p$` exists. After this, `$p$` is available as a local constant with the desired property. ## Suffices We can change the sufficency by using a step of the form `It suffices to show that ...`. In this case the automated theorem prover needs to show that the new sufficiency implies the old one within the current context. ## Proof by ∈-induction (set induction) ```tex \begin{lemma}\label{regularity_aux} For all $a, A$ such that $a\in A$ there exists $b\in A$ such that $b\notmeets A$. \end{lemma} \begin{proof}[Proof by \in-induction on $a$] \begin{byCase} \caseOf{$a\notmeets b$.} Straightforward. % This leaves the goal to the automated prover \caseOf{$a\meets b$.} Take $a'$ such that $a'\in a, b$. Straightforward. % We apply the induction hypothesis to a' \end{byCase} \end{proof} ``` ## Calculations