From f7d78857b30263d8533bcb1f3b7740771b073632 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 14 Jun 2023 10:18:43 +0200 Subject: [PATCH] Ongoing experiment with Iris hierarchy --- examples/IrisHierarchy/minimal.v | 233 ++++++++++++++++++++++++++++++ examples/IrisHierarchy/minimal2.v | 28 ++++ examples/IrisHierarchy/minimal3.v | 27 ++++ examples/IrisHierarchy/minimal4.v | 34 +++++ 4 files changed, 322 insertions(+) create mode 100644 examples/IrisHierarchy/minimal.v create mode 100644 examples/IrisHierarchy/minimal2.v create mode 100644 examples/IrisHierarchy/minimal3.v create mode 100644 examples/IrisHierarchy/minimal4.v diff --git a/examples/IrisHierarchy/minimal.v b/examples/IrisHierarchy/minimal.v new file mode 100644 index 000000000..24607cad5 --- /dev/null +++ b/examples/IrisHierarchy/minimal.v @@ -0,0 +1,233 @@ +From Coq Require Import ssreflect ssrfun. +From HB Require Import structures. +From Coq Require Import List Relations Morphisms. + +HB.mixin Record isSetoid A := { + equiv : relation A; + equivP : Equivalence equiv +}. +#[short(type="setoid")] +HB.structure Definition Setoid := {A of isSetoid A}. +#[global] Existing Instance equivP. + +HB.mixin Record isFoo A := {}. +HB.structure Definition Foo := {A of isFoo A }. + +HB.mixin Record isPU A := {}. +HB.structure Definition PU := {A of isFoo A & isSetoid A & isPU A}. + +Lemma not_breaking (A : setoid) : Equivalence (@equiv A). +Proof. apply equivP. Qed. + +Lemma breaking (A : PU.type) : Equivalence (@equiv A). +Proof. apply equivP. + + + +#[global] +Instance equiv_Proper (A : setoid) : + Proper (@equiv A ==> equiv ==> iff) equiv. +Admitted. + +(* Module setoid_list. *) +#[local] +Instance Forall2_equivalence A (R : relation A) + of Equivalence R : Equivalence (Forall2 R). +Proof. +Admitted. + +HB.instance Definition test (A : setoid) := + isSetoid.Build (list A) (Forall2 (@equiv A)) _. +(* End setoid_list. *) +(* HB.instance Definition _ A := setoid_list.test A. *) + +#[global] +Lemma cons_Proper (A : setoid) : + Proper (equiv ==> equiv ==> equiv) (@cons A). +Proof. by constructor. Qed. +#[global] +Hint Extern 0 (Proper _ cons) => + apply: cons_Proper : typeclass_instances. + +Lemma foo (A : setoid) (x y : A) : + equiv x y -> equiv (x :: y :: nil) (y :: x :: nil). +Proof. move->. reflexivity. Qed. + +Definition trivialSetoid T := isSetoid.Build T eq eq_equivalence. + +Definition discrete T : Type := T. +HB.instance Definition _ T := trivialSetoid (discrete T). + +HB.instance Definition _ := Setoid.copy nat (discrete nat). + +Lemma foo' (x y : list (list nat)) : + equiv x y -> equiv (x :: y :: nil) (y :: x :: nil). +Proof. move->. reflexivity. Qed. + +HB.mixin Record RawSetoid_isRawOfe A of RawSetoid A := { + dist : nat -> relation A; +}. +#[short(type="rawofe")] +HB.structure Definition RawOfe := + { A of RawSetoid A & RawSetoid_isRawOfe A}. + +(* TODO: improve error message when removing explicit A *) +HB.mixin Record Setoid_Raw_isOfe A of + Setoid A & RawSetoid_isRawOfe A := { + distP : forall n, Equivalence (@dist A n); + equiv_dist : forall x y : A, + equiv x y <-> (forall n, dist n x y); + dist_S : forall n (x y : A), dist (S n) x y -> dist n x y +}. + +HB.factory Record Setoid_isOfe A of Setoid A := { + dist : nat -> relation A; + distP : forall n, Equivalence (dist n); + equiv_dist : forall x y, + equiv x y <-> (forall n, dist n x y); + dist_S : forall n x y, dist (S n) x y -> dist n x y +}. +HB.builders Context A of Setoid_isOfe A. + HB.instance Definition _ := RawSetoid_isRawOfe.Build A dist. + HB.instance Definition _ := + Setoid_Raw_isOfe.Build A distP equiv_dist dist_S. +HB.end. + +#[short(type="ofe")] +HB.structure Definition Ofe := {A of Setoid_isOfe A & Setoid A}. + +HB.factory Record isOfe A := { + dist : nat -> relation A; + distP : forall n, Equivalence (dist n); + dist_S : forall n x y, dist (S n) x y -> dist n x y +}. +HB.builders Context A of isOfe A. + Definition equiv x y := forall n, dist n x y. + Lemma equivP : Equivalence equiv. + Proof. Admitted. + HB.instance Definition _ := isSetoid.Build A equiv equivP. + (* TODO: this should emit a warning! *) + HB.instance Definition _ := isSetoid.Build A equiv equivP. + HB.instance Definition _ := Setoid_isOfe.Build A dist distP + (fun _ _ => iff_refl _) dist_S. + + Definition equiv' x y := forall n, dist (S n) x y. + Lemma equiv'P : Equivalence equiv'. + Proof. Admitted. + (* TODO: this should error now! *) + HB.instance Definition _ := isSetoid.Build A equiv' equiv'P. +HB.end. + +HB.factory Record Setoid_isTrivialOfe A of Setoid A := {}. +HB.builders Context A of Setoid_isTrivialOfe A. + Lemma equiv_dist : + forall x y : A, equiv x y <-> (forall _ : nat, equiv x y). + Proof. by move=> x y; split => //; apply; exact: 0. Qed. + HB.instance Definition _ : Setoid_isOfe A := + Setoid_isOfe.Build A (fun _ => equiv) (fun _ => equivP) + equiv_dist (fun _ _ _ => id). +HB.end. + +HB.instance Definition _ T := Setoid_isTrivialOfe.Build (discrete T). + +HB.instance Definition _ := Ofe.copy nat (discrete nat). + +#[global] Existing Instance distP. + +#[global] +Instance dist_Proper (A : ofe) n : + Proper (@dist A n ==> dist n ==> iff) (dist n). +Admitted. + +#[global] +Instance dist_equiv_Proper (A : ofe) n : + Proper (@equiv A ==> equiv ==> iff) (dist n). +Admitted. + +Section ofe_ist. +Variable (A : ofe). + +HB.instance Definition _ := + RawSetoid_isRawOfe.Build (list A) + (fun n => Forall2 (@dist A n)). + +(* TODO: Fix printing *) +Lemma list_isOfe : Setoid_Raw_isOfe (list A). +Proof. +constructor. +Admitted. + +HB.instance Definition _ := list_isOfe. +End ofe_ist. + +#[global] +Instance cons_ofe_Proper (A : ofe) n : + Proper (dist n ==> dist n ==> dist n) (@cons A). +Proof. by constructor. Qed. + +Global Instance : Params (@cons) 1 := {}. +Global Instance : Params (@dist) 2 := {}. +Global Instance : Params (@equiv) 1 := {}. + +Lemma breaking (A : setoid) : Equivalence (@equiv A). +Proof. apply equivP. Qed. + +Lemma breaking' (A : ofe) : Equivalence (@equiv A). +Proof. Fail apply equivP. exact: equivP. Qed. + +Lemma foo'' (A : ofe) (x y : A) : + equiv x y -> dist 2 (x :: y :: nil) (y :: x :: nil). +Proof. + +move=> exy. +Set Printing All. +Set Typeclasses Debug. + +Fail rewrite exy. +assert (@Equivalence _ (@equiv A)). + apply: equivP. + + +assert +(@Equivalence (Ofe.sort A) + (@equiv (iris_Setoid__to__iris_RawSetoid + (iris_Ofe__to__iris_Setoid A)))). + apply: equivP. + eauto with typeclass_instances. + +assert (exists r0 r, +(@Proper + (forall (_ : Ofe.sort A) + (_ : list (Ofe.sort A)), list (Ofe.sort A)) + (@respectful (Ofe.sort A) + (forall _ : list (Ofe.sort A), list (Ofe.sort A)) + (@equiv (iris_Ofe__to__iris_RawSetoid A)) + (@respectful (list (Ofe.sort A)) + (list (Ofe.sort A)) r0 r)) + (@cons (Ofe.sort A)))). +eexists _, _. + eauto with typeclass_instances. + + eapply cons_Proper. + eauto with typeclass_instances. + +Fail rewrite -> exy. + +eapply dist_equiv_Proper. +eapply cons_Proper. + exact exy. +reflexivity. +eapply cons_Proper. + reflexivity. +eapply cons_Proper. + exact exy. + reflexivity. + +eapply equiv_Proper. + +apply/dist_equiv_Proper. +apply: (dist_equiv_Proper _ _ _ _ _ _ _ _).2. +rewrite -> exy. +move->. + + move->. reflexivity. Qed. diff --git a/examples/IrisHierarchy/minimal2.v b/examples/IrisHierarchy/minimal2.v new file mode 100644 index 000000000..48a8bf4a4 --- /dev/null +++ b/examples/IrisHierarchy/minimal2.v @@ -0,0 +1,28 @@ +From HB Require Import structures. +From Coq Require Import Relations Morphisms. + +HB.mixin Record isRawSetoid A := { equiv: relation A }. +HB.structure Definition RawSetoid := { A of isRawSetoid A }. + +HB.mixin Record Raw_isSetoid A of RawSetoid A := { + equivP : Equivalence (@equiv A) +}. +HB.structure Definition Setoid := {A of isRawSetoid A & Raw_isSetoid A}. +#[global] Existing Instance equivP. + +HB.mixin Record RawSetoid_isRawOfe A of RawSetoid A := { +}. +HB.structure Definition RawOfe := + { A of RawSetoid A & RawSetoid_isRawOfe A}. + +HB.mixin Record Setoid_Raw_isOfe A of + Setoid A & RawSetoid_isRawOfe A := { +}. +HB.structure Definition Ofe := {A of RawSetoid_isRawOfe A & Setoid A}. + +Lemma not_breaking (A : Setoid.type) : Equivalence (@equiv A). +Proof. apply equivP. Qed. + +Lemma breaking (A : Ofe.type) : Equivalence (@equiv A). +Proof. Fail apply equivP. Succeed refine (@equivP _). Abort. + diff --git a/examples/IrisHierarchy/minimal3.v b/examples/IrisHierarchy/minimal3.v new file mode 100644 index 000000000..a572386db --- /dev/null +++ b/examples/IrisHierarchy/minimal3.v @@ -0,0 +1,27 @@ +From HB Require Import structures. +From Coq Require Import Relations Morphisms. + +HB.mixin Record hasEquiv A := { equiv : relation A }. +HB.structure Definition Equiv := { A of hasEquiv A }. + +HB.mixin Record Equiv_isSetoid A of Equiv A := { + equivP : Equivalence (@equiv A) +}. +HB.structure Definition Setoid := {A of hasEquiv A & Equiv_isSetoid A}. +#[global] Existing Instance equivP. + +HB.mixin Record isFoo A of Setoid A := {}. +HB.structure Definition Foo := {A of isFoo A & Setoid A}. + +Lemma not_breaking (A : Setoid.type) : Equivalence (@equiv A). +Proof. apply equivP. Qed. + +Lemma breaking (A : Foo.type) : + @Equivalence (Foo.sort A) (@equiv (minimal3_Foo__to__minimal3_Equiv A)). +Proof. +Set Printing All. +Fail apply @equivP. +Set Typeclasses Debug. +Fail typeclasses eauto. +Succeed refine (@equivP _). +Abort. diff --git a/examples/IrisHierarchy/minimal4.v b/examples/IrisHierarchy/minimal4.v new file mode 100644 index 000000000..6eac5a3f3 --- /dev/null +++ b/examples/IrisHierarchy/minimal4.v @@ -0,0 +1,34 @@ +From HB Require Import structures. +From Coq Require Import Relations Morphisms. + +HB.mixin Record hasEquiv A := { equiv : relation A }. +HB.structure Definition Equiv := { A of hasEquiv A }. + +HB.mixin Record Equiv_isSetoid A of Equiv A := { + equivP : Equivalence (@equiv A) +}. +HB.structure Definition Setoid := {A of hasEquiv A & Equiv_isSetoid A}. +#[global] Existing Instance equivP. + +HB.mixin Record isFoo A of Setoid A := {}. +HB.structure Definition Foo := {A of isFoo A & Setoid A}. + +Lemma not_breaking (A : Setoid.type) : @Equivalence A (@equiv A). +Proof. apply @equivP. Qed. + +Lemma not_breaking2 (A : Foo.type) : @Equivalence _ (@equiv A). +Proof. apply @equivP. Qed. + +Lemma breaking (A : Foo.type) : @Equivalence A (@equiv A). +Proof. +Set Printing All. +Check @equivP. +Set Debug "all". +refine (@equivP _). + +(* Check @equivP. *) +Fail apply @equivP. +Set Typeclasses Debug. +Fail typeclasses eauto. +Succeed refine (@equivP _). +Abort.