From ba09905d1508f5ca0b8f6c03339bd9150fe5416d Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Fri, 12 Oct 2018 17:16:59 +0200 Subject: [PATCH] Prove `denv_wf_delete_full_2` and `denv_wf_delete_frac_2`. --- theories/vcgen/denv.v | 160 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 153 insertions(+), 7 deletions(-) diff --git a/theories/vcgen/denv.v b/theories/vcgen/denv.v index 788b9fb..ef1ffc4 100644 --- a/theories/vcgen/denv.v +++ b/theories/vcgen/denv.v @@ -904,6 +904,20 @@ Section denv_spec. eapply IHm; eauto. Qed. + Lemma denv_delete_frac_len i m m' q dv : + denv_delete_frac i m = Some (m', q, dv) → + length m' = length m. + Proof. + revert i m' q dv. induction m as [|dio m]; first done. + intros i m' q dv Hdel; + destruct i as [|j] eqn: Hi; + destruct dio as [[x q' dv']|] eqn: Hdio; simpl in Hdel; + [ case_option_guard; simplify_eq/=; naive_solver | naive_solver | |]; + destruct m'; simpl in Hdel; + destruct (denv_delete_frac j m) as [[[m1 q1] dv1]|] eqn:Hdel'; + simplify_eq/=; naive_solver. + Qed. + Lemma denv_delete_full_len i m m' q dv : denv_delete_full_aux i m = Some (m', q, dv) → length m' = length m. @@ -918,7 +932,16 @@ Section denv_spec. simplify_eq/=; naive_solver. Qed. - Lemma denv_delete_full_len_aux_wf E i m m' q dv : + Lemma denv_wf_len_delete_frac E i m m' q dv : + denv_wf_len E m → denv_delete_frac i m = Some (m', q, dv) → + denv_wf_len E m'. + Proof. + rewrite /denv_wf_len. + intros ? ?%denv_delete_frac_len. + bool_decide_unfold. omega. + Qed. + + Lemma denv_wf_len_delete_full_aux E i m m' q dv : denv_wf_len E m → denv_delete_full_aux i m = Some (m', q, dv) → denv_wf_len E m'. Proof. @@ -927,6 +950,17 @@ Section denv_spec. bool_decide_unfold. omega. Qed. + Lemma denv_delete_frac_idx i m m' q dv : + denv_delete_frac i m = Some (m', q, dv) → + i < length m. + Proof. + revert i m' q dv. induction m as [|dio m] =>i m' q dv/=//. + destruct i. + - destruct dio as [[]|]; naive_solver. + - destruct (denv_delete_frac i m) as [[[? ?] ?]|] eqn:Hm =>//. + simpl. naive_solver lia. + Qed. + Lemma denv_delete_full_idx i m m' q dv : denv_delete_full_aux i m = Some (m', q, dv) → i < length m. @@ -938,7 +972,7 @@ Section denv_spec. simpl. naive_solver lia. Qed. - Lemma denv_delete_full_aux_wf E i m m' q dv : + Lemma denv_wf_delete_full_aux E i m m' q dv : denv_wf E m → denv_delete_full_aux i m = Some (m', q, dv) → denv_wf E m' ∧ dval_wf E dv ∧ dloc_wf E (dLoc i 0). Proof. @@ -947,7 +981,7 @@ Section denv_spec. specialize (denv_delete_full_val_aux_wf E i m m' q dv Haux Hdel) as [Hdel1 Hdel2]. repeat split; try fast_done. - unfold denv_wf. - split_and; eauto using denv_delete_full_len_aux_wf. + split_and; eauto using denv_wf_len_delete_full_aux. - rewrite /dloc_wf. unfold denv_wf_len in Hlen. bool_decide_unfold. apply lookup_lt_is_Some. @@ -961,7 +995,7 @@ Section denv_spec. destruct (denv_delete_full_aux i m) as [[[? q0] dv0]|] eqn:Hdel; last naive_solver. intros; simplify_eq/=. - eapply denv_delete_full_aux_wf; eauto. + eapply denv_wf_delete_full_aux; eauto. Qed. Lemma denv_wf_delete_full E dv i m m': @@ -972,7 +1006,7 @@ Section denv_spec. destruct (denv_delete_full_aux i m) as [[[m0 q0] dv0]|] eqn:Hdel; last naive_solver. simpl; intros; case_option_guard; simplify_eq/=. - eapply denv_delete_full_aux_wf; eauto. + eapply denv_wf_delete_full_aux; eauto. Qed. Lemma denv_singleton_length i x q dv : @@ -1044,6 +1078,82 @@ Section denv_spec. eauto using denv_wf_len_insert, denv_wf_val_insert. Qed. + Tactic Notation "naive_solver" "using" constr(lem) := + naive_solver (eapply lem; eauto). + + Lemma denv_wf_val_delete_frac E i m m' q dv : + denv_wf_val E m → denv_delete_frac i m = Some (m', q, dv) → + denv_wf_val E m' ∧ dval_wf E dv. + Proof. + revert i m'; induction m as [|[di|] m]; + intros i m'; simpl; first naive_solver. + - destruct di as [dl df dval]. destruct i. + case_option_guard; simplify_eq/=; try naive_solver. + intros ? ?; destruct_and!. + destruct (denv_delete_frac i m) + as [[[m1 q1] dv1]|] eqn:Hdel; simplify_eq/=. + split_and!; eauto; eapply IHm; eauto. + - destruct i; first naive_solver. + intros ??. + destruct (denv_delete_frac i m) + as [[[m1 q1] dv1]|] eqn:Hdel; simplify_eq/=. + eapply IHm; eauto. + Qed. + + Lemma denv_wf_delete_frac E i m m' q dv : + denv_wf E m → denv_delete_frac i m = Some (m', q, dv) → + denv_wf E m' ∧ dval_wf E dv ∧ dloc_wf E (dLoc i 0). + Proof. + intros Hwf Hdel. + unfold denv_wf in Hwf; apply andb_True in Hwf as [Haux Hlen]. + specialize (denv_wf_val_delete_frac E i m m' q dv Haux Hdel) + as [Hdel1 Hdel2]. repeat split; try fast_done. + - unfold denv_wf. + split_and; eauto using denv_wf_len_delete_frac. + - rewrite /dloc_wf. unfold denv_wf_len in Hlen. + bool_decide_unfold. + apply lookup_lt_is_Some. + apply denv_delete_frac_idx in Hdel. lia. + Qed. + + Lemma denv_stack_wf_delete_frac_2 ms ms' q i E dv : + Forall (denv_wf E) ms → + denv_delete_frac_stack i ms = Some (ms', q, dv) → + Forall (denv_wf E) ms' ∧ dval_wf E dv. + Proof. + revert ms' q dv. induction ms as [|m ms]=>ms' q dv; first done. + rewrite !Forall_cons. intros [Hm Hms] =>/=. + destruct (denv_delete_frac i m) as [[[? ?] ?]|] eqn:Hi. + - intros; simplify_eq/=. + rewrite Forall_cons. repeat split; [|naive_solver|]; + eapply denv_wf_delete_frac; eauto. + - destruct (denv_delete_frac_stack i ms) as [[[? ?] ?]|] eqn:Hms'. + + intros; simplify_eq/=. + rewrite Forall_cons. repeat split; naive_solver. + + intros; simplify_eq/=. + Qed. + + Lemma denv_stack_wf_delete_full_2 ms ms' q i E dv : + Forall (denv_wf E) ms → + denv_delete_full_stack_aux i ms = Some (ms', q, dv) → + Forall (denv_wf E) ms' ∧ dval_wf E dv. + Proof. + revert ms' q dv. induction ms as [|m ms]=>ms' q dv; first done. + rewrite !Forall_cons. intros [Hm Hms] =>/=. + destruct (denv_delete_full_aux i m) as [[[? ?] ?]|] eqn:Hi. + - destruct (denv_delete_full_stack_aux i ms) as [[[? ?] ?]|] eqn:Hms'. + + intros; simplify_eq/=. + rewrite Forall_cons. repeat split; [|naive_solver|]; + eapply denv_wf_delete_full_aux; eauto. + + intros; simplify_eq/=. + rewrite Forall_cons. repeat split; eauto; + eapply denv_wf_delete_full_aux; eauto. + - destruct (denv_delete_full_stack_aux i ms) as [[[? ?] ?]|] eqn:Hms'. + + intros; simplify_eq/=. + rewrite Forall_cons. repeat split; naive_solver. + + intros; simplify_eq/=. + Qed. + Lemma denv_wf_delete_frac_2 ms m ms' m' i E q dv : Forall (denv_wf E) ms → denv_wf E m → @@ -1051,7 +1161,25 @@ Section denv_spec. Forall (denv_wf E) ms' ∧ denv_wf E m' ∧ dval_wf E dv. - Proof. Admitted. + Proof. + intros Hms Hm. + rewrite /denv_delete_frac_2. + destruct (denv_delete_frac_stack i ms) as [[[ms1 q1] dv1]|] eqn:Heq1. + - destruct (denv_delete_frac i m) as [[[m2 q2] dv2]|] eqn:Heq2. + + intros; simplify_eq/=. + repeat split; + naive_solver using denv_stack_wf_delete_frac_2 + || naive_solver using denv_delete_frac_aux_wf. + + intros; simplify_eq/=. + repeat split; + naive_solver using denv_stack_wf_delete_frac_2 + || naive_solver using denv_delete_frac_aux_wf. + - destruct (denv_delete_frac i m) as [[[m2 q2] dv2]|] eqn:Heq2 =>//. + intros; simplify_eq/=. + repeat split; + naive_solver using denv_stack_wf_delete_frac_2 + || naive_solver using denv_wf_delete_frac. + Qed. Lemma denv_wf_delete_full_2 ms m ms' m' i E dv : Forall (denv_wf E) ms → @@ -1060,7 +1188,25 @@ Section denv_spec. Forall (denv_wf E) ms' ∧ denv_wf E m' ∧ dval_wf E dv. - Proof. Admitted. + Proof. + intros Hms Hm. + rewrite /denv_delete_full_2. + destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] dv1]|] eqn:Heq1. + - destruct (denv_delete_full_aux i m) as [[[m2 q2] dv2]|] eqn:Heq2. + + case_option_guard; intros; simplify_eq/=. + repeat split; + naive_solver using denv_stack_wf_delete_full_2 + || naive_solver using denv_wf_delete_full_aux. + + case_option_guard; intros; simplify_eq/=. + repeat split; + naive_solver using denv_stack_wf_delete_full_2 + || naive_solver using denv_delete_full_aux_wf. + - destruct (denv_delete_full_aux i m) as [[[m2 q2] dv2]|] eqn:Heq2 =>//. + case_option_guard; intros; simplify_eq/=. + repeat split; + naive_solver using denv_stack_wf_delete_full_2 + || naive_solver using denv_wf_delete_full_aux. + Qed. Lemma denv_wf_extend E m dv l x q : denv_wf E m → dval_wf E dv → -- GitLab