Proof Strategies, Quantifiers & Daphne Techniques

Knights & Knaves Recap

• Lecturer revisits previous session’s puzzle to correct a hurriedly-written branch of the proof.

  • Situation: assumed Nave A is true (A lies) and Knight B is true (B tells the truth).

  • Because B is a knight, B’s statement "door D1 is not the exit" must be true ⇒ $\neg\,Exit(D1)$.

  • If A is a nave, A’s response to the same question must be the opposite: A would claim $Exit(D1)$.

  • Combination (A says exit, B says not-exit) produced contradiction → conclusion: B cannot actually be a knight in that branch.

• Larger lesson:

  • Enumerate all cases systematically (truth–lie combinations) to localise contradictions or missing branches.

  • An unprovable branch often indicates either (1) you selected the wrong goal or (2) the specification is incomplete.

Specification Accuracy & Vacuous Truths

• Original English spec ≠ formal Daphne spec; mismatch hid a silent third case:

  • P, Q, R all false ⇒ antecedent of one implication and consequent of the other both false → no contradiction.

  • Required adding extra disjunction $\big(Nave(A)\land Nave(B)\land Exit(D2)\big)$.

• Verify:

  • Does your formalisation reflect every English clause independently?

  • Are you unintentionally proving goals vacuously (e.g. antecedent permanently false, empty set of people, etc.)?

Implication ($A\;\Rightarrow\;B$) – Proof & Use

• To prove $A\to B$:

  1. Assume $A$.

  2. Derive $B$ under that assumption.

  • Daphne syntax:
    dafny if A { // ... prove B inside ... }

• To use a proven implication:

  • If you already have $A\to B$ and $A$, you may assert $B$. Daphne usually infers this automatically.

Case Split (Law of Excluded Middle)

• Any Boolean predicate $P$ is either true or false.

• Pattern:

  1. Assert $P \lor \neg P$.

  2. Case 1: assume $P$, prove goal.

  3. Case 2: assume $\neg P$, prove same goal.

• If both branches succeed, overall goal succeeds.

  assert P || !P;
  if (P) { /* ... */ } else { /* ... */ }

Proof by Contradiction

• Want to prove $A$.

  1. Assume $\neg A$.

  2. Derive contradiction ⇒ $false$.

  3. Conclude $A$.

• Daphne: assert false; at end of contradiction branch signals success.

Existential Quantifier ($\exists$)

• To prove $\exists x\,A(x)$:

  • Produce a concrete witness $e$ and show $A(e)$.

  • Daphne: after assert A(e) you may assert exists x :: A(x).

• To use $\exists x\,A(x)$ in a proof:

  1. Introduce a fresh, unconstrained variable $v$.

  2. Assume $A(v)$ holds.

  • Daphne idiom:
    dafny var v : T :| A(v); // v now usable with property A(v)

• Variable-capture danger:

  • Re-using an already-constrained name can create contradictions (e.g. showing $0=1$ in the transcript’s counter-example).

Universal Quantifier ($\forall$)

• To prove $\forall x\,A(x)$:

  1. Take a fresh arbitrary $v$ of the right type.

  2. Show $A(v)$ with no extra assumptions about $v$.

  • Daphne pattern:
    dafny forall x : T ensures A(x) { // proof body using arbitrary x }

• To use $\forall x\,A(x)$:

  • Plug in any expression $e$ of the same type and assert $A(e)$.

Worked Math Examples

1 Sum of Two Even Integers is Even

• Definition: $even(n)\;:\; \exists k\in\mathbb Z\, .\, n = 2k$.

• Goal: $\forall m,n\in \mathbb Z .\; even(m) \land even(n) \to even(m+n)$.

• Proof outline:

  1. Assume $even(m)$ ⇒ $m = 2i$ for some $i$.

  2. Assume $even(n)$ ⇒ $n = 2j$ for some $j$.

  3. $m+n = 2i + 2j = 2(i+j)$; $i+j\in\mathbb Z$.

  4. Matches even pattern ⇒ $even(m+n)$.

2 Transitivity of Divisibility

• Define $div\,(a, b)\;:\; \exists k\in\mathbb N\, .\, b = a k$ .

• Claim: $\forall x,y,z .\; x|y \land y|z \to x|z$.

• Proof:

  • $x|y$ ⇒ $y = xk$.

  • $y|z$ ⇒ $z = yj$.

  • Substitute ⇒ $z = (xk)j = x(kj)$ with $kj\in\mathbb N$ ⇒ $x|z$.

3 Consecutive Integers Have Opposite Parity

• Odd definition: $odd(n)\;:\; \exists k\, .\, n = 2k + 1$.

• Theorem used: every integer is either even or odd.

• Let arbitrary $m$, then handle two cases:

  • Case even(m):
    $m = 2k$ ⇒ $m+1 = 2k+1$ ⇒ odd.

  • Case odd(m):
    $m = 2k+1$ ⇒ $m+1 = 2k+2 = 2(k+1)$ ⇒ even.

• Therefore one of $even(m)\land odd(m+1)$ or $odd(m)\land even(m+1)$ always holds.

4 Daphne Example – Multiples of 5

• Predicate: divBy5(x) == exists k:int :: x == 5 * k.

• Lemma goal (pseudo-Daphne):

  lemma mult_of_fives()
    ensures forall x y :: divBy5(x) && divBy5(y) ==> divBy5(x*y)

• Proof sketch inside lemma:

  forall x y
    ensures divBy5(x) && divBy5(y) ==> divBy5(x*y)
  {
    if (divBy5(x) && divBy5(y)) {
      var k :| x == 5*k;        // witness from first existential
      var j :| y == 5*j;        // witness from second existential
      assert x*y == 5*(k*j);    // algebra → spotted pattern
    }
  }

• Once product is positioned as $5 \cdot (k j)$ Daphne recognises divBy5(x*y).

Daphne Syntax Patterns & Tips

• if A { … } acts as "assume A" block for proving implications.

• assert P || !P; handy to trigger case-splits.

• Introduce existential witness: var v : T :| Property(v);.

• Freshness rule: variable introduced by var must not appear in earlier context.

• For universal proofs, wrap body inside forall x :: ensures … { … } so x is visible.

• Naming numbered assertions (assert A; label A1;) clarifies substitution steps.

Common Pitfalls & Defensive Checks

• Re-using already-constrained variable names under $\exists$ or $\forall$ leads to unsound proofs.

• Joining independent English clauses into a single logical formula can accidentally bind them together; keep independent predicates separate.

• Vacuous success: proof might pass because antecedent is unreachable; always test with manual counter-examples.

• Arithmetic simplifications (e.g. factoring 2) sometimes need explicit assert steps for Daphne to "see" them.

Why The Theory Matters

• Final exam has no Daphne; manual reasoning mandatory.

• Understanding formal patterns accelerates Daphne work: you know why a branch cannot be proved and where to insert hints.

• Aligns specifications with intended behaviour, preventing subtle logical errors in code and proofs.

Real-World & Ethical Connections

• Formal verification (e.g. Dafny) is used in safety-critical domains (aviation, medical, crypto).
  Rigorous specifications avert catastrophic mismatches between design and implementation.

• Highlight ethical responsibility: an incorrect but "successfully proved" spec may mask real faults—thorough human reasoning remains essential.