feat: OFE step-indexing parametrisation, port `algebra/stepindex_finite.v` #550

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open

alvinylt wants to merge 34 commits into leanprover-community:master from ISTA-PLV:StepIndexOFE

Iris/Iris/Algebra/Agree.lean

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -80,7 +80,7 @@ theorem map'_sameElems {f : α → β} {x y : Raw α} (h : SameElems x y) :
  
        obtain ⟨b, hb, rfl⟩ := ha

        exact ⟨b, by first | exact h.1 _ hb | exact h.2 _ hb, rfl⟩

    variable [OFE α]

    variable [OFE Nat α]

    def dist (n : Nat) (x y : Raw α) : Prop :=

      (∀ a ∈ x.car, ∃ b ∈ y.car, a ≡{n}≡ b) ∧

    @@ -227,7 +227,7 @@ theorem toAgree_uninj {x : Raw α} : x.valid → ∃ a, ∀ n, dist n (toAgree a
  
      · exists a; simp_all [toAgree]

      · simp_all [toAgree]

    variable [OFE β] {f : α → β}

    variable [OFE Nat β] {f : α → β}

    theorem map'_ne [OFE.NonExpansive f] {x₁ x₂ : Raw α} (h : dist n x₁ x₂) :

        dist n (map' f x₁) (map' f x₂) := by

    @@ -347,14 +347,14 @@ end Agree
  
    namespace Agree

    variable [OFE α] [OFE β]

    variable [OFE Nat α] [OFE Nat β]

    @[rocq_alias agree_dist]

    def dist (n : Nat) : Agree α → Agree α → Prop :=

      lift₂ (Raw.dist n) (fun _ _ _ _ hac hbd => propext (Raw.dist_congr hac hbd))

    @[rocq_alias agree_ofe_mixin]

    instance instOFE : OFE (Agree α) where

    instance instOFE : OFE Nat (Agree α) where

      Dist := dist

      dist_eqv := by

        refine ⟨Quotient.ind fun a => Raw.dist_equiv.refl a, fun {x y} h => ?_, fun {x y z} h₁ h₂ => ?_⟩

    @@ -524,7 +524,7 @@ theorem toAgree_def {a : α} : toAgree a = Agree.mk (Agree.Raw.toAgree a) := rfl
  
    section

    variable [OFE α]

    variable [OFE Nat α]

    @[rocq_alias to_agree_ne]

    instance instNonExpansive_toAgree : OFE.NonExpansive (@toAgree α) where

    @@ -640,7 +640,7 @@ theorem Agree.map'_compose {f : α → β} {g : β → γ} (x : Agree α) :
  
        Agree.map' (g ∘ f) x = Agree.map' g (Agree.map' f x) :=

      x.ind fun _ => congrArg mk (Raw.ext (by simp [Raw.map'_car, List.map_map]))

    variable {α β γ : Type _} [OFE α] [OFE β] [OFE γ] {f : α → β} [hne : OFE.NonExpansive f]

    variable {α β γ : Type _} [OFE Nat α] [OFE Nat β] [OFE Nat γ] {f : α → β} [hne : OFE.NonExpansive f]

    @[rocq_alias agree_map_ne]

    instance instNonExpansive_AgreeMap' : OFE.NonExpansive (Agree.map' f) where

    @@ -694,10 +694,10 @@ end agree_map
  
    section agree_rfunctor

    @[rocq_alias agreeRF]

    abbrev AgreeRF (F : COFE.OFunctorPre) : COFE.OFunctorPre :=

    abbrev AgreeRF (F : COFE.OFunctorPre Nat) : COFE.OFunctorPre Nat :=

      fun A B _ _ => Agree (F A B)

    instance {F} [COFE.OFunctor F] : RFunctor (AgreeRF F) where

    instance {F} [COFE.OFunctor Nat F] : RFunctor (AgreeRF F) where

      map f g := Agree.map (COFE.OFunctor.map f g)

      map_ne.ne _ _ _ Hx _ _ Hy _ := Agree.map_ne <| COFE.OFunctor.map_ne.ne Hx Hy

      map_id x := by

    @@ -708,7 +708,7 @@ instance {F} [COFE.OFunctor F] : RFunctor (AgreeRF F) where
  
        exact Agree.agree_map_ext (fun a => COFE.OFunctor.map_comp f g f' g' a)

    @[rocq_alias agreeRF_contractive]

    instance {F} [COFE.OFunctorContractive F] : RFunctorContractive (AgreeRF F) where

    instance {F} [COFE.OFunctorContractive Nat F] : RFunctorContractive (AgreeRF F) where

      map_contractive.1 H _ := Agree.map_ne (COFE.OFunctorContractive.map_contractive.1 H)

    end agree_rfunctor

Iris/Iris/Algebra/Auth.lean

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -71,7 +71,7 @@ abbrev Auth (A : Type _) [UCMRA A] :=
  
    namespace Auth

    variable [UCMRA A]

    instance : OFE (Auth A) := View.instOFE

    instance : OFE Nat (Auth A) := View.instOFE

    instance : CMRA (Auth A) := View.instCMRA

    instance : UCMRA (Auth A) := View.instUCMRA

    @@ -464,10 +464,10 @@ theorem authViewRel_map [UCMRA A'] [UCMRA B'] (g : A' -C> B') (n : Nat) (a : A')
  
      fun ⟨hinc, hv⟩ => ⟨CMRA.Hom.monoN g n hinc, CMRA.Hom.validN g hv⟩

    @[rocq_alias authURF]

    abbrev AuthURF (T : COFE.OFunctorPre) [URFunctor T] : COFE.OFunctorPre :=

    abbrev AuthURF (T : COFE.OFunctorPre Nat) [URFunctor T] : COFE.OFunctorPre Nat :=

      fun A B _ _ => Auth (T A B)

    instance instURFunctorAuthURF {T : COFE.OFunctorPre} [URFunctor T] :

    instance instURFunctorAuthURF {T : COFE.OFunctorPre Nat} [URFunctor T] :

        URFunctor (AuthURF T) where

      map {A A'} {B B'} _ _ _ _ f g :=

        mapC

    @@ -487,16 +487,16 @@ instance instURFunctorAuthURF {T : COFE.OFunctorPre} [URFunctor T] :
  
          (congrArg (View.map _ _ · _) (funext fun _ => URFunctor.map_comp f g f' g' _))

    @[rocq_alias authURF_contractive]

    instance instURFunctorContractiveAuthURF {T : COFE.OFunctorPre} [URFunctorContractive T] :

    instance instURFunctorContractiveAuthURF {T : COFE.OFunctorPre Nat} [URFunctorContractive T] :

        URFunctorContractive (AuthURF T) where

      map_contractive.1 h x := by

        apply map_ne <;> apply URFunctorContractive.map_contractive.1 h

    @[rocq_alias authRF]

    abbrev AuthRF (T : COFE.OFunctorPre) [URFunctor T] : COFE.OFunctorPre :=

    abbrev AuthRF (T : COFE.OFunctorPre Nat) [URFunctor T] : COFE.OFunctorPre Nat :=

      fun A B _ _ => Auth (T A B)

    instance instRFunctorAuthRF {T : COFE.OFunctorPre} [URFunctor T] :

    instance instRFunctorAuthRF {T : COFE.OFunctorPre Nat} [URFunctor T] :

        RFunctor (AuthRF T) where

      map {A A'} {B B'} _ _ _ _ f g :=

        mapC

    @@ -516,7 +516,7 @@ instance instRFunctorAuthRF {T : COFE.OFunctorPre} [URFunctor T] :
  
          (congrArg (View.map _ _ · _) (funext fun _ => URFunctor.map_comp f g f' g' _))

    @[rocq_alias authRF_contractive]

    instance instRFunctorContractiveAuthRF {T : COFE.OFunctorPre} [URFunctorContractive T] :

    instance instRFunctorContractiveAuthRF {T : COFE.OFunctorPre Nat} [URFunctorContractive T] :

        RFunctorContractive (AuthRF T) where

      map_contractive.1 h x := by

        apply View.map_ne <;> apply URFunctorContractive.map_contractive.1 h

Iris/Iris/Algebra/BigOp.lean

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -26,29 +26,29 @@ These are parameterized by a monoid operation and include theorems about their p
  
    open OFE Iris.Std

    @[rocq_alias big_opL, expose] public def bigOpL {M : Type u} {A : Type v} [OFE M] (op : M → M → M) {unit : M} [MonoidOps op unit]

    @[rocq_alias big_opL, expose] public def bigOpL {M : Type u} {A : Type v} [OFE Nat M] (op : M → M → M) {unit : M} [MonoidOps op unit]

        (Φ : Nat → A → M) (l : List A) : M :=

      match l with

      | [] => unit

      | x :: xs => op (Φ 0 x) (bigOpL op (fun n => Φ (n + 1)) xs)

    @[rocq_alias big_opM, expose] public def bigOpM {M : Type u} [OFE M] (op : M → M → M) {unit : M} [MonoidOps op unit] {K : Type _}

    @[rocq_alias big_opM, expose] public def bigOpM {M : Type u} [OFE Nat M] (op : M → M → M) {unit : M} [MonoidOps op unit] {K : Type _}

        {V : Type _} (Φ : K → V → M) {M' : Type _ → Type _} [LawfulFiniteMap M' K] (m : M' V) : M :=

      bigOpL op (fun _ kv => Φ kv.1 kv.2) (toList m)

    #rocq_ignore big_opM_aux "Not needed"

    #rocq_ignore big_opM_def "Not needed"

    #rocq_ignore big_opM_unseal "Not needed"

    @[rocq_alias big_opS, expose] public def bigOpS {M : Type u} [OFE M] (op : M → M → M) {unit : M} [MonoidOps op unit]

    @[rocq_alias big_opS, expose] public def bigOpS {M : Type u} [OFE Nat M] (op : M → M → M) {unit : M} [MonoidOps op unit]

        {A : Type _} {S : Type _} [FiniteSet S A] (Φ : A → M) (m : S) : M :=

      bigOpL op (fun _ x => Φ x) (toList m)

    #rocq_ignore big_opS_aux "Not needed"

    #rocq_ignore big_opS_def "Not needed"

    #rocq_ignore big_opS_unseal "Not needed"

    @[rocq_alias big_opMS, expose] public def bigOpMS {M : Type u} [OFE M] (op : M → M → M)

    @[rocq_alias big_opMS, expose] public def bigOpMS {M : Type u} [OFE Nat M] (op : M → M → M)

        {unit : M} [MonoidOps op unit] {A : Type _} {MS : Type _} [FiniteMultiSet MS A]

        (Φ : A → M) (X : MS) : M :=

      bigOpL op (fun _ x => Φ x) (FiniteMultiSet.toList X)

    @@ -84,7 +84,7 @@ scoped macro_rules
  
    public section

    namespace BigOpL

    variable {M : Type _} {A : Type _} [OFE M] {op : M → M → M} {unit : M} [MonoidOps op unit]

    variable {M : Type _} {A : Type _} [OFE Nat M] {op : M → M → M} {unit : M} [MonoidOps op unit]

    open MonoidOps

    @@ -216,7 +216,7 @@ theorem bigOpL_gen_proper (R : M → M → Prop) {Φ Ψ : Nat → A → M} {l :
  
    #rocq_ignore big_opL_ext "Merged into bigOpL_eq"

    @[rocq_alias big_opL_proper_2]

    theorem bigOpL_proper_2 [OFE A] {Φ Ψ : Nat → A → M} {l₁ l₂ : List A} (hlen : l₁.length = l₂.length)

    theorem bigOpL_proper_2 [OFE Nat A] {Φ Ψ : Nat → A → M} {l₁ l₂ : List A} (hlen : l₁.length = l₂.length)

        (hf : ∀ {k y₁ y₂}, l₁[k]? = some y₁ → l₂[k]? = some y₂ → Φ k y₁ = Ψ k y₂) :

        ([^ op list] k ↦ x ∈ l₁, Φ k x) = ([^ op list] k ↦ x ∈ l₂, Ψ k x) :=

      bigOpL_gen_proper_2 (· = ·) rfl (· ▸ · ▸ rfl) hlen hf

    @@ -287,7 +287,7 @@ end CMRA
  
    section Hom

    variable {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂]

    variable {M₁ : Type u} {M₂ : Type v} [OFE Nat M₁] [OFE Nat M₂]

    variable {op₁ : M₁ → M₁ → M₁} {op₂ : M₂ → M₂ → M₂} {unit₁ : M₁} {unit₂ : M₂}

    variable [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂]

    variable {B : Type w} {R : M₂ → M₂ → Prop} {f : M₁ → M₂}

    @@ -319,7 +319,7 @@ namespace BigOpM
  
    open scoped PartialMap

    variable {M : Type u} [OFE M] {op : M → M → M} {unit : M} [MonoidOps op unit]

    variable {M : Type u} [OFE Nat M] {op : M → M → M} {unit : M} [MonoidOps op unit]

    variable {M' : Type _ → Type _} {K : Type _} {V : Type _}

    variable [LawfulFiniteMap M' K]

    @@ -401,7 +401,7 @@ theorem bigOpM_eq {Φ Ψ : K → V → M} {m : M' V} (hf : ∀ {k x}, get? m k =
  
      bigOpM_gen_proper rfl (· ▸ · ▸ rfl) hf

    @[rocq_alias big_opM_proper_2]

    theorem bigOpM_eq_strong [OFE A] {Φ Ψ : K → A → M} {m1 m2 : M' A} (hm : ∀ k, get? m1 k = get? m2 k)

    theorem bigOpM_eq_strong [OFE Nat A] {Φ Ψ : K → A → M} {m1 m2 : M' A} (hm : ∀ k, get? m1 k = get? m2 k)

        (hf : ∀ {k y1 y2}, get? m1 k = some y1 → get? m2 k = some y2 → y1 = y2 → Φ k y1 = Ψ k y2) :

        ([^ op map] k ↦ x ∈ m1, Φ k x) = ([^ op map] k ↦ x ∈ m2, Ψ k x) :=

      bigOpM_gen_proper_2 id equivalence_eq (· ▸ · ▸ rfl) (fun k => by rw [hm k])

    @@ -577,8 +577,8 @@ theorem bigOpM_none {f : K → V → Option M} {m : M' V} :
  
    end CMRA

    variable {M₁} [OFE M₁]

    variable {M₂} [OFE M₂]

    variable {M₁} [OFE Nat M₁]

    variable {M₂} [OFE Nat M₂]

    variable {op₁ : M₁ → M₁ → M₁} {op₂ : M₂ → M₂ → M₂} {unit₁ : M₁} {unit₂ : M₂}

    variable [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂]

    @@ -604,7 +604,7 @@ end BigOpM
  
    namespace BigOpS

    variable {M : Type _} {A : Type _} {S : Type _} [OFE M] {op : M → M → M} {unit : M}

    variable {M : Type _} {A : Type _} {S : Type _} [OFE Nat M] {op : M → M → M} {unit : M}

      [MonoidOps op unit] [LawfulFiniteSet S A]

    open BigOpL MonoidOps LawfulSet FiniteSet

    @@ -717,7 +717,7 @@ end CMRA
  
    section Homomorphism

    variable {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂]

    variable {M₁ : Type u} {M₂ : Type v} [OFE Nat M₁] [OFE Nat M₂]

    variable {op₁ : M₁ → M₁ → M₁} {op₂ : M₂ → M₂ → M₂} {unit₁ : M₁} {unit₂ : M₂}

    variable [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂]

    @@ -747,7 +747,7 @@ end BigOpS
  
    namespace BigOpMS

    variable {M : Type _} {A : Type _} {MS : Type _} [OFE M] {op : M → M → M} {unit : M}

    variable {M : Type _} {A : Type _} {MS : Type _} [OFE Nat M] {op : M → M → M} {unit : M}

      [MonoidOps op unit] [LawfulFiniteMultiSet MS A]

    open BigOpL MonoidOps

    @@ -856,7 +856,7 @@ end CMRA
  
    section Homomorphism

    variable {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂]

    variable {M₁ : Type u} {M₂ : Type v} [OFE Nat M₁] [OFE Nat M₂]

    variable {op₁ : M₁ → M₁ → M₁} {op₂ : M₂ → M₂ → M₂} {unit₁ : M₁} {unit₂ : M₂}

    variable [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂]

Navigation Menu

Uh oh!

feat: OFE step-indexing parametrisation, port `algebra/stepindex_finite.v` #550

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!

feat: OFE step-indexing parametrisation, port algebra/stepindex_finite.v #550

Are you sure you want to change the base?

Uh oh!

feat: OFE step-indexing parametrisation, port algebra/stepindex_finite.v #550

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

feat: OFE step-indexing parametrisation, port `algebra/stepindex_finite.v` #550

feat: OFE step-indexing parametrisation, port `algebra/stepindex_finite.v` #550