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)


Require Import List.
Require Import Decidable.

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)


Section tagged.
tag data type
  Variable tag : Set.

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.

data data type
  Variable data : Type.

Mapping data to tag
  Variable tagOf : data -> 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.

Target dependent type for taggedMap
  Variable mapType : tag -> Type.

Map function for taggedMap
  Variable mapF : forall t:tag, {d:data | t=tagOf d} -> mapType t.

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).

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.

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.
  Definition mapTag (f : forall t:tag, {d:data | t=tagOf d} -> data) (l:list data) : list data :=
    let f' (d:data) : data := f (tagOf d) (exist _ d (refl_equal (tagOf d))) in
    List.map f' l.

End tagged.