Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Require Import Coq.Program.Equality.
Require Import Coq.Arith.EqNat.
Import ListNotations.
Open Scope list_scope.
Open Scope string_scope.
Open Scope type_scope.

Inductive label : Type := (* efficiency hack *)
| lUnquote : label
| lQuasiquote : label
| lDiscard : label
| lStr : string -> label.

Inductive value : Type :=
| vBool : bool -> value
| vSymbol : label -> value
| vRecord: value -> list value -> value
| vSeq : list value -> value.

Inductive pattern : nat -> Type :=
| pBool : bool -> pattern 0
| pSymbol : label -> pattern 0
| pUnquote : forall n, pattern n -> pattern (S n)
| pQuasiquote : forall n, pattern n -> pattern (pred n)
| pRecord : forall n m, pattern n -> patseq m -> pattern (max n m)
| pSeq : forall m, patseq m -> pattern m
with patseq : nat -> Type :=
| psNil : patseq 0
| psCons : forall n m, pattern n -> patseq m -> patseq (max n m).

Inductive command : Type :=
| cDiscard : command
| cQuasiquote : forall n, pattern n -> pred n = 0 -> command.

Scheme Equality for label.

Fixpoint value_ind'
         (P : value -> Prop)
         (PBool : forall b, P (vBool b))
         (PSymbol : forall sym, P (vSymbol sym))
         (PRecord : forall v vs, P v -> Forall P vs -> P (vRecord v vs))
         (PSeq : forall vs, Forall P vs -> P (vSeq vs))
         p
         : P p.
Proof.
  induction p; auto; [ apply PRecord; [ apply IHp | ] | apply PSeq ];
    try solve [ induction l; [ apply Forall_nil | ];
                apply Forall_cons; [ apply value_ind'; try assumption | ];
                apply IHl ].
Defined.

Inductive psForall
          (P : forall n, pattern n -> Prop)
  : forall n, patseq n -> Prop :=
| psfNil : psForall P 0 psNil
| psfCons : forall n m p ps,
    P n p -> psForall P m ps -> psForall P (max n m) (psCons n m p ps)
.

Fixpoint pattern_ind'
         (P : forall n, pattern n -> Prop)
         (PBool : forall b, P 0 (pBool b))
         (PSymbol : forall sym, P 0 (pSymbol sym))
         (PUnquote : forall n p, P n p -> P (S n) (pUnquote n p))
         (PQuasiquote : forall n p, P n p -> P (pred n) (pQuasiquote n p))
         (PRecord : forall n m p ps, P n p -> psForall P m ps -> P (max n m) (pRecord n m p ps))
         (PSeq : forall m ps, psForall P m ps -> P m (pSeq m ps))
         n
         p
  : P n p.
Proof.
  induction p; auto.

  apply PRecord; [ apply IHp | ];
    induction p0; [ apply psfNil | apply psfCons; [ apply pattern_ind' | ]; assumption ].

  apply PSeq;
    induction p; [ apply psfNil | apply psfCons; [ apply pattern_ind' | ]; assumption ].
Defined.

Definition unquote_count {n:nat} (p : pattern n) : nat :=
  match p with
  | pBool _ => 0
  | pSymbol _ => 0
  | pUnquote n _ => S n
  | pQuasiquote n _ => pred n
  | pRecord n m _ _ => max n m
  | pSeq m _ => m
  end.

Definition unquote_count_seq {m:nat} (ps : patseq m) : nat :=
  match ps with
  | psNil => 0
  | psCons n m _ _ => max n m
  end.

Lemma unquote_count_accurate : forall n (p : pattern n), unquote_count p = n.
Proof.
  destruct p; reflexivity.
Defined.

Lemma unquote_count_seq_accurate : forall n (ps : patseq n), unquote_count_seq ps = n.
Proof.
  destruct ps; reflexivity.
Defined.

Fixpoint parse v : option { n:nat & pattern n } :=
  let parseSeq := (fix parseSeq vs : option { n:nat & patseq n } :=
                     match vs with
                     | [] => Some (existT patseq 0 psNil)
                     | v :: vs' =>
                       match parse v with
                       | Some (existT _ n p) =>
                         match parseSeq vs' with
                         | Some (existT _ m ps') => Some (existT patseq (max n m) (psCons n m p ps'))
                         | None => None
                         end
                       | None => None
                       end
                     end) in
  match v with
  | vBool b => Some (existT pattern 0 (pBool b))
  | vSymbol l => Some (existT pattern 0 (pSymbol l))
  | vRecord (vSymbol lUnquote) [v'] =>
    match parse v' with
    | Some (existT _ n p') => Some (existT pattern (S n) (pUnquote n p'))
    | None => None
    end
  | vRecord (vSymbol lQuasiquote) [v'] =>
    match parse v' with
    | Some (existT _ n p') => Some (existT pattern (pred n) (pQuasiquote n p'))
    | None => None
    end
  | vRecord v' vs =>
    match parse v' with
    | Some (existT _ n p') =>
      match parseSeq vs with
      | Some (existT _ m ps) => Some (existT pattern (max n m) (pRecord n m p' ps))
      | None => None
      end
    | None => None
    end
  | vSeq vs =>
    match parseSeq vs with
    | Some (existT _ m ps) => Some (existT pattern m (pSeq m ps))
    | None => None
    end
  end.

Example parse1 :
  parse (vBool true) =
  Some (existT pattern 0 (pBool true)).
reflexivity.
Qed.

Example parse2 :
  parse (vRecord (vSymbol lDiscard) []) =
  Some (existT pattern 0 (pRecord 0 0 (pSymbol lDiscard) psNil)).
reflexivity.
Qed.

Example parse3 :
  parse (vRecord (vSymbol lDiscard) [vBool true]) =
  Some (existT pattern 0 (pRecord 0 0 (pSymbol lDiscard) (psCons 0 0 (pBool true) psNil))).
reflexivity.
Qed.

Example parse4 :
  parse (vRecord (vSymbol lUnquote) [vRecord (vSymbol lDiscard) []]) =
  Some (existT pattern 1 (pUnquote 0 (pRecord 0 0 (pSymbol lDiscard) psNil))).
reflexivity.
Qed.

Fixpoint unparse n (p : pattern n) : value :=
  let unparseSeq := (fix unparseSeq m (ps : patseq m) : list value :=
                       match ps with
                       | psNil => []
                       | psCons n m p ps' => unparse n p :: unparseSeq m ps'
                       end) in
  match p with
  | pBool b => vBool b
  | pSymbol l => vSymbol l
  | pUnquote n p' => vRecord (vSymbol lUnquote) [unparse n p']
  | pQuasiquote n p' => vRecord (vSymbol lQuasiquote) [unparse n p']
  | pRecord n m p' ps => vRecord (unparse n p') (unparseSeq m ps)
  | pSeq m ps => vSeq (unparseSeq m ps)
  end.

Definition parseSeq :=
  (fix parseSeq vs : option { n:nat & patseq n } :=
                     match vs with
                     | [] => Some (existT patseq 0 psNil)
                     | v :: vs' =>
                       match parse v with
                       | Some (existT _ n p) =>
                         match parseSeq vs' with
                         | Some (existT _ m ps') => Some (existT patseq (max n m) (psCons n m p ps'))
                         | None => None
                         end
                       | None => None
                       end
                     end).

Definition unparseSeq :=
  (fix unparseSeq m (ps : patseq m) : list value :=
     match ps with
     | psNil => []
     | psCons n m p ps' => unparse n p :: unparseSeq m ps'
     end).

Ltac destruct_useless_discriminant :=
  match goal with
  | hp:(Some _ = match ?e with | Some _ => _ | None => _ end) |- _ =>
    destruct e as [[] | ]; simpl in hp
  end.

Ltac destruct_value v :=
  let Hv := fresh "Heq" v in destruct v as [ | [] | | ] eqn: Hv using value_ind'.

Ltac destruct_fields vs :=
  let Hvs := fresh "Heq" vs in let vs0 := fresh vs in destruct vs as [ | ? vs0 ] eqn: Hvs; try destruct vs0.

Ltac destruct_record v vs :=
  destruct_value v; destruct_fields vs.

Lemma unparseSeq_parseSeq_id vs :
  forall m ps,
    (Forall (fun v : value => forall (n : nat) (p : pattern n), Some (existT pattern n p) = parse v -> unparse n p = v) vs) ->
    Some (existT patseq m ps) = parseSeq vs ->
    unparseSeq m ps = vs.
Proof.
  induction vs; intros m ps Hvs Hlhs; [ inversion Hlhs; subst; simpl_existTs; subst; reflexivity | ];
    destruct ps; [ simpl in Hlhs; repeat destruct_useless_discriminant; inversion Hlhs | ].
  simpl; f_equal; simpl in Hlhs;
    [ inversion Hvs; apply H1 |
      apply IHvs; [ inversion Hvs; assumption | ] ];
    repeat destruct_useless_discriminant;
    inversion Hlhs; subst; simpl_existTs; subst; reflexivity.
Qed.

Lemma unparse_parse_id v :
  forall n p,
    Some (existT pattern n p) = parse v -> unparse n p = v.
Proof.
  induction v using value_ind'; intros n p Hlhs;
    destruct p using pattern_ind';
    fold parseSeq in * |- *;
    try solve [ inversion Hlhs; reflexivity
              | simpl in Hlhs; destruct_useless_discriminant; inversion Hlhs
              | destruct_record v vs; simpl in Hlhs; repeat destruct_useless_discriminant; inversion Hlhs
              | destruct_record v vs;
                try solve [simpl in Hlhs; repeat destruct_useless_discriminant; inversion Hlhs];
                simpl; repeat f_equal;
                inversion H;
                apply H2;
                simpl in Hlhs; destruct_useless_discriminant;
                inversion Hlhs; subst; simpl_existTs; subst; reflexivity ].

  simpl; fold unparseSeq;
    f_equal;
    [ apply IHv |
      apply unparseSeq_parseSeq_id; [ assumption | ];
      simpl in Hlhs; fold parseSeq in Hlhs ];
    destruct_record v vs; simpl in Hlhs; simpl;
      try solve [ rewrite <- Heqvs in * |- *;
                  repeat destruct_useless_discriminant;
                  inversion Hlhs; subst; simpl_existTs; subst; reflexivity ].

  simpl; fold unparseSeq; f_equal.
  apply unparseSeq_parseSeq_id; [ assumption | ].
  simpl in Hlhs; fold parseSeq in Hlhs.
  destruct_useless_discriminant;
    inversion Hlhs; subst; simpl_existTs; subst; reflexivity.
Qed.

Fixpoint compact n (p : pattern n) : { m:nat & pattern m } :=
  let compactSeq := (fix compactSeq m ps : { m': nat & patseq m' } :=
                       match ps with
                       | psNil => existT patseq 0 psNil
                       | psCons n m p ps =>
                         let '(existT _ n p) := compact n p in
                         let '(existT _ m ps) := compactSeq m ps in
                         existT patseq (max n m) (psCons n m p ps)
                       end) in
  match p with
  | pBool b => (existT pattern n p)
  | pSymbol l => (existT pattern n p)
  | pUnquote n p =>
    let '(existT _ n p) := compact n p in
    (existT pattern (S n) (pUnquote n p))
  | pQuasiquote n p =>
    let '(existT _ n p) := compact n p in
    (existT pattern (pred n) (pQuasiquote n p))
  | pRecord _ _ (pSymbol lUnquote) (psCons n _ p psNil) =>
    let '(existT _ n p) := compact n p in
    (existT pattern (S n) (pUnquote n p))
  | pRecord _ _ (pSymbol lQuasiquote) (psCons n _ p psNil) =>
    let '(existT _ n p) := compact n p in
    (existT pattern (pred n) (pQuasiquote n p))
  | pRecord n m p ps =>
    let '(existT _ n p) := compact n p in
    let '(existT _ m ps) := compactSeq m ps in
    existT pattern (max n m) (pRecord n m p ps)
  | pSeq m ps =>
    let '(existT _ m ps) := compactSeq m ps in
    existT pattern m (pSeq m ps)
  end.

Definition compactSeq :=
  (fix compactSeq m ps : { m': nat & patseq m' } :=
     match ps with
     | psNil => existT patseq 0 psNil
     | psCons n m p ps =>
       let '(existT _ n p) := compact n p in
       let '(existT _ m ps) := compactSeq m ps in
       existT patseq (max n m) (psCons n m p ps)
     end).

Lemma parseSeq_unparseSeq_id m ps :
  forall m' ps',
    (psForall
       (fun (n_uncompacted : nat) (p_uncompacted : pattern n_uncompacted) =>
          forall (n : nat) (p : pattern n),
            existT pattern n p = compact n_uncompacted p_uncompacted -> Some (existT pattern n p) = parse (unparse n p)) m ps) ->
    existT patseq m' ps' = compactSeq m ps ->
    Some (existT patseq m' ps') = parseSeq (unparseSeq m' ps').
Proof.
  induction ps; intros m' ps' Hps Hcompact.

  inversion Hcompact; subst; simpl_existTs; subst.
  reflexivity.

  inversion Hps; subst; simpl_existTs; subst.
  simpl in Hcompact.
  destruct (compact n p).
  destruct (compactSeq m ps).
  inversion Hcompact; subst; simpl_existTs; subst.
  simpl.
  rewrite <- H2; auto.
  rewrite <- IHps; auto.
Qed.

Ltac destruct_pattern p :=
  let Hp := fresh "Heq" p in destruct p as [ | [] | | | | ] eqn: Hp using pattern_ind'.

Ltac destruct_params ps :=
  let Hps := fresh "Heq" ps in
  let ps0 := fresh ps in
  destruct ps as [ | ? ? ? ps0 ] eqn: Hps; try destruct ps0.

Lemma parse_unparse_id n p :
  forall nn pp,
    existT pattern nn pp = compact n p ->
    Some (existT pattern nn pp) = parse (unparse nn pp).
Proof.
  induction p using pattern_ind'; intros nn pp Hcompact;
    try solve [ inversion Hcompact; subst; simpl_existTs; subst; reflexivity
              | simpl in Hcompact;
                destruct (compact n p);
                inversion Hcompact; subst; simpl_existTs; subst;
                simpl; rewrite <- IHp; reflexivity ];
    try (dependent destruction p; destruct_all label);
    try solve [
          simpl in Hcompact; fold parseSeq compactSeq in Hcompact;
          destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps;
          apply parseSeq_unparseSeq_id in Heqps; [ | assumption ];
          inversion Hcompact; subst; simpl_existTs; subst;
          simpl; fold parseSeq unparseSeq;
          rewrite <- Heqps;
          reflexivity ].

  simpl in Hcompact; fold parseSeq compactSeq in Hcompact;
    destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps;
      remember Heqps as Heqps'; clear HeqHeqps';
        apply parseSeq_unparseSeq_id in Heqps; [ | assumption ];
          destruct_params ps;
          try solve [
                inversion Hcompact; try subst nn; simpl_existTs; try subst pp;
                simpl; fold parseSeq unparseSeq;
                rewrite <- Heqps;
                simpl in Heqps';
                try destruct (compact n p0);
                try destruct (compact n0 p1);
                try destruct (compactSeq m ps0);
                inversion Heqps'; subst; simpl_existTs; subst;
                simpl;
                reflexivity ];
          (simpl in Heqps';
           destruct (compact n p0) eqn: Heqp0; symmetry in Heqp0;
           inversion Hcompact; subst; simpl_existTs; subst;
           inversion H; subst; simpl_existTs; subst;
           simpl;
           rewrite <- H3; [ reflexivity | assumption ]).

  simpl in Hcompact; fold parseSeq compactSeq in Hcompact;
    destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps;
      remember Heqps as Heqps'; clear HeqHeqps';
        apply parseSeq_unparseSeq_id in Heqps; [ | assumption ];
          destruct_params ps;
          try solve [
                inversion Hcompact; try subst nn; simpl_existTs; try subst pp;
                simpl; fold parseSeq unparseSeq;
                rewrite <- Heqps;
                simpl in Heqps';
                try destruct (compact n p0);
                try destruct (compact n0 p1);
                try destruct (compactSeq m ps0);
                inversion Heqps'; subst; simpl_existTs; subst;
                simpl;
                reflexivity ];
          (simpl in Heqps';
           destruct (compact n p0) eqn: Heqp0; symmetry in Heqp0;
           inversion Hcompact; subst; simpl_existTs; subst;
           inversion H; subst; simpl_existTs; subst;
           simpl;
           rewrite <- H3; [ reflexivity | assumption ]).

  simpl in Hcompact; fold parseSeq compactSeq in Hcompact;
    destruct (compact n p) eqn: Heqp; symmetry in Heqp;
      assert (existT pattern (S x) (pUnquote x p0) = compact (S n) (pUnquote n p));
      [ simpl; rewrite <- Heqp; reflexivity | ];
      apply IHp in H0;
      destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps;
        apply parseSeq_unparseSeq_id in Heqps; [ | assumption ];
          inversion Hcompact; subst; simpl_existTs; subst;
            simpl; fold parseSeq unparseSeq;
              rewrite <- Heqps;
              simpl in H0; rewrite <- H0; reflexivity.

  simpl in Hcompact; fold parseSeq compactSeq in Hcompact;
    destruct (compact n p) eqn: Heqp; symmetry in Heqp;
      assert (existT pattern (pred x) (pQuasiquote x p0) = compact (pred n) (pQuasiquote n p));
      [ simpl; rewrite <- Heqp; reflexivity | ];
      apply IHp in H0;
      destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps;
        apply parseSeq_unparseSeq_id in Heqps; [ | assumption ];
          inversion Hcompact; subst; simpl_existTs; subst;
            simpl; fold parseSeq unparseSeq;
              rewrite <- Heqps;
              simpl in H0; rewrite <- H0; reflexivity.

  assert (exists ln lp, existT pattern ln lp = compact (max n m0) (pRecord n m0 p p0)).
  destruct (compact (max n m0) (pRecord n m0 p p0)) eqn: Hlabel.
  exists x, p1.
  reflexivity.
  inversion H0 as [ln [lp Hlabel]].
  remember Hlabel as Hlabel'; clear HeqHlabel'.
  apply IHp in Hlabel.
  simpl in Hcompact.
  simpl in Hlabel'.
  fold compactSeq in Hcompact, Hlabel'.
  rewrite <- Hlabel' in Hcompact.
  destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps.
  apply parseSeq_unparseSeq_id in Heqps; [ | assumption ].
  inversion Hcompact; subst; simpl_existTs; subst.
  simpl; fold parseSeq unparseSeq.
  rewrite <- Heqps.
  rewrite <- Hlabel.
  destruct (compact n p) eqn: Hnp.
  destruct (compactSeq m0 p0) eqn: Hm0p0.
  destruct_pattern p;
    inversion Hlabel'; subst; simpl_existTs; subst; simpl; try reflexivity;
      destruct p0; try destruct p0; try destruct (compact n p) eqn: Hnp2;
        inversion Hlabel'; subst; simpl_existTs; subst; simpl; try reflexivity.

  simpl in Hcompact; fold compactSeq in Hcompact.
  simpl in IHp; fold compactSeq in IHp.
  destruct (compactSeq m0 p) eqn: Hm0p; symmetry in Hm0p.
  destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps.
  apply parseSeq_unparseSeq_id in Heqps; [ | assumption ].
  inversion Hcompact; subst; simpl_existTs; subst.
  simpl; fold parseSeq unparseSeq.
  rewrite <- Heqps.
  replace (parseSeq (unparseSeq x p0)) with (Some (existT patseq x p0)); [ reflexivity | ].
  apply (parseSeq_unparseSeq_id m0 p); [ | assumption ].
  clear H Hcompact0 Heqps x0 p1 ps m.
  dependent induction p; [ apply psfNil | apply psfCons ].

  intros n0 p2 Hc.
  simpl in Hm0p.
  destruct (compact n p) eqn: Hnp.
  destruct (compactSeq m p0) eqn: Hm0p2.
  inversion Hm0p; subst; simpl_existTs; subst.
  assert (Some (existT pattern (Nat.max x0 x1) (pSeq (Nat.max x0 x1) (psCons x0 x1 p3 p4)))
          = parse (unparse (Nat.max x0 x1) (pSeq (Nat.max x0 x1) (psCons x0 x1 p3 p4))));
    [ apply IHp0; reflexivity | ].
  inversion Hc; subst; simpl_existTs; subst.
  simpl in H; fold parseSeq unparseSeq in H.
  destruct (parse (unparse x0 p3)) as [[]|] eqn: Hx0p3;
    destruct (parseSeq (unparseSeq x1 p4)) as [[]|] eqn: Hx1p4;
    inversion H; subst; simpl_existTs; subst; reflexivity.

  simpl in Hm0p.
  destruct (compact n p) eqn: Hnp.
  destruct (compactSeq m p0) eqn: Hm0p2.
  inversion Hm0p; subst; simpl_existTs; subst.
  apply (IHp x1 p3); [ reflexivity | ].
  intros.
  inversion H; subst; simpl_existTs; subst.
  assert (Some (existT pattern (Nat.max x0 x1) (pSeq (Nat.max x0 x1) (psCons x0 x1 p2 p3)))
          = parse (unparse (Nat.max x0 x1) (pSeq (Nat.max x0 x1) (psCons x0 x1 p2 p3))));
    [ apply IHp0; reflexivity | ].
  simpl in H; fold parseSeq unparseSeq in H.
  simpl; fold parseSeq unparseSeq.
  destruct (parseSeq (unparseSeq x1 p3)) as [[]|];
    destruct (parse (unparse x0 p2)) as [[]|];
    inversion H; subst; simpl_existTs; subst; reflexivity.
Qed.

Fixpoint mat n p v level : bool :=
  let matSeq := (fix matSeq m ps vs level : bool :=
                   match ps, vs with
                   | psNil, [] => true
                   | psCons n' m' p' ps', (v' :: vs') => andb (mat n' p' v' level) (matSeq m' ps' vs' level)
                   | _, _ => false
                   end) in
  match p with
  | pBool b =>
    match v with
    | vBool b0 => bool_beq b b0
    | _ => false
    end
  | pSymbol l =>
    match v with
    | vSymbol l0 => label_beq l l0
    | _ => false
    end
  | pUnquote n' p' =>
    match level with
    | 0 =>
      match p' with
      | pQuasiquote n'' p'' => mat n'' p'' v 0
      | pRecord _ _ (pSymbol lDiscard) psNil => true
      | _ => (* unreachable unless bogus commands present *) false
      end
    | S level' =>
      match v with
      | vRecord (vSymbol lUnquote) [v'] =>
        mat n' p' v' level'
      | _ => false
      end
    end
  | pQuasiquote n' p' =>
    match v with
    | vRecord (vSymbol lQuasiquote) [v'] =>
      mat n' p' v' (S level)
    | _ => false
    end
  | pRecord n' m' p' ps' =>
    match v with
    | vRecord v vs => andb (mat n' p' v level) (matSeq m' ps' vs level)
    | _ => false
    end
  | pSeq m' ps' =>
    match v with
    | vSeq vs' => matSeq m' ps' vs' level
    | _ => false
    end
  end.

Fixpoint well_formed n (p : pattern n) level : Prop :=
  let well_formedSeq := (fix well_formedSeq m ps level : Prop :=
                           match ps with
                           | psNil => True
                           | psCons n' m' p' ps' =>
                             well_formed n' p' level /\ well_formedSeq m' ps' level
                           end) in
  match p with
  | pBool _ => True
  | pSymbol _ => True
  | pUnquote n' p' =>
    match level with
    | 0 =>
      match p' with
      | pQuasiquote n'' p'' => well_formed n'' p'' 0
      | pRecord _ _ (pSymbol lDiscard) psNil => True
      | _ => False
      end
    | S level' =>
      well_formed n' p' level'
    end
  | pQuasiquote n' p' =>
    well_formed n' p' (S level)
  | pRecord n' m' p' ps' =>
    well_formed n' p' level /\ well_formedSeq m' ps' level
  | pSeq m' ps' =>
    well_formedSeq m' ps' level
  end.

Definition is_compact n (p : pattern n) : Prop :=
  (existT pattern n p) = compact n p.

Lemma compactness_of_parseSeq vs :
  forall m ps,
    (Forall
       (fun v : value =>
          forall (n : nat) (p : pattern n),
            Some (existT pattern n p) = parse v -> is_compact n p) vs) ->
    Some (existT patseq m ps) = parseSeq vs ->
    psForall is_compact m ps.
Proof.
  induction vs; intros m ps Hvs Hparse;
    inversion Hparse; subst; simpl_existTs; subst.
  apply psfNil.
  inversion Hvs;
    destruct (parse a) as [[]|] eqn: Ha; [ | congruence ];
      destruct (parseSeq vs) as [[]|] eqn: Hvs'; [ | congruence ];
        inversion H0; subst; simpl_existTs; subst;
          apply psfCons; [ apply H2; reflexivity
                         | apply IHvs; [ assumption | reflexivity ] ].
Qed.

Lemma convert_compactSeq:
  forall m ps,
    psForall is_compact m ps -> existT patseq m ps = compactSeq m ps.
Proof.
  induction ps; intros Hlhs.
  reflexivity.
  inversion Hlhs; subst; simpl_existTs; subst.
  simpl.
  unfold is_compact in H2; rewrite <- H2.
  apply IHps in H6; rewrite <- H6.
  reflexivity.
Qed.

Lemma compactness_of_parse v :
  forall n p,
    Some (existT pattern n p) = parse v ->
    is_compact n p.
Proof.
  induction v using value_ind'; intros n p Hlhs;
    try solve [inversion Hlhs; subst; simpl_existTs; subst; reflexivity].

  destruct_value v.

  simpl in Hlhs; fold parseSeq in Hlhs;
    (destruct (parseSeq vs) as [[m ps]|] eqn: Hvs; [ | congruence ]);
    (apply (compactness_of_parseSeq vs m ps) in H; [ | symmetry; assumption ]);
    apply convert_compactSeq in H;
    inversion Hlhs; subst; simpl_existTs; subst;
      unfold is_compact; simpl; fold compactSeq;
        rewrite <- H;
        reflexivity.

  admit.
  admit.
  admit.

  simpl in Hlhs; fold parseSeq in Hlhs;
    (destruct (parseSeq vs) as [[m ps]|] eqn: Hvs; [ | congruence ]);
    (apply (compactness_of_parseSeq vs m ps) in H; [ | symmetry; assumption ]);
    apply convert_compactSeq in H;
    inversion Hlhs; subst; simpl_existTs; subst;
      unfold is_compact; simpl; fold compactSeq;
        rewrite <- H;
        reflexivity.

  simpl in Hlhs; fold parseSeq in Hlhs.
  destruct (parse v) as [[n' p']|] eqn: Hv'.
  rewrite Heqv in Hv'; simpl in Hv'; fold parseSeq in Hv'.
  rewrite Hv' in Hlhs.
  (destruct (parseSeq vs) as [[m ps]|] eqn: Hvs; [ | congruence ]);
    (apply (compactness_of_parseSeq vs m ps) in H; [ | symmetry; assumption ]);
    apply convert_compactSeq in H;
    inversion Hlhs; subst; simpl_existTs; subst;
      unfold is_compact; simpl; fold compactSeq;
        rewrite <- H.
  symmetry in Hv'.
  apply IHv in Hv'.
  unfold is_compact in Hv'.
  rewrite <- Hv'.



  destruct_fields vs;
    simpl in Hlhs; fold parseSeq in Hlhs;
    rewrite <- Heqvs in * |- *;
      (destruct (parseSeq vs) as [[m ps]|] eqn: Hvs; [ | try congruence ]);
      try ((apply (compactness_of_parseSeq vs m ps) in H; [ | symmetry; assumption ]);
           apply convert_compactSeq in H;
           inversion Hlhs; subst; simpl_existTs; subst;
           unfold is_compact; simpl; fold compactSeq;
           rewrite <- H;
           reflexivity).
  admit.
  admit.



  destruct_value v;
    (simpl in Hlhs; fold parseSeq in Hlhs;
     destruct_fields vs;
     try rewrite <- Heqvs in H;
     try rewrite <- Heqvs in Hlhs;
     (destruct (parseSeq vs) as [[m ps]|] eqn: Hvs; [ | try congruence ]);
     try (apply (compactness_of_parseSeq vs m ps) in H;
          [ | symmetry; assumption ];
          apply convert_compactSeq in H);
     inversion Hlhs; subst; simpl_existTs; subst;
     unfold is_compact; simpl; fold compactSeq;
     inversion Hvs;
     try (destruct (parse v0) as [[]|]; [ | congruence ]);
     try inversion H1; try inversion H2;
     subst; simpl_existTs; subst;
     try (rewrite <- H));
    try solve [ reflexivity
              | inversion H as [Hp0]; simpl; destruct (compact x p0);
                inversion Hp0; subst; simpl_existTs; subst;
                reflexivity ].


  admit.
  simpl.
  reflexivity.

(* STOP DELETING, the vSeq case follows *)

  simpl in Hlhs; fold parseSeq in Hlhs.
  destruct (parseSeq vs) as [[]|] eqn: Hvs; [ | congruence ].
  inversion Hlhs; subst; simpl_existTs; subst.
  unfold is_compact; simpl; fold compactSeq.
  apply (compactness_of_parseSeq vs x p0) in H.
  rewrite <- convert_compactSeq; [ reflexivity | assumption ].
  symmetry; assumption.

  destruct_value v;
    try solve [inversion Hlhs; subst; simpl_existTs; subst; reflexivity].


  (Forall
     (fun v : value =>
        forall (n : nat) (p : pattern n),
          Some (existT pattern n p) = parse v -> is_compact n p) vs) ->
  
  b : bool
  Heqv : v = vBool b
  IHv : forall (n : nat) (p : pattern n),
        Some (existT pattern n p) = parse (vBool b) -> is_compact n p
  n : nat
  p : pattern n
  Hlhs : Some (existT pattern n p) = parse (vRecord (vBool b) vs)



  simpl in Hlhs; fold parseSeq in Hlhs.
  unfold is_compact in IHp; rewrite <- IHp.
  reflexivity.
  

Theorem quotation_invariant v :
  forall ,
    Some (existT pattern n p) = parse v ->
    

Ltac flatten_conj :=
  match goal with
  | hp:(?x /\ ?y) |- _ =>
    let hp1 := fresh hp in
    let hp2 := fresh hp in
    inversion hp as [hp1 hp2]; clear hp
  end.

Lemma quotation_invariant_lit s :
  forall v level,
    value_size v = s ->
    wellFormedLit level v ->
    (forall u, matLit (S level) v u = Some true <-> u = v).
Proof.
  induction s using Wf_nat.lt_wf_ind; intros v level Hs Hwf u.

  destruct v; split; intro Hlhs; destruct u; try solve [inversion Hlhs].

  inversion Hlhs as [Hlhs']; apply internal_bool_dec_bl in Hlhs'; subst; reflexivity.
  rewrite Hlhs; simpl; rewrite internal_bool_dec_lb; reflexivity.

  inversion Hlhs as [Hlhs']; apply internal_label_dec_bl in Hlhs'; subst; reflexivity.
  rewrite Hlhs; simpl; rewrite internal_label_dec_lb; reflexivity.

  destruct v; destruct_all label; do 2 (try destruct l); inversion Hlhs; inversion Hwf.
  destruct v; destruct_all label; do 2 (try destruct l); inversion Hlhs; inversion Hwf.

  destruct v; destruct_all label; do 2 (try destruct l);
    destruct u; destruct_all label; do 2 (try destruct l0).

      try congruence;
      try (apply optand_Some_true in Hlhs'; flatten_conj).
  apply H with (m := 0) in Hlhs'0.

      inversion Hlhs'; try inversion Hwf.
  f_equal; f_equal.
  rewrite <- quotation_invariant_lit with (level := 0) (s := value_size v).
  assumption.
  reflexivity.

Lemma qSeq : forall level l,
    (forall (level : nat) (v : value),
        wellFormedLit level v -> forall u : value, matLit (S level) v u = Some true <-> u = v) ->
    (fix wellFormedList (level : nat) (ps : list value) {struct ps} : Prop :=
       match ps with
       | [] => True
       | p :: ps' => wellFormedLit level p /\ wellFormedList level ps'
       end) level l ->
    forall l0,
      ((fix matList (level : nat) (ps vs : list value) {struct ps} : option bool :=
          match ps with
          | [] => match vs with
                  | [] => Some true
                  | _ :: _ => Some false
                  end
          | p :: ps' => match vs with
                        | [] => Some false
                        | v :: vs' => optand (matLit level p v) (matList level ps' vs')
                        end
          end) (S level) l l0 = Some true) <-> l = l0.
Proof.
  intros level l Hquotation_invariant_lit Hwf; dependent induction l; destruct l0;
    split; try congruence; intro Hlhs.

  inversion_clear Hwf as [Hwfa Hwfl].
  apply optand_Some_true in Hlhs; inversion_clear Hlhs as [Hmatav Hmatll0].
  apply Hquotation_invariant_lit in Hmatav; [ | assumption ]; rewrite Hmatav in * |- *; clear Hmatav.
  f_equal.
  apply IHl; assumption.

  inversion Hlhs; subst.
  inversion_clear Hwf as [Hwfv Hwfl0].
  apply optand_Some_true; split.
  apply Hquotation_invariant_lit; try assumption; reflexivity.
  apply IHl; try assumption; reflexivity.
Qed.

Lemma matLit_true :
  forall level v,
    (forall (level : nat) (v : value),
        wellFormedLit level v -> forall u : value, matLit (S level) v u = Some true <-> u = v) ->
    wellFormedLit level v -> matLit (S level) v v = Some true.
Proof.
  intros; apply H; [ assumption | reflexivity ].
Defined.

Lemma matList_true :forall level l,
    (forall (level : nat) (v : value),
        wellFormedLit level v -> forall u : value, matLit (S level) v u = Some true <-> u = v) ->
    (fix wellFormedList (level : nat) (ps : list value) {struct ps} : Prop :=
       match ps with
       | [] => True
       | p :: ps' => wellFormedLit level p /\ wellFormedList level ps'
       end) level l ->
    (fix matList (level : nat) (ps vs : list value) {struct ps} : option bool :=
       match ps with
       | [] => match vs with
               | [] => Some true
               | _ :: _ => Some false
               end
       | p :: ps' => match vs with
                     | [] => Some false
                     | v :: vs' => optand (matLit level p v) (matList level ps' vs')
                     end
       end) (S level) l l = Some true.
Proof.
  intros; apply qSeq; auto.
Defined.

Fixpoint quotation_invariant v :
  wellFormed v -> (forall u, mat (vQuasiquote v) u = Some true <-> u = v)
with quotation_invariant_lit level v :
  wellFormedLit level v -> (forall u, matLit (S level) v u = Some true <-> u = v).
Proof.
  (* quotation_invariant *)

  destruct v; intros Hwf u; split; intro Hlhs; try solve [inversion Hwf].

  destruct u; destruct v; destruct_all label; try inversion Hwf;
    try solve [do 2 (try destruct l); simpl in Hlhs; congruence];
    (do 2 (try destruct l; try inversion Hwf);
     destruct u; do 2 (try destruct l0); destruct_all label; simpl in Hlhs; try congruence;
     (apply quotation_invariant_lit in Hlhs; [ subst; reflexivity | ];
      simpl in Hwf); assumption).

  destruct u; destruct v; destruct_all label; try inversion Hwf;
    try solve [do 2 (try destruct l); simpl in Hlhs; congruence];
    (do 2 (try destruct l; try inversion Hwf);
     destruct u; do 2 (try destruct l0); destruct_all label; simpl in Hlhs; try congruence);
    [ apply quotation_invariant_lit; [ simpl in Hwf; assumption | ];
      inversion Hlhs; reflexivity
    | reflexivity ].

  (* quotation_invariant_lit *)

  destruct v; intros Hwf u; split; intro Hlhs.

  destruct u; inversion Hlhs; apply internal_bool_dec_bl in H0; subst; auto.
  inversion Hlhs; simpl; rewrite internal_bool_dec_lb; reflexivity.

  destruct u; inversion Hlhs; apply internal_label_dec_bl in H0; subst; auto.
  inversion Hlhs; simpl; rewrite internal_label_dec_lb; reflexivity.

  destruct u;
    try solve [destruct v; destruct_all label; do 2 (try destruct l); simpl in Hlhs; congruence];
    remember v as v'; destruct v; rewrite Heqv' in Hwf, Hlhs;
      (assert (wellFormedLit level v'); [rewrite Heqv'; try solve [reflexivity | inversion Hwf; assumption] | ];
       apply quotation_invariant_lit with (u := u) in H;
       destruct_all label;
       try (apply optand_Some_true in Hlhs; inversion Hlhs as [Hlhsv Hlhsl]; clear Hlhs;
            rewrite Heqv' in H; simpl in H;
            apply H in Hlhsv; subst;
            f_equal;
            inversion_clear Hwf as [Hwfv Hwfl];
            symmetry; apply (qSeq level); try assumption)).

  admit.
  admit.


  subst; destruct v; destruct_all label; do 2 (try destruct l); try (simpl; reflexivity);
    try solve [ simpl in Hwf; repeat flatten_conj;
                repeat (simpl; rewrite matLit_true; auto);
                repeat (simpl; rewrite matList_true; auto);
                try solve [ simpl; rewrite internal_bool_dec_lb; reflexivity
                          | simpl; rewrite internal_string_dec_lb; reflexivity ]
              | replace (matLit (S level) (vRecord (vRecord v l0) []) (vRecord (vRecord v l0) []))
                with (optand (matLit (S level) (vRecord v l0) (vRecord v l0)) (Some true)); [ | reflexivity ];
                simpl in Hwf; repeat flatten_conj;
                rewrite matLit_true; auto;
                repeat (split; try assumption) ].

  destruct level; simpl in Hwf; [ | simpl; rewrite matLit_true; auto ].
  destruct v; try solve [inversion Hwf];
    destruct v; try solve [inversion Hwf];
      destruct l0; try solve [inversion Hwf];
        do 2 (try destruct l); try solve [inversion Hwf].
  apply quotation_invariant with (u := (vRecord (vSymbol lQuasiquote) [v])) in Hwf.
  simpl in Hwf.
  simpl.

  Lemma matList_S vs level :
    (Forall (fun v : value => matLit level v v = Some true -> matLit (S level) v v = Some true) vs) ->
    (fix matList (level : nat) (ps vs : list value) {struct ps} : option bool :=
       match ps with
       | [] => match vs with
               | [] => Some true
               | _ :: _ => Some false
               end
       | p :: ps' => match vs with
                     | [] => Some false
                     | v :: vs' => optand (matLit level p v) (matList level ps' vs')
                     end
       end) level vs vs = Some true ->
    (fix matList (level0 : nat) (ps vs0 : list value) {struct ps} : option bool :=
       match ps with
       | [] => match vs0 with
               | [] => Some true
               | _ :: _ => Some false
               end
       | p :: ps' => match vs0 with
                     | [] => Some false
                     | v :: vs' => optand (matLit level0 p v) (matList level0 ps' vs')
                     end
       end) (S level) vs vs = Some true.
  Proof.
    induction vs; intros; [ reflexivity | ].
    inversion H.
    apply optand_Some_true in H0; flatten_conj.
    apply optand_Some_true.
    split.
    apply H3.
    assumption.
    apply IHvs.
    assumption.
    assumption.
  Qed.

  Lemma useless_match : forall A (v : option A),
      match v with | Some v' => Some v' | None => None end = v.
  Proof.
    destruct v; reflexivity.
  Qed.

  Lemma matLit_S_SS : forall level v,
      matLit (S level) v v = Some true ->
      matLit (S (S level)) v v = Some true.
  Proof.
    induction v using value_ind'; intro Hlhs;
      [ simpl; rewrite internal_bool_dec_lb; reflexivity
      | simpl; rewrite internal_label_dec_lb; reflexivity
      |
      | apply matList_S; assumption ].
    dependent induction v.
    simpl in Hlhs |- *;
      rewrite matList_S; [ rewrite internal_bool_dec_lb; reflexivity
                         | assumption
                         | rewrite internal_bool_dec_lb in Hlhs; [ | reflexivity ]; simpl in Hlhs;
                           rewrite useless_match in Hlhs; assumption ].

    destruct l; do 2 (try destruct vs); try (simpl in * |- *; reflexivity).

    inversion H; apply H2; apply Hlhs.

    simpl in Hlhs |- *; rewrite useless_match; rewrite useless_match in Hlhs.
    apply optand_Some_true in Hlhs; flatten_conj.
    apply optand_Some_true in Hlhs1; flatten_conj.
    inversion H.
    inversion H3.
    subst.
    apply optand_Some_true; split; [ apply H2; assumption | ].
    apply optand_Some_true; split; [ apply H6; assumption | ].
    apply matList_S; assumption.

    
      rewrite matList_S; [ rewrite internal_label_dec_lb; reflexivity
                         | assumption
                         | rewrite internal_label_dec_lb in Hlhs; [ | reflexivity ]; simpl in Hlhs;
                           rewrite useless_match in Hlhs; assumption ].
  Qed.

  apply quotation_invariant_lit; [ | reflexivity ].


  (****** STOP DELETING *)

  destruct u; inversion Hlhs; clear Hlhs;
    f_equal; symmetry; apply (qSeq level); try assumption.
  inversion Hlhs; simpl; apply (qSeq level); try assumption; reflexivity.
Qed.



















Lemma qSeq : forall level l,
    (forall (level : nat) (v : value),
        wellFormedLit level v -> forall u : value, matLit level v u = Some true <-> u = v) ->
    (fix wellFormedList (level : nat) (ps : list value) {struct ps} : Prop :=
       match ps with
       | [] => True
       | p :: ps' => wellFormedLit level p /\ wellFormedList level ps'
       end) level l ->
    forall l0,
      ((fix matList (level : nat) (ps vs : list value) {struct ps} : option bool :=
          match ps with
          | [] => match vs with
                  | [] => Some true
                  | _ :: _ => Some false
                  end
          | p :: ps' => match vs with
                        | [] => Some false
                        | v :: vs' => optand (matLit level p v) (matList level ps' vs')
                        end
          end) level l l0 = Some true) <-> l = l0.
Proof.
  intros level l Hquotation_invariant_lit Hwf; dependent induction l; destruct l0;
    split; try congruence; intro Hlhs.

  inversion_clear Hwf as [Hwfa Hwfl].
  apply optand_Some_true in Hlhs; inversion_clear Hlhs as [Hmatav Hmatll0].
  apply Hquotation_invariant_lit in Hmatav; [ | assumption ]; rewrite Hmatav in * |- *; clear Hmatav.
  f_equal.
  apply IHl; assumption.

  inversion Hlhs; subst.
  inversion_clear Hwf as [Hwfv Hwfl0].
  apply optand_Some_true; split.
  apply Hquotation_invariant_lit; try assumption; reflexivity.
  apply IHl; try assumption; reflexivity.
Qed.

(* Lemma wfList_S : *)
(*   forall l level, *)
(*     (forall (v : value) (level : nat), wellFormedLit level v -> wellFormedLit (S level) v) -> *)
(*     (fix wellFormedList (level : nat) (ps : list value) {struct ps} : Prop := *)
(*        match ps with *)
(*        | [] => True *)
(*        | p :: ps' => wellFormedLit level p /\ wellFormedList level ps' *)
(*        end) level l -> *)
(*     (fix wellFormedList (level0 : nat) (ps : list value) {struct ps} : Prop := *)
(*        match ps with *)
(*        | [] => True *)
(*        | p :: ps' => wellFormedLit level0 p /\ wellFormedList level0 ps' *)
(*        end) (S level) l. *)
(* Proof. *)
(*   induction l; intros; [ reflexivity | ]. *)
(*   inversion H0; split. *)
(*   apply H in H1; assumption. *)
(*   apply IHl; assumption. *)
(* Qed. *)

Lemma wfList_S vs level :
  (Forall (fun v : value => wellFormedLit level v -> wellFormedLit (S level) v) vs) ->
  (fix wellFormedList (level : nat) (ps : list value) {struct ps} : Prop :=
     match ps with
     | [] => True
     | p :: ps' => wellFormedLit level p /\ wellFormedList level ps'
     end) level vs ->
  (fix wellFormedList (level0 : nat) (ps : list value) {struct ps} : Prop :=
     match ps with
     | [] => True
     | p :: ps' => wellFormedLit level0 p /\ wellFormedList level0 ps'
     end) (S level) vs.
Proof.
  induction vs; intros; [ reflexivity | ].
  inversion H0; split.
  inversion H.
  apply H5 in H1.
  assumption.
  apply IHvs.
  inversion H; assumption.
  assumption.
Qed.

Lemma wfLit_S v level :
  wellFormedLit level v -> wellFormedLit (S level) v.
Proof.
  induction v using value_ind'; intros; try reflexivity.

  destruct v; destruct_all label.

  inversion_clear H0 as [H1 H2].
  split; [ reflexivity | ].
  apply wfList_S; assumption.

  do 2 (try destruct vs).
  split; reflexivity.
  inversion H.
  simpl in H0.
  destruct level.
  simpl.

  Lemma wf0 v : wellFormed v -> forall level, wellFormedLit level v.
  Proof.
    induction v using value_ind'; try reflexivity; intro Hlhs.
    destruct v; try inversion Hlhs.
    destruct l; try inversion Hlhs.
    do 2 (try destruct vs); try inversion Hlhs.
    simpl in Hlhs |- *.

    induction level; [ | ].


    dependent destruction v; try reflexivity.
    dependent destruction v; try inversion Hlhs.
    split; [ reflexivity | apply wfList_S ].
    destruct_all label.
    do 2 (try destruct vs).
    split; reflexivity.
    inversion H; apply H2.
    simpl in Hlhs.

    split; [ reflexivity | ].

  
  inversion H.
  destruct v; try reflexivity.
  destruct v; try inversion H.
  destruct_all label; try inversion H.
  do 2 (try destruct l); try inversion H.
  simpl; apply wfLit_S; assumption.
  destruct l.
  split; reflexivity.
  inversion H.

  inversion H.

  simpl in H |- *; apply wfLit_S; assumption.
  simpl in H |- *; inversion_clear H as [H0 [H1 [H2 H3]]].
  split; [ reflexivity | ].
  split; [ simpl; apply wfLit_S; assumption | ].
  split; [ simpl; apply wfLit_S; assumption | ].
  apply wfList_S; assumption.

  do 2 (try destruct l).
  split; reflexivity.
  simpl in H |- *; apply wfLit_S; assumption.
  simpl in H |- *; inversion_clear H as [H0 [H1 [H2 H3]]].
  split; [ reflexivity | ].
  split; [ simpl; apply wfLit_S; assumption | ].
  split; [ simpl; apply wfLit_S; assumption | ].
  apply wfList_S; assumption.

  destruct l.
  split; reflexivity.
  simpl in H |- *; inversion_clear H as [H0 [H1 H2]].
  split; [ reflexivity | ].
  split; [ simpl; apply wfLit_S; assumption | ].
  apply wfList_S; assumption.

  inversion_clear H as [H0 H1].
  split; [ reflexivity | ].
  apply wfList_S; assumption.

  inversion_clear H as [H0 H1].
  split.
  apply wfLit_S; assumption.
  apply wfList_S; assumption.

  inversion_clear H as [H0 H1].
  split.
  apply wfLit_S; assumption.
  apply wfList_S; assumption.

  apply wfList_S; assumption.

























  destruct v; intros; try reflexivity.

  destruct v; destruct_all label.

  (* split; [ reflexivity | ]; apply wfList_S; [ apply wfLit_S | ]; *)
  (*   inversion H; assumption. *)
  inversion_clear H as [H0 H1].
  split; [ reflexivity | ].
  apply wfList_S; assumption.

  do 2 (try destruct l).
  split; reflexivity.
  destruct level.
  simpl in H |- *; apply wfLit_S.
  destruct v; try reflexivity.
  destruct v; try inversion H.
  destruct_all label; try inversion H.
  do 2 (try destruct l); try inversion H.
  simpl; apply wfLit_S; assumption.
  destruct l.
  split; reflexivity.
  inversion H.

  inversion H.

  simpl in H |- *; apply wfLit_S; assumption.
  simpl in H |- *; inversion_clear H as [H0 [H1 [H2 H3]]].
  split; [ reflexivity | ].
  split; [ simpl; apply wfLit_S; assumption | ].
  split; [ simpl; apply wfLit_S; assumption | ].
  apply wfList_S; assumption.

  do 2 (try destruct l).
  split; reflexivity.
  simpl in H |- *; apply wfLit_S; assumption.
  simpl in H |- *; inversion_clear H as [H0 [H1 [H2 H3]]].
  split; [ reflexivity | ].
  split; [ simpl; apply wfLit_S; assumption | ].
  split; [ simpl; apply wfLit_S; assumption | ].
  apply wfList_S; assumption.

  destruct l.
  split; reflexivity.
  simpl in H |- *; inversion_clear H as [H0 [H1 H2]].
  split; [ reflexivity | ].
  split; [ simpl; apply wfLit_S; assumption | ].
  apply wfList_S; assumption.

  inversion_clear H as [H0 H1].
  split; [ reflexivity | ].
  apply wfList_S; assumption.

  inversion_clear H as [H0 H1].
  split.
  apply wfLit_S; assumption.
  apply wfList_S; assumption.

  inversion_clear H as [H0 H1].
  split.
  apply wfLit_S; assumption.
  apply wfList_S; assumption.

  apply wfList_S; assumption.


Defined.

Fixpoint quotation_invariant v :
  wellFormed v -> (forall u, mat (vQuasiquote v) u = Some true <-> u = v)
with quotation_invariant_lit level v :
  wellFormedLit level v -> (forall u, matLit level v u = Some true <-> u = v).
Proof.
  (* quotation_invariant *)

  destruct v; intros Hwf u; split; intro Hlhs; try solve [inversion Hwf].

  destruct u; destruct v; destruct_all label; try inversion Hwf;
    try solve [do 2 (try destruct l); simpl in Hlhs; congruence];
    (do 2 (try destruct l; try inversion Hwf);
     destruct u; do 2 (try destruct l0); destruct_all label; simpl in Hlhs; try congruence;
     (apply quotation_invariant_lit in Hlhs; [ subst; reflexivity | ];
      simpl in Hwf)).


  destruct u; inversion_clear Hlhs; destruct v; destruct_all label; try inversion Hwf;
    do 2 (try destruct l); try inversion Hwf;
      [ apply quotation_invariant_lit; [ apply Hwf | reflexivity ] | reflexivity ].

  (* quotation_invariant_lit *)

  destruct v; intros Hwf u; split; intro Hlhs.

  destruct u; inversion Hlhs; apply internal_bool_dec_bl in H0; subst; auto.
  inversion Hlhs; simpl; rewrite internal_bool_dec_lb; reflexivity.

  destruct u; inversion Hlhs; apply internal_label_dec_bl in H0; subst; auto.
  inversion Hlhs; simpl; rewrite internal_label_dec_lb; reflexivity.

  destruct u;
    try solve [destruct v; destruct_all label; do 2 (try destruct l); simpl in Hlhs; congruence];
    remember v as v'; destruct v; rewrite Heqv' in Hwf, Hlhs;
      (assert (wellFormedLit level v'); [rewrite Heqv'; try solve [reflexivity | inversion Hwf; assumption] | ];
       apply quotation_invariant_lit with (u := u) in H;
       destruct_all label;
       try (apply optand_Some_true in Hlhs; inversion Hlhs as [Hlhsv Hlhsl]; clear Hlhs;
            rewrite Heqv' in H; simpl in H;
            apply H in Hlhsv; subst;
            f_equal;
            inversion_clear Hwf as [Hwfv Hwfl];
            symmetry; apply (qSeq level); try assumption)).

  admit.
  admit.

  subst; destruct v; destruct_all label.

  inversion Hwf.
  assert (l = l) as Hll; [ reflexivity | ];
    apply (qSeq level) in Hll; try assumption.
  simpl; rewrite Hll.
  f_equal; apply andb_true_intro; split; try destruct b; reflexivity.

  do 2 (try destruct l).
  reflexivity.
  simpl in * |- *.
  inversion Hwf.
  assert (l = l) as Hll; [ reflexivity | ];
    apply (qSeq level) in Hll; try assumption.
  simpl; rewrite Hll.
  f_equal; apply andb_true_intro; split; try destruct b; reflexivity.

  apply (qSeq level) with (l0 := l) in H0.

  assert (l = l) as Hll; [ reflexivity | ].
  apply (qSeq level) in Hll.
  admit.
  assumption.
  destruct v; destruct_all label; try solve [inversion Hwf; assumption].
  destruct l; try destruct l; simpl in Hwf.
  reflexivity.
  

  do 2 (try destruct l); try reflexivity.
  admit.
  admit.

  (************** STOP DELETING *)

  destruct u; inversion Hlhs; clear Hlhs;
    f_equal; symmetry; apply (qSeq level); try assumption.
  inversion Hlhs; simpl; apply (qSeq level); try assumption; reflexivity.
Qed.