Commit b2109c25 authored by Robbert Krebbers's avatar Robbert Krebbers

Support function pointers and use a state monad in the frontend.

Important changes in the core semantics:
* Types extended with function types. Since function types are a special kind
  of pointer types, types now have an additional mutual part called "ptr_type".
* Pointers extended with function pointers. Theses are just names that refer
  to an actual function in the function environment.
* Typing environments extended to assign argument and return types to function
  names. Before we used a separate environment for these, but since the
  argument and return types are already needed to type function pointers, this
  environment would appear in pretty much every typing judgment.

As a side-effect, the frontend has been rewritten entirely. The important
changes are:

* Type checking of expressions is more involved: there is a special kind of
  expression type corresponding to a function designator.
* To handle things like block scoped extern function, more state-fullness was
  needed. To prepare for future extensions, the entire frontend now uses a
  state monad.
parent 8b7ea9be
...@@ -844,6 +844,8 @@ Instance idem_propholds {A} (R : relation A) f : ...@@ -844,6 +844,8 @@ Instance idem_propholds {A} (R : relation A) f :
Idempotent R f x, PropHolds (R (f x x) x). Idempotent R f x, PropHolds (R (f x x) x).
Proof. red. trivial. Qed. Proof. red. trivial. Qed.
Instance: @PreOrder A (=).
Proof. split; repeat intro; congruence. Qed.
Lemma injective_iff {A B} {R : relation A} {S : relation B} (f : A B) Lemma injective_iff {A B} {R : relation A} {S : relation B} (f : A B)
`{!Injective R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y) R x y. `{!Injective R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y) R x y.
Proof. firstorder. Qed. Proof. firstorder. Qed.
......
...@@ -254,7 +254,7 @@ Section collection. ...@@ -254,7 +254,7 @@ Section collection.
Proof. esolve_elem_of. Qed. Proof. esolve_elem_of. Qed.
Lemma difference_twice X Y : (X Y) Y X Y. Lemma difference_twice X Y : (X Y) Y X Y.
Proof. esolve_elem_of. Qed. Proof. esolve_elem_of. Qed.
Lemma empty_difference X Y : X Y X Y . Lemma subseteq_empty_difference X Y : X Y X Y .
Proof. esolve_elem_of. Qed. Proof. esolve_elem_of. Qed.
Lemma difference_diag X : X X . Lemma difference_diag X : X X .
Proof. esolve_elem_of. Qed. Proof. esolve_elem_of. Qed.
...@@ -269,8 +269,8 @@ Section collection. ...@@ -269,8 +269,8 @@ Section collection.
Proof. unfold_leibniz. apply intersection_singletons. Qed. Proof. unfold_leibniz. apply intersection_singletons. Qed.
Lemma difference_twice_L X Y : (X Y) Y = X Y. Lemma difference_twice_L X Y : (X Y) Y = X Y.
Proof. unfold_leibniz. apply difference_twice. Qed. Proof. unfold_leibniz. apply difference_twice. Qed.
Lemma empty_difference_L X Y : X Y X Y = . Lemma subseteq_empty_difference_L X Y : X Y X Y = .
Proof. unfold_leibniz. apply empty_difference. Qed. Proof. unfold_leibniz. apply subseteq_empty_difference. Qed.
Lemma difference_diag_L X : X X = . Lemma difference_diag_L X : X X = .
Proof. unfold_leibniz. apply difference_diag. Qed. Proof. unfold_leibniz. apply difference_diag. Qed.
Lemma difference_union_distr_l_L X Y Z : (X Y) Z = X Z Y Z. Lemma difference_union_distr_l_L X Y Z : (X Y) Z = X Z Y Z.
...@@ -296,12 +296,15 @@ Section collection. ...@@ -296,12 +296,15 @@ Section collection.
intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x. intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x.
destruct (decide (x X)); esolve_elem_of. destruct (decide (x X)); esolve_elem_of.
Qed. Qed.
Lemma empty_difference_subseteq X Y : X Y X Y.
Proof. intros ? x ?; apply dec_stable; esolve_elem_of. Qed.
Context `{!LeibnizEquiv C}. Context `{!LeibnizEquiv C}.
Lemma union_difference_L X Y : X Y Y = X Y X. Lemma union_difference_L X Y : X Y Y = X Y X.
Proof. unfold_leibniz. apply union_difference. Qed. Proof. unfold_leibniz. apply union_difference. Qed.
Lemma non_empty_difference_L X Y : X Y Y X . Lemma non_empty_difference_L X Y : X Y Y X .
Proof. unfold_leibniz. apply non_empty_difference. Qed. Proof. unfold_leibniz. apply non_empty_difference. Qed.
Lemma empty_difference_subseteq_L X Y : X Y = X Y.
Proof. unfold_leibniz. apply empty_difference_subseteq. Qed.
End dec. End dec.
End collection. End collection.
...@@ -432,16 +435,14 @@ Section fresh. ...@@ -432,16 +435,14 @@ Section fresh.
Definition fresh_sig (X : C) : { x : A | x X } := Definition fresh_sig (X : C) : { x : A | x X } :=
exist ( X) (fresh X) (is_fresh X). exist ( X) (fresh X) (is_fresh X).
Global Instance fresh_proper: Proper (() ==> (=)) fresh.
Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
Fixpoint fresh_list (n : nat) (X : C) : list A := Fixpoint fresh_list (n : nat) (X : C) : list A :=
match n with match n with
| 0 => [] | 0 => []
| S n => let x := fresh X in x :: fresh_list n ({[ x ]} X) | S n => let x := fresh X in x :: fresh_list n ({[ x ]} X)
end. end.
Global Instance fresh_proper: Proper (() ==> (=)) fresh.
Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
Global Instance fresh_list_proper: Proper ((=) ==> () ==> (=)) fresh_list. Global Instance fresh_list_proper: Proper ((=) ==> () ==> (=)) fresh_list.
Proof. Proof.
intros ? n ->. induction n as [|n IH]; intros ?? E; f_equal'; [by rewrite E|]. intros ? n ->. induction n as [|n IH]; intros ?? E; f_equal'; [by rewrite E|].
......
...@@ -2,91 +2,134 @@ ...@@ -2,91 +2,134 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
Require Export list. Require Export list.
Instance error_ret {E} : MRet (sum E) := λ A, inr. Definition error (S E A : Type) : Type := S E + (A * S).
Instance error_bind {E} : MBind (sum E) := λ A B f x,
match x with inr a => f a | inl e => inl e end.
Instance error_fmap {E} : FMap (sum E) := λ A B f x,
match x with inr a => inr (f a) | inl e => inl e end.
Definition error_guard {E} P {dec : Decision P} {A} Definition error_eval {S E A} (x : error S E A) (s : S) : E + A :=
(e : E) (f : P E + A) : E + A := match x s with inl e => inl e | inr (a,_) => inr a end.
match decide P with left H => f H | right _ => inl e end.
Instance error_ret {S E} : MRet (error S E) := λ A x s, inr (x,s).
Instance error_bind {S E} : MBind (error S E) := λ A B f x s,
match x s with
| inr (a,s') => f a s'
| inl e => inl e
end.
Instance error_fmap {S E} : FMap (error S E) := λ A B f x s,
match x s with
| inr (a,s') => inr (f a,s')
| inl e => inl e
end.
Definition fail {S E A} (e : E) : error S E A := λ s, inl e.
Definition modify {S E} (f : S S) : error S E () := λ s, inr ((), f s).
Definition gets {S E A} (f : S A) : error S E A := λ s, inr (f s, s).
Definition error_guard {E} P {dec : Decision P} {S A}
(e : E) (f : P error S E A) : error S E A :=
match decide P with left H => f H | right _ => fail e end.
Notation "'guard' P 'with' e ; o" := (error_guard P e (λ _, o)) Notation "'guard' P 'with' e ; o" := (error_guard P e (λ _, o))
(at level 65, next at level 35, only parsing, right associativity) : C_scope. (at level 65, next at level 35, only parsing, right associativity) : C_scope.
Definition error_of_option {A E} (x : option A) (e : E) : sum E A := Definition error_of_option {S A E} (x : option A) (e : E) : error S E A :=
match x with Some a => inr a | None => inl e end. match x with Some a => mret a | None => fail e end.
Lemma bind_inr {A B E} (f : A E + B) x b : Lemma error_bind_ret {S E A B} (f : A error S E B) s s'' x b :
x = f = inr b a, x = inr a f a = inr b. (x = f) s = mret b s'' a s', x s = mret a s' f a s' = mret b s''.
Proof. destruct x; naive_solver. Qed. Proof. compute; destruct (x s) as [|[??]]; naive_solver. Qed.
Lemma fmap_inr {A B E} (f : A B) (x : E + A) b : Lemma error_fmap_ret {S E A B} (f : A B) s s' (x : error S E A) b :
f <$> x = inr b a, x = inr a f a = b. (f <$> x) s = mret b s' a, x s = mret a s' b = f a.
Proof. destruct x; naive_solver. Qed. Proof. compute; destruct (x s) as [|[??]]; naive_solver. Qed.
Lemma error_of_option_inr {A E} (o : option A) (e : E) a : Lemma error_of_option_ret {S E A} (s s' : S) (o : option A) (e : E) a :
error_of_option o e = inr a o = Some a. error_of_option o e s = mret a s' o = Some a s = s'.
Proof. destruct o; naive_solver. Qed. Proof. compute; destruct o; naive_solver. Qed.
Lemma error_guard_ret {S E A} `{dec : Decision P} s s' (x : error S E A) e a :
(guard P with e ; x) s = mret a s' P x s = mret a s'.
Proof. compute; destruct dec; naive_solver. Qed.
Lemma error_fmap_bind {S E A B C} (f : A B) (g : B error S E C) x s :
((f <$> x) = g) s = (x = g f) s.
Proof. by compute; destruct (x s) as [|[??]]. Qed.
Tactic Notation "case_error_guard" "as" ident(Hx) := Lemma error_associative {S E A B C} (f : A error S E B) (g : B error S E C) x s :
match goal with ((x = f) = g) s = (a x; f a = g) s.
| H : context C [@error_guard _ ?P ?dec _ ?e ?x] |- _ => Proof. by compute; destruct (x s) as [|[??]]. Qed.
let X := context C [ match dec with left H => x H | _ => inl e end ] in Lemma error_of_option_bind {S E A B} (f : A option B) o e :
change X in H; destruct_decide dec as Hx error_of_option (S := S) (E:=E) (o = f) e
| |- context C [@error_guard _ ?P ?dec _ ?e ?x] => = a error_of_option o e; error_of_option (f a) e.
let X := context C [ match dec with left H => x H | _ => inl e end ] in Proof. by destruct o. Qed.
change X; destruct_decide dec as Hx
end. Lemma error_gets_spec {S E A} (g : S A) s : gets (E:=E) g s = mret (g s) s.
Tactic Notation "case_error_guard" := Proof. done. Qed.
let H := fresh in case_error_guard as H. Lemma error_modify_spec {S E} (g : S S) s : modify (E:=E) g s = mret () (g s).
Proof. done. Qed.
Lemma error_left_gets {S E A B} (g : S A) (f : A error S E B) s :
(gets (E:=E) g = f) s = f (g s) s.
Proof. done. Qed.
Lemma error_left_modify {S E B} (g : S S) (f : unit error S E B) s :
(modify (E:=E) g = f) s = f () (g s).
Proof. done. Qed.
Lemma error_left_id {S E A B} (a : A) (f : A error S E B) :
(mret a = f) = f a.
Proof. done. Qed.
Ltac generalize_errors :=
csimpl;
let gen_error e :=
try (is_var e; fail 1); generalize e;
let x := fresh "err" in intros x in
repeat match goal with
| |- appcontext[ fail ?e ] => gen_error e
| |- appcontext[ error_guard _ ?e ] => gen_error e
| |- appcontext[ error_of_option _ ?e ] => gen_error e
end.
Tactic Notation "simplify_error_equality" := Tactic Notation "simplify_error_equality" :=
repeat match goal with repeat match goal with
| H : context [ gets _ _ _ ] |- _ => rewrite error_gets_spec in H
| H : context [ modify _ _ _ ] |- _ => rewrite error_modify_spec in H
| H : (mret (M:=error _ _) _ = _) _ = _ |- _ => rewrite error_left_id in H
| H : (gets _ = _) _ = _ |- _ => rewrite error_left_gets in H
| H : (modify _ = _) _ = _ |- _ => rewrite error_left_modify in H
| H : error_guard _ _ _ _ = _ |- _ => apply error_guard_ret in H; destruct H
| _ => progress simplify_equality' | _ => progress simplify_equality'
| H : appcontext [@mret (sum ?E) _ ?A] |- _ => | H : error_of_option _ _ _ = _ |- _ =>
change (@mret (sum E) _ A) with (@inr E A) in H apply error_of_option_ret in H; destruct H
| |- appcontext [@mret (sum ?E) _ ?A] => change (@mret _ _ A) with (@inr E A) | H : mbind (M:=error _ _) _ _ _ = _ |- _ =>
| _ : maybe _ ?x = Some _ |- _ => is_var x; destruct x apply error_bind_ret in H; destruct H as (?&?&?&?)
| _ : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x | H : fmap (M:=error _ _) _ _ _ = _ |- _ =>
| _ : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x apply error_fmap_ret in H; destruct H as (?&?&?)
| _ : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x | H : mbind (M:=option) _ _ = _ |- _ =>
| H : error_of_option ?o ?e = ?x |- _ => apply error_of_option_inr in H
| H : mbind (M:=sum _) ?f ?o = ?x |- _ =>
apply bind_inr in H; destruct H as (?&?&?)
| H : fmap (M:=sum _) ?f ?o = ?x |- _ =>
apply fmap_inr in H; destruct H as (?&?&?)
| H : mbind (M:=option) ?f ?o = ?x |- _ =>
apply bind_Some in H; destruct H as (?&?&?) apply bind_Some in H; destruct H as (?&?&?)
| H : fmap (M:=option) ?f ?o = ?x |- _ => | H : fmap (M:=option) _ _ = _ |- _ =>
apply fmap_Some in H; destruct H as (?&?&?) apply fmap_Some in H; destruct H as (?&?&?)
| H : maybe _ ?x = Some _ |- _ => is_var x; destruct x
| H : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
| H : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
| H : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
| _ => progress case_decide | _ => progress case_decide
| _ => progress case_error_guard
| _ => progress case_option_guard
end. end.
Section mapM. Tactic Notation "error_proceed" :=
Context {A B E : Type} (f : A E + B). repeat match goal with
| H : context [ gets _ _ ] |- _ => rewrite error_gets_spec in H
Lemma error_mapM_ext (g : A sum E B) l : | H : context [ modify _ _ ] |- _ => rewrite error_modify_spec in H
( x, f x = g x) mapM f l = mapM g l. | H : context [ error_of_option _ _ ] |- _ => rewrite error_of_option_bind in H
Proof. intros Hfg. by induction l; simpl; rewrite ?Hfg, ?IHl. Qed. | H : (mret (M:= _ _) _ = _) _ = _ |- _ => rewrite error_left_id in H
Lemma error_Forall2_mapM_ext (g : A E + B) l k : | H : (gets _ = _) _ = _ |- _ => rewrite error_left_gets in H
Forall2 (λ x y, f x = g y) l k mapM f l = mapM g k. | H : (modify _ = _) _ = _ |- _ => rewrite error_left_modify in H
Proof. induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed. | H : ((_ <$> _) = _) _ = _ |- _ => rewrite error_fmap_bind in H
Lemma error_Forall_mapM_ext (g : A E + B) l : | H : ((_ = _) = _) _ = _ |- _ => rewrite error_associative in H
Forall (λ x, f x = g x) l mapM f l = mapM g l. | H : (error_guard _ _ _) _ = _ |- _ =>
Proof. induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed. let H' := fresh in apply error_guard_ret in H; destruct H as [H' H]
Lemma mapM_inr_1 l k : mapM f l = inr k Forall2 (λ x y, f x = inr y) l k. | _ => progress simplify_equality'
Proof. | H : maybe _ ?x = Some _ |- _ => is_var x; destruct x
revert k. induction l as [|x l]; intros [|y k]; simpl; try done. | H : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
* destruct (f x); simpl; [discriminate|]. by destruct (mapM f l). | H : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
* destruct (f x) eqn:?; intros; simplify_error_equality; auto. | H : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
Qed. end.
Lemma mapM_inr_2 l k : Forall2 (λ x y, f x = inr y) l k mapM f l = inr k. Tactic Notation "error_proceed"
Proof. simple_intropattern(a) "as" simple_intropattern(s) :=
induction 1 as [|???? Hf ? IH]; simpl; [done |]. error_proceed;
rewrite Hf. simpl. by rewrite IH. lazymatch goal with
Qed. | H : (error_of_option ?o _ = _) _ = _ |- _ => destruct o as [a|] eqn:?
Lemma mapM_inr l k : mapM f l = inr k Forall2 (λ x y, f x = inr y) l k. | H : error_of_option ?o _ _ = _ |- _ => destruct o as [a|] eqn:?
Proof. split; auto using mapM_inr_1, mapM_inr_2. Qed. | H : (_ = _) _ = _ |- _ => apply error_bind_ret in H; destruct H as (a&s&?&H)
Lemma error_mapM_length l k : mapM f l = inr k length l = length k. | H : (_ <$> _) _ = _ |- _ => apply error_fmap_ret in H; destruct H as (a&?&?)
Proof. intros. by eapply Forall2_length, mapM_inr_1. Qed. end;
End mapM. error_proceed.
...@@ -84,14 +84,8 @@ Definition map_Forall2 `{∀ A, Lookup K A (M A)} {A B} ...@@ -84,14 +84,8 @@ Definition map_Forall2 `{∀ A, Lookup K A (M A)} {A B}
| None, Some y => Q y | None, Some y => Q y
| None, None => True | None, None => True
end. end.
Definition map_Forall3 `{ A, Lookup K A (M A)} {A B C} Definition map_included `{ A, Lookup K A (M A)} {A}
(R : A B C Prop) (m1 : M A) (m2 : M B) (m3 : M C): Prop := i, (R : relation A) : relation (M A) := map_Forall2 R (λ _, False) (λ _, True).
match m1 !! i, m2 !! i, m3 !! i with
| Some x, Some y, Some z => R x y z
| None, None, None => True
| _, _, _ => False
end.
Instance map_disjoint `{ A, Lookup K A (M A)} {A} : Disjoint (M A) := Instance map_disjoint `{ A, Lookup K A (M A)} {A} : Disjoint (M A) :=
map_Forall2 (λ _ _, False) (λ _, True) (λ _, True). map_Forall2 (λ _ _, False) (λ _, True) (λ _, True).
Instance map_subseteq `{ A, Lookup K A (M A)} {A} : SubsetEq (M A) := Instance map_subseteq `{ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
...@@ -127,13 +121,17 @@ Proof. ...@@ -127,13 +121,17 @@ Proof.
intros A m. rewrite !map_subseteq_spec. intros A m. rewrite !map_subseteq_spec.
intros i x. by rewrite lookup_empty. intros i x. by rewrite lookup_empty.
Qed. Qed.
Global Instance: {A} (R : relation A), PreOrder R PreOrder (map_included R).
Proof.
split; [intros m i; by destruct (m !! i)|].
intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
destruct (m1 !! i), (m2 !! i), (m3 !! i); try done; etransitivity; eauto.
Qed.
Global Instance: PartialOrder (() : relation (M A)). Global Instance: PartialOrder (() : relation (M A)).
Proof. Proof.
repeat split. split; [apply _|].
* intros m; rewrite !map_subseteq_spec; naive_solver. intros m1 m2; rewrite !map_subseteq_spec.
* intros m1 m2 m3; rewrite !map_subseteq_spec; naive_solver. intros; apply map_eq; intros i; apply option_eq; naive_solver.
* intros m1 m2; rewrite !map_subseteq_spec.
intros; apply map_eq; intros i; apply option_eq; naive_solver.
Qed. Qed.
Lemma lookup_weaken {A} (m1 m2 : M A) i x : Lemma lookup_weaken {A} (m1 m2 : M A) i x :
m1 !! i = Some x m1 m2 m2 !! i = Some x. m1 !! i = Some x m1 m2 m2 !! i = Some x.
...@@ -342,6 +340,18 @@ Proof. ...@@ -342,6 +340,18 @@ Proof.
destruct (decide (i = j)) as [->|]; destruct (decide (i = j)) as [->|];
rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence. rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
Qed. Qed.
Lemma insert_lookup {A} (m : M A) i x : m !! i = Some x <[i:=x]>m = m.
Proof.
intros; apply map_eq; intros j; destruct (decide (i = j)) as [->|];
by rewrite ?lookup_insert, ?lookup_insert_ne by done.
Qed.
Lemma insert_included {A} R `{!Reflexive R} (m : M A) i x :
( y, m !! i = Some y R y x) map_included R m (<[i:=x]>m).
Proof.
intros ? j; destruct (decide (i = j)) as [->|].
* rewrite lookup_insert. destruct (m !! j); eauto.
* rewrite lookup_insert_ne by done. by destruct (m !! j).
Qed.
Lemma insert_subseteq {A} (m : M A) i x : m !! i = None m <[i:=x]>m. Lemma insert_subseteq {A} (m : M A) i x : m !! i = None m <[i:=x]>m.
Proof. apply partial_alter_subseteq. Qed. Proof. apply partial_alter_subseteq. Qed.
Lemma insert_subset {A} (m : M A) i x : m !! i = None m <[i:=x]>m. Lemma insert_subset {A} (m : M A) i x : m !! i = None m <[i:=x]>m.
...@@ -520,6 +530,12 @@ Proof. ...@@ -520,6 +530,12 @@ Proof.
intros. rewrite <-(map_of_to_list m1), <-(map_of_to_list m2). intros. rewrite <-(map_of_to_list m1), <-(map_of_to_list m2).
auto using map_of_list_proper, NoDup_fst_map_to_list. auto using map_of_list_proper, NoDup_fst_map_to_list.
Qed. Qed.
Lemma map_to_of_list_flip {A} (m1 : M A) l2 :
map_to_list m1 l2 m1 = map_of_list l2.
Proof.
intros. rewrite <-(map_of_to_list m1).
auto using map_of_list_proper, NoDup_fst_map_to_list.
Qed.
Lemma map_to_list_empty {A} : map_to_list = @nil (K * A). Lemma map_to_list_empty {A} : map_to_list = @nil (K * A).
Proof. Proof.
apply elem_of_nil_inv. intros [i x]. apply elem_of_nil_inv. intros [i x].
...@@ -620,6 +636,35 @@ Proof. ...@@ -620,6 +636,35 @@ Proof.
* intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x). * intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x).
* intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)). * intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)).
Qed. Qed.
Lemma map_Forall_empty : map_Forall P .
Proof. intros i x. by rewrite lookup_empty. Qed.
Lemma map_Forall_impl (Q : K A Prop) m :
map_Forall P m ( i x, P i x Q i x) map_Forall Q m.
Proof. unfold map_Forall; naive_solver. Qed.
Lemma map_Forall_insert_11 m i x : map_Forall P (<[i:=x]>m) P i x.
Proof. intros Hm. by apply Hm; rewrite lookup_insert. Qed.
Lemma map_Forall_insert_12 m i x :
m !! i = None map_Forall P (<[i:=x]>m) map_Forall P m.
Proof.
intros ? Hm j y ?; apply Hm. by rewrite lookup_insert_ne by congruence.
Qed.
Lemma map_Forall_insert_2 m i x :
P i x map_Forall P m map_Forall P (<[i:=x]>m).
Proof. intros ?? j y; rewrite lookup_insert_Some; naive_solver. Qed.
Lemma map_Forall_insert m i x :
m !! i = None map_Forall P (<[i:=x]>m) P i x map_Forall P m.
Proof.
naive_solver eauto using map_Forall_insert_11,
map_Forall_insert_12, map_Forall_insert_2.
Qed.
Lemma map_Forall_ind (Q : M A Prop) :
Q
( m i x, m !! i = None P i x map_Forall P m Q m Q (<[i:=x]>m))
m, map_Forall P m Q m.
Proof.
intros Hnil Hinsert m. induction m using map_ind; auto.
rewrite map_Forall_insert by done; intros [??]; eauto.
Qed.
Context `{ i x, Decision (P i x)}. Context `{ i x, Decision (P i x)}.
Global Instance map_Forall_dec m : Decision (map_Forall P m). Global Instance map_Forall_dec m : Decision (map_Forall P m).
...@@ -630,11 +675,10 @@ Defined. ...@@ -630,11 +675,10 @@ Defined.
Lemma map_not_Forall (m : M A) : Lemma map_not_Forall (m : M A) :
¬map_Forall P m i x, m !! i = Some x ¬P i x. ¬map_Forall P m i x, m !! i = Some x ¬P i x.
Proof. Proof.
split. split; [|intros (i&x&?&?) Hm; specialize (Hm i x); tauto].
* rewrite map_Forall_to_list. intros Hm. rewrite map_Forall_to_list. intros Hm.
apply (not_Forall_Exists _), Exists_exists in Hm. apply (not_Forall_Exists _), Exists_exists in Hm.
destruct Hm as ([i x]&?&?). exists i x. by rewrite <-elem_of_map_to_list. destruct Hm as ([i x]&?&?). exists i x. by rewrite <-elem_of_map_to_list.
* intros (i&x&?&?) Hm. specialize (Hm i x). tauto.
Qed. Qed.
End map_Forall. End map_Forall.
...@@ -745,7 +789,7 @@ Let f (mx : option A) (my : option B) : option bool := ...@@ -745,7 +789,7 @@ Let f (mx : option A) (my : option B) : option bool :=
| None, None => None | None, None => None
end. end.
Lemma map_Forall2_alt (m1 : M A) (m2 : M B) : Lemma map_Forall2_alt (m1 : M A) (m2 : M B) :
map_Forall2 R P Q m1 m2 map_Forall (λ _ P, Is_true P) (merge f m1 m2). map_Forall2 R P Q m1 m2 map_Forall (λ _, Is_true) (merge f m1 m2).
Proof. Proof.
split. split.
* intros Hm i P'; rewrite lookup_merge by done; intros. * intros Hm i P'; rewrite lookup_merge by done; intros.
...@@ -758,7 +802,7 @@ Qed. ...@@ -758,7 +802,7 @@ Qed.
Global Instance map_Forall2_dec `{ x y, Decision (R x y), x, Decision (P x), Global Instance map_Forall2_dec `{ x y, Decision (R x y), x, Decision (P x),
y, Decision (Q y)} m1 m2 : Decision (map_Forall2 R P Q m1 m2). y, Decision (Q y)} m1 m2 : Decision (map_Forall2 R P Q m1 m2).
Proof. Proof.
refine (cast_if (decide (map_Forall (λ _ P, Is_true P) (merge f m1 m2)))); refine (cast_if (decide (map_Forall (λ _, Is_true) (merge f m1 m2))));
abstract by rewrite map_Forall2_alt. abstract by rewrite map_Forall2_alt.
Defined. Defined.
(** Due to the finiteness of finite maps, we can extract a witness if the (** Due to the finiteness of finite maps, we can extract a witness if the
......
...@@ -12,24 +12,26 @@ Arguments enum _ {_ _} : clear implicits. ...@@ -12,24 +12,26 @@ Arguments enum _ {_ _} : clear implicits.
Arguments NoDup_enum _ {_ _} : clear implicits. Arguments NoDup_enum _ {_ _} : clear implicits.
Definition card A `{Finite A} := length (enum A). Definition card A `{Finite A} := length (enum A).
Program Instance finite_countable `{Finite A} : Countable A := {| Program Instance finite_countable `{Finite A} : Countable A := {|
encode := λ x, Pos.of_nat $ S $ from_option 0 $ list_find (x =) (enum A); encode := λ x,
Pos.of_nat $ S $ from_option 0 $ fst <$> list_find