Properties hold for inner slices if they do for outer ones

Sandbox.fst

module Sandbox
 
#set-options "--ifuel 0 --fuel 0 --z3rlimit 1"


open FStar.Seq
open FStar.Seq.Base
open FStar.IntegerIntervals
open FStar.UInt32
module U32 = FStar.UInt32

let uint = UInt32.t 
 
let value_of (x: UInt32.t) = UInt32.v x
 

let (!) (x:uint) = value_of x 

let slice_has_property (property: uint -> prop)
                  (g: seq uint)
                  (i: uint)
                  (j: uint { !i <= !j /\ !j <= length g })
  = (forall x. mem x (slice g !i !j) ==> property x)

let subslice_has_property_aux (property: uint -> prop)
                              (g: seq uint)
                              (i j k: uint)
                              (l: uint {!i <= !k /\ !k <= !l /\ !l <= !j /\ !j <= length g})
                              (x: uint { mem x (slice g !k !l) })
  : Lemma (requires slice_has_property property g i j)
          (ensures property x) = 
  let p = !k - !i in
  let seq_ij = slice g !i !j in
  let seq_kl = slice g !k !l in
  let id = index_mem x seq_kl in
  assert (index seq_ij (id+p) == x);
  assert (index seq_kl id == x)
  
let test_property (g:  seq uint)
                  (k:  uint {!k < length g})
                  (wz: uint {!wz < length g - (!k + 1)})
                  (i:  uint {!i <= !wz + 1 /\ !i >= 1})
  = (forall x. mem x (slice g (!k + !i) (!k + !wz + 1)) ==> !x == 3)

let test_property_on_inner_slice (g:  seq uint)
                                 (k:  uint {!k < length g})
                                 (wz: uint {!wz < length g - (!k + 1)})
                                 (i:  uint {!i <= !wz + 1 /\ !i >= 1})
                                 (j:  uint {!j >= !i /\ !j < !wz + 1})
  : Lemma (requires test_property g k wz i 
                  /\ FStar.UInt.max_int n >= (!k + !wz + 1))
          (ensures test_property g k wz j) = 
  let property (x: uint) : prop = !x == 3 in  
  Classical.forall_intro 
    (Classical.move_requires 
      (subslice_has_property_aux property g 
                                          (k +^ i) 
                                          (k +^ wz +^ one) 
                                          (k +^ j) 
                                          (k +^ wz +^ one)))