blob: 04b396f9f90d0ad13e8ccfe873be7999a3573eee (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
Require Import Int63.
Require Import List.
Section Trace.
Definition trace (step:Type) := ((list step) * step)%type.
Definition trace_length {step:Type} (t:trace step) : int :=
let (t,_) := t in
List.fold_left (fun i _ => (i+1)%int) t 0%int.
Fixpoint trace_get_aux {step:Type} (t:list step) (def:step) (i:int) : step :=
match t with
| nil => def
| s::ss =>
if (i == 0)%int then
s
else
trace_get_aux ss def (i-1)
end.
Definition trace_get {step:Type} (t:trace step) : int -> step :=
let (t,def) := t in trace_get_aux t def.
Definition trace_fold {state step:Type} (transition: state -> step -> state) (s0:state) (t:trace step) :=
let (t,_) := t in
List.fold_left transition t s0.
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)%int = true -> P s0 -> P (transition s0 (trace_get t i))) :
forall s0 : state, P s0 -> P (trace_fold transition s0 t).
Admitted.
End Trace.
|