Library TaggedList
This file is part of
A Formal Definition of JML in Coq
and its Application to Runtime Assertion Checking
Ph.D. Thesis by Hermann Lehner
Online available at jmlcoq.info
Authors:
- Hermann Lehner
- David Pichardie (Bicolano)
- Andreas Kaegi (Syntax Rewritings, Implementation of ADTs)
Utils to store tagged data in a list.
A list with tagged data is much like a multi map:
It allows to retrieve all data with a given tag.
Useful functions: taggedFilter : retrieve all data with a given tag t from a list l. taggedMap : apply a function mapF to a list with data with all the same tag t.
The relationship between tag, data, and T:Type is as follows: tagOf: data -> tag mapF: forall t:tag, t -> mapType t (T:Type = mapType t)
Useful functions: taggedFilter : retrieve all data with a given tag t from a list l. taggedMap : apply a function mapF to a list with data with all the same tag t.
The relationship between tag, data, and T:Type is as follows: tagOf: data -> tag mapF: forall t:tag, t -> mapType t (T:Type = mapType t)
tag data type
tag equality must be decidable
Variable tag_eq_dec : forall t1 t2:tag, {t1=t2}+{t1<>t2}.
Lemma dec_eq_tag : forall t1 t2:tag, decidable (t1=t2).
Proof.
intros t1 t2.
unfold decidable.
case (tag_eq_dec t1 t2).
left; assumption.
right; assumption.
Qed.
Lemma dec_eq_tag : forall t1 t2:tag, decidable (t1=t2).
Proof.
intros t1 t2.
unfold decidable.
case (tag_eq_dec t1 t2).
left; assumption.
right; assumption.
Qed.
data data type
Mapping data to tag
Filter out all data d1 from list l that are tagged with t
Fixpoint filterTag (t:tag) (l:list data) : list {d:data | t=tagOf d} :=
match l with
| nil => nil
| d1::ll =>
let t1 := tagOf d1 in
match tag_eq_dec t t1 return list {d:data | t=tagOf d} with
| left Heq => (exist (fun d : data => t = tagOf d) d1 Heq) :: (filterTag t ll)
| right _ => filterTag t ll
end
end.
match l with
| nil => nil
| d1::ll =>
let t1 := tagOf d1 in
match tag_eq_dec t t1 return list {d:data | t=tagOf d} with
| left Heq => (exist (fun d : data => t = tagOf d) d1 Heq) :: (filterTag t ll)
| right _ => filterTag t ll
end
end.
Target dependent type for taggedMap
Map function for taggedMap
Map a list l of data with tag t using function mapF to a list of element type (mapType t).
Definition mapData2Type : forall t:tag, list {d:data | t=tagOf d} -> list (mapType t) :=
fun t => map (mapF t).
fun t => map (mapF t).
Normal filter function lifted onto a list of tagged data.
Definition filterTagData (t:tag) (p:data->bool) (l:list {d:data | t=tagOf d}) : list {d:data | t=tagOf d} :=
filter (fun td:{d:data | t=tagOf d} => let (d,_) := td in p d) l.
filter (fun td:{d:data | t=tagOf d} => let (d,_) := td in p d) l.
Normal map function lifted onto a list of tagged data.
Map function f retrieves a data element together with a proof that the element has a given tag.