Commit b863cfd7 by Jacques-Henri Jourdan

Unbundle the inductives defining the metrics and equivalences of excl and csum.

```This makes the inductives defining the metrics and equivalences of
excl and csum independent of the ofe instance, so that rewriting works
even if the ofe instance is not the same.```
parent 9c0c4620
 ... ... @@ -26,21 +26,23 @@ Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x, Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x, match x with Cinr b => Some b | _ => None end. Inductive csum_equiv `{Equiv A, Equiv B} : Equiv (csum A B) := | Cinl_equiv a a' : a ≡ a' → @equiv (csum A B) _ (Cinl a) (Cinl a') | Cinr_equiv b b' : b ≡ b' → @equiv (csum A B) _ (Cinr b) (Cinr b') | CsumBot_equiv : @equiv (csum A B) _ CsumBot CsumBot. Inductive csum_dist `{Dist A, Dist B} : Dist (csum A B) := | Cinl_dist n a a' : a ≡{n}≡ a' → @dist (csum A B) _ n (Cinl a) (Cinl a') | Cinr_dist n b b' : b ≡{n}≡ b' → @dist (csum A B) _ n (Cinr b) (Cinr b') | CsumBot_dist n : @dist (csum A B) _ n CsumBot CsumBot. Section cofe. Context {A B : ofeT}. Implicit Types a : A. Implicit Types b : B. (* Cofe *) Inductive csum_equiv : Equiv (csum A B) := | Cinl_equiv a a' : a ≡ a' → Cinl a ≡ Cinl a' | Cinr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b' | CsumBot_equiv : CsumBot ≡ CsumBot. Existing Instance csum_equiv. Inductive csum_dist : Dist (csum A B) := | Cinl_dist n a a' : a ≡{n}≡ a' → Cinl a ≡{n}≡ Cinl a' | Cinr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b' | CsumBot_dist n : CsumBot ≡{n}≡ CsumBot. Existing Instance csum_dist. Global Instance Cinl_ne : NonExpansive (@Cinl A B). ... ...
 ... ... @@ -20,19 +20,20 @@ Notation ExclBot' := (Some ExclBot). Instance maybe_Excl {A} : Maybe (@Excl A) := λ x, match x with Excl a => Some a | _ => None end. Inductive excl_equiv `{Equiv A} : Equiv (excl A) := | Excl_equiv a b : a ≡ b → Excl a ≡ Excl b | ExclBot_equiv : ExclBot ≡ ExclBot. Inductive excl_dist `{Dist A} : Dist (excl A) := | Excl_dist a b n : a ≡{n}≡ b → Excl a ≡{n}≡ Excl b | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot. Section excl. Context {A : ofeT}. Implicit Types a b : A. Implicit Types x y : excl A. (* Cofe *) Inductive excl_equiv : Equiv (excl A) := | Excl_equiv a b : a ≡ b → Excl a ≡ Excl b | ExclBot_equiv : ExclBot ≡ ExclBot. Existing Instance excl_equiv. Inductive excl_dist : Dist (excl A) := | Excl_dist a b n : a ≡{n}≡ b → Excl a ≡{n}≡ Excl b | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot. Existing Instance excl_dist. Global Instance Excl_ne : NonExpansive (@Excl A). ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!