nim.py 1.03 KB
Newer Older
1 2
#@ predicate win(n)
#@ predicate lose(n)
3
#@ assume forall n. n >= 1 -> not lose(n) or not win(n)
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)

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)
20 21 22 23

start = int(input("start = "))
#@ assume start >= 1
n = start
24 25 26
while n >= 1:
    #@ invariant win(n) -> win(start)
    #@ variant n
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
46 47
    lemma(n)
    lemma(n-k)
48 49
    #@ assert win(n) -> lose(n - k)
    n = n - k