Skip to content
Snippets Groups Projects
Commit b109822a authored by Janno's avatar Janno
Browse files

Broken HB experiment.

parent 962637df
Branches janno/try-HB
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/bi/interface.v
+ 137
− 10
View file @ b109822a
From iris.bi Require Export notation. From iris.bi Require Export notation.
From iris.algebra Require Export ofe. From iris.algebra Require Export ofe.
From HB Require Import structures.
Set Primitive Projections. Set Primitive Projections.
Section bi_mixin. Section bi_mixin.
...@@ -38,14 +39,14 @@ Section bi_mixin. ...@@ -38,14 +39,14 @@ Section bi_mixin.
(** * Axioms for a general BI (logic of bunched implications) *) (** * Axioms for a general BI (logic of bunched implications) *)
(** The following axioms are satisifed by both affine and linear BIs, and BIs (** The following axioms are satisifed by both affine and linear BIs, and BIs *)
that combine both kinds of resources. In particular, we have an "ordered RA" (* that combine both kinds of resources. In particular, we have an "ordered RA" *)
model satisfying all these axioms. For this model, we extend RAs with an (* model satisfying all these axioms. For this model, we extend RAs with an *)
arbitrary partial order, and up-close resources wrt. that order (instead of (* arbitrary partial order, and up-close resources wrt. that order (instead of *)
extension order). We demand composition to be monotone wrt. the order: [x1 ≼ (* extension order). We demand composition to be monotone wrt. the order: [x1 ≼ *)
x2 → x1 ⋅ y ≼ x2 ⋅ y]. We define [emp := λ r, ε ≼ r]; persistently is still (* x2 → x1 ⋅ y ≼ x2 ⋅ y]. We define [emp := λ r, ε ≼ r]; persistently is still *)
defined with the core: [persistently P := λ r, P (core r)]. This is uplcosed (* defined with the core: [persistently P := λ r, P (core r)]. This is uplcosed *)
because the core is monotone. *) (* because the core is monotone. *)
Record BiMixin := { Record BiMixin := {
bi_mixin_entails_po : PreOrder bi_entails; bi_mixin_entails_po : PreOrder bi_entails;
...@@ -67,8 +68,8 @@ Section bi_mixin. ...@@ -67,8 +68,8 @@ Section bi_mixin.
(** Higher-order logic *) (** Higher-order logic *)
bi_mixin_pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝; bi_mixin_pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝;
bi_mixin_pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P; bi_mixin_pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P;
(* This is actually derivable if we assume excluded middle in Coq, (* This is actually derivable if we assume excluded middle in Coq, *)
via [(∀ a, φ a) ∨ (∃ a, ¬φ a)]. *) (* via [(∀ a, φ a) ∨ (∃ a, ¬φ a)]. *)
bi_mixin_pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝; bi_mixin_pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝;
bi_mixin_and_elim_l P Q : P ∧ Q ⊢ P; bi_mixin_and_elim_l P Q : P ∧ Q ⊢ P;
...@@ -148,6 +149,132 @@ Section bi_mixin. ...@@ -148,6 +149,132 @@ Section bi_mixin.
}. }.
End bi_mixin. End bi_mixin.
Unset Printing Notations.
Set Printing Implicit.
HB.structure Definition TYPE := { A of True }.
HB.mixin Record Bi_of_TYPE (PROP : Type) := {
bi_dist :> Dist PROP;
bi_equiv :> Equiv PROP;
bi_entails : PROP → PROP → Prop;
bi_emp : PROP;
bi_pure : Prop → PROP;
bi_and : PROP → PROP → PROP;
bi_or : PROP → PROP → PROP;
bi_impl : PROP → PROP → PROP;
bi_forall : ∀ A : Type, (A → PROP) → PROP;
bi_exist : ∀ A : Type, (A → PROP) → PROP;
bi_sep:PROP → PROP → PROP;
bi_wand : PROP → PROP → PROP;
bi_persistently : PROP → PROP;
bi_mixin_entails_po : PreOrder bi_entails;
bi_mixin_equiv_spec : forall P Q : PROP, iff (@equiv PROP bi_equiv P Q) (and (bi_entails P Q) (bi_entails Q P));
bi_mixin_pure_ne : forall n : nat, @Proper (forall _ : Prop, PROP) (@respectful Prop PROP iff (@dist PROP bi_dist n)) bi_pure;
bi_mixin_and_ne : forall n : nat,
@Proper (forall (_ : PROP) (_ : PROP), PROP)
(@respectful PROP (forall _ : PROP, PROP) (@dist PROP bi_dist n) (@respectful PROP PROP (@dist PROP bi_dist n) (@dist PROP bi_dist n))) bi_and;
bi_mixin_or_ne : forall n : nat,
@Proper (forall (_ : PROP) (_ : PROP), PROP)
(@respectful PROP (forall _ : PROP, PROP) (@dist PROP bi_dist n) (@respectful PROP PROP (@dist PROP bi_dist n) (@dist PROP bi_dist n))) bi_or;
bi_mixin_impl_ne : forall n : nat,
@Proper (forall (_ : PROP) (_ : PROP), PROP)
(@respectful PROP (forall _ : PROP, PROP) (@dist PROP bi_dist n) (@respectful PROP PROP (@dist PROP bi_dist n) (@dist PROP bi_dist n))) bi_impl;
bi_mixin_forall_ne : forall (A : Type) (n : nat),
@Proper (forall _ : forall _ : A, PROP, PROP)
(@respectful (forall _ : A, PROP) PROP (@pointwise_relation A PROP (@dist PROP bi_dist n)) (@dist PROP bi_dist n))
(bi_forall A);
bi_mixin_exist_ne : forall (A : Type) (n : nat),
@Proper (forall _ : forall _ : A, PROP, PROP)
(@respectful (forall _ : A, PROP) PROP (@pointwise_relation A PROP (@dist PROP bi_dist n)) (@dist PROP bi_dist n))
(bi_exist A);
bi_mixin_sep_ne : forall n : nat,
@Proper (forall (_ : PROP) (_ : PROP), PROP)
(@respectful PROP (forall _ : PROP, PROP) (@dist PROP bi_dist n) (@respectful PROP PROP (@dist PROP bi_dist n) (@dist PROP bi_dist n))) bi_sep;
bi_mixin_wand_ne : forall n : nat,
@Proper (forall (_ : PROP) (_ : PROP), PROP)
(@respectful PROP (forall _ : PROP, PROP) (@dist PROP bi_dist n) (@respectful PROP PROP (@dist PROP bi_dist n) (@dist PROP bi_dist n))) bi_wand;
bi_mixin_persistently_ne : forall n : nat, @Proper (forall _ : PROP, PROP) (@respectful PROP PROP (@dist PROP bi_dist n) (@dist PROP bi_dist n)) bi_persistently;
bi_mixin_pure_intro : forall (φ : Prop) (P : PROP) (_ : φ), bi_entails P (bi_pure φ);
bi_mixin_pure_elim' : forall (φ : Prop) (P : PROP) (_ : forall _ : φ, bi_entails (bi_pure True) P), bi_entails (bi_pure φ) P;
bi_mixin_pure_forall_2 : forall (A : Type) (φ : forall _ : A, Prop), bi_entails (bi_forall A (fun a : A => bi_pure (φ a))) (bi_pure (forall a : A, φ a));
bi_mixin_and_elim_l : forall P Q : PROP, bi_entails (bi_and P Q) P;
bi_mixin_and_elim_r : forall P Q : PROP, bi_entails (bi_and P Q) Q;
bi_mixin_and_intro : forall (P Q R : PROP) (_ : bi_entails P Q) (_ : bi_entails P R), bi_entails P (bi_and Q R);
bi_mixin_or_intro_l : forall P Q : PROP, bi_entails P (bi_or P Q);
bi_mixin_or_intro_r : forall P Q : PROP, bi_entails Q (bi_or P Q);
bi_mixin_or_elim : forall (P Q R : PROP) (_ : bi_entails P R) (_ : bi_entails Q R), bi_entails (bi_or P Q) R;
bi_mixin_impl_intro_r : forall (P Q R : PROP) (_ : bi_entails (bi_and P Q) R), bi_entails P (bi_impl Q R);
bi_mixin_impl_elim_l' : forall (P Q R : PROP) (_ : bi_entails P (bi_impl Q R)), bi_entails (bi_and P Q) R;
bi_mixin_forall_intro : forall (A : Type) (P : PROP) (Ψ : forall _ : A, PROP) (_ : forall a : A, bi_entails P (Ψ a)),
bi_entails P (bi_forall A (fun a : A => Ψ a));
bi_mixin_forall_elim : forall (A : Type) (Ψ : forall _ : A, PROP) (a : A), bi_entails (bi_forall A (fun a0 : A => Ψ a0)) (Ψ a);
bi_mixin_exist_intro : forall (A : Type) (Ψ : forall _ : A, PROP) (a : A), bi_entails (Ψ a) (bi_exist A (fun a0 : A => Ψ a0));
bi_mixin_exist_elim : forall (A : Type) (Φ : forall _ : A, PROP) (Q : PROP) (_ : forall a : A, bi_entails (Φ a) Q),
bi_entails (bi_exist A (fun a : A => Φ a)) Q;
bi_mixin_sep_mono : forall (P P' Q Q' : PROP) (_ : bi_entails P Q) (_ : bi_entails P' Q'), bi_entails (bi_sep P P') (bi_sep Q Q');
bi_mixin_emp_sep_1 : forall P : PROP, bi_entails P (bi_sep bi_emp P);
bi_mixin_emp_sep_2 : forall P : PROP, bi_entails (bi_sep bi_emp P) P;
bi_mixin_sep_comm' : forall P Q : PROP, bi_entails (bi_sep P Q) (bi_sep Q P);
bi_mixin_sep_assoc' : forall P Q R : PROP, bi_entails (bi_sep (bi_sep P Q) R) (bi_sep P (bi_sep Q R));
bi_mixin_wand_intro_r : forall (P Q R : PROP) (_ : bi_entails (bi_sep P Q) R), bi_entails P (bi_wand Q R);
bi_mixin_wand_elim_l' : forall (P Q R : PROP) (_ : bi_entails P (bi_wand Q R)), bi_entails (bi_sep P Q) R;
bi_mixin_persistently_mono : forall (P Q : PROP) (_ : bi_entails P Q), bi_entails (bi_persistently P) (bi_persistently Q);
bi_mixin_persistently_idemp_2 : forall P : PROP, bi_entails (bi_persistently P) (bi_persistently (bi_persistently P));
bi_mixin_persistently_emp_2 : bi_entails bi_emp (bi_persistently bi_emp);
bi_mixin_persistently_forall_2 : forall (A : Type) (Ψ : forall _ : A, PROP),
bi_entails (bi_forall A (fun a : A => bi_persistently (Ψ a))) (bi_persistently (bi_forall A (fun a : A => Ψ a)));
bi_mixin_persistently_exist_1 : forall (A : Type) (Ψ : forall _ : A, PROP),
bi_entails (bi_persistently (bi_exist A (fun a : A => Ψ a))) (bi_exist A (fun a : A => bi_persistently (Ψ a)));
bi_mixin_persistently_absorbing : forall P Q : PROP, bi_entails (bi_sep (bi_persistently P) Q) (bi_persistently P);
bi_mixin_persistently_and_sep_elim : forall P Q : PROP, bi_entails (bi_and (bi_persistently P) Q) (bi_sep P Q)
}.
HB.structure Definition bi := { A of Bi_of_TYPE A }.
Set Debug Unification.
Unset Printing All.
Unset Printing Notations.
From Coq Require Import Strings.String.
Import StringSyntax.
Import Strings.Ascii.
Open Scope string.
Fail HB.mixin Record Sbi_of_Bi PROP of bi PROP := {
(* (H : Dist PROP) (bi_entails : PROP → PROP → Prop) (bi_pure : Prop → PROP) (bi_or bi_impl : PROP → PROP → PROP) *)
(* (bi_forall bi_exist : ∀ A : Type, (A → PROP) → PROP) (bi_sep : PROP → PROP → PROP) (bi_persistently : PROP → PROP) *)
sbi_later : PROP → PROP;
sbi_internal_eq : ∀ T : ofeT, ofe_car T → ofe_car T → PROP;
(* sbi_mixin_later_contractive : forall n : nat, @Proper (forall _ : PROP, PROP) (@respectful PROP PROP (@dist_later PROP (bi_dist) n) (@dist PROP (bi_dist) n)) sbi_later; *)
(* sbi_mixin_internal_eq_ne : forall (A : ofeT) (n : nat), *)
(* @Proper (forall (_ : ofe_car A) (_ : ofe_car A), PROP) *)
(* (@respectful (ofe_car A) (forall _ : A, PROP) (@dist (ofe_car A) (ofe_dist A) n) (@respectful (ofe_car A) PROP (@dist (ofe_car A) (ofe_dist A) n) (@dist PROP bi_dist n))) *)
(* (sbi_internal_eq A); *)
(* sbi_mixin_internal_eq_refl : forall (A : ofeT) (P : PROP) (a : ofe_car A), bi_entails P (sbi_internal_eq A a a); *)
(* sbi_mixin_internal_eq_rewrite : forall (A : ofeT) (a b : A) (Ψ : forall _ : A, PROP) *)
(* (_ : forall n : nat, @Proper (forall _ : A, PROP) (@respectful A PROP (@dist A (ofe_dist A) n) (@dist PROP H n)) Ψ), *)
(* bi_entails (sbi_internal_eq A a b) (bi_impl (Ψ a) (Ψ b)); *)
(* sbi_mixin_fun_ext : forall (A : Type) (B : forall _ : A, ofeT) (f g : @discrete_fun A B), *)
(* bi_entails (bi_forall A (fun x : A => sbi_internal_eq (B x) (f x) (g x))) (sbi_internal_eq (@discrete_funO A B) f g); *)
(* sbi_mixin_sig_eq : forall (A : ofeT) (P : forall _ : A, Prop) (x y : @sig A P), *)
(* bi_entails (sbi_internal_eq A (@proj1_sig A P x) (@proj1_sig A P y)) (sbi_internal_eq (@sigO A P) x y); *)
(* sbi_mixin_discrete_eq_1 : forall (A : ofeT) (a b : A) (_ : @Discrete A a), bi_entails (sbi_internal_eq A a b) (bi_pure (@equiv A (ofe_equiv A) a b)); *)
(* sbi_mixin_later_eq_1 : forall (A : ofeT) (x y : A), bi_entails (sbi_internal_eq (laterO A) (@Next A x) (@Next A y)) (sbi_later (sbi_internal_eq A x y)); *)
(* sbi_mixin_later_eq_2 : forall (A : ofeT) (x y : A), bi_entails (sbi_later (sbi_internal_eq A x y)) (sbi_internal_eq (laterO A) (@Next A x) (@Next A y)); *)
(* sbi_mixin_later_mono : forall (P Q : PROP) (_ : bi_entails P Q), bi_entails (sbi_later P) (sbi_later Q); *)
sbi_mixin_later_intro : forall P : PROP, bi_entails P (sbi_later P);
(* sbi_mixin_later_forall_2 : forall (A : Type) (Φ : forall _ : A, PROP), *)
(* bi_entails (bi_forall A (fun a : A => sbi_later (Φ a))) (sbi_later (bi_forall A (fun a : A => Φ a))); *)
(* sbi_mixin_later_exist_false : forall (A : Type) (Φ : forall _ : A, PROP), *)
(* bi_entails (sbi_later (bi_exist A (fun a : A => Φ a))) *)
(* (bi_or (sbi_later (bi_pure False)) (bi_exist A (fun a : A => sbi_later (Φ a)))); *)
(* sbi_mixin_later_sep_1 : forall P Q : PROP, bi_entails (sbi_later (bi_sep P Q)) (bi_sep (sbi_later P) (sbi_later Q)); *)
(* sbi_mixin_later_sep_2 : forall P Q : PROP, bi_entails (bi_sep (sbi_later P) (sbi_later Q)) (sbi_later (bi_sep P Q)); *)
(* sbi_mixin_later_persistently_1 : forall P : PROP, bi_entails (sbi_later (bi_persistently P)) (bi_persistently (sbi_later P)); *)
(* sbi_mixin_later_persistently_2 : forall P : PROP, bi_entails (bi_persistently (sbi_later P)) (sbi_later (bi_persistently P)); *)
(* sbi_mixin_later_false_em : forall P : PROP, bi_entails (sbi_later P) (bi_or (sbi_later (bi_pure False)) (bi_impl (sbi_later (bi_pure False)) P)) *)
}.
Structure bi := Bi { Structure bi := Bi {
bi_car :> Type; bi_car :> Type;
bi_dist : Dist bi_car; bi_dist : Dist bi_car;
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment