Commit 5f737816 by Robbert Krebbers

### Type punning for lookup/alter on values.

parent 5644d68f
 ... @@ -1972,6 +1972,15 @@ Section Forall_Exists. ... @@ -1972,6 +1972,15 @@ Section Forall_Exists. Proof. intros H. apply Forall_proper. red; apply H. done. Qed. Proof. intros H. apply Forall_proper. red; apply H. done. Qed. Lemma Forall_not l : length l ≠ 0 → Forall (not ∘ P) l → ¬Forall P l. Lemma Forall_not l : length l ≠ 0 → Forall (not ∘ P) l → ¬Forall P l. Proof. by destruct 2; inversion 1. Qed. Proof. by destruct 2; inversion 1. Qed. Lemma Forall_and {Q} l : Forall (λ x, P x ∧ Q x) l ↔ Forall P l ∧ Forall Q l. Proof. split; [induction 1; constructor; naive_solver|]. intros [Hl Hl']; revert Hl'; induction Hl; inversion_clear 1; auto. Qed. Lemma Forall_and_l {Q} l : Forall (λ x, P x ∧ Q x) l → Forall P l. Proof. rewrite Forall_and; tauto. Qed. Lemma Forall_and_r {Q} l : Forall (λ x, P x ∧ Q x) l → Forall Q l. Proof. rewrite Forall_and; tauto. Qed. Lemma Forall_delete l i : Forall P l → Forall P (delete i l). Lemma Forall_delete l i : Forall P l → Forall P (delete i l). Proof. intros H. revert i. by induction H; intros [|i]; try constructor. Qed. Proof. intros H. revert i. by induction H; intros [|i]; try constructor. Qed. Lemma Forall_lookup l : Forall P l ↔ ∀ i x, l !! i = Some x → P x. Lemma Forall_lookup l : Forall P l ↔ ∀ i x, l !! i = Some x → P x. ... @@ -2275,26 +2284,39 @@ Section Forall2. ... @@ -2275,26 +2284,39 @@ Section Forall2. intros. rewrite !resize_spec, (Forall2_length l k) by done. intros. rewrite !resize_spec, (Forall2_length l k) by done. auto using Forall2_app, Forall2_take, Forall2_replicate. auto using Forall2_app, Forall2_take, Forall2_replicate. Qed. Qed. Lemma Forall2_resize_ge_l l k x y n m : Lemma Forall2_resize_l l k x y n m : P x y → Forall (flip P y) l → n ≤ m → P x y → Forall (flip P y) l → Forall2 P (resize n x l) k → Forall2 P (resize m x l) (resize m y k). Forall2 P (resize n x l) k → Forall2 P (resize m x l) (resize m y k). Proof. Proof. intros. assert (n = length k) as ->. intros. destruct (decide (m ≤ n)). { rewrite <-(resize_resize l m n) by done. by apply Forall2_resize. } intros. assert (n = length k); subst. { by rewrite <-(Forall2_length (resize n x l) k), resize_length. } { by rewrite <-(Forall2_length (resize n x l) k), resize_length. } rewrite (le_plus_minus (length k) m), !resize_plus, resize_all, rewrite (le_plus_minus (length k) m), !resize_plus, drop_all, resize_nil by done; auto using Forall2_app, Forall2_replicate_r, resize_all, drop_all, resize_nil by lia. auto using Forall2_app, Forall2_replicate_r, Forall_resize, Forall_drop, resize_length. Forall_resize, Forall_drop, resize_length. Qed. Qed. Lemma Forall2_resize_ge_r l k x y n m : Lemma Forall2_resize_r l k x y n m : P x y → Forall (P x) k → n ≤ m → P x y → Forall (P x) k → Forall2 P l (resize n y k) → Forall2 P (resize m x l) (resize m y k). Forall2 P l (resize n y k) → Forall2 P (resize m x l) (resize m y k). Proof. Proof. intros. assert (n = length l) as ->. intros. destruct (decide (m ≤ n)). { rewrite <-(resize_resize k m n) by done. by apply Forall2_resize. } assert (n = length l); subst. { by rewrite (Forall2_length l (resize n y k)), resize_length. } { by rewrite (Forall2_length l (resize n y k)), resize_length. } rewrite (le_plus_minus (length l) m), !resize_plus, resize_all, rewrite (le_plus_minus (length l) m), !resize_plus, drop_all, resize_nil by done; auto using Forall2_app, Forall2_replicate_l, resize_all, drop_all, resize_nil by lia. auto using Forall2_app, Forall2_replicate_l, Forall_resize, Forall_drop, resize_length. Forall_resize, Forall_drop, resize_length. Qed. Qed. Lemma Forall2_resize_r_flip l k x y n m : P x y → Forall (P x) k → length k = m → Forall2 P l (resize n y k) → Forall2 P (resize m x l) k. Proof. intros ?? <- ?. rewrite <-(resize_all k y) at 2. apply Forall2_resize_r with n; auto using Forall_true. Qed. Lemma Forall2_sublist_lookup_l l k n i l' : Lemma Forall2_sublist_lookup_l l k n i l' : Forall2 P l k → sublist_lookup n i l = Some l' → Forall2 P l k → sublist_lookup n i l = Some l' → ∃ k', sublist_lookup n i k = Some k' ∧ Forall2 P l' k'. ∃ k', sublist_lookup n i k = Some k' ∧ Forall2 P l' k'. ... @@ -3243,14 +3265,16 @@ Ltac decompose_Forall_hyps := ... @@ -3243,14 +3265,16 @@ Ltac decompose_Forall_hyps := let E := fresh in let E := fresh in assert (P x) as E by (apply (Forall_lookup_1 P _ _ _ H H1)); lazy beta in E assert (P x) as E by (apply (Forall_lookup_1 P _ _ _ H H1)); lazy beta in E | H : Forall2 ?P ?l ?k |- _ => | H : Forall2 ?P ?l ?k |- _ => lazymatch goal with match goal with | H1 : l !! ?i = Some ?x, H2 : k !! ?i = Some ?y |- _ => | H1 : l !! ?i = Some ?x, H2 : k !! ?i = Some ?y |- _ => unless (P x y) by done; let E := fresh in unless (P x y) by done; let E := fresh in assert (P x y) as E by (by apply (Forall2_lookup_lr P l k i x y)); assert (P x y) as E by (by apply (Forall2_lookup_lr P l k i x y)); lazy beta in E lazy beta in E | H1 : l !! _ = Some ?x |- _ => | H1 : l !! ?i = Some ?x |- _ => try (match goal with _ : k !! i = Some _ |- _ => fail 2 end); destruct (Forall2_lookup_l P _ _ _ _ H H1) as (?&?&?) destruct (Forall2_lookup_l P _ _ _ _ H H1) as (?&?&?) | H2 : k !! _ = Some ?y |- _ => | H2 : k !! ?i = Some ?y |- _ => try (match goal with _ : l !! i = Some _ |- _ => fail 2 end); destruct (Forall2_lookup_r P _ _ _ _ H H2) as (?&?&?) destruct (Forall2_lookup_r P _ _ _ _ H H2) as (?&?&?) end end | H : Forall3 ?P ?l ?l' ?k |- _ => | H : Forall3 ?P ?l ?l' ?k |- _ => ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!