Unverified Commit ad25eb87 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Work around #461: Revert bi.telescope changes

parent de41b20f
Pipeline #66020 passed with stage
in 15 minutes and 29 seconds
...@@ -6,10 +6,10 @@ Import bi. ...@@ -6,10 +6,10 @@ Import bi.
(* This cannot import the proofmode because it is imported by the proofmode! *) (* This cannot import the proofmode because it is imported by the proofmode! *)
(** Telescopic quantifiers *) (** Telescopic quantifiers *)
Definition bi_texist {PROP : bi} {TT : tele@{Quant}} (Ψ : TT PROP) : PROP := Definition bi_texist {PROP : bi} {TT : tele} (Ψ : TT PROP) : PROP :=
tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ). tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ).
Global Arguments bi_texist {_ !_} _ /. Global Arguments bi_texist {_ !_} _ /.
Definition bi_tforall {PROP : bi} {TT : tele@{Quant}} (Ψ : TT PROP) : PROP := Definition bi_tforall {PROP : bi} {TT : tele} (Ψ : TT PROP) : PROP :=
tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ). tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ).
Global Arguments bi_tforall {_ !_} _ /. Global Arguments bi_tforall {_ !_} _ /.
...@@ -21,7 +21,7 @@ Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) .. ...@@ -21,7 +21,7 @@ Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) ..
format "∀.. x .. y , P") : bi_scope. format "∀.. x .. y , P") : bi_scope.
Section telescopes. Section telescopes.
Context {PROP : bi} {TT : tele@{Quant}}. Context {PROP : bi} {TT : tele}.
Implicit Types Ψ : TT PROP. Implicit Types Ψ : TT PROP.
Lemma bi_tforall_forall Ψ : bi_tforall Ψ bi_forall Ψ. Lemma bi_tforall_forall Ψ : bi_tforall Ψ bi_forall Ψ.
...@@ -34,7 +34,7 @@ Section telescopes. ...@@ -34,7 +34,7 @@ Section telescopes.
- simpl. apply (anti_symm _); apply forall_intro; intros a. - simpl. apply (anti_symm _); apply forall_intro; intros a.
+ rewrite /= -IH. apply forall_intro; intros p. + rewrite /= -IH. apply forall_intro; intros p.
by rewrite (forall_elim (TargS a p)). by rewrite (forall_elim (TargS a p)).
+ destruct a=> /=. + move/tele_arg_inv : (a) => [x [pf ->]] {a} /=.
setoid_rewrite <- IH. setoid_rewrite <- IH.
rewrite 2!forall_elim. done. rewrite 2!forall_elim. done.
Qed. Qed.
...@@ -47,7 +47,7 @@ Section telescopes. ...@@ -47,7 +47,7 @@ Section telescopes.
rewrite (tele_arg_O_inv p) //. rewrite (tele_arg_O_inv p) //.
+ by rewrite -(exist_intro TargO). + by rewrite -(exist_intro TargO).
- simpl. apply (anti_symm _); apply exist_elim. - simpl. apply (anti_symm _); apply exist_elim.
+ intros p. destruct p => /=. + intros p. move/tele_arg_inv: (p) => [x [pf ->]] {p} /=.
by rewrite -exist_intro -IH -exist_intro. by rewrite -exist_intro -IH -exist_intro.
+ intros x. + intros x.
rewrite /= -IH. apply exist_elim; intros p. rewrite /= -IH. apply exist_elim; intros p.
......
Require Import stdpp.coPset.
Require Import iris.bi.telescopes.
Require Import iris.bi.lib.atomic.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic. From iris.program_logic Require Export atomic.
From iris.heap_lang Require Import proofmode notation atomic_heap. From iris.heap_lang Require Import proofmode notation atomic_heap.
...@@ -5,6 +8,18 @@ From iris.prelude Require Import options. ...@@ -5,6 +8,18 @@ From iris.prelude Require Import options.
Unset Mangle Names. Unset Mangle Names.
Section definition.
Context `{BiFUpd PROP} {TA TB : tele} (Eo Ei : coPset).
Definition AU_succeed (TA TB : tele) : Prop :=
(α : TA PROP) (β Φ : TA TB PROP),
atomic_update Eo Ei α β Φ.
Definition AU_fail : Prop :=
(TA TB : tele) (α : TA PROP) (β Φ : TA TB PROP),
atomic_update Eo Ei α β Φ.
End definition.
Section tests. Section tests.
Context `{!heapGS Σ} {aheap: atomic_heap Σ}. Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
Import atomic_heap.notation. Import atomic_heap.notation.
......
Supports Markdown
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