Commit 8734dd1c authored by Robbert Krebbers's avatar Robbert Krebbers

Stacks annotated with types, variables no longer annotated.

parent bf8cda8b
......@@ -13,17 +13,15 @@ Require Export fin_maps.
[lexico], it automatically guarantees that no duplicates exist. *)
Definition assoc (K : Type) `{Lexico K, !TrichotomyT lexico,
!StrictOrder lexico} (A : Type) : Type :=
dsig (λ l : list (K * A), StronglySorted lexico (fst <$> l)).
dsig (λ l : list (K * A), StronglySorted lexico (l.*1)).
Section assoc.
Context `{Lexico K, !StrictOrder lexico,
x y : K, Decision (x = y), !TrichotomyT lexico}.
Infix "⊂" := lexico.
Notation assoc_before j l :=
(Forall (lexico j) (fst <$> l)) (only parsing).
Notation assoc_wf l :=
(StronglySorted (lexico) (fst <$> l)) (only parsing).
Notation assoc_before j l := (Forall (lexico j) (l.*1)) (only parsing).
Notation assoc_wf l := (StronglySorted (lexico) (l.*1)) (only parsing).
Lemma assoc_before_transitive {A} (l : list (K * A)) i j :
i j assoc_before j l assoc_before i l.
......
......@@ -431,6 +431,11 @@ Notation "' ( x1 , x2 , x3 , x4 , x5 , x6 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4,x5,x6) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
Notation "ps .*1" := (fmap (M:=list) fst ps)
(at level 10, format "ps .*1").
Notation "ps .*2" := (fmap (M:=list) snd ps)
(at level 10, format "ps .*2").
Class MGuard (M : Type Type) :=
mguard: P {dec : Decision P} {A}, (P M A) M A.
Arguments mguard _ _ _ !_ _ _ /.
......
......@@ -455,7 +455,7 @@ Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
Lemma map_to_list_unique {A} (m : M A) i x y :
(i,x) map_to_list m (i,y) map_to_list m x = y.
Proof. rewrite !elem_of_map_to_list. congruence. Qed.
Lemma NoDup_fst_map_to_list {A} (m : M A) : NoDup (fst <$> map_to_list m).
Lemma NoDup_fst_map_to_list {A} (m : M A) : NoDup ((map_to_list m).*1).
Proof. eauto using NoDup_fmap_fst, map_to_list_unique, NoDup_map_to_list. Qed.
Lemma elem_of_map_of_list_1_help {A} (l : list (K * A)) i x :
(i,x) l ( y, (i,y) l y = x) map_of_list l !! i = Some x.
......@@ -468,11 +468,11 @@ Proof.
* rewrite lookup_insert_ne by done; eauto.
Qed.
Lemma elem_of_map_of_list_1 {A} (l : list (K * A)) i x :
NoDup (fst <$> l) (i,x) l map_of_list l !! i = Some x.
NoDup (l.*1) (i,x) l map_of_list l !! i = Some x.
Proof.
intros ? Hx; apply elem_of_map_of_list_1_help; eauto using NoDup_fmap_fst.
intros y; revert Hx. rewrite !elem_of_list_lookup; intros [i' Hi'] [j' Hj'].
cut (i' = j'); [naive_solver|]. apply NoDup_lookup with (fst <$> l) i;
cut (i' = j'); [naive_solver|]. apply NoDup_lookup with (l.*1) i;
by rewrite ?list_lookup_fmap, ?Hi', ?Hj'.
Qed.
Lemma elem_of_map_of_list_2 {A} (l : list (K * A)) i x :
......@@ -483,16 +483,16 @@ Proof.
rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
Qed.
Lemma elem_of_map_of_list {A} (l : list (K * A)) i x :
NoDup (fst <$> l) (i,x) l map_of_list l !! i = Some x.
NoDup (l.*1) (i,x) l map_of_list l !! i = Some x.
Proof. split; auto using elem_of_map_of_list_1, elem_of_map_of_list_2. Qed.
Lemma not_elem_of_map_of_list_1 {A} (l : list (K * A)) i :
i fst <$> l map_of_list l !! i = None.
i l.*1 map_of_list l !! i = None.
Proof.
rewrite elem_of_list_fmap, eq_None_not_Some. intros Hi [x ?]; destruct Hi.
exists (i,x); simpl; auto using elem_of_map_of_list_2.
Qed.
Lemma not_elem_of_map_of_list_2 {A} (l : list (K * A)) i :
map_of_list l !! i = None i fst <$> l.
map_of_list l !! i = None i l.*1.
Proof.
induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|].
rewrite elem_of_cons. destruct (decide (i = j)); simplify_equality.
......@@ -500,17 +500,16 @@ Proof.
* by rewrite lookup_insert_ne; intuition.
Qed.
Lemma not_elem_of_map_of_list {A} (l : list (K * A)) i :
i fst <$> l map_of_list l !! i = None.
i l.*1 map_of_list l !! i = None.
Proof. red; auto using not_elem_of_map_of_list_1,not_elem_of_map_of_list_2. Qed.
Lemma map_of_list_proper {A} (l1 l2 : list (K * A)) :
NoDup (fst <$> l1) l1 l2 map_of_list l1 = map_of_list l2.
NoDup (l1.*1) l1 l2 map_of_list l1 = map_of_list l2.
Proof.
intros ? Hperm. apply map_eq. intros i. apply option_eq. intros x.
by rewrite <-!elem_of_map_of_list; rewrite <-?Hperm.
Qed.
Lemma map_of_list_inj {A} (l1 l2 : list (K * A)) :
NoDup (fst <$> l1) NoDup (fst <$> l2)
map_of_list l1 = map_of_list l2 l1 l2.
NoDup (l1.*1) NoDup (l2.*1) map_of_list l1 = map_of_list l2 l1 l2.
Proof.
intros ?? Hl1l2. apply NoDup_Permutation; auto using (NoDup_fmap_1 fst).
intros [i x]. by rewrite !elem_of_map_of_list, Hl1l2.
......@@ -522,7 +521,7 @@ Proof.
by auto using NoDup_fst_map_to_list.
Qed.
Lemma map_to_of_list {A} (l : list (K * A)) :
NoDup (fst <$> l) map_to_list (map_of_list l) l.
NoDup (l.*1) map_to_list (map_of_list l) l.
Proof. auto using map_of_list_inj, NoDup_fst_map_to_list, map_of_to_list. Qed.
Lemma map_to_list_inj {A} (m1 m2 : M A) :
map_to_list m1 map_to_list m2 m1 = m2.
......@@ -564,9 +563,9 @@ Lemma map_to_list_insert_inv {A} (m : M A) l i x :
map_to_list m (i,x) :: l m = <[i:=x]>(map_of_list l).
Proof.
intros Hperm. apply map_to_list_inj.
assert (NoDup (fst <$> (i, x) :: l)) as Hnodup.
{ rewrite <-Hperm. auto using NoDup_fst_map_to_list. }
csimpl in *. rewrite NoDup_cons in Hnodup. destruct Hnodup.
assert (i l.*1 NoDup (l.*1)) as [].
{ rewrite <-NoDup_cons. change (NoDup (((i,x)::l).*1)). rewrite <-Hperm.
auto using NoDup_fst_map_to_list. }
rewrite Hperm, map_to_list_insert, map_to_of_list;
auto using not_elem_of_map_of_list_1.
Qed.
......@@ -597,7 +596,7 @@ Qed.
Lemma map_ind {A} (P : M A Prop) :
P ( i x m, m !! i = None P m P (<[i:=x]>m)) m, P m.
Proof.
intros ? Hins. cut ( l, NoDup (fst <$> l) m, map_to_list m l P m).
intros ? Hins. cut ( l, NoDup (l.*1) m, map_to_list m l P m).
{ intros help m.
apply (help (map_to_list m)); auto using NoDup_fst_map_to_list. }
induction l as [|[i x] l IH]; intros Hnodup m Hml.
......
......@@ -2053,6 +2053,8 @@ Section Forall_Exists.
Proof. rewrite Forall_lookup. eauto. Qed.
Lemma Forall_lookup_2 l : (∀ i x, l !! i = Some x → P x) → Forall P l.
Proof. by rewrite Forall_lookup. Qed.
Lemma Forall_tail l : Forall P l → Forall P (tail l).
Proof. destruct 1; simpl; auto. Qed.
Lemma Forall_alter f l i :
Forall P l → (∀ x, l!!i = Some x → P x → P (f x)) → Forall P (alter f i l).
Proof.
......@@ -2575,6 +2577,8 @@ Section fmap.
Proof.
induction l as [|?? IH]; csimpl; by rewrite ?reverse_cons, ?fmap_app, ?IH.
Qed.
Lemma fmap_tail l : f <$> tail l = tail (f <$> l).
Proof. by destruct l. Qed.
Lemma fmap_last l : last (f <$> l) = f <$> last l.
Proof. induction l as [|? []]; simpl; auto. Qed.
Lemma fmap_replicate n x : f <$> replicate n x = replicate n (f x).
......@@ -2673,7 +2677,7 @@ Lemma list_alter_fmap_mono {A} (f : A → A) (g : A → A) l i :
Forall (λ x, f (g x) = g (f x)) l → f <$> alter g i l = alter g i (f <$> l).
Proof. auto using list_alter_fmap. Qed.
Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
( x y1 y2, (x,y1) l (x,y2) l y1 = y2) NoDup l NoDup (fst <$> l).
(∀ x y1 y2, (x,y1) ∈ l → (x,y2) ∈ l → y1 = y2) → NoDup l → NoDup (l.*1).
Proof.
intros Hunique. induction 1 as [|[x1 y1] l Hin Hnodup IH]; csimpl; constructor.
* rewrite elem_of_list_fmap.
......@@ -3040,8 +3044,7 @@ Section zip_with.
Proof. revert l. induction k; intros [|??] ??; f_equal'; auto with lia. Qed.
Lemma zip_with_zip l k : zip_with f l k = curry f <$> zip l k.
Proof. revert k. by induction l; intros [|??]; f_equal'. Qed.
Lemma zip_with_fst_snd lk :
zip_with f (fst <$> lk) (snd <$> lk) = curry f <$> lk.
Lemma zip_with_fst_snd lk : zip_with f (lk.*1) (lk.*2) = curry f <$> lk.
Proof. by induction lk as [|[]]; f_equal'. Qed.
Lemma zip_with_replicate n x y :
zip_with f (replicate n x) (replicate n y) = replicate n (f x y).
......@@ -3095,11 +3098,11 @@ Section zip.
Context {A B : Type}.
Implicit Types l : list A.
Implicit Types k : list B.
Lemma fst_zip l k : length l length k fst <$> zip l k = l.
Lemma fst_zip l k : length l ≤ length k → (zip l k).*1 = l.
Proof. by apply fmap_zip_with_l. Qed.
Lemma snd_zip l k : length k length l snd <$> zip l k = k.
Lemma snd_zip l k : length k ≤ length l → (zip l k).*2 = k.
Proof. by apply fmap_zip_with_r. Qed.
Lemma zip_fst_snd (lk : list (A * B)) : zip (fst <$> lk) (snd <$> lk) = lk.
Lemma zip_fst_snd (lk : list (A * B)) : zip (lk.*1) (lk.*2) = lk.
Proof. by induction lk as [|[]]; f_equal'. Qed.
Lemma Forall2_fst P l1 l2 k1 k2 :
length l2 = length k2 → Forall2 P l1 k1 →
......@@ -3292,6 +3295,8 @@ Ltac simplify_list_equality ::= repeat
rewrite take_app_alt in H by solve_length
| H : context [drop _ (_ ++ _)] |- _ =>
rewrite drop_app_alt in H by solve_length
| H : ?l !! ?i = _, H2 : context [(_ <$> ?l) !! ?i] |- _ =>
rewrite list_lookup_fmap, H in H2
end.
Ltac decompose_Forall_hyps :=
repeat match goal with
......
......@@ -24,7 +24,7 @@ Instance mapset_intersection: Intersection (mapset (M unit)) := λ X1 X2,
Instance mapset_difference: Difference (mapset (M unit)) := λ X1 X2,
let (m1) := X1 in let (m2) := X2 in Mapset (m1 m2).
Instance mapset_elems: Elements K (mapset (M unit)) := λ X,
let (m) := X in fst <$> map_to_list m.
let (m) := X in (map_to_list m).*1.
Lemma mapset_eq (X1 X2 : mapset (M unit)) : X1 = X2 x, x X1 x X2.
Proof.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment