Commit c83251df authored by Ralf Jung's avatar Ralf Jung

Merge branch 'coq-8.6' into 'master'

Coq 8.6

Once we make Coq 8.6 mandatory, we should merge this.

@robbertkrebbers I removed your `v8.6` branch (last commit: <https://gitlab.mpi-sws.org/FP/iris-coq/commit/b144f52f94c14ee5da1412b73a2d49981f9850b8>).  For once, it had the wrong name (you're not talking about Iris 8.6, are you? ;-); also, all it was doing was working around a bug in Coq that has since been fixed there.

See merge request !30
parents 8706664d b00ace04
......@@ -202,9 +202,9 @@ Qed.
Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A A)
`{!Contractive f} : A := compl (fixpoint_chain f).
Definition fixpoint_aux : { x | x = @fixpoint_def }. by eexists. Qed.
Definition fixpoint {A AC AiH} f {Hf} := proj1_sig fixpoint_aux A AC AiH f Hf.
Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux.
Definition fixpoint_aux : seal (@fixpoint_def). by eexists. Qed.
Definition fixpoint {A AC AiH} f {Hf} := unseal fixpoint_aux A AC AiH f Hf.
Definition fixpoint_eq : @fixpoint = @fixpoint_def := seal_eq fixpoint_aux.
Section fixpoint.
Context `{Cofe A, Inhabited A} (f : A A) `{!Contractive f}.
......
......@@ -33,6 +33,7 @@ Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P.
Arguments timelessP {_} _ {_}.
Class PersistentP {M} (P : uPred M) := persistentP : P P.
Hint Mode PersistentP - ! : typeclass_instances.
Arguments persistentP {_} _ {_}.
Module uPred.
......
......@@ -11,9 +11,9 @@ Import uPred.
Program Definition fupd_def `{invG Σ}
(E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
(wsat ownE E1 == (wsat ownE E2 P))%I.
Definition fupd_aux : { x | x = @fupd_def }. by eexists. Qed.
Definition fupd := proj1_sig fupd_aux.
Definition fupd_eq : @fupd = @fupd_def := proj2_sig fupd_aux.
Definition fupd_aux : seal (@fupd_def). by eexists. Qed.
Definition fupd := unseal fupd_aux.
Definition fupd_eq : @fupd = @fupd_def := seal_eq fupd_aux.
Arguments fupd {_ _} _ _ _%I.
Instance: Params (@fupd) 4.
......
......@@ -34,9 +34,9 @@ Section definitions.
Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
own gen_heap_name ( {[ l := (q, to_agree (v : leibnizC V)) ]}).
Definition mapsto_aux : { x | x = @mapsto_def }. by eexists. Qed.
Definition mapsto := proj1_sig mapsto_aux.
Definition mapsto_eq : @mapsto = @mapsto_def := proj2_sig mapsto_aux.
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
Definition mapsto := unseal mapsto_aux.
Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
End definitions.
Local Notation "l ↦{ q } v" := (mapsto l q v)
......
......@@ -8,9 +8,9 @@ Import uPred.
(** Derived forms and lemmas about them. *)
Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i N ownI i P)%I.
Definition inv_aux : { x | x = @inv_def }. by eexists. Qed.
Definition inv {Σ i} := proj1_sig inv_aux Σ i.
Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux.
Definition inv_aux : seal (@inv_def). by eexists. Qed.
Definition inv {Σ i} := unseal inv_aux Σ i.
Definition inv_eq : @inv = @inv_def := seal_eq inv_aux.
Instance: Params (@inv) 3.
Typeclasses Opaque inv.
......
......@@ -11,14 +11,14 @@ Definition nroot : namespace := nil.
Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace :=
encode x :: N.
Definition ndot_aux : { x | x = @ndot_def }. by eexists. Qed.
Definition ndot {A A_dec A_count}:= proj1_sig ndot_aux A A_dec A_count.
Definition ndot_eq : @ndot = @ndot_def := proj2_sig ndot_aux.
Definition ndot_aux : seal (@ndot_def). by eexists. Qed.
Definition ndot {A A_dec A_count}:= unseal ndot_aux A A_dec A_count.
Definition ndot_eq : @ndot = @ndot_def := seal_eq ndot_aux.
Definition nclose_def (N : namespace) : coPset := coPset_suffixes (encode N).
Definition nclose_aux : { x | x = @nclose_def }. by eexists. Qed.
Instance nclose : UpClose namespace coPset := proj1_sig nclose_aux.
Definition nclose_eq : @nclose = @nclose_def := proj2_sig nclose_aux.
Definition nclose_aux : seal (@nclose_def). by eexists. Qed.
Instance nclose : UpClose namespace coPset := unseal nclose_aux.
Definition nclose_eq : @nclose = @nclose_def := seal_eq nclose_aux.
Notation "N .@ x" := (ndot N x)
(at level 19, left associativity, format "N .@ x") : C_scope.
......
......@@ -54,9 +54,9 @@ Instance: Params (@iRes_singleton) 4.
Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
uPred_ownM (iRes_singleton γ a).
Definition own_aux : { x | x = @own_def }. by eexists. Qed.
Definition own {Σ A i} := proj1_sig own_aux Σ A i.
Definition own_eq : @own = @own_def := proj2_sig own_aux.
Definition own_aux : seal (@own_def). by eexists. Qed.
Definition own {Σ A i} := unseal own_aux Σ A i.
Definition own_eq : @own = @own_def := seal_eq own_aux.
Instance: Params (@own) 4.
Typeclasses Opaque own.
......@@ -104,7 +104,7 @@ Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 - own γ a2 - own γ a3 - (a1 a2 a3).
Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
Lemma own_valid_r γ a : own γ a own γ a a.
Proof. apply (uPred.always_entails_r _ _). apply own_valid. Qed.
Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a a own γ a.
Proof. by rewrite comm -own_valid_r. Qed.
......
......@@ -9,26 +9,26 @@ Local Hint Extern 10 (_ ≤ _) => omega.
Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
{| uPred_holds n x := φ |}.
Solve Obligations with done.
Definition uPred_pure_aux : { x | x = @uPred_pure_def }. by eexists. Qed.
Definition uPred_pure {M} := proj1_sig uPred_pure_aux M.
Definition uPred_pure_aux : seal (@uPred_pure_def). by eexists. Qed.
Definition uPred_pure {M} := unseal uPred_pure_aux M.
Definition uPred_pure_eq :
@uPred_pure = @uPred_pure_def := proj2_sig uPred_pure_aux.
@uPred_pure = @uPred_pure_def := seal_eq uPred_pure_aux.
Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_pure True).
Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := P n x Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_and_aux : { x | x = @uPred_and_def }. by eexists. Qed.
Definition uPred_and {M} := proj1_sig uPred_and_aux M.
Definition uPred_and_eq: @uPred_and = @uPred_and_def := proj2_sig uPred_and_aux.
Definition uPred_and_aux : seal (@uPred_and_def). by eexists. Qed.
Definition uPred_and {M} := unseal uPred_and_aux M.
Definition uPred_and_eq: @uPred_and = @uPred_and_def := seal_eq uPred_and_aux.
Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := P n x Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_or_aux : { x | x = @uPred_or_def }. by eexists. Qed.
Definition uPred_or {M} := proj1_sig uPred_or_aux M.
Definition uPred_or_eq: @uPred_or = @uPred_or_def := proj2_sig uPred_or_aux.
Definition uPred_or_aux : seal (@uPred_or_def). by eexists. Qed.
Definition uPred_or {M} := unseal uPred_or_aux M.
Definition uPred_or_eq: @uPred_or = @uPred_or_def := seal_eq uPred_or_aux.
Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := n' x',
......@@ -39,33 +39,33 @@ Next Obligation.
eapply HPQ; auto. exists (x2 x4); by rewrite assoc.
Qed.
Next Obligation. intros M P Q [|n1] [|n2] x; auto with lia. Qed.
Definition uPred_impl_aux : { x | x = @uPred_impl_def }. by eexists. Qed.
Definition uPred_impl {M} := proj1_sig uPred_impl_aux M.
Definition uPred_impl_aux : seal (@uPred_impl_def). by eexists. Qed.
Definition uPred_impl {M} := unseal uPred_impl_aux M.
Definition uPred_impl_eq :
@uPred_impl = @uPred_impl_def := proj2_sig uPred_impl_aux.
@uPred_impl = @uPred_impl_def := seal_eq uPred_impl_aux.
Program Definition uPred_forall_def {M A} (Ψ : A uPred M) : uPred M :=
{| uPred_holds n x := a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_forall_aux : { x | x = @uPred_forall_def }. by eexists. Qed.
Definition uPred_forall {M A} := proj1_sig uPred_forall_aux M A.
Definition uPred_forall_aux : seal (@uPred_forall_def). by eexists. Qed.
Definition uPred_forall {M A} := unseal uPred_forall_aux M A.
Definition uPred_forall_eq :
@uPred_forall = @uPred_forall_def := proj2_sig uPred_forall_aux.
@uPred_forall = @uPred_forall_def := seal_eq uPred_forall_aux.
Program Definition uPred_exist_def {M A} (Ψ : A uPred M) : uPred M :=
{| uPred_holds n x := a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_exist_aux : { x | x = @uPred_exist_def }. by eexists. Qed.
Definition uPred_exist {M A} := proj1_sig uPred_exist_aux M A.
Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := proj2_sig uPred_exist_aux.
Definition uPred_exist_aux : seal (@uPred_exist_def). by eexists. Qed.
Definition uPred_exist {M A} := unseal uPred_exist_aux M A.
Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := seal_eq uPred_exist_aux.
Program Definition uPred_internal_eq_def {M} {A : ofeT} (a1 a2 : A) : uPred M :=
{| uPred_holds n x := a1 {n} a2 |}.
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
Definition uPred_internal_eq_aux : { x | x = @uPred_internal_eq_def }. by eexists. Qed.
Definition uPred_internal_eq {M A} := proj1_sig uPred_internal_eq_aux M A.
Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). by eexists. Qed.
Definition uPred_internal_eq {M A} := unseal uPred_internal_eq_aux M A.
Definition uPred_internal_eq_eq:
@uPred_internal_eq = @uPred_internal_eq_def := proj2_sig uPred_internal_eq_aux.
@uPred_internal_eq = @uPred_internal_eq_def := seal_eq uPred_internal_eq_aux.
Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := x1 x2, x {n} x1 x2 P n x1 Q n x2 |}.
......@@ -79,9 +79,9 @@ Next Obligation.
exists x1, x2; cofe_subst; split_and!;
eauto using dist_le, uPred_closed, cmra_validN_op_l, cmra_validN_op_r.
Qed.
Definition uPred_sep_aux : { x | x = @uPred_sep_def }. by eexists. Qed.
Definition uPred_sep {M} := proj1_sig uPred_sep_aux M.
Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := proj2_sig uPred_sep_aux.
Definition uPred_sep_aux : seal (@uPred_sep_def). by eexists. Qed.
Definition uPred_sep {M} := unseal uPred_sep_aux M.
Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := seal_eq uPred_sep_aux.
Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := n' x',
......@@ -92,10 +92,10 @@ Next Obligation.
eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
Qed.
Next Obligation. naive_solver. Qed.
Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed.
Definition uPred_wand {M} := proj1_sig uPred_wand_aux M.
Definition uPred_wand_aux : seal (@uPred_wand_def). by eexists. Qed.
Definition uPred_wand {M} := unseal uPred_wand_aux M.
Definition uPred_wand_eq :
@uPred_wand = @uPred_wand_def := proj2_sig uPred_wand_aux.
@uPred_wand = @uPred_wand_def := seal_eq uPred_wand_aux.
Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n (core x) |}.
......@@ -103,10 +103,10 @@ Next Obligation.
intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
Qed.
Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
Definition uPred_always {M} := proj1_sig uPred_always_aux M.
Definition uPred_always_aux : seal (@uPred_always_def). by eexists. Qed.
Definition uPred_always {M} := unseal uPred_always_aux M.
Definition uPred_always_eq :
@uPred_always = @uPred_always_def := proj2_sig uPred_always_aux.
@uPred_always = @uPred_always_def := seal_eq uPred_always_aux.
Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
......@@ -116,10 +116,10 @@ Qed.
Next Obligation.
intros M P [|n1] [|n2] x; eauto using uPred_closed, cmra_validN_S with lia.
Qed.
Definition uPred_later_aux : { x | x = @uPred_later_def }. by eexists. Qed.
Definition uPred_later {M} := proj1_sig uPred_later_aux M.
Definition uPred_later_aux : seal (@uPred_later_def). by eexists. Qed.
Definition uPred_later {M} := unseal uPred_later_aux M.
Definition uPred_later_eq :
@uPred_later = @uPred_later_def := proj2_sig uPred_later_aux.
@uPred_later = @uPred_later_def := seal_eq uPred_later_aux.
Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M :=
{| uPred_holds n x := a {n} x |}.
......@@ -128,18 +128,18 @@ Next Obligation.
exists (a' x2). by rewrite (assoc op) Hx1.
Qed.
Next Obligation. naive_solver eauto using cmra_includedN_le. Qed.
Definition uPred_ownM_aux : { x | x = @uPred_ownM_def }. by eexists. Qed.
Definition uPred_ownM {M} := proj1_sig uPred_ownM_aux M.
Definition uPred_ownM_aux : seal (@uPred_ownM_def). by eexists. Qed.
Definition uPred_ownM {M} := unseal uPred_ownM_aux M.
Definition uPred_ownM_eq :
@uPred_ownM = @uPred_ownM_def := proj2_sig uPred_ownM_aux.
@uPred_ownM = @uPred_ownM_def := seal_eq uPred_ownM_aux.
Program Definition uPred_cmra_valid_def {M} {A : cmraT} (a : A) : uPred M :=
{| uPred_holds n x := {n} a |}.
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
Definition uPred_cmra_valid_aux : { x | x = @uPred_cmra_valid_def }. by eexists. Qed.
Definition uPred_cmra_valid {M A} := proj1_sig uPred_cmra_valid_aux M A.
Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def). by eexists. Qed.
Definition uPred_cmra_valid {M A} := unseal uPred_cmra_valid_aux M A.
Definition uPred_cmra_valid_eq :
@uPred_cmra_valid = @uPred_cmra_valid_def := proj2_sig uPred_cmra_valid_aux.
@uPred_cmra_valid = @uPred_cmra_valid_def := seal_eq uPred_cmra_valid_aux.
Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
{| uPred_holds n x := k yf,
......@@ -152,9 +152,9 @@ Next Obligation.
apply uPred_mono with x'; eauto using cmra_includedN_l.
Qed.
Next Obligation. naive_solver. Qed.
Definition uPred_bupd_aux : { x | x = @uPred_bupd_def }. by eexists. Qed.
Definition uPred_bupd {M} := proj1_sig uPred_bupd_aux M.
Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := proj2_sig uPred_bupd_aux.
Definition uPred_bupd_aux : seal (@uPred_bupd_def). by eexists. Qed.
Definition uPred_bupd {M} := unseal uPred_bupd_aux M.
Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := seal_eq uPred_bupd_aux.
(* Latest notation *)
Notation "'⌜' φ '⌝'" := (uPred_pure φ%C%type)
......@@ -194,11 +194,11 @@ Notation "P -∗ Q" := (P ⊢ Q)
(at level 99, Q at level 200, right associativity) : C_scope.
Module uPred.
Definition unseal :=
Definition unseal_eqs :=
(uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq, uPred_bupd_eq).
Ltac unseal := rewrite !unseal /=.
Ltac unseal := rewrite !unseal_eqs /=.
Section primitive.
Context {M : ucmraT}.
......
......@@ -14,6 +14,13 @@ Export ListNotations.
From Coq.Program Require Export Basics Syntax.
Obligation Tactic := idtac.
(** Sealing off definitions *)
Set Primitive Projections.
Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
Arguments unseal {_ _} _.
Arguments seal_eq {_ _} _.
Unset Primitive Projections.
(** Throughout this development we use [C_scope] for all general purpose
notations that do not belong to a more specific scope. *)
Delimit Scope C_scope with C.
......
......@@ -31,9 +31,9 @@ Qed.
Definition wp_def `{irisG Λ Σ} :
coPset expr Λ (val Λ iProp Σ) iProp Σ := fixpoint wp_pre.
Definition wp_aux : { x | x = @wp_def }. by eexists. Qed.
Definition wp := proj1_sig wp_aux.
Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux.
Definition wp_aux : seal (@wp_def). by eexists. Qed.
Definition wp := unseal wp_aux.
Definition wp_eq : @wp = @wp_def := seal_eq wp_aux.
Arguments wp {_ _ _} _ _%E _.
Instance: Params (@wp) 5.
......
......@@ -7,22 +7,22 @@ Arguments Envs _ _%proof_scope _%proof_scope.
Arguments Enil {_}.
Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
Notation "​" := Enil (format "​") : proof_scope.
Notation H : P" := (Esnoc Γ H P)
Notation "​" := Enil (format "​", only printing) : proof_scope.
Notation "Γ H : P" := (Esnoc Γ H P)
(at level 1, P at level 200,
left associativity, format ​ H : P '//'") : proof_scope.
left associativity, format H : P '//'", only printing) : proof_scope.
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(of_envs (Envs Γ Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'") :
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
C_scope.
Notation "Δ '--------------------------------------' ∗ Q" :=
(of_envs (Envs Enil Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Δ '--------------------------------------' ∗ '//' Q '//'") : C_scope.
format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.
Notation "Γ '--------------------------------------' □ Q" :=
(of_envs (Envs Γ Enil) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Q '//'") : C_scope.
format "Γ '--------------------------------------' □ '//' Q '//'", only printing) : C_scope.
Notation "​​ Q" := (of_envs (Envs Enil Enil) Q%I)
(at level 1, Q at level 200, format "​​ Q") : C_scope.
(at level 1, Q at level 200, format "​​ Q", only printing) : C_scope.
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