Commit 89425063 authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Bump stdpp and proofmode.

parent 058a6f69
......@@ -6,6 +6,6 @@ install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/fri" ]
depends: [
"coq" { >= "8.7" }
"coq-stdpp" { (= "dev.2017-11-22.1") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2017-11-26.0") }
"coq-stdpp" { (>= "1.1.0") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-01-11.3" ) }
]
......@@ -1277,7 +1277,7 @@ Section cofair.
Proof.
intros Hae.
pose (f := fun2tr R2 O (skip_fun e Hae) (skip_fun_tfun _ _)).
assert (Hhd: skip_fun e Hae 0.1 = erasure x).
assert (Hhd: (skip_fun e Hae 0).1 = erasure x).
{ simpl.
unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
......@@ -1472,7 +1472,7 @@ Section cofair.
Qed.
Lemma glue_isteps:
a e n, isteps_aux' R2 (glue a e n) ((flatten a).1) (flatten ((tr2fun e n).1).1).
a e n, isteps_aux' R2 (glue a e n) ((flatten a).1) ((flatten ((tr2fun e n).1)).1).
Proof.
intros a e n. revert a e; induction n; intros.
- simpl. destruct e. simpl. econstructor.
......@@ -1583,7 +1583,7 @@ Section cofair.
destruct glue_lookup as ((b&i)&l1&l2&Heq&Hlen). simpl. destruct e as [i' x y HS e].
destruct l1; [| simpl in *; omega].
simpl.
assert (flatten x.1 = b) as ->.
assert ((flatten x).1 = b) as ->.
{
simpl in *. destruct constructive_indefinite_description as (?&Histep&?).
destruct constructive_indefinite_description as (?&?&Histep').
......@@ -1736,7 +1736,7 @@ simpl. destruct e. simpl in *.
exists (e': trace R2 ((flatten a).1)), fair_pres e e'.
Proof.
pose (f := fun2tr R2 O (flatten_trace_fun a e) (flatten_trace_tfun _ _)).
assert (Hhd: flatten_trace_fun a e 0.1 = flatten a.1).
assert (Hhd: (flatten_trace_fun a e 0).1 = (flatten a).1).
{
unfold flatten_trace_fun. destruct glue_lookup as (?&l1&l2&Heq&?); simpl.
specialize (glue_isteps a e 1); intros Histeps.
......@@ -1768,14 +1768,14 @@ simpl. destruct e. simpl in *.
eapply (tr2fun_ev_al _ _ _ (λ p, enabled R2 (fst p) i)) in Hea_f.
destruct Hea_f as (k2&Hk2).
destruct (flatten_trace_match a e (k1 + k2)) as (kb&Hlt&Hmatch&l&?&Hinblock&Hoffset).
edestruct (flatten_spec_cover (tr2fun e (k1 + k2).1) i) as (j&Hin).
edestruct (flatten_spec_cover ((tr2fun e (k1 + k2)).1) i) as (j&Hin).
{ rewrite Hmatch.
specialize (Hk2 kb).
unfold f in Hk2. rewrite tr2fun_fun2tr in Hk2.
simpl in Hk2. eauto.
eapply Hk2. omega.
}
assert (enabled R1 (tr2fun e (k1 + k2).1) j) as Henj.
assert (enabled R1 (tr2fun e (k1 + k2)).1 j) as Henj.
{
eapply flatten_spec_enabled_reflect.
rewrite Hmatch.
......
......@@ -384,15 +384,24 @@ Definition uPred_relevant_if {M} (p : bool) (P : uPred M) : uPred M :=
Instance: Params (@uPred_relevant_if) 2.
Arguments uPred_relevant_if _ !_ _/.
Notation "□? p P" := (uPred_relevant_if p P)
(at level 20, p at level 0, P at level 20, format "□? p P").
(at level 20, p at level 9, P at level 20, format "□? p P").
Definition uPred_laterN {M} (n : nat) (P : uPred M) : uPred M :=
Nat.iter n uPred_later P.
Instance: Params (@uPred_laterN) 2.
Notation "▷^ n P" := (uPred_laterN n P)
(at level 20, n at level 9, right associativity,
(at level 20, n at level 9, P at level 20, right associativity,
format "▷^ n P") : uPred_scope.
Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x y := P n |}.
Solve Obligations with naive_solver eauto using uPred_closed, ucmra_unit_validN.
Definition uPred_plainly_aux : { x | x = @uPred_plainly_def}. by eexists. Qed.
Definition uPred_plainly {M} := proj1_sig uPred_plainly_aux M.
Definition uPred_plainly_eq :
@uPred_plainly = @uPred_plainly_def := proj2_sig uPred_plainly_aux.
Class TimelessP {M} (P : uPred M) := timelessP : P (P False).
Arguments timelessP {_} _ {_}.
......@@ -421,7 +430,8 @@ Module uPred.
Definition unseal :=
(uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_relevant_eq, uPred_affine_eq,
uPred_later_eq, uPred_ownM_eq, uPred_ownMl_eq, uPred_valid_eq, uPred_emp_eq, uPred_stopped_eq).
uPred_later_eq, uPred_ownM_eq, uPred_ownMl_eq, uPred_valid_eq, uPred_emp_eq, uPred_stopped_eq,
uPred_plainly_eq).
Ltac unseal := rewrite !unseal /=.
Section uPred_logic.
......@@ -581,6 +591,14 @@ Qed.
Global Instance valid_proper {A : cmraT} :
Proper (() ==> (⊣⊢)) (@uPred_valid M A) := ne_proper _.
Global Instance plainly_ne n : Proper (dist n ==> dist n) (@uPred_plainly M).
Proof.
intros P1 P2 HP.
unseal; split=> n' x y; split; apply HP; eauto using ucmra_unit_validN.
Qed.
Global Instance plainly_proper :
Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_plainly M) := ne_proper _.
(** Introduction and elimination rules *)
Lemma pure_intro φ P : φ P φ.
Proof. by intros ?; unseal; split. Qed.
......@@ -2179,4 +2197,5 @@ Hint Resolve relevant_mono affine_elim : I.
Hint Resolve sep_elim_l' sep_elim_r' sep_mono affine_sep_elim_l' affine_sep_elim_r' : I.
Hint Immediate True_intro False_elim : I.
Hint Immediate iff_refl eq_refl' : I.
End uPred.
......@@ -170,7 +170,7 @@ Proof.
Qed.
Lemma typ_context_closed_2 Γ e ty:
has_typ Γ e ty Closed (map_to_list Γ.*1) e.
has_typ Γ e ty Closed ((map_to_list Γ).*1) e.
Proof.
intros Htyp. eapply typ_context_closed_1 in Htyp; eauto.
intros x. rewrite elem_of_dom. intros [ty' Heq].
......
......@@ -72,7 +72,7 @@ Proof.
by eapply Hclo, Hsub.
Qed.
Lemma ClosedSubst_map l S: ClosedSubst l S Forall (Closed l) (map_to_list S.*2).
Lemma ClosedSubst_map l S: ClosedSubst l S Forall (Closed l) ((map_to_list S).*2).
Proof.
rewrite /ClosedSubst map_Forall_to_list.
remember (map_to_list S) as lS eqn:Heq.
......@@ -280,7 +280,7 @@ Lemma msubst_weaken_2 e S1 S2:
msubst S1 e = msubst S2 e.
Proof.
intros HcloS Hsub Hclosing.
eapply (msubst_weaken_1 _ _ _ (map_to_list S1.*1)); eauto.
eapply (msubst_weaken_1 _ _ _ ((map_to_list S1).*1)); eauto.
- eapply Hclosing=>x. rewrite elem_of_dom.
intros (es&Hlook). apply elem_of_list_fmap.
exists (x, es); split; auto. rewrite elem_of_map_to_list //.
......@@ -574,7 +574,7 @@ Qed.
Lemma msubst_closing_inv_1 S l e:
ClosedSubst [] S
Closed l (msubst S e)
Closed (map_to_list S.*1 ++ l) e.
Closed ((map_to_list S).*1 ++ l) e.
Proof. intros; eapply lsubst_closing_inv_1; eauto using ClosedSubst_map. Qed.
Lemma msubst_closing_inv_2 S x l e:
......
......@@ -72,7 +72,7 @@ Proof.
by eapply Hclo, Hsub.
Qed.
Lemma ClosedSubst_map l S: ClosedSubst l S Forall (Closed l) (map_to_list S.*2).
Lemma ClosedSubst_map l S: ClosedSubst l S Forall (Closed l) ((map_to_list S).*2).
Proof.
rewrite /ClosedSubst map_Forall_to_list.
remember (map_to_list S) as lS eqn:Heq.
......@@ -280,7 +280,7 @@ Lemma msubst_weaken_2 e S1 S2:
msubst S1 e = msubst S2 e.
Proof.
intros HcloS Hsub Hclosing.
eapply (msubst_weaken_1 _ _ _ (map_to_list S1.*1)); eauto.
eapply (msubst_weaken_1 _ _ _ ((map_to_list S1).*1)); eauto.
- eapply Hclosing=>x. rewrite elem_of_dom.
intros (es&Hlook). apply elem_of_list_fmap.
exists (x, es); split; auto. rewrite elem_of_map_to_list //.
......@@ -581,7 +581,7 @@ Qed.
Lemma msubst_closing_inv_1 S l e:
ClosedSubst [] S
Closed l (msubst S e)
Closed (map_to_list S.*1 ++ l) e.
Closed ((map_to_list S).*1 ++ l) e.
Proof. intros; eapply lsubst_closing_inv_1; eauto using ClosedSubst_map. Qed.
Lemma msubst_closing_inv_2 S x l e:
......
......@@ -125,7 +125,7 @@ Proof.
Qed.
Lemma typ_context_closed_2 Γ e e' ty:
Γ e e' : ty Closed (map_to_list Γ.*1) e Closed (map_to_list Γ.*1) e'.
Γ e e' : ty Closed ((map_to_list Γ).*1) e Closed ((map_to_list Γ).*1) e'.
Proof.
intros Hmap. eapply typ_context_closed_1 in Hmap; eauto.
intros x. rewrite elem_of_dom. intros [ty' Heq].
......
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