Drastically improve quoting.v - including a much better main theorem

This commit is contained in:
Tony Garnock-Jones 2020-06-18 23:57:42 +02:00
parent 95cdd84db4
commit 3f76049f13
1 changed files with 305 additions and 50 deletions

355
quoting.v
View File

@ -1,5 +1,6 @@
Require Import Coq.Lists.List.
Require Import String.
Require Import Coq.Strings.String.
Require Import Coq.Program.Equality.
Import ListNotations.
Open Scope list_scope.
Open Scope string_scope.
@ -26,46 +27,21 @@ Inductive pat : Type :=
Definition vQuote v : value := vRecord (vSymbol lQuote) [v].
Fixpoint value_dec (x y : value) : { x = y } + { x <> y }.
repeat decide equality.
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_dec (x y : pat) : { x = y } + { x <> y }.
repeat decide equality.
Defined.
Fixpoint qp p : value :=
match p with
| pDiscard => vRecord (vSymbol lDiscard) []
| pCapture p' => vRecord (vSymbol lCapture) [qp p']
| pBool b => vBool b
| pSymbol s => vSymbol s
| pRecord (pSymbol lDiscard) [] => vRecord (vQuote (vSymbol lDiscard)) []
| pRecord (pSymbol lCapture) [p'] => vRecord (vQuote (vSymbol lCapture)) [qp p']
| pRecord (pSymbol lQuote) [p'] => vRecord (vQuote (vSymbol lQuote)) [qp p']
| pRecord l ps => vRecord (qp l) (map qp ps)
| pSeq ps => vSeq (map qp ps)
end.
Fixpoint raw_uqp v : pat :=
match v with
| vBool b => pBool b
| vSymbol s => pSymbol s
| vRecord l fs => pRecord (raw_uqp l) (map raw_uqp fs)
| vSeq vs => pSeq (map raw_uqp vs)
end.
Fixpoint uqp v : pat :=
match v with
| vRecord (vSymbol lDiscard) [] => pDiscard
| vRecord (vSymbol lCapture) [v'] => pCapture (uqp v')
| vRecord (vSymbol lQuote) [v'] => raw_uqp v'
| vBool b => pBool b
| vSymbol s => pSymbol s
| vRecord l fs => pRecord (uqp l) (map uqp fs)
| vSeq vs => pSeq (map uqp vs)
end.
Fixpoint pat_ind'
(P : pat -> Prop)
(PDiscard : P pDiscard)
@ -83,8 +59,68 @@ Proof.
apply IHl ].
Defined.
Lemma Forall_map_map_id : forall ps, Forall (fun p : pat => uqp (qp p) = p) ps ->
(map uqp (map qp ps)) = ps.
Fixpoint value_dec (x y : value) : { x = y } + { x <> y }.
repeat decide equality.
Defined.
Fixpoint pat_dec (x y : pat) : { x = y } + { x <> y }.
repeat decide equality.
Defined.
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
match p with
| 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
end.
Fixpoint raw_v_to_p v : pat :=
match v with
| vBool b => pBool b
| vSymbol s => pSymbol s
| vRecord l fs => pRecord (raw_v_to_p l) (map raw_v_to_p fs)
| vSeq vs => pSeq (map raw_v_to_p vs)
end.
Fixpoint v_to_p v : pat :=
match v with
| vRecord (vSymbol lDiscard) [] => pDiscard
| vRecord (vSymbol lCapture) [v'] => pCapture (v_to_p v')
| vRecord (vSymbol lQuote) [v'] => raw_v_to_p v'
| vBool b => pBool b
| vSymbol s => pSymbol s
| vRecord l fs => pRecord (v_to_p l) (map v_to_p fs)
| vSeq vs => pSeq (map v_to_p vs)
end.
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.
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.
Proof.
intros; rewrite map_map; induction H; [ reflexivity | ].
simpl; rewrite IHForall; rewrite H; reflexivity.
@ -92,27 +128,246 @@ Qed.
Ltac solve_map_map_id := repeat f_equal; apply Forall_map_map_id; assumption.
Theorem quoting_sensible : forall p, uqp (qp p) = p.
Theorem reflection_after_interpretation_sensible : forall p, v_to_p (p_to_v p) = p.
Proof.
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 *)
destruct l;
[ destruct ps; [ reflexivity | inversion H; simpl; rewrite H2; solve_map_map_id ]
| | | simpl; solve_map_map_id ];
try solve [ destruct ps; [ reflexivity | ];
destruct ps; [ inversion H; simpl; rewrite H2; reflexivity | ];
inversion H; simpl; rewrite H2;
inversion H3; simpl; rewrite H6;
solve_map_map_id ].
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 ].
(* label pRecord *)
destruct p; try solve_map_map_id;
destruct l0; destruct l; try solve_map_map_id;
destruct l; solve_map_map_id.
Qed.
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.