def range_get.cases

minebender-game@1.0.0.0 · proof_base.bend:356

import Base

356def range_get.cases(+p: Nat, +i: Nat,
357  r: Or({Nat.is_lt(i, p) == True{} : Bool}, {i == p : Nat}),
358  ih: {Nat.is_lt(i, p) == True{} : Bool} -> {List.get(&2, Nat, List.range(p), i) == Some{i} : Maybe<&2, Nat>}) ->
359  {List.get(&2, Nat, List.append(&2, Nat, List.range(p), [p]), i) == Some{i} : Maybe<&2, Nat>}:
360  match r:
361    case Inl{+lt}:
362      +lt2 = {%Equal.sym(Nat, List.length(&2, Nat, List.range(p)), p, range_length(p)) :
363        {Nat.is_lt(i, _) == True{} : Bool}; lt : {Nat.is_lt(i, List.length(&2, Nat, List.range(p))) == True{} : Bool}}
364      %Equal.sym(Maybe<&2, Nat>, List.get(&2, Nat, List.append(&2, Nat, List.range(p), [p]), i),
365        List.get(&2, Nat, List.range(p), i), get_append_l(Nat, List.range(p), [p], i, lt2)) :
366        {_ == Some{i} : Maybe<&2, Nat>}
367      ih(lt)
368    case Inr{eq}:
369      %Equal.sym(Nat, i, p, eq) :
370        {List.get(&2, Nat, List.append(&2, Nat, List.range(p), [p]), _) == Some{_} : Maybe<&2, Nat>}
371      %range_length(p) :
372        {List.get(&2, Nat, List.append(&2, Nat, List.range(p), [p]), _) == Some{p} : Maybe<&2, Nat>}
373      get_append_len(Nat, List.range(p), p, Nil{})