```
(* Basic imports *)
Require Import Coq.Strings.String.  (* For string operations *)
Require Import Coq.Lists.List.      (* For list operations *)
Require Import Coq.Numbers.BinNums. (* For Z, N, positive numbers *)
Require Import Coq.ZArith.ZArith.   (* For Z arithmetic *)
Require Import Coq.Reals.Reals.     (* For real numbers *)
Require Import Coq.Bool.Bool.       (* For boolean operations *)
Require Import Coq.Numbers.DecimalNat.
Require Import Coq.Numbers.DecimalString.
Require Import String Ascii.
Require Import Decimal Ascii String.

(* Optional but useful *)
Import ListNotations.               (* For list notation like [1;2;3] *)
Open Scope string_scope.            (* For string literals *)
Open Scope Z_scope.                 (* For integer literals *)

(* For tactics *)
Require Import Coq.Program.Tactics.

(* Basic types that Leaf can represent *)
Inductive LeafType :=
  | TString
  | TInt
  | TFloat
  | TBool
  | TDate.

(* A path is a list of identifiers *)
Definition Path := list string.

(* A value can be either scalar or array *)
Inductive LeafValue :=
  | VString : string -> LeafValue
  | VInt : Z -> LeafValue
  | VBool : bool -> LeafValue
  | VFloat : R -> LeafValue
  | VDate : string -> LeafValue  (* ISO8601 format *)
  | VArray : list LeafValue -> LeafValue.

(* A record is either metadata or data *)
Inductive LeafRecord :=
  | Metadata : string -> string -> LeafRecord  (* key, value *)
  | DataRecord : Path -> option LeafType -> LeafValue -> LeafRecord.

(* The full document is a list of records *)
Definition LeafDocument := list LeafRecord.

(* Basic encoder functions *)
Definition encode_type (t: LeafType) : string :=
  match t with
  | TString => "s"
  | TInt => "i"
  | TFloat => "f"
  | TBool => "b"
  | TDate => "d"
  end.

Definition encode_path (p: Path) : string :=
  String.concat "." p.

(* A placeholder: we’ll just show “0.0” for every float. *)
Definition string_of_R (_: R) : string := "0.0".

Definition Z_to_Decimal_int (z : Z) : Decimal.int :=
  match z with
  | Z0 => Decimal.int p  (* zero is represented as Pos Nil *)
  | Zpos p => Decimal.int p
  | Zneg p => Decimal.int p
  end.

(* For a basic working version: *)
Definition my_string_of_Z (z : Z) : string :=
  match z with
  | 0%Z => "0"
  | _ => DecimalString.NilZero.string_of_int 
         (if Z.ltb z 0 
          then DecimalString.NilZero.Neg (Z.to_pos (Z.abs z))
          else DecimalString.NilZero.Pos (Z.to_pos z))
  end.

(* Test it: *)
Compute (my_string_of_Z 42). (* = "42" *)
Compute (my_string_of_Z (-42)). (* = "-42" *)
Compute (my_string_of_Z 0). (* = "0" *)

Check DecimalString.NilZero.int_of_string.

(* Main encoder *)
Fixpoint encode_value (v: LeafValue) : string :=
  match v with
  | VString s => s
  | VInt n => DecimalString.NilZero.string_of_int n
  | VBool b => if b then "true" else "false"
  | VFloat f => string_of_R f
  | VDate d => d
  | VArray vs => String.concat "," (map encode_value vs)
  end.

Definition encode_record (r: LeafRecord) : string :=
  match r with
  | Metadata k v => "@" ++ k ++ "=" ++ v
  | DataRecord path type_hint value =>
      encode_path path ++ 
      match type_hint with
      | Some t => ":" ++ encode_type t
      | None => ""
      end ++
      "=" ++ encode_value value
  end.


(* Parser combinators *)
Definition parse_path (s: string) : option Path :=
  (* Split on dots, validate components *)
  (* Implementation omitted *).

Definition parse_type_hint (s: string) : option LeafType :=
  match s with
  | "s" => Some TString
  | "i" => Some TInt
  | "f" => Some TFloat
  | "b" => Some TBool
  | "d" => Some TDate
  | _ => None
  end.

(* Main decoder *)
Definition decode_line (s: string) : option LeafRecord :=
  (* Parse either metadata or data record *)
  (* Implementation would use string parsing *)
  (* and above helper functions *).

Definition decode_document (lines: list string) : option LeafDocument :=
  sequence (map decode_line lines).


(* Round-trip property *)
Theorem encode_decode_identity :
  forall (doc: LeafDocument),
    decode_document (map encode_record doc) = Some doc.

(* Type safety *)
Theorem type_preservation :
  forall (r: LeafRecord) (t: LeafType),
    has_type r t ->
    has_type (decode_line (encode_record r)) t.
```
Remove all types other than string from this code. Then write how to use it to parse actual file.