2018-12-06 21:25:51 +00:00
|
|
|
Require Import Coq.Lists.List.
|
2020-06-18 21:57:42 +00:00
|
|
|
Require Import Coq.Strings.String.
|
|
|
|
Require Import Coq.Program.Equality.
|
2018-12-06 21:25:51 +00:00
|
|
|
Import ListNotations.
|
|
|
|
Open Scope list_scope.
|
|
|
|
Open Scope string_scope.
|
|
|
|
|
|
|
|
Inductive label : Type := (* efficiency hack *)
|
|
|
|
| lDiscard : label
|
|
|
|
| lCapture : label
|
|
|
|
| lQuote: label
|
|
|
|
| lStr : string -> label.
|
|
|
|
|
|
|
|
Inductive value : Type :=
|
|
|
|
| vBool : bool -> value
|
|
|
|
| vSymbol : label -> value
|
2018-12-06 23:40:09 +00:00
|
|
|
| vRecord: value -> list value -> value
|
|
|
|
| vSeq : list value -> value.
|
2018-12-06 21:25:51 +00:00
|
|
|
|
|
|
|
Inductive pat : Type :=
|
|
|
|
| pDiscard : pat
|
|
|
|
| pCapture : pat -> pat
|
|
|
|
| pBool : bool -> pat
|
|
|
|
| pSymbol : label -> pat
|
2018-12-06 23:40:09 +00:00
|
|
|
| pRecord: pat -> list pat -> pat
|
|
|
|
| pSeq : list pat -> pat.
|
2018-12-06 21:25:51 +00:00
|
|
|
|
2018-12-06 23:40:09 +00:00
|
|
|
Definition vQuote v : value := vRecord (vSymbol lQuote) [v].
|
2018-12-06 21:25:51 +00:00
|
|
|
|
2020-06-18 21:57:42 +00:00
|
|
|
Fixpoint value_ind'
|
|
|
|
(P : value -> Prop)
|
|
|
|
(PBool : forall b, P (vBool b))
|
|
|
|
(PSymbol : forall l, P (vSymbol l))
|
|
|
|
(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.
|
|
|
|
|
|
|
|
Fixpoint pat_ind'
|
|
|
|
(P : pat -> Prop)
|
|
|
|
(PDiscard : P pDiscard)
|
|
|
|
(PCapture : forall p, P p -> P (pCapture p))
|
|
|
|
(PBool : forall b, P (pBool b))
|
|
|
|
(PSymbol : forall l, P (pSymbol l))
|
|
|
|
(PRecord : forall p ps, P p -> Forall P ps -> P (pRecord p ps))
|
|
|
|
(PSeq : forall ps, Forall P ps -> P (pSeq ps))
|
|
|
|
p
|
|
|
|
: P p.
|
|
|
|
Proof.
|
|
|
|
induction p; auto; [ apply PRecord; [ apply IHp | ] | apply PSeq ];
|
|
|
|
try solve [ induction l; [ apply Forall_nil | ];
|
|
|
|
apply Forall_cons; [ apply pat_ind'; try assumption | ];
|
|
|
|
apply IHl ].
|
|
|
|
Defined.
|
|
|
|
|
2018-12-06 23:40:09 +00:00
|
|
|
Fixpoint value_dec (x y : value) : { x = y } + { x <> y }.
|
2018-12-06 21:25:51 +00:00
|
|
|
repeat decide equality.
|
|
|
|
Defined.
|
|
|
|
|
2018-12-06 23:40:09 +00:00
|
|
|
Fixpoint pat_dec (x y : pat) : { x = y } + { x <> y }.
|
2018-12-06 21:25:51 +00:00
|
|
|
repeat decide equality.
|
|
|
|
Defined.
|
|
|
|
|
2020-06-18 21:57:42 +00:00
|
|
|
Scheme Equality for label.
|
|
|
|
|
|
|
|
Fixpoint mat p v : bool :=
|
|
|
|
let matseq := (fix matseq ps vs : bool :=
|
|
|
|
match ps, vs with
|
|
|
|
| [], [] => true
|
|
|
|
| (p :: ps'), (v :: vs') => andb (mat p v) (matseq ps' vs')
|
|
|
|
| _, _ => false
|
|
|
|
end) in
|
2018-12-06 21:25:51 +00:00
|
|
|
match p with
|
2020-06-18 21:57:42 +00:00
|
|
|
| pDiscard => true
|
|
|
|
| pCapture p' => mat p' v
|
|
|
|
| pBool b => match v with vBool b' => bool_beq b b' | _ => false end
|
|
|
|
| pSymbol s => match v with vSymbol s' => label_beq s s' | _ => false end
|
|
|
|
| pRecord p' ps => match v with vRecord v' vs => mat p' v' && matseq ps vs | _ => false end
|
|
|
|
| pSeq ps => match v with vSeq vs => matseq ps vs | _ => false end
|
2018-12-06 23:40:09 +00:00
|
|
|
end.
|
2018-12-06 21:25:51 +00:00
|
|
|
|
2020-06-18 21:57:42 +00:00
|
|
|
Fixpoint raw_v_to_p v : pat :=
|
2018-12-06 21:25:51 +00:00
|
|
|
match v with
|
|
|
|
| vBool b => pBool b
|
|
|
|
| vSymbol s => pSymbol s
|
2020-06-18 21:57:42 +00:00
|
|
|
| vRecord l fs => pRecord (raw_v_to_p l) (map raw_v_to_p fs)
|
|
|
|
| vSeq vs => pSeq (map raw_v_to_p vs)
|
2018-12-06 23:40:09 +00:00
|
|
|
end.
|
2018-12-06 21:25:51 +00:00
|
|
|
|
2020-06-18 21:57:42 +00:00
|
|
|
Fixpoint v_to_p v : pat :=
|
2018-12-06 21:25:51 +00:00
|
|
|
match v with
|
2018-12-06 23:40:09 +00:00
|
|
|
| vRecord (vSymbol lDiscard) [] => pDiscard
|
2020-06-18 21:57:42 +00:00
|
|
|
| vRecord (vSymbol lCapture) [v'] => pCapture (v_to_p v')
|
|
|
|
| vRecord (vSymbol lQuote) [v'] => raw_v_to_p v'
|
2018-12-06 21:25:51 +00:00
|
|
|
| vBool b => pBool b
|
|
|
|
| vSymbol s => pSymbol s
|
2020-06-18 21:57:42 +00:00
|
|
|
| vRecord l fs => pRecord (v_to_p l) (map v_to_p fs)
|
|
|
|
| vSeq vs => pSeq (map v_to_p vs)
|
2018-12-06 23:40:09 +00:00
|
|
|
end.
|
|
|
|
|
2020-06-18 21:57:42 +00:00
|
|
|
Fixpoint p_to_v p : value :=
|
|
|
|
match p with
|
|
|
|
| pDiscard => vRecord (vSymbol lDiscard) []
|
|
|
|
| pCapture p' => vRecord (vSymbol lCapture) [p_to_v p']
|
|
|
|
| pBool b => vBool b
|
|
|
|
| pSymbol s => vSymbol s
|
|
|
|
| pRecord (pSymbol lDiscard) [] => vRecord (vQuote (vSymbol lDiscard)) []
|
|
|
|
| pRecord (pSymbol lCapture) [p'] => vRecord (vQuote (vSymbol lCapture)) [p_to_v p']
|
|
|
|
| pRecord (pSymbol lQuote) [p'] => vRecord (vQuote (vSymbol lQuote)) [p_to_v p']
|
|
|
|
| pRecord l ps => vRecord (p_to_v l) (map p_to_v ps)
|
|
|
|
| pSeq ps => vSeq (map p_to_v ps)
|
|
|
|
end.
|
2018-12-06 23:40:09 +00:00
|
|
|
|
2020-06-18 21:57:42 +00:00
|
|
|
Lemma Forall_map_map_id :
|
|
|
|
forall A X xs (f : X -> A) (g : A -> X),
|
|
|
|
Forall (fun x : X => g (f x) = x) xs ->
|
|
|
|
(map g (map f xs)) = xs.
|
2018-12-06 23:40:09 +00:00
|
|
|
Proof.
|
|
|
|
intros; rewrite map_map; induction H; [ reflexivity | ].
|
|
|
|
simpl; rewrite IHForall; rewrite H; reflexivity.
|
2018-12-06 21:25:51 +00:00
|
|
|
Qed.
|
|
|
|
|
2018-12-06 23:40:09 +00:00
|
|
|
Ltac solve_map_map_id := repeat f_equal; apply Forall_map_map_id; assumption.
|
|
|
|
|
2020-06-18 21:57:42 +00:00
|
|
|
Theorem reflection_after_interpretation_sensible : forall p, v_to_p (p_to_v p) = p.
|
2018-12-06 21:25:51 +00:00
|
|
|
Proof.
|
2018-12-06 23:40:09 +00:00
|
|
|
induction p using pat_ind';
|
|
|
|
try solve [ reflexivity
|
|
|
|
| rewrite <- IHp at 2; reflexivity
|
|
|
|
| simpl; solve_map_map_id ].
|
|
|
|
destruct p; simpl; try rewrite <- IHp; try solve [ solve_map_map_id ].
|
|
|
|
|
|
|
|
(* label pSymbol *)
|
2020-06-18 21:57:42 +00:00
|
|
|
|
2018-12-06 23:40:09 +00:00
|
|
|
destruct l;
|
2020-06-18 21:57:42 +00:00
|
|
|
apply Forall_map_map_id in H;
|
|
|
|
destruct ps; simpl in H; inversion H; clear H; auto;
|
|
|
|
destruct ps; simpl; repeat f_equal;
|
|
|
|
try solve [ repeat rewrite H1; reflexivity
|
|
|
|
| inversion H2; repeat rewrite H0; repeat rewrite H3; reflexivity ].
|
2018-12-06 23:40:09 +00:00
|
|
|
|
|
|
|
(* label pRecord *)
|
|
|
|
destruct p; try solve_map_map_id;
|
|
|
|
destruct l0; destruct l; try solve_map_map_id;
|
|
|
|
destruct l; solve_map_map_id.
|
2018-12-06 21:25:51 +00:00
|
|
|
Qed.
|
2020-06-18 21:57:42 +00:00
|
|
|
|
|
|
|
Theorem interpretation_after_reflection_not_sensible :
|
|
|
|
exists v, p_to_v (v_to_p v) <> v.
|
|
|
|
Proof.
|
|
|
|
exists (vQuote (vRecord (vSymbol lDiscard) [])).
|
|
|
|
simpl; intro H; inversion H.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
Fixpoint escape v : value :=
|
|
|
|
match v with
|
|
|
|
| vBool b => vBool b
|
|
|
|
| vSymbol s => vSymbol s
|
|
|
|
| vRecord (vSymbol lDiscard) [] => vRecord (vQuote (vSymbol lDiscard)) []
|
|
|
|
| vRecord (vSymbol lCapture) [v'] => vRecord (vQuote (vSymbol lCapture)) [escape v']
|
|
|
|
| vRecord (vSymbol lQuote) [v'] => vRecord (vQuote (vSymbol lQuote)) [escape v']
|
|
|
|
| vRecord l vs => vRecord (escape l) (map escape vs)
|
|
|
|
| vSeq vs => vSeq (map escape vs)
|
|
|
|
end.
|
|
|
|
|
|
|
|
Fixpoint unescape v : value :=
|
|
|
|
match v with
|
|
|
|
| vBool b => vBool b
|
|
|
|
| vSymbol s => vSymbol s
|
|
|
|
| vRecord (vSymbol lQuote) [v'] => v'
|
|
|
|
| vRecord l vs => vRecord (unescape l) (map unescape vs)
|
|
|
|
| vSeq vs => vSeq (map unescape vs)
|
|
|
|
end.
|
|
|
|
|
|
|
|
Theorem unescape_after_escape_id : forall v, unescape (escape v) = v.
|
|
|
|
Proof.
|
|
|
|
induction v using value_ind'; auto.
|
|
|
|
|
|
|
|
destruct v; simpl; try rewrite <- IHv; try solve [ solve_map_map_id ].
|
|
|
|
|
|
|
|
(* vRecord with a vSymbol label *)
|
|
|
|
|
|
|
|
destruct l;
|
|
|
|
apply Forall_map_map_id in H;
|
|
|
|
destruct vs; simpl in H; inversion H; clear H; auto;
|
|
|
|
destruct vs; simpl; repeat f_equal;
|
|
|
|
try solve [ repeat rewrite H1; reflexivity
|
|
|
|
| inversion H2; repeat rewrite H0; repeat rewrite H3; reflexivity ].
|
|
|
|
|
|
|
|
(* vRecord with a vRecord label *)
|
|
|
|
|
|
|
|
destruct v; try solve_map_map_id;
|
|
|
|
destruct l0; destruct l; try solve_map_map_id;
|
|
|
|
destruct l; solve_map_map_id.
|
|
|
|
|
|
|
|
(* vSeq *)
|
|
|
|
|
|
|
|
destruct vs; inversion H; clear H;
|
|
|
|
simpl; repeat rewrite H2; repeat rewrite H3; solve_map_map_id.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
Lemma Forall_map_map_assoc_id :
|
|
|
|
forall A X Y ys (h : Y -> X) (f : X -> A) (g : A -> X),
|
|
|
|
Forall (fun y : Y => g (f (h y)) = (h y)) ys ->
|
|
|
|
map g (map f (map h ys)) = (map h ys).
|
|
|
|
Proof.
|
|
|
|
intros; rewrite map_map; induction H; [ reflexivity | ].
|
|
|
|
simpl; rewrite IHForall; rewrite H; reflexivity.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
Ltac solve_map_map_assoc_id := repeat f_equal; apply Forall_map_map_assoc_id; assumption.
|
|
|
|
|
|
|
|
Lemma escape_record_record_label :
|
|
|
|
forall l inner outer,
|
|
|
|
escape (vRecord (vRecord l inner) outer) = vRecord (escape (vRecord l inner)) (map escape outer).
|
|
|
|
Proof.
|
|
|
|
reflexivity.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
Lemma Forall_map_map_raw :
|
|
|
|
forall B A X xs (h : X -> A) (f : X -> B) (g : B -> A),
|
|
|
|
Forall (fun x : X => (g (f x)) = (h x)) xs ->
|
|
|
|
map g (map f xs) = (map h xs).
|
|
|
|
Proof.
|
|
|
|
intros; rewrite map_map; induction H; [ reflexivity | ].
|
|
|
|
simpl; rewrite IHForall; rewrite H; reflexivity.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
Lemma escaped_record_is_record :
|
|
|
|
forall v l, exists l' v', escape (vRecord v l) = vRecord v' l'.
|
|
|
|
Proof.
|
|
|
|
intros.
|
|
|
|
exists (map escape l).
|
|
|
|
remember v as x.
|
|
|
|
induction x using value_ind'; try destruct l0; try destruct l; try destruct l;
|
|
|
|
try solve [ exists v; subst; reflexivity
|
|
|
|
| exists (vQuote (vSymbol lDiscard)); reflexivity
|
|
|
|
| exists (vQuote (vSymbol lCapture)); reflexivity
|
|
|
|
| exists (vQuote (vSymbol lQuote)); reflexivity
|
|
|
|
| exists (escape (vRecord x vs)); reflexivity
|
|
|
|
| exists (escape (vSeq vs)); reflexivity ].
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
Lemma v_to_p_escaped_record_is_raw_v_to_p :
|
|
|
|
forall v, v_to_p (escape v) = (raw_v_to_p v).
|
|
|
|
Proof.
|
|
|
|
induction v using value_ind'; try reflexivity.
|
|
|
|
|
|
|
|
destruct v.
|
|
|
|
|
|
|
|
simpl; rewrite Forall_map_map_raw with (h := raw_v_to_p); auto.
|
|
|
|
|
|
|
|
destruct l; destruct vs; simpl; inversion IHv; try reflexivity;
|
|
|
|
(destruct vs; simpl; inversion H; rewrite H2; try reflexivity;
|
|
|
|
inversion H3; rewrite H6;
|
|
|
|
rewrite Forall_map_map_raw with (h := raw_v_to_p); auto).
|
|
|
|
|
|
|
|
unfold raw_v_to_p; fold raw_v_to_p;
|
|
|
|
(replace (pRecord (raw_v_to_p v) (map raw_v_to_p l)) with (raw_v_to_p (vRecord v l));
|
|
|
|
[ | reflexivity ]);
|
|
|
|
rewrite <- IHv;
|
|
|
|
rewrite escape_record_record_label;
|
|
|
|
(assert (exists (l' : list value) (v' : value), escape (vRecord v l) = vRecord v' l');
|
|
|
|
[ apply escaped_record_is_record | ]);
|
|
|
|
inversion_clear H0; inversion_clear H1;
|
|
|
|
rewrite H0; rewrite <- Forall_map_map_raw with (f := escape) (g := v_to_p); auto.
|
|
|
|
|
|
|
|
simpl; f_equal; [ apply IHv | ]; apply Forall_map_map_raw; assumption.
|
|
|
|
|
|
|
|
simpl; f_equal; apply Forall_map_map_raw; assumption.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
Lemma p_to_v_of_raw_v_to_p_is_escape :
|
|
|
|
forall v,
|
|
|
|
p_to_v (raw_v_to_p v) = escape v.
|
|
|
|
Proof.
|
|
|
|
induction v using value_ind'; try reflexivity.
|
|
|
|
|
|
|
|
dependent induction v.
|
|
|
|
(* unfold raw_v_to_p; fold raw_v_to_p; *)
|
|
|
|
(* unfold p_to_v; fold p_to_v. *)
|
|
|
|
|
|
|
|
simpl; f_equal; f_equal; apply Forall_map_map_raw; assumption.
|
|
|
|
|
|
|
|
destruct l; destruct vs; simpl; inversion IHv; try reflexivity;
|
|
|
|
(destruct vs; simpl; inversion H; rewrite H2; try reflexivity;
|
|
|
|
inversion H3; rewrite H6;
|
|
|
|
rewrite Forall_map_map_raw with (h := escape); [ | assumption ]; reflexivity).
|
|
|
|
|
|
|
|
destruct v; simpl; inversion IHv0; f_equal; f_equal;
|
|
|
|
try solve [ apply Forall_map_map_raw; assumption ].
|
|
|
|
|
|
|
|
simpl; inversion IHv;
|
|
|
|
rewrite <- Forall_map_map_raw with (f := raw_v_to_p) (g := p_to_v); [ | assumption ]; reflexivity.
|
|
|
|
|
|
|
|
inversion H; try reflexivity;
|
|
|
|
simpl; rewrite H0;
|
|
|
|
rewrite <- Forall_map_map_raw with (f := raw_v_to_p) (g := p_to_v); [ | assumption ]; reflexivity.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
Lemma interpretation_after_reflection_after_escape_sensible v : p_to_v (v_to_p (escape v)) = (escape v).
|
|
|
|
Proof.
|
|
|
|
rewrite v_to_p_escaped_record_is_raw_v_to_p.
|
|
|
|
apply p_to_v_of_raw_v_to_p_is_escape.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
Theorem unescape_interpretation_reflection_escape_sensible v : unescape (p_to_v (v_to_p (escape v))) = v.
|
|
|
|
Proof.
|
|
|
|
rewrite interpretation_after_reflection_after_escape_sensible.
|
|
|
|
apply unescape_after_escape_id.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
Fixpoint quotation_invariant v u : mat (v_to_p (escape v)) u = true <-> u = v.
|
|
|
|
Proof.
|
|
|
|
destruct v;
|
|
|
|
destruct u;
|
|
|
|
rewrite v_to_p_escaped_record_is_raw_v_to_p;
|
|
|
|
(split; intro Hlhs; [ | rewrite Hlhs ]);
|
|
|
|
try solve [ simpl in * |- *; congruence ].
|
|
|
|
|
|
|
|
apply internal_bool_dec_bl in Hlhs; congruence.
|
|
|
|
apply internal_bool_dec_lb; reflexivity.
|
|
|
|
|
|
|
|
apply internal_label_dec_bl in Hlhs; congruence.
|
|
|
|
apply internal_label_dec_lb; reflexivity.
|
|
|
|
|
|
|
|
simpl in Hlhs; symmetry in Hlhs; apply Bool.andb_true_eq in Hlhs; inversion_clear Hlhs.
|
|
|
|
symmetry in H, H0.
|
|
|
|
rewrite <- v_to_p_escaped_record_is_raw_v_to_p in H.
|
|
|
|
rewrite quotation_invariant in H.
|
|
|
|
subst u; f_equal.
|
|
|
|
dependent induction l; dependent induction l0;
|
|
|
|
try solve [ reflexivity
|
|
|
|
| simpl in H0; congruence ].
|
|
|
|
simpl in H0.
|
|
|
|
simpl in H0; symmetry in H0; apply Bool.andb_true_eq in H0; inversion_clear H0.
|
|
|
|
symmetry in H, H1.
|
|
|
|
rewrite <- v_to_p_escaped_record_is_raw_v_to_p in H.
|
|
|
|
rewrite quotation_invariant in H.
|
|
|
|
subst a0; f_equal.
|
|
|
|
apply IHl.
|
|
|
|
assumption.
|
|
|
|
|
|
|
|
simpl; apply andb_true_intro; rewrite <- v_to_p_escaped_record_is_raw_v_to_p; split.
|
|
|
|
rewrite quotation_invariant; reflexivity.
|
|
|
|
clear Hlhs; induction l; [ reflexivity | ].
|
|
|
|
simpl; apply andb_true_intro; rewrite <- v_to_p_escaped_record_is_raw_v_to_p; split.
|
|
|
|
rewrite quotation_invariant; reflexivity.
|
|
|
|
apply IHl.
|
|
|
|
|
|
|
|
dependent induction l; dependent induction l0;
|
|
|
|
try solve [ reflexivity
|
|
|
|
| simpl in Hlhs; congruence ].
|
|
|
|
simpl in Hlhs.
|
|
|
|
simpl in Hlhs; symmetry in Hlhs; apply Bool.andb_true_eq in Hlhs; inversion_clear Hlhs.
|
|
|
|
symmetry in H, H0.
|
|
|
|
rewrite <- v_to_p_escaped_record_is_raw_v_to_p in H.
|
|
|
|
rewrite quotation_invariant in H.
|
|
|
|
subst a0; f_equal.
|
|
|
|
apply IHl in H0.
|
|
|
|
congruence.
|
|
|
|
|
|
|
|
clear Hlhs; induction l; [ reflexivity | ].
|
|
|
|
simpl; apply andb_true_intro; rewrite <- v_to_p_escaped_record_is_raw_v_to_p; split.
|
|
|
|
rewrite quotation_invariant; reflexivity.
|
|
|
|
apply IHl.
|
|
|
|
Qed.
|