[FMFP] remarks on tasks from exam, title page

2026-09-10 19:15:25 +02:00 · 2026-07-28 13:41:56 +02:00
parent 516a85a8b5
commit 1503299b4c
9 changed files with 108 additions and 16 deletions
@@ -8,6 +8,12 @@ Since often we are not restricted to just simple statements, such where we know
 we need to perform case distinction on all possible last rules applied in the derivation tree $T$.
 If all are to be proven, this will yield $7$, one for each rule of the big-step semantics.

+When we have multiple options in a second stage that also differ from the premise, we may want use another case distinction there,
+drawing separate trees for them, or stating that we draw the common tree and then use a subtree $T_N$ for the case distinction to reduce the amount of writing required.
+
+Also be sure that you \textit{always} mention the side conditions and also mention the Induction Hypothesis, if applicable or needed.
+
+
 \inlinedefinition[Subderivation] We define $T' \sqsubset T$, where $T$ is a derivation tree. $T'$ is called a \textit{subderivation} of $T$,
 or more simply, a \textit{subtree} of $T$. Definition is analogous to the subterm relation.

@@ -0,0 +1,41 @@
+\subsection{Proofs using CYP syntax}
+\label{sec:cyp}
+Using CYP (Check Your Proof) syntax is allowed at the exams and can be a bit less to write depending on your writing style.
+However, if you are very concise, you can achieve an even shorter version using a mix of CYP and non-CYP syntax.
+
+In CYP, if doing it with pen and paper, we typically state that we use CYP for the proof,
+when doing it on the computer, we need a \texttt{defs.txt} file, containing all things we assume,
+as well as the function definitions, similar to Haskell syntax.
+Any property we don't want to, or don't have to prove, we can denote with \texttt{axiom axiom\_name: definition of the axiom}.
+Finally, we state the proof's goal, exactly as the statement to prove:
+\verb|goal statement|
+
+If we have to generalize, we add a generalized lemma and prove it, then followed by proving the specific case
+
+For the actual proofs, it start like this:
+\begin{code}{haskell}
+    Lemma lemma_name: statement to prove
+
+    Proof by induction on DataStructureHere x generalizing y -- or any other variable, or possibly without generalization
+    Case Leaf -- or any other of course
+        For fixed y -- only if we generalized
+        Show: statement to prove for this case -- (e.g. substitute x with Leaft in this case)
+        Proof
+            -- The proof goes here
+            statement
+            (by def a_definition) .=. statement'
+            (by any_axiom)        .=. statement''
+        QED
+    
+    Case (Node x y) -- another case
+        Fix x, y -- same as otherwise saying for arbitrary x, y
+        Assume
+            IH1: forall y: induction_hypothesis here
+            IH2: forall y: another IH here -- only needed for something like this, if there are two vars.
+            -- The second IH will (typically) be the same, simply a different var name
+        Show: statement to prove for this case
+        Proof
+        -- The proof (as above)
+        QED
+    QED
+\end{code}
@@ -17,9 +17,6 @@ For the cases notation, there are equal signs. We can use underscores as a ``don

 Always consider making use of functions defined in previous subtasks. This can save a lot of time.

-Note that in a type definition using \texttt{data}, everything beyond the equality sign is part of an argument of the type.
-So e.g. in a type like \texttt{data LTS = LTS Transition Int}, \texttt{LTS} also needs to be supplied.
-
 \subparagraph{Lists}
 In list comprehensions, to draw from a list, \texttt{<-} is used, to delimit the description of the list contents from the generator part, we use a pipe character
 and to separate each statement in the generator part, we use a comma.
@@ -30,6 +27,10 @@ We can initialize infinite lists using the \texttt{..} syntax. We define the int

 More advanced types can be ``disassembled'' like this: \texttt{Node x l r} for type \texttt{Node a (Tree x) (Tree x)}

+Note that for lists, \texttt{(==)} is defined if and only if it is defined for the types in the lists that we are comparing, i.e.
+\mint{haskell}|comp :: (Eq a, Eq b) => [a] -> [b] -> Bool|
+\mint{haskell}|comp ls rs = ls == rs|
+

 \subparagraph{Fold}
 One of the most important functions to understand is \texttt{foldr} (and \texttt{foldl}).
@@ -62,7 +63,10 @@ the type of the canonical fold function is simply \texttt{b -> ([a] -> a -> b) -
 To combine a \texttt{map} and a \texttt{zip} function, use \texttt{zipWith}, type:
 \mint{haskell}|zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]|

-\TODO Add more remarks
+The \texttt{zip} function creates a tuple:
+\mint{haskell}|zip :: [a] -> [b] -> [(a, b)]|
+
+

 \paragraph{Proofs}
 These proofs use structural induction, often it is easiest to use strong structural induction, see Section~\ref{sec:induction-proofs} for that.
@@ -79,3 +83,5 @@ For generalizing, a very helpful tactic is to think about the statement some, co
 after only a very short amount of time, as the correct generalized statement will become apparent there very quickly.

 Remember to always check that parenthesis are set correctly and to only apply one rule exactly once.
+
+Depending on your writing style, it may be worth using the CYP syntax (see Section~\ref{sec:cyp}), as it \textit{can} be more concise.
@@ -1,3 +1,4 @@
+\newpage
 \subsubsection{Natural Deduction}
 \paragraph{Parenthesis}
 This task (if it were to even ever appear in the exams) is simply applying precedences, as well as remembering associativity.
@@ -17,3 +17,6 @@ Of course, if \texttt{x} is decreasing, it itself can become the variant, as it
 Proof outlines work by providing post and pre-condition for each sub-statement in a statement.
 If we need to rewrite a statement (e.g. before the first loop body to change to our loop invariant from the overall precondition),
 we use the $\models$ symbol.
+
+There are also tasks in which we need to find errors in rule applications. This works ``simply'' by checking that the rules are applied correctly
+and semantic entailment and general transformation rules hold for the transformations.
@@ -1,3 +1,4 @@
+\newpage
 \subsubsection{Linear Time Properties (LTL)}
 We refer to Section~\ref{sec:ltl} for intuition, as these tend to mostly be intuition exercises.

@@ -19,18 +20,26 @@ As a reminder, these are the operators (details in Section~\ref{sec:ltl-details}
 For the implication (where the left hand side is called the \textit{antecedent}, right hand side is called the \textit{consequent}),
 remember to show the case where the antecedent is true and state that for antecedent false, it is trivially true

-Another important remark is that you can't just write $\Diamond \neg s_1$, where $s_1$ is a state, you need to specify the propositions.

-We can also create statements, such as never as $\square \neg \Phi$ (always not $\Phi$), etc.
-
-Overall, be careful with parenthesis!
+\paragraph{Tips and tricks}
+\begin{itemize}
+    \item You can't just write $\Diamond \neg s_1$, where $s_1$ is a state,
+          you need to specify the propositions (as a set, such as $\{ A, B \}$ instead of the $s_1$.
+    \item We can also create statements, such as never as $\square \neg \Phi$ (always not $\Phi$), etc.
+    \item Often, an \texttt{if} in the description means we should use a $\Rightarrow$.
+    \item A typical task is ``something will do something (denoted $A$ here) $N$ times'' ($N$ in that case known an low),
+          an LTL formula in the $N = 2$ case is then $\Diamond (A \land \bigcirc \Diamond A)$.
+          Note that $\Diamond (A \land \Diamond A)$ is \bi{NOT} correct (because that is true also for $A$ happening only once).
+    \item If property $A$ has to be true infinitely many times, the LTL formula is $\square \Diamond A$
+    \item Be careful with parenthesis (e.g. with $\neg$)!
+\end{itemize}


-\subparagraph{Liveness and Safety Properties}
+\paragraph{Liveness and Safety Properties}
 Proofs here run using the definitions directly, either by showing a counter example (for disproving) or showing that, in fact, the definition holds.
-Indirect proofs may also come in handy, because it is typically easier to show that something is not a safety property (or liveness property) that to show that it is.
+Indirect proofs may also come in handy, because it is typically easier to show that something is not a safety property (or liveness property) than to show that it is.

 These two properties are \textit{mutually exclusive} (with one exception, \texttt{true}), to the extent that an LTL formula can't be both at the same time, but be a conjunct of both.
 In fact, every LTL formula is a either one of the two, or a conjunct of both.

-Finally, as a reminder, an LTL formula is for example $\square \Diamond a$, with $a$ a property.
+Finally, as a reminder, an LTL formula is for example $\square \Diamond A$, with $A$ an atomic proposition.
@@ -9,6 +9,7 @@ These are (some of) the things that we need to learn by heart for the exam
    \item Induction scheme (especially structural induction and shape of derivation tree)
    \item Ideally for shortness the CYP syntax (roughly, they said they'd not deduct points for incorrect CYP syntax)
    \item Promela syntax
+    \item Read through PVW script (it's VERY good and has some handy tips and tricks for all types of exercises)
 \end{todolist}

 \subsubsection{What to bring to the exam}