def gen_cell.go

minebender-game@1.0.0.0 · proof_gen.bend:414

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/game.bend as G

414def gen_cell.go(+z: G.Zone, +p: T.Pos, +need: Nat, +left: Nat, +rs: List<&2, U32>, +lp: Nat,
415  inv: {Nat.is_le(need, left) == True{} : Bool}, +s: Bool, e: {G.gen.out(z, p) == s : Bool},
416  +lft: {left == Nat.add(Bool.pick(Nat, s, 0n, 1n), lp) : Nat}) ->
417  GenStep(z, p, G.GenState{need, left, rs}, lp):
418  match s:
419    case True{}:
420      %Equal.sym(Bool, G.gen.out(z, p), True{}, e) :
421        {Nat.add(one(Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)), G.gen.pick(need, left, rs))),
422          st_need(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
423            G.gen.pick(need, left, rs)), need, left, rs))) == need : Nat} &
424        {Nat.is_le(st_need(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
425            G.gen.pick(need, left, rs)), need, left, rs)),
426          st_left(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
427            G.gen.pick(need, left, rs)), need, left, rs))) == True{} : Bool} &
428        {st_left(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
429            G.gen.pick(need, left, rs)), need, left, rs)) == lp : Nat}
430      ({==}, (inv, lft))
431    case False{}:
432      %Equal.sym(Bool, G.gen.out(z, p), False{}, e) :
433        {Nat.add(one(Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)), G.gen.pick(need, left, rs))),
434          st_need(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
435            G.gen.pick(need, left, rs)), need, left, rs))) == need : Nat} &
436        {Nat.is_le(st_need(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
437            G.gen.pick(need, left, rs)), need, left, rs)),
438          st_left(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
439            G.gen.pick(need, left, rs)), need, left, rs))) == True{} : Bool} &
440        {st_left(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
441            G.gen.pick(need, left, rs)), need, left, rs)) == lp : Nat}
442      %Equal.sym(Nat, left, 1n+lp, lft) :
443        {Nat.add(one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, _, rs))),
444          Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, _, rs))))) == need : Nat} &
445        {Nat.is_le(Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, _, rs)))),
446          Nat.sub(_, 1n)) == True{} : Bool} &
447        {Nat.sub(_, 1n) == lp : Nat}
448      gen_cell.need(z, p, need, lp, rs,
449        {%lft : {Nat.is_le(need, _) == True{} : Bool}; inv : {Nat.is_le(need, 1n+lp) == True{} : Bool}})