Commit e474caaf authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of https://gitlab.mpi-sws.org/iris/iris

parents a3969eb5 3012972e
Pipeline #31485 canceled with stage
in 15 minutes and 13 seconds
...@@ -11,7 +11,7 @@ synopsis: "This is the Coq development of the Iris Project" ...@@ -11,7 +11,7 @@ synopsis: "This is the Coq development of the Iris Project"
depends: [ depends: [
"coq" { (>= "8.9.1" & < "8.13~") | (= "dev") } "coq" { (>= "8.9.1" & < "8.13~") | (= "dev") }
"coq-stdpp" { (= "dev.2020-07-02.1.c8129a37") | (= "dev") } "coq-stdpp" { (= "dev.2020-07-15.1.92dc4869") | (= "dev") }
] ]
build: [make "-j%{jobs}%"] build: [make "-j%{jobs}%"]
......
...@@ -322,8 +322,8 @@ Lemma tac_specialize_assert Δ j (q am neg : bool) js R P1 P2 P1' Q : ...@@ -322,8 +322,8 @@ Lemma tac_specialize_assert Δ j (q am neg : bool) js R P1 P2 P1' Q :
IntoWand q false R P1 P2 IntoWand q false R P1 P2
(if am then AddModal P1' P1 Q else TCEq P1' P1) (if am then AddModal P1' P1 Q else TCEq P1' P1)
match match
''(Δ1,Δ2) envs_split (if neg is true then Right else Left) '(Δ1,Δ2) envs_split (if neg is true then Right else Left)
js (envs_delete true j q Δ); js (envs_delete true j q Δ);
Δ2' envs_app (negb am &&& q &&& env_spatial_is_nil Δ1) (Esnoc Enil j P2) Δ2; Δ2' envs_app (negb am &&& q &&& env_spatial_is_nil Δ1) (Esnoc Enil j P2) Δ2;
Some (Δ1,Δ2') (* does not preserve position of [j] *) Some (Δ1,Δ2') (* does not preserve position of [j] *)
with with
......
...@@ -22,7 +22,7 @@ Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A := ...@@ -22,7 +22,7 @@ Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
Module env_notations. Module env_notations.
Notation "y ≫= f" := (pm_option_bind f y). Notation "y ≫= f" := (pm_option_bind f y).
Notation "x ← y ; z" := (y = λ x, z). Notation "x ← y ; z" := (y = λ x, z).
Notation "' x1 .. xn ← y ; z" := (y = (λ x1, .. (λ xn, z) .. )). Notation "' x1 ← y ; z" := (y = (λ x1, z)).
Notation "Γ !! j" := (env_lookup j Γ). Notation "Γ !! j" := (env_lookup j Γ).
End env_notations. End env_notations.
Import env_notations. Import env_notations.
...@@ -71,7 +71,7 @@ Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) := ...@@ -71,7 +71,7 @@ Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
| Enil => None | Enil => None
| Esnoc Γ j x => | Esnoc Γ j x =>
if ident_beq i j then Some (x,Γ) if ident_beq i j then Some (x,Γ)
else ''(y,Γ') env_lookup_delete i Γ; Some (y, Esnoc Γ' j x) else '(y,Γ') env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
end. end.
Inductive env_Forall2 {A B} (P : A B Prop) : env A env B Prop := Inductive env_Forall2 {A B} (P : A B Prop) : env A env B Prop :=
...@@ -296,7 +296,7 @@ Definition envs_lookup_delete {PROP} (remove_intuitionistic : bool) ...@@ -296,7 +296,7 @@ Definition envs_lookup_delete {PROP} (remove_intuitionistic : bool)
let (Γp,Γs,n) := Δ in let (Γp,Γs,n) := Δ in
match env_lookup_delete i Γp with match env_lookup_delete i Γp with
| Some (P,Γp') => Some (true, P, Envs (if remove_intuitionistic then Γp' else Γp) Γs n) | Some (P,Γp') => Some (true, P, Envs (if remove_intuitionistic then Γp' else Γp) Γs n)
| None => ''(P,Γs') env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n) | None => '(P,Γs') env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
end. end.
Fixpoint envs_lookup_delete_list {PROP} (remove_intuitionistic : bool) Fixpoint envs_lookup_delete_list {PROP} (remove_intuitionistic : bool)
...@@ -304,8 +304,8 @@ Fixpoint envs_lookup_delete_list {PROP} (remove_intuitionistic : bool) ...@@ -304,8 +304,8 @@ Fixpoint envs_lookup_delete_list {PROP} (remove_intuitionistic : bool)
match js with match js with
| [] => Some (true, [], Δ) | [] => Some (true, [], Δ)
| j :: js => | j :: js =>
''(p,P,Δ') envs_lookup_delete remove_intuitionistic j Δ; '(p,P,Δ') envs_lookup_delete remove_intuitionistic j Δ;
''(q,Ps,Δ'') envs_lookup_delete_list remove_intuitionistic js Δ'; '(q,Ps,Δ'') envs_lookup_delete_list remove_intuitionistic js Δ';
Some ((p:bool) &&& q, P :: Ps, Δ'') Some ((p:bool) &&& q, P :: Ps, Δ'')
end. end.
...@@ -352,7 +352,7 @@ Fixpoint envs_split_go {PROP} ...@@ -352,7 +352,7 @@ Fixpoint envs_split_go {PROP}
match js with match js with
| [] => Some (Δ1, Δ2) | [] => Some (Δ1, Δ2)
| j :: js => | j :: js =>
''(p,P,Δ1') envs_lookup_delete true j Δ1; '(p,P,Δ1') envs_lookup_delete true j Δ1;
if p : bool then envs_split_go js Δ1 Δ2 else if p : bool then envs_split_go js Δ1 Δ2 else
envs_split_go js Δ1' (envs_snoc Δ2 false j P) envs_split_go js Δ1' (envs_snoc Δ2 false j P)
end. end.
...@@ -360,7 +360,7 @@ Fixpoint envs_split_go {PROP} ...@@ -360,7 +360,7 @@ Fixpoint envs_split_go {PROP}
if [d = Left] then [result = (hyps named js, remaining hyps)] *) if [d = Left] then [result = (hyps named js, remaining hyps)] *)
Definition envs_split {PROP} (d : direction) Definition envs_split {PROP} (d : direction)
(js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP) := (js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
''(Δ1,Δ2) envs_split_go js Δ (envs_clear_spatial Δ); '(Δ1,Δ2) envs_split_go js Δ (envs_clear_spatial Δ);
if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1). if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
Fixpoint env_to_prop_go {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP := Fixpoint env_to_prop_go {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP :=
...@@ -688,7 +688,7 @@ Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Q ...@@ -688,7 +688,7 @@ Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Q
Lemma envs_lookup_envs_clear_spatial Δ j : Lemma envs_lookup_envs_clear_spatial Δ j :
envs_lookup j (envs_clear_spatial Δ) envs_lookup j (envs_clear_spatial Δ)
= ''(p,P) envs_lookup j Δ; if p : bool then Some (p,P) else None. = '(p,P) envs_lookup j Δ; if p : bool then Some (p,P) else None.
Proof. Proof.
rewrite /envs_lookup /envs_clear_spatial. rewrite /envs_lookup /envs_clear_spatial.
destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto. destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto.
......
...@@ -44,9 +44,9 @@ Fixpoint close_list (k : stack) ...@@ -44,9 +44,9 @@ Fixpoint close_list (k : stack)
| StList :: k => Some (StPat (IList (ps :: pss)) :: k) | StList :: k => Some (StPat (IList (ps :: pss)) :: k)
| StPat pat :: k => close_list k (pat :: ps) pss | StPat pat :: k => close_list k (pat :: ps) pss
| StIntuitionistic :: k => | StIntuitionistic :: k =>
''(p,ps) maybe2 (::) ps; close_list k (IIntuitionistic p :: ps) pss '(p,ps) maybe2 (::) ps; close_list k (IIntuitionistic p :: ps) pss
| StModalElim :: k => | StModalElim :: k =>
''(p,ps) maybe2 (::) ps; close_list k (IModalElim p :: ps) pss '(p,ps) maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
| StBar :: k => close_list k [] (ps :: pss) | StBar :: k => close_list k [] (ps :: pss)
| _ => None | _ => None
end. end.
...@@ -121,9 +121,9 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) := ...@@ -121,9 +121,9 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
match k with match k with
| [] => Some ps | [] => Some ps
| StPat pat :: k => close k (pat :: ps) | StPat pat :: k => close k (pat :: ps)
| StIntuitionistic :: k => ''(p,ps) maybe2 (::) ps; close k (IIntuitionistic p :: ps) | StIntuitionistic :: k => '(p,ps) maybe2 (::) ps; close k (IIntuitionistic p :: ps)
| StSpatial :: k => ''(p,ps) maybe2 (::) ps; close k (ISpatial p :: ps) | StSpatial :: k => '(p,ps) maybe2 (::) ps; close k (ISpatial p :: ps)
| StModalElim :: k => ''(p,ps) maybe2 (::) ps; close k (IModalElim p :: ps) | StModalElim :: k => '(p,ps) maybe2 (::) ps; close k (IModalElim p :: ps)
| _ => None | _ => None
end. end.
......
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