Commit 3503a91f authored by Robbert Krebbers's avatar Robbert Krebbers

Changes in preparation of the C type system and C front-end language

Major changes:
* Make void a base type, and include a proper void base value. This is necessary
  because expressions (free, functions without return value) can yield a void.
  We now also allow void casts conforming to the C standard.
* Various missing lemmas about typing, weakening, decidability, ...
* The operations "free" and "alloc" now operate on l-values instead of r-values.
  This removes some duplication.
* Improve notations of expressions and statements. Change the presence of the
  operators conforming to the C standard.

Small changes:
* Use the classes "Typed" and "TypeCheck" for validity of indexes in memory.
  This gives more uniform notations.
* New tactic "typed_inversion" performs inversion on an inductive predicate
  of type "Typed" and folds the premises.
* Remove a horrible hack in the definitions of the classes "FMap", "MBind",
  "OMap", "Alter" that was used to let "simpl" behave better. Instead, we have
  defined a tactic "csimpl" that folds the results after performing an
  ordinary "simpl".
* Fast operation to remove duplicates from lists using hashsets.
* Make various type constructors (mainly finite map implementations) universe
  polymorphic by packing them into an inductive. This way, the whole C syntax
  can live in type, avoiding the need for (slow) universe checks.
parent af633db2
......@@ -271,7 +271,7 @@ End assoc.
(** * Finite sets *)
(** We construct finite sets using the above implementation of maps. *)
Notation assoc_set K := (mapset (assoc K)).
Notation assoc_set K := (mapset (assoc K unit)).
Instance assoc_map_dom `{Lexico K, !TrichotomyT (@lexico K _),
!StrictOrder lexico} {A} : Dom (assoc K A) (assoc_set K) := mapset_dom.
Instance assoc_map_dom_spec `{Lexico K} `{!TrichotomyT (@lexico K _)}
......
......@@ -32,6 +32,10 @@ Notation "'False'" := False : type_scope.
Notation curry := prod_curry.
Notation uncurry := prod_uncurry.
Definition curry3 {A B C D} (f : A B C D) (p : A * B * C) : D :=
let '(a,b,c) := p in f a b c.
Definition curry4 {A B C D E} (f : A B C D E) (p : A * B * C * D) : E :=
let '(a,b,c,d) := p in f a b c d.
(** Throughout this development we use [C_scope] for all general purpose
notations that do not belong to a more specific scope. *)
......@@ -376,45 +380,24 @@ Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B →
(** ** Monadic operations *)
(** We define operational type classes for the monadic operations bind, join
and fmap. These type classes are defined in a non-standard way by taking the
function as a parameter of the class. For example, we define
<<
Class FMapD := fmap: ∀ {A B}, (A → B) → M A → M B.
>>
instead of
<<
Class FMap {A B} (f : A → B) := fmap: M A → M B.
>>
This approach allows us to define [fmap] on lists such that [simpl] unfolds it
in the appropriate way, and so that it can be used for mutual recursion
(the mapped function [f] is not part of the fixpoint) as well. This is a hack,
and should be replaced by something more appropriate in future versions. *)
(** We use these type classes merely for convenient overloading of notations and
do not formalize any theory on monads (we do not even define a class with the
monad laws). *)
and fmap. We use these type classes merely for convenient overloading of
notations and do not formalize any theory on monads (we do not even define a
class with the monad laws). *)
Class MRet (M : Type Type) := mret: {A}, A M A.
Instance: Params (@mret) 3.
Arguments mret {_ _ _} _.
Class MBindD (M : Type Type) {A B} (f : A M B) := mbind: M A M B.
Notation MBind M := ( {A B} (f : A M B), MBindD M f)%type.
Class MBind (M : Type Type) := mbind : {A B}, (A M B) M A M B.
Arguments mbind {_ _ _ _} _ !_ /.
Instance: Params (@mbind) 5.
Arguments mbind {_ _ _} _ {_} !_ /.
Class MJoin (M : Type Type) := mjoin: {A}, M (M A) M A.
Instance: Params (@mjoin) 3.
Arguments mjoin {_ _ _} !_ /.
Class FMapD (M : Type Type) {A B} (f : A B) := fmap: M A M B.
Notation FMap M := ( {A B} (f : A B), FMapD M f)%type.
Class FMap (M : Type Type) := fmap : {A B}, (A B) M A M B.
Instance: Params (@fmap) 6.
Arguments fmap {_ _ _} _ {_} !_ /.
Class OMapD (M : Type Type) {A B} (f : A option B) := omap: M A M B.
Notation OMap M := ( {A B} (f : A option B), OMapD M f)%type.
Arguments fmap {_ _ _ _} _ !_ /.
Class OMap (M : Type Type) := omap: {A B}, (A option B) M A M B.
Instance: Params (@omap) 6.
Arguments omap {_ _ _} _ {_} !_ /.
Arguments omap {_ _ _ _} _ !_ /.
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : C_scope.
......@@ -430,6 +413,9 @@ Notation "'( x1 , x2 ) ← y ; z" :=
Notation "'( x1 , x2 , x3 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
Notation "'( x1 , x2 , x3 , x4 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
Class MGuard (M : Type Type) :=
mguard: P {dec : Decision P} {A}, (P M A) M A.
......@@ -468,10 +454,9 @@ Arguments delete _ _ _ !_ !_ / : simpl nomatch.
(** The function [alter f k m] should update the value at key [k] using the
function [f], which is called with the original value. *)
Class AlterD (K A M : Type) (f : A A) := alter: K M M.
Notation Alter K A M := ( (f : A A), AlterD K A M f)%type.
Class Alter (K A M : Type) := alter: (A A) K M M.
Instance: Params (@alter) 5.
Arguments alter {_ _ _} _ {_} !_ !_ / : simpl nomatch.
Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
(** The function [alter f k m] should update the value at key [k] using the
function [f], which is called with the original value at key [k] or [None]
......
......@@ -165,7 +165,7 @@ Program Instance prod_countable `{Countable A} `{Countable B} :
Next Obligation.
intros ?????? [x y]; simpl.
rewrite prod_decode_encode_fst, prod_decode_encode_snd.
simpl. by rewrite !decode_encode.
csimpl. by rewrite !decode_encode.
Qed.
Fixpoint list_encode_ (l : list positive) : positive :=
......@@ -188,7 +188,7 @@ Lemma list_decode_encode l : list_decode (list_encode l) = Some l.
Proof.
cut (list_decode_ (length l) (list_encode_ l) = Some l).
{ intros help. unfold list_decode, list_encode.
rewrite prod_decode_encode_fst, prod_decode_encode_snd; simpl.
rewrite prod_decode_encode_fst, prod_decode_encode_snd; csimpl.
by rewrite Nat2Pos.id by done; simpl. }
induction l; simpl; auto.
by rewrite prod_decode_encode_fst, prod_decode_encode_snd;
......@@ -227,5 +227,5 @@ Program Instance nat_countable : Countable nat := {|
decode p := N.to_nat <$> decode p
|}.
Next Obligation.
intros x. rewrite decode_encode; simpl. by rewrite Nat2N.id.
intros x. rewrite decode_encode; csimpl. by rewrite Nat2N.id.
Qed.
......@@ -205,9 +205,9 @@ Lemma alter_ext {A} (f g : A → A) (m : M A) i :
( x, m !! i = Some x f x = g x) alter f i m = alter g i m.
Proof. intro. apply partial_alter_ext. intros [x|] ?; f_equal'; auto. Qed.
Lemma lookup_alter {A} (f : A A) m i : alter f i m !! i = f <$> m !! i.
Proof. apply lookup_partial_alter. Qed.
Proof. unfold alter. apply lookup_partial_alter. Qed.
Lemma lookup_alter_ne {A} (f : A A) m i j : i j alter f i m !! j = m !! j.
Proof. apply lookup_partial_alter_ne. Qed.
Proof. unfold alter. apply lookup_partial_alter_ne. Qed.
Lemma alter_compose {A} (f g : A A) (m : M A) i:
alter (f g) i m = alter f i (alter g i m).
Proof.
......@@ -375,6 +375,13 @@ Proof.
* eauto using insert_delete_subset.
* by rewrite lookup_delete.
Qed.
Lemma fmap_insert {A B} (f : A B) (m : M A) i x :
f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
Proof.
apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
* by rewrite lookup_fmap, !lookup_insert.
* by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
Qed.
(** ** Properties of the singleton maps *)
Lemma lookup_singleton_Some {A} i j (x y : A) :
......@@ -430,7 +437,7 @@ Proof. eauto using NoDup_fmap_fst, map_to_list_unique, NoDup_map_to_list. 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.
Proof.
induction l as [|[j y] l IH]; simpl; [by rewrite elem_of_nil|].
induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|].
rewrite NoDup_cons, elem_of_cons, elem_of_list_fmap.
intros [Hl ?] [?|?]; simplify_equality; [by rewrite lookup_insert|].
destruct (decide (i = j)) as [->|]; [|rewrite lookup_insert_ne; auto].
......@@ -455,7 +462,7 @@ Qed.
Lemma not_elem_of_map_of_list_2 {A} (l : list (K * A)) i :
map_of_list l !! i = None i fst <$> l.
Proof.
induction l as [|[j y] l IH]; simpl; [rewrite elem_of_nil; tauto|].
induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|].
rewrite elem_of_cons. destruct (decide (i = j)); simplify_equality.
* by rewrite lookup_insert.
* by rewrite lookup_insert_ne; intuition.
......@@ -499,7 +506,7 @@ Qed.
Lemma map_to_list_insert {A} (m : M A) i x :
m !! i = None map_to_list (<[i:=x]>m) (i,x) :: map_to_list m.
Proof.
intros. apply map_of_list_inj; simpl.
intros. apply map_of_list_inj; csimpl.
* apply NoDup_fst_map_to_list.
* constructor; auto using NoDup_fst_map_to_list.
rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
......@@ -521,7 +528,7 @@ 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. }
simpl in Hnodup. rewrite NoDup_cons in Hnodup. destruct Hnodup.
csimpl in *. rewrite NoDup_cons in Hnodup. destruct Hnodup.
rewrite Hperm, map_to_list_insert, map_to_of_list;
auto using not_elem_of_map_of_list_1.
Qed.
......@@ -1374,7 +1381,7 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
| H : = {[?i,?x]} |- _ => by destruct (map_non_empty_singleton i x)
end.
Tactic Notation "simplify_map_equality'" "by" tactic3(tac) :=
repeat (progress simpl in * || simplify_map_equality by tac).
repeat (progress csimpl in * || simplify_map_equality by tac).
Tactic Notation "simplify_map_equality" :=
simplify_map_equality by eauto with simpl_map map_disjoint.
Tactic Notation "simplify_map_equality'" :=
......
......@@ -56,7 +56,7 @@ Proof.
destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
intros Hx. destruct (list_find_elem_of P xs x) as [i Hi]; auto.
rewrite Hi. destruct (list_find_Some P xs i) as (y&?&?); subst; auto.
exists y. simpl. by rewrite !Nat2Pos.id by done.
exists y. csimpl. by rewrite !Nat2Pos.id by done.
Qed.
Lemma card_0_inv P `{finA: Finite A} : card A = 0 A P.
......
......@@ -3,7 +3,7 @@
(** This file implements finite set using hash maps. Hash sets are represented
using radix-2 search trees. Each hash bucket is thus indexed using an binary
integer of type [Z], and contains an unordered list without duplicates. *)
Require Export fin_maps.
Require Export fin_maps listset.
Require Import zmap.
Record hashset {A} (hash : A Z) := Hashset {
......@@ -15,7 +15,7 @@ Arguments Hashset {_ _} _ _.
Arguments hashset_car {_ _} _.
Section hashset.
Context {A : Type} {hash : A Z} `{ x y : A, Decision (x = y)}.
Context `{ x y : A, Decision (x = y)} (hash : A Z).
Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, l,
hashset_car m !! hash x = Some l x l.
......@@ -106,7 +106,7 @@ Proof.
* unfold elements, hashset_elems. intros [m Hm]; simpl.
rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
induction Hm as [|[n l] m' [??]];
simpl; inversion_clear 1 as [|?? Hn]; [constructor|].
csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
apply NoDup_app; split_ands; eauto.
setoid_rewrite elem_of_list_bind; intros x ? ([n' l']&?&?); simpl in *.
assert (hash x = n hash x = n') as [??]; subst.
......@@ -115,6 +115,25 @@ Proof.
rewrite Forall_forall in Hm. eapply (Hm (_,_)); eauto. }
destruct Hn; rewrite elem_of_list_fmap; exists (hash x, l'); eauto.
Qed.
Definition remove_dups_fast (l : list A) : list A :=
elements (foldr (λ x, ({[ x ]} )) l : hashset hash).
Lemma elem_of_remove_dups_fast l x : x remove_dups_fast l x l.
Proof.
unfold remove_dups_fast. rewrite elem_of_elements. split.
* revert x. induction l as [|y l IH]; intros x; simpl.
{ by rewrite elem_of_empty. }
rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto.
* induction 1; esolve_elem_of.
Qed.
Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
Proof. unfold remove_dups_fast. apply NoDup_elements. Qed.
Definition listset_normalize (X : listset A) : listset A :=
let (l) := X in Listset (remove_dups_fast l).
Lemma listset_normalize_correct X : listset_normalize X X.
Proof.
destruct X as [l]. apply elem_of_equiv; intro; apply elem_of_remove_dups_fast.
Qed.
End hashset.
(** These instances are declared using [Hint Extern] to avoid too
......
......@@ -45,11 +45,11 @@ Instance list_lookup {A} : Lookup nat A (list A) :=
(** The operation [alter f i l] applies the function [f] to the [i]th element
of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
Instance list_alter {A} (f : A A) : AlterD nat A (list A) f :=
fix go i l {struct l} := let _ : AlterD _ _ _ f := @go in
Instance list_alter {A} : Alter nat A (list A) := λ f,
fix go i l {struct l} :=
match l with
| [] => []
| x :: l => match i with 0 => f x :: l | S i => x :: alter f i l end
| x :: l => match i with 0 => f x :: l | S i => x :: go i l end
end.
(** The operation [<[i:=x]> l] overwrites the element at position [i] with the
......@@ -139,12 +139,10 @@ Definition foldl {A B} (f : A → B → A) : A → list B → A :=
(** The monadic operations. *)
Instance list_ret: MRet list := λ A x, x :: @nil A.
Instance list_fmap {A B} (f : A B) : FMapD list f :=
fix go (l : list A) :=
match l with [] => [] | x :: l => f x :: @fmap _ _ _ f go l end.
Instance list_bind {A B} (f : A list B) : MBindD list f :=
fix go (l : list A) :=
match l with [] => [] | x :: l => f x ++ @mbind _ _ _ f go l end.
Instance list_fmap : FMap list := λ A B f,
fix go (l : list A) := match l with [] => [] | x :: l => f x :: go l end.
Instance list_bind : MBind list := λ A B f,
fix go (l : list A) := match l with [] => [] | x :: l => f x ++ go l end.
Instance list_join: MJoin list :=
fix go A (ls : list (list A)) : list A :=
match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end.
......@@ -192,6 +190,8 @@ Definition suffix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
Definition prefix_of {A} : relation (list A) := λ l1 l2, k, l2 = l1 ++ k.
Infix "`suffix_of`" := suffix_of (at level 70) : C_scope.
Infix "`prefix_of`" := prefix_of (at level 70) : C_scope.
Hint Extern 0 (?x `prefix_of` ?y) => reflexivity.
Hint Extern 0 (?x `suffix_of` ?y) => reflexivity.
Section prefix_suffix_ops.
Context `{ x y : A, Decision (x = y)}.
......@@ -219,6 +219,7 @@ Inductive sublist {A} : relation (list A) :=
| sublist_skip x l1 l2 : sublist l1 l2 sublist (x :: l1) (x :: l2)
| sublist_cons x l1 l2 : sublist l1 l2 sublist l1 (x :: l2).
Infix "`sublist`" := sublist (at level 70) : C_scope.
Hint Extern 0 (?x `sublist` ?y) => reflexivity.
(** A list [l2] contains a list [l1] if [l2] is obtained by removing elements
from [l1] while possiblity changing the order. *)
......@@ -229,6 +230,7 @@ Inductive contains {A} : relation (list A) :=
| contains_cons x l1 l2 : contains l1 l2 contains l1 (x :: l2)
| contains_trans l1 l2 l3 : contains l1 l2 contains l2 l3 contains l1 l3.
Infix "`contains`" := contains (at level 70) : C_scope.
Hint Extern 0 (?x `contains` ?y) => reflexivity.
Section contains_dec_help.
Context {A} {dec : x y : A, Decision (x = y)}.
......@@ -439,7 +441,7 @@ Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
Lemma list_lookup_alter_ne f l i j : i j alter f i l !! j = l !! j.
Proof.
revert i j. induction l; [done|]. intros [] [] ?; simpl; auto with congruence.
revert i j. induction l; [done|]. intros [][] ?; csimpl; auto with congruence.
Qed.
Lemma list_lookup_insert l i x : i < length l <[i:=x]>l !! i = Some x.
Proof. revert i. induction l; intros [|?] ?; f_equal'; auto with lia. Qed.
......@@ -2390,7 +2392,7 @@ Section fmap.
Proof. by induction l; f_equal'. Qed.
Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
Proof.
induction l as [|?? IH]; simpl; by rewrite ?reverse_cons, ?fmap_app, ?IH.
induction l as [|?? IH]; csimpl; by rewrite ?reverse_cons, ?fmap_app, ?IH.
Qed.
Lemma fmap_last l : last (f <$> l) = f <$> last l.
Proof. induction l as [|? []]; simpl; auto. Qed.
......@@ -2419,7 +2421,7 @@ Section fmap.
Forall (λ x, f (g x) = h (f x)) l f <$> alter g i l = alter h i (f <$> l).
Proof. intros Hl. revert i. by induction Hl; intros [|i]; f_equal'. Qed.
Lemma elem_of_list_fmap_1 l x : x l f x f <$> l.
Proof. induction 1; simpl; rewrite elem_of_cons; intuition. Qed.
Proof. induction 1; csimpl; rewrite elem_of_cons; intuition. Qed.
Lemma elem_of_list_fmap_1_alt l x y : x l y = f x y f <$> l.
Proof. intros. subst. by apply elem_of_list_fmap_1. Qed.
Lemma elem_of_list_fmap_2 l x : x f <$> l y, x = f y y l.
......@@ -2478,7 +2480,7 @@ Section fmap.
Proof. revert l2; induction l1; intros [|??]; inversion_clear 1; auto. Qed.
Lemma Forall2_fmap_2 {C D} (g : C D) (P : B D Prop) l1 l2 :
Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2 Forall2 P (f <$> l1) (g <$> l2).
Proof. induction 1; simpl; auto. Qed.
Proof. induction 1; csimpl; auto. Qed.
Lemma Forall2_fmap {C D} (g : C D) (P : B D Prop) l1 l2 :
Forall2 P (f <$> l1) (g <$> l2) Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
......@@ -2492,7 +2494,7 @@ 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).
Proof.
intros Hunique. induction 1 as [|[x1 y1] l Hin Hnodup IH]; simpl; constructor.
intros Hunique. induction 1 as [|[x1 y1] l Hin Hnodup IH]; csimpl; constructor.
* rewrite elem_of_list_fmap.
intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin.
rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto.
......@@ -2511,12 +2513,11 @@ Section bind.
Global Instance bind_sublist: Proper (sublist ==> sublist) (mbind f).
Proof.
induction 1; simpl; auto;
[done|by apply sublist_app|by apply sublist_inserts_l].
[by apply sublist_app|by apply sublist_inserts_l].
Qed.
Global Instance bind_contains: Proper (contains ==> contains) (mbind f).
Proof.
induction 1; simpl; auto.
* done.
induction 1; csimpl; auto.
* by apply contains_app.
* by rewrite !(associative_L (++)), (commutative (++) (f _)).
* by apply contains_inserts_l.
......@@ -2524,7 +2525,7 @@ Section bind.
Qed.
Global Instance bind_Permutation: Proper (() ==> ()) (mbind f).
Proof.
induction 1; simpl; auto.
induction 1; csimpl; auto.
* by f_equiv.
* by rewrite !(associative_L (++)), (commutative (++) (f _)).
* etransitivity; eauto.
......@@ -2532,30 +2533,30 @@ Section bind.
Lemma bind_cons x l : (x :: l) = f = f x ++ l = f.
Proof. done. Qed.
Lemma bind_singleton x : [x] = f = f x.
Proof. simpl. by rewrite (right_id_L _ (++)). Qed.
Proof. csimpl. by rewrite (right_id_L _ (++)). Qed.
Lemma bind_app l1 l2 : (l1 ++ l2) = f = (l1 = f) ++ (l2 = f).
Proof. by induction l1; simpl; rewrite <-?(associative_L (++)); f_equal. Qed.
Proof. by induction l1; csimpl; rewrite <-?(associative_L (++)); f_equal. Qed.
Lemma elem_of_list_bind (x : B) (l : list A) :
x l = f y, x f y y l.
Proof.
split.
* induction l as [|y l IH]; simpl; [inversion 1|].
* induction l as [|y l IH]; csimpl; [inversion 1|].
rewrite elem_of_app. intros [?|?].
+ exists y. split; [done | by left].
+ destruct IH as [z [??]]. done. exists z. split; [done | by right].
* intros [y [Hx Hy]]. induction Hy; simpl; rewrite elem_of_app; intuition.
* intros [y [Hx Hy]]. induction Hy; csimpl; rewrite elem_of_app; intuition.
Qed.
Lemma Forall_bind (P : B Prop) l :
Forall P (l = f) Forall (Forall P f) l.
Proof.
split.
* induction l; simpl; rewrite ?Forall_app; constructor; simpl; intuition.
* induction 1; simpl; rewrite ?Forall_app; auto.
* induction l; csimpl; rewrite ?Forall_app; constructor; csimpl; intuition.
* induction 1; csimpl; rewrite ?Forall_app; auto.
Qed.
Lemma Forall2_bind {C D} (g : C list D) (P : B D Prop) l1 l2 :
Forall2 (λ x1 x2, Forall2 P (f x1) (g x2)) l1 l2
Forall2 P (l1 = f) (l2 = g).
Proof. induction 1; simpl; auto using Forall2_app. Qed.
Proof. induction 1; csimpl; auto using Forall2_app. Qed.
End bind.
Section ret_join.
......@@ -2676,7 +2677,7 @@ Section permutations.
Lemma permutations_swap x y l : y :: x :: l permutations (x :: y :: l).
Proof.
simpl. apply elem_of_list_bind. exists (y :: l). split; simpl.
* destruct l; simpl; rewrite !elem_of_cons; auto.
* destruct l; csimpl; rewrite !elem_of_cons; auto.
* apply elem_of_list_bind. simpl.
eauto using interleave_cons, permutations_refl.
Qed.
......@@ -2694,12 +2695,12 @@ Section permutations.
intros Hl1 [? | [l2' [??]]]; simplify_equality'.
* rewrite !elem_of_cons, elem_of_list_fmap in Hl1.
destruct Hl1 as [? | [? | [l4 [??]]]]; subst.
+ exists (x1 :: y :: l3). simpl. rewrite !elem_of_cons. tauto.
+ exists (x1 :: y :: l3). simpl. rewrite !elem_of_cons. tauto.
+ exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto.
+ exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto.
+ exists l4. simpl. rewrite elem_of_cons. auto using interleave_cons.
* rewrite elem_of_cons, elem_of_list_fmap in Hl1.
destruct Hl1 as [? | [l1' [??]]]; subst.
+ exists (x1 :: y :: l3). simpl.
+ exists (x1 :: y :: l3). csimpl.
rewrite !elem_of_cons, !elem_of_list_fmap.
split; [| by auto]. right. right. exists (y :: l2').
rewrite elem_of_list_fmap. naive_solver.
......@@ -3006,7 +3007,7 @@ Section eval.
Lemma eval_alt t : eval E t = to_list t = from_option [] (E !!).
Proof.
induction t; simpl.
induction t; csimpl.
* done.
* by rewrite (right_id_L [] (++)).
* rewrite bind_app. by f_equal.
......
(* Copyright (c) 2012-2014, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export separation.
Require Import refinements.
Record map (A : Set) := Map { map_car : indexmap (list A) }.
Arguments Map {_} _.
Arguments map_car {_} _.
Add Printing Constructor map.
Instance: Injective (=) (=) (@Map A).
Proof. by injection 1. Qed.
Instance map_ops {A : Set} `{SeparationOps A} : SeparationOps (map A) := {
sep_empty := Map ;
sep_union m1 m2 :=
let (m1) := m1 in let (m2) := m2 in
Map (union_with (λ xs1 xs2, Some (xs1 * xs2)) m1 m2);
sep_difference m1 m2 :=
let (m1) := m1 in let (m2) := m2 in
Map (difference_with (λ xs1 xs2,
let xs' := xs1 * xs2 in guard (¬Forall ( =) xs'); Some xs'
) m1 m2);
sep_half m := let (m) := m in Map (½* <$> m);
sep_valid m :=
let (m) := m in map_Forall (λ _ xs, Forall sep_valid xs ¬Forall ( =) xs) m;
sep_disjoint m1 m2 :=
let (m1) := m1 in let (m2) := m2 in map_Forall2
(λ xs1 xs2, xs1 * xs2 ¬Forall ( =) xs1 ¬Forall ( =) xs2)
(λ xs1, Forall sep_valid xs1 ¬Forall ( =) xs1)
(λ xs2, Forall sep_valid xs2 ¬Forall ( =) xs2) m1 m2;
sep_splittable m :=
let (m) := m in
map_Forall (λ _ xs,
Forall sep_valid xs ¬Forall ( =) xs Forall sep_splittable xs) m;
sep_subseteq m1 m2 :=
let (m1) := m1 in let (m2) := m2 in map_Forall2
(λ xs1 w2, xs1 * w2 ¬Forall ( =) xs1)
(λ xs1, False)
(λ xs2, Forall sep_valid xs2 ¬Forall ( =) xs2) m1 m2;
sep_unmapped m := map_car m = ;
sep_unshared m := False
}.
Proof.
* intros []; apply _.
* intros [] []; apply _.
* intros [] []; apply _.
* solve_decision.
* intros []; apply _.
Defined.
Instance map_sep {A : Set} `{Separation A} : Separation (map A).
Proof.
split.
* destruct (sep_inhabited A) as (x&?&?).
eexists (Map {[fresh , [x]]}).
split; [|by intro]. intros o w ?; simplify_map_equality'. split.
+ by rewrite Forall_singleton.
+ by inversion_clear 1; decompose_Forall_hyps'.
* sep_unfold; intros [m1] [m2] Hm o w; specialize (Hm o); simpl in *.
intros Hx. rewrite Hx in Hm.
destruct (m2 !! o); intuition eauto using seps_disjoint_valid_l.
* sep_unfold; intros [m1] [m2] Hm o w; specialize (Hm o); simpl in *.
rewrite lookup_union_with. intros. destruct (m1 !! o), (m2 !! o);
simplify_equality'; intuition eauto using seps_union_valid, seps_positive_l.
* sep_unfold. intros [m] Hm o; specialize (Hm o); simplify_map_equality'.
destruct (m !! o); eauto.
* sep_unfold; intros [m] ?; f_equal'. by rewrite (left_id_L _).
* sep_unfold. intros [m1] [m2] Hm o; specialize (Hm o); simpl in *.
destruct (m1 !! o), (m2 !! o); intuition.
* sep_unfold; intros [m1] [m2] Hm; f_equal'. apply union_with_commutative.
intros o w1 w2 ??; specialize (Hm o); simplify_option_equality.
f_equal; intuition auto using seps_commutative.
* sep_unfold; intros [m1] [m2] [m3] Hm Hm' o; specialize (Hm o);
specialize (Hm' o); simpl in *; rewrite lookup_union_with in Hm'.
destruct (m1 !! o) eqn:?, (m2 !! o), (m3 !! o); simplify_equality';
intuition eauto using seps_disjoint_valid_l, seps_disjoint_ll.
* sep_unfold; intros [m1] [m2] [m3] Hm Hm' o; specialize (Hm o);
specialize (Hm' o); simpl in *; rewrite lookup_union_with in Hm' |- *.
destruct (m1 !! o) eqn:?, (m2 !! o), (m3 !! o); simplify_equality';
intuition eauto using seps_disjoint_valid_l, seps_disjoint_move_l,
seps_union_valid, seps_positive_l, seps_disjoint_lr.
* sep_unfold; intros [m1] [m2] [m3] Hm Hm'; f_equal'.
apply map_eq; intros o; specialize (Hm o); specialize (Hm' o); simpl in *;
rewrite !lookup_union_with; rewrite lookup_union_with in Hm'.
destruct (m1 !! o) eqn:?, (m2 !! o), (m3 !! o); simplify_equality'; eauto.
f_equal; intuition auto using seps_associative.
* sep_unfold; intros [m1] [m2] _; rewrite !(injective_iff Map); intros Hm.
apply map_eq; intros o. rewrite lookup_empty.
apply (f_equal (!! o)) in Hm; rewrite lookup_union_with, lookup_empty in Hm.
by destruct (m1 !! o), (m2 !! o); simplify_equality'.
* sep_unfold; intros [m1] [m2] [m3] Hm Hm'; rewrite !(injective_iff Map);
intros Hm''; apply map_eq; intros o.
specialize (Hm o); specialize (Hm' o);
apply (f_equal (!! o)) in Hm''; rewrite !lookup_union_with in Hm''.
destruct (m1 !! o) eqn:?, (m2 !! o), (m3 !! o); simplify_equality';
f_equal; naive_solver eauto using seps_cancel_l,
seps_cancel_empty_l, seps_cancel_empty_r.
* sep_unfold; intros [m1] [m2] Hm o; specialize (Hm o).
rewrite lookup_union_with. destruct (m1 !! o), (m2 !! o); simpl;
intuition auto using seps_union_subseteq_l, seps_reflexive.
* sep_unfold; intros [m1] [m2] Hm o; specialize (Hm o).
rewrite lookup_difference_with; destruct (m1 !! o), (m2 !! o);
simplify_option_equality;
intuition eauto using seps_disjoint_difference, seps_disjoint_valid_l.
* sep_unfold; intros [m1] [m2] Hm; f_equal; apply map_eq; intros o;
specialize (Hm o); rewrite lookup_union_with, lookup_difference_with.
destruct (m1 !! o), (m2 !! o); simplify_option_equality; f_equal;
intuition eauto using seps_union_difference, seps_difference_empty_rev.
* sep_unfold; intros [m] Hm o w; specialize (Hm o).
rewrite lookup_union_with; intros; destruct (m !! o); simplify_equality'.
intuition eauto using seps_union_valid,
seps_splittable_union, seps_positive_l.
* sep_unfold; intros [m1] [m2] Hm Hm' o w ?; specialize (Hm o);
specialize (Hm' o); simplify_option_equality.
destruct (m2 !! o); naive_solver eauto using seps_disjoint_difference,
seps_disjoint_valid_l, seps_splittable_weaken.
* sep_unfold; intros [m] Hm o; specialize (Hm o); rewrite lookup_fmap.
destruct (m !! o); try naive_solver
auto using seps_half_empty_rev, seps_disjoint_half.
* sep_unfold; intros [m] Hm; f_equal; apply map_eq; intros o;
specialize (Hm o); rewrite lookup_union_with, lookup_fmap.
destruct (m !! o); f_equal'; naive_solver auto using seps_union_half.
* sep_unfold; intros [m1] [m2] Hm Hm'; f_equal; apply map_eq; intros o;
rewrite lookup_fmap, !lookup_union_with, !lookup_fmap;
specialize (Hm o); specialize (Hm' o); rewrite lookup_union_with in Hm'.
destruct (m1 !! o), (m2 !! o); simplify_equality'; f_equal; auto.
naive_solver auto using seps_union_half_distr.
* sep_unfold; intros [m] ????; simplify_map_equality'.
* done.
* sep_unfold; intros [m1] [m2] ? Hm; simplify_equality'. apply map_empty.
intros o. specialize (Hm o); simplify_map_equality. by destruct (m1 !! o).
* sep_unfold; intros [m1] [m2] ???; simpl in *; subst.
by rewrite (left_id_L (union_with _)).
* sep_unfold; intros [m]. split; [done|].
intros [? Hm]. destruct (sep_inhabited A) as (x&?&?).
specialize (Hm (Map {[fresh (dom _ m), [x]]}));
feed specialize Hm; [|simplify_map_equality'].
intros o. destruct (m !! o) as [w|] eqn:Hw; simplify_map_equality'.
{ rewrite lookup_singleton_ne; eauto. intros <-.
eapply (is_fresh (dom indexset m)), fin_map_dom.elem_of_dom_2; eauto. }
destruct ({[_]} !! _) eqn:?; simplify_map_equality; split.
+ by rewrite Forall_singleton.
+ by inversion_clear 1; decompose_Forall_hyps'.
Qed.
......@@ -5,27 +5,28 @@ elements of the unit type. Since maps enjoy extensional equality, the
constructed finite sets do so as well. *)
Require Export fin_map_dom.
Record mapset (M : Type Type) := Mapset { mapset_car: M unit }.
Record mapset (Mu : Type) := Mapset { mapset_car: Mu }.
Arguments Mapset {_} _.
Arguments mapset_car {_} _.