Qcert.Basic.Data.DDataNorm

Section DDataNorm.


  Context {fdata:foreign_data}.
  Context (h:brand_relation_t).

  Definition normalize_ddata (d:ddata) : ddata :=
    match d with
    | Dlocal d ⇒ Dlocal (normalize_data h d)
    | Ddistr l ⇒ Ddistr (map (normalize_data h) l)
    end.

  Inductive ddata_normalized : ddata → Prop :=
  | dnlocal d :
      data_normalized h d → ddata_normalized (Dlocal d)
  | dndistr l :
      Forall (fun x ⇒ data_normalized h x) l → ddata_normalized (Ddistr l).

  Theorem dnormalize_normalizes :
    ∀ (d:ddata), ddata_normalized (normalize_ddata d).

  Theorem dnormalize_normalized_eq {d} :
    ddata_normalized d →
    normalize_ddata d = d.

  Corollary dnormalize_idem d :
    normalize_ddata (normalize_ddata d) = normalize_ddata d.

  Corollary dnormalize_normalizes_local :
    ∀ (d:data), ddata_normalized (Dlocal (normalize_data h d)).

End DDataNorm.