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

Simplify by using builtin list and a custom induction principle

This commit is contained in:
Tony Garnock-Jones 2018-12-06 23:40:09 +00:00
parent fdd7eb6e94
commit 8f20ae7a48
1 changed files with 76 additions and 114 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

190
quoting.v
View File

@ -1,8 +1,5 @@
Require Import Coq.Lists.List. Require Import Coq.Lists.List.
Require Import Coq.Program.Equality.
Require Import Omega.
Require Import String. Require Import String.
Require Import Bool.
Import ListNotations. Import ListNotations.
Open Scope list_scope. Open Scope list_scope.
Open Scope string_scope. Open Scope string_scope.
@ -16,151 +13,116 @@ Inductive label : Type := (* efficiency hack *)
Inductive value : Type := Inductive value : Type :=
| vBool : bool -> value | vBool : bool -> value
| vSymbol : label -> value | vSymbol : label -> value
| vRecord: value -> values -> value | vRecord: value -> list value -> value
| vSeq : values -> value | vSeq : list value -> value.
with values : Type :=
| vsNil : values
| vsCons : value -> values -> values.
Inductive pat : Type := Inductive pat : Type :=
| pDiscard : pat | pDiscard : pat
| pCapture : pat -> pat | pCapture : pat -> pat
| pBool : bool -> pat | pBool : bool -> pat
| pSymbol : label -> pat | pSymbol : label -> pat
| pRecord: pat -> pats -> pat | pRecord: pat -> list pat -> pat
| pSeq : pats -> pat | pSeq : list pat -> pat.
with pats : Type :=
| psNil : pats
| psCons : pat -> pats -> pats.
Definition vs1 v : values := vsCons v vsNil. Definition vQuote v : value := vRecord (vSymbol lQuote) [v].
Definition ps1 p : pats := psCons p psNil.
Definition vQuote v : value := vRecord (vSymbol lQuote) (vs1 v). Fixpoint value_dec (x y : value) : { x = y } + { x <> y }.
Lemma value_dec : forall x y : value, { x = y } + { x <> y }
with values_dec : forall xs ys : values, { xs = ys } + { xs <> ys }.
repeat decide equality.
repeat decide equality. repeat decide equality.
Defined. Defined.
Lemma pat_dec : forall x y : pat, { x = y } + { x <> y } Fixpoint pat_dec (x y : pat) : { x = y } + { x <> y }.
with pats_dec : forall xs ys : pats, { xs = ys } + { xs <> ys }.
repeat decide equality.
repeat decide equality. repeat decide equality.
Defined. Defined.
Fixpoint qp p : value := Fixpoint qp p : value :=
match p with match p with
| pDiscard => vRecord (vSymbol lDiscard) vsNil | pDiscard => vRecord (vSymbol lDiscard) []
| pCapture p' => vRecord (vSymbol lCapture) (vs1 (qp p')) | pCapture p' => vRecord (vSymbol lCapture) [qp p']
| pBool b => vBool b | pBool b => vBool b
| pSymbol s => vSymbol s | pSymbol s => vSymbol s
| pRecord (pSymbol lDiscard) psNil => vRecord (vQuote (vSymbol lDiscard)) vsNil | pRecord (pSymbol lDiscard) [] => vRecord (vQuote (vSymbol lDiscard)) []
| pRecord (pSymbol lCapture) (psCons p' psNil) => vRecord (vQuote (vSymbol lCapture)) (vs1 (qp p')) | pRecord (pSymbol lCapture) [p'] => vRecord (vQuote (vSymbol lCapture)) [qp p']
| pRecord (pSymbol lQuote) (psCons p' psNil) => vRecord (vQuote (vSymbol lQuote)) (vs1 (qp p')) | pRecord (pSymbol lQuote) [p'] => vRecord (vQuote (vSymbol lQuote)) [qp p']
| pRecord l ps => vRecord (qp l) (qps ps) | pRecord l ps => vRecord (qp l) (map qp ps)
| pSeq ps => vSeq (qps ps) | pSeq ps => vSeq (map qp ps)
end end.
with qps ps : values :=
match ps with
| psNil => vsNil
| psCons p' ps' => vsCons (qp p') (qps ps')
end.
Fixpoint raw_uqp v : pat := Fixpoint raw_uqp v : pat :=
match v with match v with
| vBool b => pBool b | vBool b => pBool b
| vSymbol s => pSymbol s | vSymbol s => pSymbol s
| vRecord l fs => pRecord (raw_uqp l) (raw_uqps fs) | vRecord l fs => pRecord (raw_uqp l) (map raw_uqp fs)
| vSeq vs => pSeq (raw_uqps vs) | vSeq vs => pSeq (map raw_uqp vs)
end end.
with raw_uqps vs : pats :=
match vs with
| vsNil => psNil
| vsCons v vs' => psCons (raw_uqp v) (raw_uqps vs')
end.
Fixpoint uqp v : pat := Fixpoint uqp v : pat :=
match v with match v with
| vRecord (vSymbol lDiscard) vsNil => pDiscard | vRecord (vSymbol lDiscard) [] => pDiscard
| vRecord (vSymbol lCapture) (vsCons v' vsNil) => pCapture (uqp v') | vRecord (vSymbol lCapture) [v'] => pCapture (uqp v')
| vRecord (vSymbol lQuote) (vsCons v' vsNil) => raw_uqp v' | vRecord (vSymbol lQuote) [v'] => raw_uqp v'
| vBool b => pBool b | vBool b => pBool b
| vSymbol s => pSymbol s | vSymbol s => pSymbol s
| vRecord l fs => pRecord (uqp l) (uqps fs) | vRecord l fs => pRecord (uqp l) (map uqp fs)
| vSeq vs => pSeq (uqps vs) | vSeq vs => pSeq (map uqp vs)
end end.
with uqps vs : pats :=
match vs with
| vsNil => psNil
| vsCons v vs' => psCons (uqp v) (uqps vs')
end.
Lemma quoting_for_record_sensible : Fixpoint pat_ind'
forall p ps, (P : pat -> Prop)
p <> pSymbol lDiscard -> (PDiscard : P pDiscard)
p <> pSymbol lCapture -> (PCapture : forall p, P p -> P (pCapture p))
p <> pSymbol lQuote -> (PBool : forall b, P (pBool b))
uqp (qp (pRecord p ps)) = pRecord (uqp (qp p)) (uqps (qps ps)). (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. Proof.
destruct p; try reflexivity. induction p; auto.
destruct l; try congruence; reflexivity.
intros; destruct p; try reflexivity. apply PRecord.
destruct l; try reflexivity; destruct p0; try reflexivity. apply IHp; try assumption.
destruct p0; try reflexivity. induction l; [ apply Forall_nil | ].
destruct p0; try reflexivity. apply Forall_cons; [ apply pat_ind'; try assumption | ].
apply IHl; apply IHp.
apply PSeq.
induction l; [ apply Forall_nil | ].
apply Forall_cons; [ apply pat_ind'; try assumption | ].
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.
Proof.
intros; rewrite map_map; induction H; [ reflexivity | ].
simpl; rewrite IHForall; rewrite H; reflexivity.
Qed. Qed.
Theorem quoting_sensible : forall p, uqp (qp p) = p Ltac solve_map_map_id := repeat f_equal; apply Forall_map_map_id; assumption.
with quoting_list_sensible : forall ps, uqps (qps ps) = ps.
Theorem quoting_sensible : forall p, uqp (qp p) = p.
Proof. Proof.
clear quoting_sensible. induction p using pat_ind';
induction p; try reflexivity. try solve [ reflexivity
remember (qp (pCapture p)) as p'; simpl in Heqp'; rewrite Heqp'; simpl; rewrite IHp; reflexivity. | rewrite <- IHp at 2; reflexivity
| simpl; solve_map_map_id ].
remember (pat_dec p (pSymbol lDiscard)) as HisDiscard; inversion HisDiscard. destruct p; simpl; try rewrite <- IHp; try solve [ solve_map_map_id ].
remember (pats_dec p0 psNil) as HisEmpty; inversion HisEmpty.
rewrite H, H0; reflexivity.
rewrite H; remember p0 as p0'; destruct p0'.
congruence.
simpl.
rewrite Heqp0'.
rewrite <- quoting_list_sensible with (ps := p0).
rewrite <- Heqp0'.
reflexivity.
remember (pat_dec p (pSymbol lCapture)) as HisCapture; inversion HisCapture; (* label pSymbol *)
[ rewrite H0; clear H0 | ]. destruct l;
remember p0 as p0'; destruct p0'; [ reflexivity | ]. [ destruct ps; [ reflexivity | inversion H; simpl; rewrite H2; solve_map_map_id ]
rewrite Heqp0'. | | | simpl; solve_map_map_id ];
destruct p0'; try solve [ destruct ps; [ reflexivity | ];
[ simpl | unfold qp]; destruct ps; [ inversion H; simpl; rewrite H2; reflexivity | ];
rewrite <- quoting_list_sensible with (ps := p0) at 2; inversion H; simpl; rewrite H2;
rewrite <- Heqp0'; inversion H3; simpl; rewrite H6;
reflexivity. solve_map_map_id ].
remember (pat_dec p (pSymbol lQuote)) as HisQuote; inversion HisQuote; (* label pRecord *)
[ rewrite H1; clear H1 | ]. destruct p; try solve_map_map_id;
remember p0 as p0'; destruct p0'; [ reflexivity | ]. destruct l0; destruct l; try solve_map_map_id;
rewrite Heqp0'. destruct l; solve_map_map_id.
destruct p0';
[ simpl | unfold qp];
rewrite <- quoting_list_sensible with (ps := p0) at 2;
rewrite <- Heqp0';
reflexivity.
rewrite quoting_for_record_sensible; try assumption.
rewrite <- IHp at 2.
rewrite <- quoting_list_sensible with (ps := p0) at 2.
reflexivity.
rewrite <- quoting_list_sensible with (ps := p) at 2; reflexivity.
clear quoting_list_sensible.
induction ps; try reflexivity.
simpl.
rewrite quoting_sensible.
f_equal.
apply IHps.
Qed. Qed.