Lvc.IL.Subterm
Require Import List IL DecSolve.
Set Implicit Arguments.
Inductive subTermInd : stmt → stmt → Prop :=
| subTermInd_refl s : subTermInd s s
| subTermIndExp s x e s' : subTermInd s s' → subTermInd s (stmtLet x e s')
| subTermIndIf1 e s s' t : subTermInd s s' → subTermInd s (stmtIf e s' t)
| subTermIndIf2 e s t t' : subTermInd t t' → subTermInd t (stmtIf e s t')
| subTermIndLet1 F t t' : subTermInd t t' → subTermInd t (stmtFun F t')
| subTermIndLet2 s Zs F t n : get F n Zs → subTermInd s (snd Zs) → subTermInd s (stmtFun F t).
Instance eq_dec_pair A B `{EqDec A eq} `{EqDec B eq} : EqDec (A×B) eq.
Proof.
hnf; intros [] []; unfold equiv, complement.
decide (a = a0); try dec_solve; subst.
decide (b = b0); try dec_solve; subst.
left. eauto.
Defined.
Instance eq_dec_pair_inst A B (x y: A×B) `{Computable (fst x = fst y)}
`{Computable (snd x = snd y)} : Computable (x = y).
Proof.
destruct x,y; simpl in ×.
decide (a = a0); try dec_solve; subst.
decide (b = b0); try dec_solve; subst.
left. eauto.
Defined.
Ltac decide_tac_rec P :=
first [ destruct (@decision_procedure P _)
| let X := fresh "C" in
first [ assert (X:Computable(P))
by eauto 20 using get with typeclass_instances;
destruct (@decision_procedure P X)
| let P' := eval symmetry in P in
assert (X:Computable(P'))
by eauto 20 using get with typeclass_instances;
destruct (@decision_procedure P' X)
]
].
Tactic Notation "rdecide" constr(P) := decide_tac_rec P.
Ltac eq_decide :=
match goal with
| [ |- {?f ?a ?b ?c = ?f ?a' ?b' ?c'} + {?f ?a ?b ?c ≠ ?f ?a' ?b' ?c'} ]
⇒ try rdecide (a = a'); try rdecide (b = b'); try rdecide (c = c'); subst;
try dec_solve
| [ |- {?f ?a ?b = ?f ?a' ?b'} + {?f ?a ?b ≠ ?f ?a' ?b'} ]
⇒ try rdecide (a = a'); try rdecide (b = b'); subst; try dec_solve
| [ |- {?f ?a = ?f ?a'} + {?f ?a ≠ ?f ?a'} ]
⇒ try rdecide (a = a'); subst; try dec_solve
end.
Instance list_equal_computable X
: ∀ (L L':list X), (∀ n x x', get L n x → get L' n x' → Computable (x = x'))
→ Computable (eq L L').
Proof.
intros. decide (length L = length L').
- general induction L; destruct L'; isabsurd; try dec_solve.
rdecide (a = x); try dec_solve.
edestruct IHL with (L':=L'); eauto using get; subst; try dec_solve.
- right; intro; subst. eauto.
Qed.
Instance stmt_eq_dec (s t:stmt) : Computable (s = t).
revert t; sind s; intros;
destruct s, t; try dec_solve; hnf; try eq_decide.
Qed.
Instance exists_in_set_computable X (L:list X) (P:X→Prop)
`{∀ n x, get L n x → Computable (P x)}
: Computable (∃ n x, get L n x ∧ P x).
Proof.
general induction L.
- dec_solve.
- rdecide (P a).
+ left. eauto using get.
+ edestruct IHL; dcr; eauto using get.
× left. dcr. do 2 eauto using get.
× right. intro. dcr. inv H1; eauto.
Qed.
Lemma subTermInd_dec s t : Computable (subTermInd s t).
Proof.
revert s.
sind t; intros; decide (s = t); subst; try dec_solve; destruct t; simpl in ×.
- edestruct (IH t); eauto; dec_solve.
- edestruct (IH t1); eauto; try dec_solve.
edestruct (IH t2); eauto; try dec_solve.
- dec_solve.
- dec_solve.
- rdecide (subTermInd s t); try dec_solve.
rdecide (∃ n x, get F n x ∧ subTermInd s (snd x)).
+ left. destruct e as [? [? ?]]; dcr.
eauto using subTermInd.
+ right. intro A; inv A; eauto.
Qed.
Instance subTermInd_refl' : Reflexive subTermInd.
Proof.
hnf; intros. eapply subTermInd_refl.
Qed.
Instance subTermInd_trans : Transitive subTermInd.
Proof.
hnf; intros s t u ST1 ST2.
general induction ST1; eauto;
general induction ST2; eauto using subTermInd.
Qed.
Lemma subTermInd_occurVars s t
: subTermInd s t
→ occurVars s ⊆ occurVars t.
Proof.
intros. general induction H; simpl; eauto with cset.
- eapply incl_union_left.
eapply incl_list_union. eapply map_get_1; eauto.
eauto with cset.
Qed.
Lemma subTermIndF_occurVars F t sT
: subTermInd (stmtFun F t) sT
→ list_union (of_list ⊝ fst ⊝ F) ⊆ occurVars sT.
Proof.
intros. general induction H; simpl.
- eapply list_union_incl; intros; eauto with cset.
inv_get.
rewrite <- incl_list_union; eauto using map_get_1.
cset_tac. cset_tac.
- rewrite IHsubTermInd; eauto. cset_tac.
- rewrite IHsubTermInd; eauto. cset_tac.
- rewrite IHsubTermInd; eauto. cset_tac.
- rewrite IHsubTermInd; eauto.
- rewrite IHsubTermInd; eauto.
rewrite <- incl_list_union; eauto using map_get_1.
instantiate (1:=occurVars (snd Zs)). cset_tac. cset_tac.
Qed.
Definition subTerm (s t:stmt) := sumbool_bool (subTermInd_dec s t) = true.
Require Import Coq.Logic.Eqdep_dec.
Lemma subTerm_PI s t (p1 p2:subTerm s t)
: p1 = p2.
Proof.
unfold subTerm in ×.
eapply dec_UIP.
eapply bool_eqdec.
Qed.
Lemma sTI_sT s sT
: (sumbool_bool (subTermInd_dec s sT) = true) ↔ subTermInd s sT.
Proof.
split; intros.
- destruct (subTermInd_dec s sT); eauto; isabsurd.
- destruct (subTermInd_dec s sT); eauto; isabsurd.
Qed.
Ltac sTE := unfold subTerm in *; rewrite sTI_sT in ×.
Lemma subTerm_EQ_Let sT st x e s
(EQ:st = stmtLet x e s)
(ST:subTerm st sT)
: subTerm s sT.
Proof.
subst st; sTE.
etransitivity; eauto. econstructor; reflexivity.
Qed.
Lemma subTerm_EQ_If1 sT st x s t
(EQ:st = stmtIf x s t)
(ST:subTerm st sT)
: subTerm s sT.
Proof.
subst st; sTE; etransitivity; eauto. econstructor; reflexivity.
Qed.
Lemma subTerm_EQ_If2 sT st x s t
(EQ:st = stmtIf x s t)
(ST:subTerm st sT)
: subTerm t sT.
Proof.
subst st; sTE; etransitivity; eauto. econstructor; reflexivity.
Qed.
Lemma subTerm_EQ_Fun1 sT st F t
(EQ:st = stmtFun F t)
(ST:subTerm st sT)
: subTerm t sT.
Proof.
intros. sTE. subst. etransitivity; eauto.
eapply subTermIndLet1; eauto. reflexivity.
Qed.
Lemma subTerm_EQ_Fun2 sT st F t
(EQ:st = stmtFun F t)
(ST:subTerm st sT)
: ∀ (n : nat) (s : params × stmt), get F n s → subTerm (snd s) sT.
Proof.
intros. sTE. subst. etransitivity; eauto.
eapply subTermIndLet2; eauto. reflexivity.
Qed.
Lemma subTerm_occurVars s t
: subTerm s t
→ occurVars s ⊆ occurVars t.
Proof.
intros. sTE.
eapply subTermInd_occurVars; eauto.
Qed.
Lemma subTerm_refl s
: subTerm s s.
Proof.
sTE. econstructor.
Qed.
Lemma subTermF_occurVars F t sT
: subTerm (stmtFun F t) sT
→ list_union (of_list ⊝ fst ⊝ F) ⊆ occurVars sT.
Proof.
sTE. intros.
eapply subTermIndF_occurVars; eauto.
Qed.
Lemma subTerm_EQ_If_freeVars_e
: ∀ (sT st : stmt) (e : op) (s t : stmt),
st = stmtIf e s t → subTerm st sT → Ops.freeVars e ⊆ occurVars sT.
Proof.
intros; subst.
eapply subTerm_occurVars in H0. simpl in ×.
cset_tac.
Qed.
Lemma subTerm_EQ_Let_x (sT st : stmt) (x : var) (e : exp) (s : stmt)
: st = stmtLet x e s → subTerm st sT → x ∈ occurVars sT.
Proof.
intros; subst. eapply subTerm_occurVars in H0; simpl in ×. cset_tac.
Qed.
Set Implicit Arguments.
Inductive subTermInd : stmt → stmt → Prop :=
| subTermInd_refl s : subTermInd s s
| subTermIndExp s x e s' : subTermInd s s' → subTermInd s (stmtLet x e s')
| subTermIndIf1 e s s' t : subTermInd s s' → subTermInd s (stmtIf e s' t)
| subTermIndIf2 e s t t' : subTermInd t t' → subTermInd t (stmtIf e s t')
| subTermIndLet1 F t t' : subTermInd t t' → subTermInd t (stmtFun F t')
| subTermIndLet2 s Zs F t n : get F n Zs → subTermInd s (snd Zs) → subTermInd s (stmtFun F t).
Instance eq_dec_pair A B `{EqDec A eq} `{EqDec B eq} : EqDec (A×B) eq.
Proof.
hnf; intros [] []; unfold equiv, complement.
decide (a = a0); try dec_solve; subst.
decide (b = b0); try dec_solve; subst.
left. eauto.
Defined.
Instance eq_dec_pair_inst A B (x y: A×B) `{Computable (fst x = fst y)}
`{Computable (snd x = snd y)} : Computable (x = y).
Proof.
destruct x,y; simpl in ×.
decide (a = a0); try dec_solve; subst.
decide (b = b0); try dec_solve; subst.
left. eauto.
Defined.
Ltac decide_tac_rec P :=
first [ destruct (@decision_procedure P _)
| let X := fresh "C" in
first [ assert (X:Computable(P))
by eauto 20 using get with typeclass_instances;
destruct (@decision_procedure P X)
| let P' := eval symmetry in P in
assert (X:Computable(P'))
by eauto 20 using get with typeclass_instances;
destruct (@decision_procedure P' X)
]
].
Tactic Notation "rdecide" constr(P) := decide_tac_rec P.
Ltac eq_decide :=
match goal with
| [ |- {?f ?a ?b ?c = ?f ?a' ?b' ?c'} + {?f ?a ?b ?c ≠ ?f ?a' ?b' ?c'} ]
⇒ try rdecide (a = a'); try rdecide (b = b'); try rdecide (c = c'); subst;
try dec_solve
| [ |- {?f ?a ?b = ?f ?a' ?b'} + {?f ?a ?b ≠ ?f ?a' ?b'} ]
⇒ try rdecide (a = a'); try rdecide (b = b'); subst; try dec_solve
| [ |- {?f ?a = ?f ?a'} + {?f ?a ≠ ?f ?a'} ]
⇒ try rdecide (a = a'); subst; try dec_solve
end.
Instance list_equal_computable X
: ∀ (L L':list X), (∀ n x x', get L n x → get L' n x' → Computable (x = x'))
→ Computable (eq L L').
Proof.
intros. decide (length L = length L').
- general induction L; destruct L'; isabsurd; try dec_solve.
rdecide (a = x); try dec_solve.
edestruct IHL with (L':=L'); eauto using get; subst; try dec_solve.
- right; intro; subst. eauto.
Qed.
Instance stmt_eq_dec (s t:stmt) : Computable (s = t).
revert t; sind s; intros;
destruct s, t; try dec_solve; hnf; try eq_decide.
Qed.
Instance exists_in_set_computable X (L:list X) (P:X→Prop)
`{∀ n x, get L n x → Computable (P x)}
: Computable (∃ n x, get L n x ∧ P x).
Proof.
general induction L.
- dec_solve.
- rdecide (P a).
+ left. eauto using get.
+ edestruct IHL; dcr; eauto using get.
× left. dcr. do 2 eauto using get.
× right. intro. dcr. inv H1; eauto.
Qed.
Lemma subTermInd_dec s t : Computable (subTermInd s t).
Proof.
revert s.
sind t; intros; decide (s = t); subst; try dec_solve; destruct t; simpl in ×.
- edestruct (IH t); eauto; dec_solve.
- edestruct (IH t1); eauto; try dec_solve.
edestruct (IH t2); eauto; try dec_solve.
- dec_solve.
- dec_solve.
- rdecide (subTermInd s t); try dec_solve.
rdecide (∃ n x, get F n x ∧ subTermInd s (snd x)).
+ left. destruct e as [? [? ?]]; dcr.
eauto using subTermInd.
+ right. intro A; inv A; eauto.
Qed.
Instance subTermInd_refl' : Reflexive subTermInd.
Proof.
hnf; intros. eapply subTermInd_refl.
Qed.
Instance subTermInd_trans : Transitive subTermInd.
Proof.
hnf; intros s t u ST1 ST2.
general induction ST1; eauto;
general induction ST2; eauto using subTermInd.
Qed.
Lemma subTermInd_occurVars s t
: subTermInd s t
→ occurVars s ⊆ occurVars t.
Proof.
intros. general induction H; simpl; eauto with cset.
- eapply incl_union_left.
eapply incl_list_union. eapply map_get_1; eauto.
eauto with cset.
Qed.
Lemma subTermIndF_occurVars F t sT
: subTermInd (stmtFun F t) sT
→ list_union (of_list ⊝ fst ⊝ F) ⊆ occurVars sT.
Proof.
intros. general induction H; simpl.
- eapply list_union_incl; intros; eauto with cset.
inv_get.
rewrite <- incl_list_union; eauto using map_get_1.
cset_tac. cset_tac.
- rewrite IHsubTermInd; eauto. cset_tac.
- rewrite IHsubTermInd; eauto. cset_tac.
- rewrite IHsubTermInd; eauto. cset_tac.
- rewrite IHsubTermInd; eauto.
- rewrite IHsubTermInd; eauto.
rewrite <- incl_list_union; eauto using map_get_1.
instantiate (1:=occurVars (snd Zs)). cset_tac. cset_tac.
Qed.
Definition subTerm (s t:stmt) := sumbool_bool (subTermInd_dec s t) = true.
Require Import Coq.Logic.Eqdep_dec.
Lemma subTerm_PI s t (p1 p2:subTerm s t)
: p1 = p2.
Proof.
unfold subTerm in ×.
eapply dec_UIP.
eapply bool_eqdec.
Qed.
Lemma sTI_sT s sT
: (sumbool_bool (subTermInd_dec s sT) = true) ↔ subTermInd s sT.
Proof.
split; intros.
- destruct (subTermInd_dec s sT); eauto; isabsurd.
- destruct (subTermInd_dec s sT); eauto; isabsurd.
Qed.
Ltac sTE := unfold subTerm in *; rewrite sTI_sT in ×.
Lemma subTerm_EQ_Let sT st x e s
(EQ:st = stmtLet x e s)
(ST:subTerm st sT)
: subTerm s sT.
Proof.
subst st; sTE.
etransitivity; eauto. econstructor; reflexivity.
Qed.
Lemma subTerm_EQ_If1 sT st x s t
(EQ:st = stmtIf x s t)
(ST:subTerm st sT)
: subTerm s sT.
Proof.
subst st; sTE; etransitivity; eauto. econstructor; reflexivity.
Qed.
Lemma subTerm_EQ_If2 sT st x s t
(EQ:st = stmtIf x s t)
(ST:subTerm st sT)
: subTerm t sT.
Proof.
subst st; sTE; etransitivity; eauto. econstructor; reflexivity.
Qed.
Lemma subTerm_EQ_Fun1 sT st F t
(EQ:st = stmtFun F t)
(ST:subTerm st sT)
: subTerm t sT.
Proof.
intros. sTE. subst. etransitivity; eauto.
eapply subTermIndLet1; eauto. reflexivity.
Qed.
Lemma subTerm_EQ_Fun2 sT st F t
(EQ:st = stmtFun F t)
(ST:subTerm st sT)
: ∀ (n : nat) (s : params × stmt), get F n s → subTerm (snd s) sT.
Proof.
intros. sTE. subst. etransitivity; eauto.
eapply subTermIndLet2; eauto. reflexivity.
Qed.
Lemma subTerm_occurVars s t
: subTerm s t
→ occurVars s ⊆ occurVars t.
Proof.
intros. sTE.
eapply subTermInd_occurVars; eauto.
Qed.
Lemma subTerm_refl s
: subTerm s s.
Proof.
sTE. econstructor.
Qed.
Lemma subTermF_occurVars F t sT
: subTerm (stmtFun F t) sT
→ list_union (of_list ⊝ fst ⊝ F) ⊆ occurVars sT.
Proof.
sTE. intros.
eapply subTermIndF_occurVars; eauto.
Qed.
Lemma subTerm_EQ_If_freeVars_e
: ∀ (sT st : stmt) (e : op) (s t : stmt),
st = stmtIf e s t → subTerm st sT → Ops.freeVars e ⊆ occurVars sT.
Proof.
intros; subst.
eapply subTerm_occurVars in H0. simpl in ×.
cset_tac.
Qed.
Lemma subTerm_EQ_Let_x (sT st : stmt) (x : var) (e : exp) (s : stmt)
: st = stmtLet x e s → subTerm st sT → x ∈ occurVars sT.
Proof.
intros; subst. eapply subTerm_occurVars in H0; simpl in ×. cset_tac.
Qed.