blob: 47ae21fbf5f706275f20d3bdc08705898b0b1511 (
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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2021 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
Require Import PArray.
Section Trace.
(* We use [array array step] to allow bigger trace *)
Definition trace (step:Type) := array (array step).
Definition trace_to_list {step:Type} (t:trace step) : list step :=
PArray.fold_left (fun res a => List.app res (PArray.to_list a)) nil t.
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.
Definition nat_eqb := beq_nat.
Definition nat_eqb_eq := beq_nat_true_iff.
Definition nat_eqb_refl := NPeano.Nat.eqb_refl.
|
