syndicate-lang
/
preserves
mirror of https://gitlab.com/preserves/preserves.git
1
0
Fork 1
Code Releases Activity
preserves/unquoting.v

1394 lines
46 KiB
Coq
Raw Permalink Blame History

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.
View Git Blame Copy Permalink