nim.py 1.03 KB
 Jean-Christophe Filliâtre committed Mar 17, 2017 1 2 ``````#@ predicate win(n) #@ predicate lose(n) `````` Andrei Paskevich committed Mar 21, 2017 3 ``````#@ assume forall n. n >= 1 -> not lose(n) or not win(n) `````` Jean-Christophe Filliâtre committed Mar 17, 2017 4 5 6 7 8 9 10 `````` #@ assume lose(1) #@ assume forall n. n >= 1 and lose(n) -> win(n+1) \ #@ and win(n+2) and win(n+3) #@ assume forall n. n >= 1 and win(n) and win(n+1) \ #@ and win(n+2) -> lose(n+3) `````` Jean-Christophe Filliâtre committed Mar 21, 2017 11 12 13 14 15 16 17 18 19 ``````def lemma(n): #@ requires n >= 1 #@ ensures lose(n) <-> n % 4 == 1 #@ variant n if n >= 5: lemma(n-1) lemma(n-2) lemma(n-3) lemma(n-4) `````` Jean-Christophe Filliâtre committed Mar 17, 2017 20 21 22 23 `````` start = int(input("start = ")) #@ assume start >= 1 n = start `````` Andrei Paskevich committed Mar 21, 2017 24 25 26 ``````while n >= 1: #@ invariant win(n) -> win(start) #@ variant n `````` Jean-Christophe Filliâtre committed Mar 17, 2017 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 `````` print(n, " matches") k = int(input("your turn: ")) #@ assume k == 1 or k == 2 or k == 3 #@ assume k <= n n = n - k if n == 0: print("you lose") break if n == 1: #@ assert win(start) print("you win") break m = n % 4 if m == 1: k = 1 elif m == 0: k = 3 else: k = m - 1 `````` Jean-Christophe Filliâtre committed Mar 21, 2017 46 47 `````` lemma(n) lemma(n-k) `````` Jean-Christophe Filliâtre committed Mar 17, 2017 48 49 `````` #@ assert win(n) -> lose(n - k) n = n - k``````