def gen_take

minebender-game@1.0.0.0 · proof_gen.bend:380

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

380def gen_take(+z: G.Zone, +p: T.Pos, +m: Nat, +lp: Nat, +rs: List<&2, U32>,
381  inv: {Nat.is_le(1n+m, 1n+lp) == True{} : Bool}, +c: Bool,
382  ce: {G.gen.pick(1n+m, 1n+lp, rs) == c : Bool}) ->
383  {Nat.add(one(c), Nat.sub(1n+m, one(c))) == 1n+m : Nat} &
384  {Nat.is_le(Nat.sub(1n+m, one(c)), Nat.sub(1n+lp, 1n)) == True{} : Bool} &
385  {Nat.sub(1n+lp, 1n) == lp : Nat}:
386  match c:
387    case True{}:
388      %Equal.sym(Nat, Nat.sub(m, 0n), m, P.sub_zero(m)) :
389        {1n+_ == 1n+m : Nat} & {Nat.is_le(_, Nat.sub(lp, 0n)) == True{} : Bool} &
390        {Nat.sub(lp, 0n) == lp : Nat}
391      %Equal.sym(Nat, Nat.sub(lp, 0n), lp, P.sub_zero(lp)) :
392        {1n+m == 1n+m : Nat} & {Nat.is_le(m, _) == True{} : Bool} & {_ == lp : Nat}
393      ({==}, (inv, {==}))
394    case False{}:
395      %Equal.sym(Nat, Nat.sub(lp, 0n), lp, P.sub_zero(lp)) :
396        {1n+m == 1n+m : Nat} & {Nat.is_le(1n+m, _) == True{} : Bool} & {_ == lp : Nat}
397      ({==}, (P.le_ne(m, lp, inv, gen_pick_false(1n+m, 1n+lp, rs, ce)), {==}))