def indexed_fold_preserves_invariant

stelliferous@0.0.2.0 · proofs/traversal_array_refinement.bend:273

import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order

273def indexed_fold_preserves_invariant(~State: Data,~Context: Data,
274  ~limit: Context -> Nat,~Invariant: Context -> Nat -> State -> Data,
275  ~update: U32 -> Context -> State -> State,
276  ~preserve: @+context: Context -> @+index: Nat -> @+state: State ->
277    {Nat.is_lt(index,limit(context)) == True{} : Bool} -> Invariant(context,index,state) ->
278    Invariant(context,1n+index,update(U32.from_nat(index),context,state)),
279  +count: Nat,+first: Nat,+context: Context,+state: State,
280  +room: {Nat.is_le(Nat.add(first,count),limit(context)) == True{} : Bool},
281  evidence: Invariant(context,first,state)) ->
282  Invariant(context,Nat.add(first,count),Traversal.indexed_fold(~State,~Context,~update,count,U32.from_nat(first),context,state)):
283  match count:
284    case 0n:
285      %Equal.sym(Nat,Nat.add(first,0n),first,Addition.zero_right(first)) : Invariant(context,_,state)
286      evidence
287    case 1n+ +rest:
288      %Equal.sym(U32,(U32.from_nat(first) + 1 : U32),U32.from_nat(1n+first),Bounds.add_one(U32.from_nat(first))) :
289        Invariant(context,Nat.add(first,1n+rest),Traversal.indexed_fold(~State,~Context,~update,rest,_,context,update(U32.from_nat(first),context,state)))
290      %Equal.sym(Nat,Nat.add(first,1n+rest),1n+Nat.add(first,rest),Addition.successor_right(first,rest)) :
291        Invariant(context,_,Traversal.indexed_fold(~State,~Context,~update,rest,U32.from_nat(1n+first),context,update(U32.from_nat(first),context,state)))
292      indexed_fold_preserves_invariant(~State,~Context,~limit,~Invariant,~update,~preserve,rest,1n+first,context,update(U32.from_nat(first),context,state),
293        Order.advance_room(first,rest,limit(context),room),preserve(context,first,state,Order.room_index(first,rest,limit(context),room),evidence))