Library string_c
Require Import ssreflect.
Require Import ZArith_ext Lists_ext.
Require Import ZArith_ext Lists_ext.
Definition of C-like strings and some properties.
Preliminary. Used in a Seplog example that illustrated buffer-overflows.
Preliminary. Used in a Seplog example that illustrated buffer-overflows.
Definition string' (lst : list nat) := ~ In O lst.
Definition string (lst : list Z) := exists lst',
string' lst' /\ lst = (map (fun x => Z_of_nat x) lst') ++ (0::nil).
Lemma string_nil : ~ string nil.
Lemma string'_sub : forall lst, string' lst -> string' (tail lst).
Lemma string_sub : forall lst, (2 <= length lst)%nat -> string lst -> string (tail lst).
Lemma string_sup : forall lst, string lst ->
forall lst', string' lst' -> string (map (fun x => Z_of_nat x) lst' ++ lst).
Lemma string_last : forall lst, string lst -> forall i, nth i lst (-1) = 0 ->
(i = length lst - 1)%nat.
Lemma string_hd_ge0: forall a l, string (a::l) -> a >= 0.
Lemma string_last' : forall i lst, string lst -> (i = length lst - 1)%nat ->
nth i lst (-1) = 0.
Lemma string_last'' : forall i lst, string lst -> (i < length lst)%nat ->
nth i lst (-1) >= 0.