Commit ba09905d by Dan Frumin

### Prove `denv_wf_delete_full_2` and `denv_wf_delete_frac_2`.

parent 613aeee6
 ... ... @@ -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 → ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!