From 4be43131e2b3dc60a530de5b3a8f23cd93564ad7 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 23 Sep 2016 16:01:42 +0200 Subject: More modularity on the format of traces depending on the version of coq --- src/versions/native/Structures_native.v | 39 +++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 src/versions/native/Structures_native.v (limited to 'src/versions/native/Structures_native.v') diff --git a/src/versions/native/Structures_native.v b/src/versions/native/Structures_native.v new file mode 100644 index 0000000..950d7bd --- /dev/null +++ b/src/versions/native/Structures_native.v @@ -0,0 +1,39 @@ +Require Import PArray. + + +Section Trace. + + (* We use [array array step] to allow bigger trace *) + Definition trace (step:Type) := array (array step). + + Definition trace_length {step:Type} (t:trace step) : int := + PArray.fold_left (fun l a => (l + (length a))%int63) 0%int63 t. + + Definition trace_get {step:Type} (t:trace step) (i:int) : step := + snd (PArray.fold_left (fun (jres:(option int) * step) a => + let (j,res) := jres in + match j with + | Some j' => + let l := length a in + if (j' < l)%int63 then + (None, get a j') + else + ((Some ((j' - l)%int63)),res) + | None => (None,res) + end + ) (Some i, (get (get t 0) 0)) t). + + Definition trace_fold {state step:Type} (transition: state -> step -> state) (s0:state) (t:trace step) := + PArray.fold_left (PArray.fold_left transition) s0 t. + + Lemma trace_fold_ind (state step : Type) (P : state -> Prop) (transition : state -> step -> state) (t : trace step) + (IH: forall (s0 : state) (i : int), (i < trace_length t)%int63 = true -> P s0 -> P (transition s0 (trace_get t i))) : + forall s0 : state, P s0 -> P (trace_fold transition s0 t). + Proof. + apply PArray.fold_left_ind. + intros a i Hi Ha. + apply PArray.fold_left_ind;trivial. + intros a0 i0 Hi0 Ha0. (* IH applied to a0 and (sum of the lengths of the first i arrays + i0) *) + Admitted. + +End Trace. -- cgit