Commit d6eb24f2 authored by Robbert Krebbers's avatar Robbert Krebbers

More type annotations for https://github.com/coq/coq/pull/9996.

parent 0f2d2c8a
Pipeline #16273 passed with stage
in 12 minutes and 4 seconds
......@@ -897,6 +897,9 @@ Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : stdpp_scope.
Infix "∈@{ B }" := (@elem_of _ B _) (at level 70, only parsing) : stdpp_scope.
Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope.
Notation "x ∉@{ B } X" := (¬x @{B} X) (at level 80, only parsing) : stdpp_scope.
Notation "(∉@{ B } )" := (λ x X, x @{B} X) (only parsing) : stdpp_scope.
Class Disjoint A := disjoint : A A Prop.
Hint Mode Disjoint ! : typeclass_instances.
Instance: Params (@disjoint) 2 := {}.
......@@ -1136,15 +1139,15 @@ Note that we cannot use the name [Set] since that is a reserved keyword. Hence
we use [Set_]. *)
Class SemiSet A C `{ElemOf A C,
Empty C, Singleton A C, Union C} : Prop := {
not_elem_of_empty (x : A) : x ;
elem_of_singleton (x y : A) : x {[ y ]} x = y;
elem_of_union X Y (x : A) : x X Y x X x Y
not_elem_of_empty (x : A) : x @{C} ;
elem_of_singleton (x y : A) : x @{C} {[ y ]} x = y;
elem_of_union (X Y : C) (x : A) : x X Y x X x Y
}.
Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
Union C, Intersection C, Difference C} : Prop := {
set_semi_set :>> SemiSet A C;
elem_of_intersection X Y (x : A) : x X Y x X x Y;
elem_of_difference X Y (x : A) : x X Y x X x Y
elem_of_intersection (X Y : C) (x : A) : x X Y x X x Y;
elem_of_difference (X Y : C) (x : A) : x X Y x X x Y
}.
(** We axiomative a finite set as a set whose elements can be
......@@ -1183,8 +1186,8 @@ anyway so as to avoid cycles in type class search. *)
Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
fin_set_set :>> Set_ A C;
elem_of_elements X x : x elements X x X;
NoDup_elements X : NoDup (elements X)
elem_of_elements (X : C) x : x elements X x X;
NoDup_elements (X : C) : NoDup (elements X)
}.
Class Size C := size: C nat.
Hint Mode Size ! : typeclass_instances.
......@@ -1205,10 +1208,11 @@ Class MonadSet M `{∀ A, ElemOf A (M A),
monad_set_semi_set A :> SemiSet A (M A);
elem_of_bind {A B} (f : A M B) (X : M A) (x : B) :
x X = f y, x f y y X;
elem_of_ret {A} (x y : A) : x mret y x = y;
elem_of_ret {A} (x y : A) : x @{M A} mret y x = y;
elem_of_fmap {A B} (f : A B) (X : M A) (x : B) :
x f <$> X y, x = f y y X;
elem_of_join {A} (X : M (M A)) (x : A) : x mjoin X Y, x Y Y X
elem_of_join {A} (X : M (M A)) (x : A) :
x mjoin X Y : M A, x Y Y X
}.
(** The [Infinite A] class axiomatizes types [A] with infinitely many elements.
......@@ -1255,7 +1259,7 @@ Notation "(⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation () := {}.
Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (@{A}) := {}.
Hint Extern 0 (_ _) => reflexivity : core.
......
......@@ -318,7 +318,7 @@ Proof.
Qed.
(** * Conversion to and from gsets of positives *)
Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf (K:=positive) m.
Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf positive m.
Proof. done. Qed.
Definition coPset_to_gset (X : coPset) : gset positive :=
let 'Mapset m := coPset_to_Pset X in
......
......@@ -18,14 +18,14 @@ Definition encode_nat `{Countable A} (x : A) : nat :=
pred (Pos.to_nat (encode x)).
Definition decode_nat `{Countable A} (i : nat) : option A :=
decode (Pos.of_nat (S i)).
Instance encode_inj `{Countable A} : Inj (=) (=) encode.
Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
Proof.
intros x y Hxy; apply (inj Some).
by rewrite <-(decode_encode x), Hxy, decode_encode.
Qed.
Instance encode_nat_inj `{Countable A} : Inj (=) (=) encode_nat.
Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed.
Lemma decode_encode_nat `{Countable A} x : decode_nat (encode_nat x) = Some x.
Lemma decode_encode_nat `{Countable A} (x : A) : decode_nat (encode_nat x) = Some x.
Proof.
pose proof (Pos2Nat.is_pos (encode x)).
unfold decode_nat, encode_nat. rewrite Nat.succ_pred by lia.
......
......@@ -145,12 +145,12 @@ Proof. unfold_leibniz; apply dom_fmap. Qed.
End fin_map_dom.
Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
dom D (map_seq start xs) set_seq start (length xs).
dom D (map_seq start (M:=M A) xs) set_seq start (length xs).
Proof.
revert start. induction xs as [|x xs IH]; intros start; simpl.
- by rewrite dom_empty.
- by rewrite dom_insert, IH.
Qed.
Lemma dom_seq_L `{FinMapDom nat M D, !LeibnizEquiv D} {A} start (xs : list A) :
dom D (map_seq start xs) = set_seq start (length xs).
dom D (map_seq (M:=M A) start xs) = set_seq start (length xs).
Proof. unfold_leibniz. apply dom_seq. Qed.
......@@ -42,8 +42,10 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
NoDup_map_to_list {A} (m : M A) : NoDup (map_to_list m);
elem_of_map_to_list {A} (m : M A) i x :
(i,x) map_to_list m m !! i = Some x;
lookup_omap {A B} (f : A option B) m i : omap f m !! i = m !! i = f;
lookup_merge {A B C} (f: option A option B option C) `{!DiagNone f} m1 m2 i :
lookup_omap {A B} (f : A option B) (m : M A) i :
omap f m !! i = m !! i = f;
lookup_merge {A B C} (f : option A option B option C)
`{!DiagNone f} (m1 : M A) (m2 : M B) i :
merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
}.
......@@ -943,7 +945,7 @@ Proof.
Qed.
Lemma elem_of_map_to_set_pair `{FinSet (K * A) C} (m : M A) i x :
(i,x) map_to_set pair m m !! i = Some x.
(i,x) @{C} map_to_set pair m m !! i = Some x.
Proof. rewrite elem_of_map_to_set. naive_solver. Qed.
(** ** Induction principles *)
......
......@@ -33,7 +33,7 @@ Hint Immediate finite_countable : typeclass_instances.
Definition find `{Finite A} P `{ x, Decision (P x)} : option A :=
list_find P (enum A) = decode_nat fst.
Lemma encode_lt_card `{finA: Finite A} x : encode_nat x < card A.
Lemma encode_lt_card `{finA: Finite A} (x : A) : encode_nat x < card A.
Proof.
destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
rewrite Nat2Pos.id by done; simpl.
......@@ -42,7 +42,7 @@ Proof.
- destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
Qed.
Lemma encode_decode A `{finA: Finite A} i :
i < card A x, decode_nat i = Some x encode_nat x = i.
i < card A x : A, decode_nat i = Some x encode_nat x = i.
Proof.
destruct finA as [xs Hxs HA].
unfold encode_nat, decode_nat, encode, decode, card; simpl.
......@@ -52,7 +52,7 @@ Proof.
destruct (list_find_Some (x =) xs j y) as [? ->]; auto.
rewrite Hj; csimpl; eauto using NoDup_lookup.
Qed.
Lemma find_Some `{finA: Finite A} P `{ x, Decision (P x)} x :
Lemma find_Some `{finA: Finite A} P `{ x, Decision (P x)} (x : A) :
find P = Some x P x.
Proof.
destruct finA as [xs Hxs HA]; unfold find, decode_nat, decode; simpl.
......@@ -60,7 +60,7 @@ Proof.
rewrite !Nat2Pos.id in Hx by done.
destruct (list_find_Some P xs i y); naive_solver.
Qed.
Lemma find_is_Some `{finA: Finite A} P `{ x, Decision (P x)} x :
Lemma find_is_Some `{finA: Finite A} P `{ x, Decision (P x)} (x : A) :
P x y, find P = Some y P y.
Proof.
destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
......@@ -309,7 +309,7 @@ Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n
| S n => foldr (λ x, (sig_map (x ::) (λ _ H, f_equal S H) <$> (go n) ++)) [] l
end.
Program Instance list_finite `{Finite A} n : Finite { l | length l = n } :=
Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
{| enum := list_enum (enum A) n |}.
Next Obligation.
intros ????. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
......@@ -335,7 +335,7 @@ Next Obligation.
- rewrite elem_of_app. eauto.
Qed.
Lemma list_card `{Finite A} n : card { l | length l = n } = card A ^ n.
Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
Proof.
unfold card; simpl. induction n as [|n IH]; simpl; auto.
rewrite <-IH. clear IH. generalize (list_enum (enum A) n).
......
......@@ -9,11 +9,11 @@ From stdpp Require Import pmap mapset propset.
(** * The data structure *)
(** We pack a [Pmap] together with a proof that ensures that all keys correspond
to codes of actual elements of the countable type. *)
Definition gmap_wf `{Countable K} {A} : Pmap A Prop :=
map_Forall (λ p _, encode <$> decode p = Some p).
Definition gmap_wf K `{Countable K} {A} : Pmap A Prop :=
map_Forall (λ p _, encode (A:=K) <$> decode p = Some p).
Record gmap K `{Countable K} A := GMap {
gmap_car : Pmap A;
gmap_prf : bool_decide (gmap_wf gmap_car)
gmap_prf : bool_decide (gmap_wf K gmap_car)
}.
Arguments GMap {_ _ _ _} _ _ : assert.
Arguments gmap_car {_ _ _ _} _ : assert.
......@@ -35,7 +35,7 @@ Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m,
Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap I.
Global Opaque gmap_empty.
Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A option A) m i :
gmap_wf m gmap_wf (partial_alter f (encode i) m).
gmap_wf K m gmap_wf K (partial_alter f (encode (A:=K) i) m).
Proof.
intros Hm p x. destruct (decide (encode i = p)) as [<-|?].
- rewrite decode_encode; eauto.
......@@ -47,13 +47,13 @@ Instance gmap_partial_alter `{Countable K} {A} :
(bool_decide_pack _ (gmap_partial_alter_wf f m i
(bool_decide_unpack _ Hm))).
Lemma gmap_fmap_wf `{Countable K} {A B} (f : A B) m :
gmap_wf m gmap_wf (f <$> m).
gmap_wf K m gmap_wf K (f <$> m).
Proof. intros ? p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto. Qed.
Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f m,
let (m,Hm) := m in GMap (f <$> m)
(bool_decide_pack _ (gmap_fmap_wf f m (bool_decide_unpack _ Hm))).
Lemma gmap_omap_wf `{Countable K} {A B} (f : A option B) m :
gmap_wf m gmap_wf (omap f m).
gmap_wf K m gmap_wf K (omap f m).
Proof. intros ? p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto. Qed.
Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f m,
let (m,Hm) := m in GMap (omap f m)
......@@ -61,7 +61,7 @@ Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f m,
Lemma gmap_merge_wf `{Countable K} {A B C}
(f : option A option B option C) m1 m2 :
let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
gmap_wf m1 gmap_wf m2 gmap_wf (merge f' m1 m2).
gmap_wf K m1 gmap_wf K m2 gmap_wf K (merge f' m1 m2).
Proof.
intros f' Hm1 Hm2 p z; rewrite lookup_merge by done; intros.
destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
......
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