Commit e925f4ca authored by Ralf Jung's avatar Ralf Jung

port to Coq 8.10

parent a9c0edba
......@@ -29,15 +29,15 @@ variables:
- api
## Build jobs
build-coq.8.9.1:
build-coq.8.10.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.1"
OPAM_PINS: "coq version 8.10.2"
build-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.1 coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
OPAM_PINS: "coq version 8.10.2 coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
except:
only:
- triggers
......
-Q theories spygame
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
theories/conjunction.v
theories/fix_simple.v
theories/fix.v
......
......@@ -8,18 +8,17 @@ From spygame Require Import lists type_repr proph_lib modulus.
Section Preamble.
Instance bnat_countable (m : nat) : Countable { n : nat | (n < m)%nat } := {|
countable.encode bn :=
match bn with exist _ n _ => Pos.of_nat (S n) end;
Program Instance bnat_countable (m : nat) : Countable { n : nat | (n < m)%nat } := {|
countable.encode bn := Pos.of_nat (S bn); (* [Program] coerces [bn] to [nat] here. *)
countable.decode p :=
let n := pred (Pos.to_nat p) in
match lt_dec n m with
match lt_dec n m return _ with
| left pf => Some (exist _ n pf)
| right _ => None
end
|}.
Proof.
intros bn; case bn; intros n pf; simpl; rewrite Nat2Pos.id; [ simpl | done ].
Next Obligation.
intros m bn; case bn; intros n pf; simpl; rewrite Nat2Pos.id; [ simpl | done ].
case (lt_dec n m); intro pf'; [ | contradiction ].
rewrite (_ : n pf = n pf'); [ |
apply sig_eq_pi; [ intro; apply nat_lt_pi | ] ]; done.
......
......@@ -18,7 +18,7 @@ Class Map Σ `{!heapG Σ} := {
make_map_spec A B `{Countable A} :
{{{ True }}} make_map #() {{{ (m : val), RET m; is_map m ( : gmap A B) }}};
map_lookup_spec {A B} `{Encodable A, Encodable B, Countable A} m map a :
map_lookup_spec {A B} `{Encodable A, Encodable B, Countable A} m (map : gmap A B) a :
{{{ is_map m map }}}
map_lookup m (encode' a)
{{{ RET (match map !! a with
......@@ -27,17 +27,17 @@ Class Map Σ `{!heapG Σ} := {
end);
is_map m map }}};
map_insert_spec {A B} `{Encodable A, Encodable B, Countable A} m map a b :
map_insert_spec {A B} `{Encodable A, Encodable B, Countable A} m (map : gmap A B) a b :
{{{ is_map m map }}}
map_insert m (encode' a) (encode' b)
{{{ RET #(); is_map m (<[ a := b ]> map) }}};
map_delete_spec {A B} `{Encodable A, Countable A} m map a :
map_delete_spec {A B} `{Encodable A, Countable A} m (map : gmap A B) a :
{{{ is_map m (map : gmap A B) }}}
map_delete m (encode' a)
{{{ RET #(); is_map m (delete a map) }}};
map_to_assoc_list_spec {A B} `{Encodable A, Encodable B, Countable A} m map :
map_to_assoc_list_spec {A B} `{Encodable A, Encodable B, Countable A} m (map : gmap A B) :
{{{ is_map m map }}}
map_to_assoc_list m
{{{ RET (encode' ((map_to_list map) : list (A * B))); is_map m map }}}
......
......@@ -28,10 +28,10 @@ Section ValEncoding.
Global Instance val_decoding : Decodable val := {
decode' := Some; decode_encode' := λ l, eq_refl (Some l)
}.
Global Instance nat_decoding : Decodable nat := {
decode' := λ v, match v with LitV (LitInt n) => Some (Z.abs_nat n) | _ => None end
Global Program Instance nat_decoding : Decodable nat := {
decode' := λ v, match v return _ with LitV (LitInt n) => Some (Z.abs_nat n) | _ => None end
}.
Proof. intro t; unfold encode'; simpl; by rewrite Zabs2Nat.id. Qed.
Next Obligation. intro t; unfold encode'; simpl; by rewrite Zabs2Nat.id. Qed.
Global Instance int_decoding : Decodable Z := {
decode' := λ v, match v with LitV (LitInt n) => Some n | _ => None end;
decode_encode' := λ l, eq_refl (Some l)
......@@ -44,31 +44,31 @@ Section ValEncoding.
decode' := λ v, match v with LitV LitUnit => Some () | _ => None end;
decode_encode' := λ l, match l with () => eq_refl (Some ()) end
}.
Global Instance bnat_decoding m : Decodable { n | (n < m)%nat } := {
Global Program Instance bnat_decoding m : Decodable { n | (n < m)%nat } := {
decode' := λ v,
match v with
match v return _ with
| LitV (LitInt n) =>
let n := Z.abs_nat n in
match lt_dec n m with
match lt_dec n m return _ with
| left pf => Some (exist _ n pf)
| right _ => None
end
| _ => None
end
}.
Proof.
case; intros n pf; simpl.
Next Obligation.
intros m. case; intros n pf; simpl.
case (lt_dec (Z.abs_nat n) m); rewrite Zabs2Nat.id; intro pf'; [ | contradiction ].
rewrite (_ : n pf = n pf'); [ | apply sig_eq_pi; [ intro; apply nat_lt_pi | ] ]; done.
Qed.
Global Instance option_decoding `{Decodable A} : Decodable (option A) := {
decode' := λ v, match v with SOMEV a => Some (decode' a) | NONEV => Some None | _ => None end;
Global Program Instance option_decoding `{Decodable A} : Decodable (option A) := {
decode' := λ v, match v return _ with SOMEV a => Some (decode' a) | NONEV => Some None | _ => None end;
}.
Proof. case; simpl; [|done]. intro. by rewrite decode_encode'. Qed.
Global Instance list_decoding `{Decodable A} : Decodable (list A) := {
Next Obligation. intros ???. case; simpl; [|done]. intro. by rewrite decode_encode'. Qed.
Global Program Instance list_decoding `{Decodable A} : Decodable (list A) := {
decode' :=
(fix decode_ v :=
match v with
match v return _ with
| NONEV => option_ret _ []
| SOMEV (a, bs) =>
decode' a = λ u,
......@@ -77,27 +77,27 @@ Section ValEncoding.
| _ => None
end)
}.
Proof.
Next Obligation.
induction t as [ | v vs ]; [ by simpl | ]; intros; simpl; rewrite decode_encode' IHvs //=.
Qed.
Global Instance sum_decoding `{Decodable A, Decodable B} : Decodable (A + B) := {
Global Program Instance sum_decoding `{Decodable A, Decodable B} : Decodable (A + B) := {
decode' := λ v,
match v with
match v return _ with
| InjLV u => decode' u = λ a, option_ret _ (inl a)
| InjRV u => decode' u = λ b, option_ret _ (inr b)
| _ => None
end }.
Proof. case; intro u; simpl; rewrite decode_encode'; done. Qed.
Global Instance prod_decoding `{Decodable A, Decodable B} : Decodable (A * B) := {
Next Obligation. intros ??????. case; intro u; simpl; rewrite ?decode_encode'; done. Qed.
Global Program Instance prod_decoding `{Decodable A, Decodable B} : Decodable (A * B) := {
decode' := λ v,
match v with
match v return _ with
| PairV u v =>
decode' u = λ a,
decode' v = λ b,
option_ret _ (a, b)
| _ => None
end }.
Proof. case; intros a b; simpl; do 2 rewrite decode_encode'; done. Qed.
Next Obligation. intros ??????. case; intros a b; simpl; do 2 rewrite decode_encode'; done. Qed.
Lemma encode_injective `{Decodable A} (u v : A) : encode' u = encode' v u = v.
Proof. intro eq; specialize (decode_encode' u); rewrite eq decode_encode'; by case. Qed.
......
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