## Lemma Direct Proof ### 1. Prove by Cases In a direct proof, we can sometimes prove the property case by case. If the property $P$ is true for domain $D$ then we can instead prove $P$ is true for each of its sub-domains $D_i$ where $D=D_0\cap D_1\cap D_2\dots$ > [!EXAMPLE] Example > If $p$ and $q$ are Booleans, and the property is $p\rightarrow(q\rightarrow p)$, then a case by case proof that this property is a tautology is a truth table. > > ![[Pasted image 20251202200808.png|400]] #### Product of Two Consecutive Numbers is Even ![[Pasted image 20251202201039.png]] **Verify.** See if Dafny has learnt the property. ```Dafny ghost method ValidateProperty() { var n:int := *; Lem2Cons(n); assert (n*(n+1))%2==0; } ``` #### $n^2$ is a Multiple of 3 or One More Translate: - All square numbers are either a multiple of 3 or one more than a multiple of 3. To: - Given any integer n there exists a k such that $n*n=3*k$ or $n*n=3*k+1$. ![[Pasted image 20251202201728.png]] ### 2. Prove by Example An example can be used to prove an 'existence' property. 1. Property: there exists a prime number that is not odd (an example is 2, so the property is **true**) A counterexample is usually used to disprove a property. 2. Property: All prime numbers are odd numbers (a counterexample is 2, so the property is **false**) #### Primes A number $x$ is prime if $x$ is greater than or equal to $2$ and $x$ is not divisible by any number $m$, where $2\leq m\lt x$. Dafny predicate that defines a prime: ```Dafny ghost predicate prime(x:nat) { x>=2 && !exists m :: 2<=m=2 && !exists m :: 2<=m= b // Loop as long as remainder >= divisor invariant euclid(a,b,q,r) // q increments, r decrements { q := q + 1; // Quotient count-down the number of times r := r - b; // we decrement r } } ``` - Postcondition consists of just Euclid's division lemma - The invariant says just that Euclid's predicate is 'invariant' (q and r change) > [!INFO] Euclid's lemma just says a unique $q$ and $r$ exist. #### Algebraic Property: $x*y/y=x$ Property: $x*y/y=x$ where $x\geq0$ and $y\gt0$. Dafny doesn't know this property. ```Dafny lemma LemPropXYYX(x:nat, y:nat) requires y>0 ensures x*y/y == x { var q := x*y/y; // quotient, must prove = x var xmq := x - q; // convenience var, used later LemRemainder(x*y, y); // 1. prove bounds on remainder assert 0 <= x*y - y*q < y; // 2. from lemma assert 0 <= (x - q)*y < y; // 3. y*q = q*y, factor out y assert 0 <= xmq * y < y; // substitute for var assert 0/y <= (xmq * y)/y < (y)/y; // 4. divide everything by y assert 0 <= (xmq * y)/y < 1; // 5. uses 0/y=0 and y/y=1 assert (xmq * y)/y == 0; // 6. upper bound is 0, simplify LemXYY(xmq, y); // prove xmq = 0 assert xmq == 0; // 7. from lemma assert x*y/y == x; // 8. subst for xmq, QED } ``` ### 4. Singleton Sets Property: If $s$ is a singleton set and $i\in s$ then $s=\{i\}$. Dafny doesn't know this property. This is the proof strategy: - We are told there is an element $i$ in a singleton set - We remove this element $i$ - If the result set is an empty set, then originally the set must have been $\{i\}$ ```Dafny lemma LemIAmSingle(s:set, i:int) requires |s|==1 && i in s ensures s=={i} { assert |s-{i}|==0; // Deleting 'i' should make the set empty } ``` ### 5. Disjoint Sets Property: If $A$ and $B$ are disjoint sets and $x\in A$, then $x \not\in B$. Dafny doesn't know this property. ![[Pasted image 20251202210115.png|150]] ```Dafny lemma LemDisjoint(a:set, b:set) // Level-1 proof requires a*b == {} ensures forall x:int | x in a :: x !in b { var ax := a; // ax initially is a copy of a while ax != {} // as long as ax is not empty invariant ax<=a // ax stays a subset of a invariant ax*b=={} // ax and b stay disjoint decreases |ax| // ax gets smaller and smaller { var x :| (x in ax && x !in b); // x is in ax but x is not in b ax := ax - {x}; // remove x } // loop terminates when a == {} } // :| --> non-deterministic assignment ``` *** ## Lemma Contra Techniques ### 1. Direct and Indirect Logic **Example of direct logic**. It uses forward reasoning. "If the course schedule indicates there is a lecture today, then I'll go to uni." **Example of indirect logic.** It works 'backwards'. "If there is a lecture today, then the lecture would now be full." ### 2. Proof of the Contrapositive Indirect logic can be based on the equivalence: $$P\rightarrow Q\equiv\neg Q\rightarrow\neg P$$ #### a. If $n^2$ is Even then $n$ is Even Property: If $n^2$ is an even number, then $n$ is an even number for all integers $n$. We can write this property as: `(n*n)%2==0 ==> n%2==0`. - The postcondition is the original property - The proof is the contrapositive of the property ```Dafny lemma LemN2Neven(n:nat) ensures (n*n)%2==0 ==> n%2==0 // original property P -> Q { // Prove the contrapositive if n%2==1 // if !Q { var k := (n+1)/2; // n is odd, so can halve n+1 assert n == 2*k - 1; // simplify assert n*n == (2*k-1)*(2*k-1); // square previous line assert n*n == 2*k*2*k - 2*2*k + 1; // expand RHS assert n*n == 2*(k*2*k - 2*k) + 1; // factor 2, form 2X+1 assert (n*n)%2 == 1; // QED, !P } } ghost method ValidateN2Neven() { var n:nat := *; LemN2Neven(n); assert (n*n)%2==0 ==> n%2==0; // Original property } ``` #### b. If $n^2-42n+3$ is Even then $n$ is Odd Property: If $n^2-42n+3$ is even then $n$ is odd for any integer $n$. We can write this property as: `(n*n-42*n+3)%2==0 ==> n%2==1`. ```Dafny lemma LemQuadratic(n:int) ensures (n*n-42*n+3)%2==0 ==> n%2==1 // original property P -> Q { // Prove the contrapositive if n%2==0 { // if !Q var q := n/2; // can divide by 2 assert n == 2*q; // x2, swap sides assert n*n-42*n+3 == 2*q*2*q - 42*2*q + 3; // substitute into antec. assert n*n-42*n+3 == 2*q*2*q - 2*42*q + 2 + 1; // rearrange assert n*n-42*n+3 == 2*(q*2*q - 42*q + 1) + 1; // factor 2, form 2X+1 assert (n*n - 42*n + 3)%2==1; // QED, !P } } ghost method ValidateQuad() { var x:int := *; LemQuadratic(x); assert (n*n-42*n+3)%2==0 ==> n%2==1; } ``` ### 3. Proof by Contradiction Another example of indirect logic is proof by contradiction. A proof by contradiction of a property $P$ can be written as a deductive rule: for some $S$ $$\frac{\neg P\rightarrow(S\wedge\neg S)}{P}$$ **General Format.** ```Dafny lemma LemName(x) ensures P(x) { // Proof by contradiction if !P(x) { ... assert Q(x) && !Q(x); assert false; } assert P(x); } ``` #### a. If $x=x+x$ then $x=0$ Property: If $x=x+x$ then $x=0$ for all integers $x$. - The assumption that the property is false is *absurd* - So the property is true ```Dafny lemma LemXXXX(x:int) ensures x==x+x ==> x==0 { // Proof by contradiction if x==x+x && x!=0 { assert x == 2*x; assert x/x == (2*x)/x; assert x/x == 2*(x/x); assert 1 == 2; assert false; } // QED } ``` #### b. If $n^2$ is Odd then $n$ is Odd Property: If $n^2$ is an odd number, then $n$ is an odd number for all integers $n$. ```Dafny lemma LemN2Nodd(n:int) ensures (n*n)%2==1 ==> n%2==1 { // Proof by contradiction if (n*n)%2==1 && n%2==0 // Assumption: antecedent is true and conseq is false { var k := n/2; // n is even, so we halve it assert n == 2*k; // multiply both sides by 2 assert n*n == (2*k)*(2*k); // square both sides assert n*n == 2*(k*2*k); // * is associative assert (n*n)%2 == 0; // contradicts the 1st conjugate assert false; // reductio ad absurdum } // QED } ghost method Validate() { var n:nat := *; LemN2Nodd(n); assert (n*n)%2==1 ==> n%2==1; } ``` #### c. $n^2$ is Odd if and Only if $n$ is Odd Property: $n^2$ is an odd number if and only if $n$ is an odd number for all integers $n$. ```Dafny lemma LemN2N2odd(n:int) ensures (n*n)%2==1 <==> n%2==1 { // left-to-right: LHS ==> RHS uses proof by contradiction if (n*n)%2==1 && n%2==0 { // assumption: LHS==>RHS is false var k := n/2; // n is even, so we can halve it assert n == 2*k; // multiply both sides by 2 assert n*n == (2*k)*(2*k); // square both sides assert n*n == 2*(k*2*k); // * is associative assert (n*n)%2 == 0; // contradicts the contradiction assert false; // reductio ad absurdum } // QED // right-to-left: RHS ==> LHS uses a direct proof if n%2==1 { var k := (n-1)/2; // n odd, so n+1 is even assert n == 2*k + 1; // make n subject assert n*n == (2*k + 1)*(2*k + 1); // square both sides assert n*n == 2*k*2*k + 2*2*k + 1; // expand assert n*n == 2*(k*2*k) + 2*(2*k) + 1; // associativity assert n*n == 2*(k*2*k + 2*k) + 1; // factor out 2, form 2X+1 assert (n*n)%2 == 1; // n*n is odd, QED } } ``` #### d. Disjoint Sets Property: Given disjoint sets $A$ and $B$, and $x\in A$, then $x\not\in B$. - There is no implication in this property specification - The assumption is the negation of the postcondition ```Dafny lemma LemDisjoint(a:set, b:set, x:int) requires a*b == {} requires x in a ensures x !in b // property { // Proof by contradiction if x in b // assumption: postcondition is false { assert (x in b) && (x in a); // condition and reqt assert a*b=={x}; // hence x is in both sets assert a*b=={x} && a*b=={}; // && the reqt: contradiction assert false; // reduction ad absurdum } } ``` #### e. $\sqrt{2}$ is Irrational > [!INFO] Rational Number > A rational number is a number that can be written as a fraction $p/q$, where $p$ and $q$ are integers that have no common factors and $q\neq0$. Property: Integers $p$ and $q$ have a common factor $n\geq 2$ if $p\mod n=0$ and $q\mod n=0$. We can express this as: ```Dafny ghost predicate commfact(p:nat, q:nat) { exists n:nat :: 2<=n<=p && 2<=n<=q && p%n==0 && q%n==0 } ``` So if $\sqrt{2}$ is irrational, then the following predicate is false: ```Dafny ghost predicate pqexist() { exists p:nat, q:nat :: root2(p,q) } ghost predicate root2(p:nat, q:nat) { 0, b:set) requires a*b == {} ensures forall x:int | x in a :: x !in b { if a == {} { // base case assert true; // forall vacuously true } else { LemMemberExists(a,b); // sublemma element exists var x :| (x in a && x !in b); // (*) x is in a and not b LemDisjointMember(a-{x},b); // IH for reduced set assert forall y | y in a-{x} :: y !in b; // proved for IH assert x !in b; // using (*) assert forall y | y in a :: y !in b; // combine last 2 lines } } lemma {:induction false} LemMemberExists(a:set, b:set) requires a != {} requires a*b == {} ensures exists x:int :: (x in a && x !in b) { // Proof by contradiction if !exists x:: (x in a && x !in b) // assume postcondition is false { assert forall x :: (x in a && x in b); // rewrite if-condition assert a <= b; // a is a subset of b assert a*b != {}; // so a and b not disjoint assert false; // contradicts precondition } } ghost method Validator() { var a:set := *; var b:set := *; if a*b == {} { LemDisjointMember(a,b); assert forall x:int | x in a :: x !in b; } } ``` ### 5. Cardinality #### Concatenated Sets Property: If $A$ and $B$ are disjoint sets then the sum of their cardinalities, $|A|+|B|$, is equal to the cardinality of their concatenation $|A+B|$. ```Dafny ghost method Validator() { var a:set := *; var b:set := *; if a*b=={} { assert |a+b| == |a| + |b|; } } ``` #### Subset Cardinality Property: If $A$ is a subset of $B$ then $|A|\leq|B|$. ```Dafny lemma {:induction false} LemSubsetCard(a:set, b:set) ensures a==b ==> |a|==|b| // sets equal (for completeness) ensures a |a|<|b| // if a is a proper subset then it is smaller { if a==b { assert |a|==|b|; } // the eual case else if a := *; var b:set := *; if a==b { assert |a|==|b|; } LemSubsetCard(a,b); assert a |a|<|b|; } ```

SENG2011