---

Step * of Lemma bag-map-as-accum

∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[bs:bag(A)].  (bag-map(f;bs) = bag-accum(b,x.f[x].b;{};bs) ∈ bag(B))
BY
{ (Auto
   THEN BagInd (-1)
   THEN Auto
   THEN Try ((RepUR ``bag-accum bag-map`` 0 THEN Fold `empty-bag` 0 THEN Auto))
   THEN Try ((Repeat ((RWO "cons-bag-as-append" 0 THENA Auto))
              THEN (RWO "bag-append-assoc<" 0 THENA Auto)
              THEN (MemCD THEN Auto)
              THEN BLemma `bag-append-comm`
              THEN Auto))
   THEN Try (Fold `cons-bag` 0)
   THEN (RWO "bag-map-cons" 0 THENA Auto)
   THEN (HypSubst' (-1) 0
         THENA (Auto
                THEN Repeat ((RWO "cons-bag-as-append" 0 THENA Auto))
                THEN (RWO "bag-append-assoc<" 0 THENA Auto)
                THEN (MemCD THEN Auto)
                THEN BLemma `bag-append-comm`
                THEN Auto)
         )
   THEN Thin (-1)
   THEN (RWO "cons-bag-as-append" 0 THENA Auto)
   THEN (InstLemma `bag-append-comm` [⌜A⌝;⌜{u}⌝;⌜v⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0
         THENA (Auto
                THEN Repeat ((RWO "cons-bag-as-append" 0 THENA Auto))
                THEN (RWO "bag-append-assoc<" 0 THENA Auto)
                THEN (MemCD THEN Auto)
                THEN BLemma `bag-append-comm`
                THEN Auto)
         )
   THEN RepUR ``bag-accum bag-append`` 0
   THEN (RWO "list_accum_append" 0 THENA (Auto THEN Unfold `single-bag` 0 THEN Auto))
   THEN Try (Folds ``bag-accum bag-append`` 0)) }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. u : A
5. v : A List
6. ({u} + v) = (v + {u}) ∈ bag(A)
⊢ ({f u} + bag-accum(b,x.f[x].b;{};v)) = bag-accum(b,x.{f[x]} + b;bag-accum(b,x.{f[x]} + b;{};v);{u}) ∈ bag(B)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[bs:bag(A)].    (bag-map(f;bs)  =  bag-accum(b,x.f[x].b;\{\};bs))


By

---

Latex:
(Auto
  THEN  BagInd  (-1)
  THEN  Auto
  THEN  Try  ((RepUR  ``bag-accum  bag-map``  0  THEN  Fold  `empty-bag`  0  THEN  Auto))
  THEN  Try  ((Repeat  ((RWO  "cons-bag-as-append"  0  THENA  Auto))
                        THEN  (RWO  "bag-append-assoc<"  0  THENA  Auto)
                        THEN  (MemCD  THEN  Auto)
                        THEN  BLemma  `bag-append-comm`
                        THEN  Auto))
  THEN  Try  (Fold  `cons-bag`  0)
  THEN  (RWO  "bag-map-cons"  0  THENA  Auto)
  THEN  (HypSubst'  (-1)  0
              THENA  (Auto
                            THEN  Repeat  ((RWO  "cons-bag-as-append"  0  THENA  Auto))
                            THEN  (RWO  "bag-append-assoc<"  0  THENA  Auto)
                            THEN  (MemCD  THEN  Auto)
                            THEN  BLemma  `bag-append-comm`
                            THEN  Auto)
              )
  THEN  Thin  (-1)
  THEN  (RWO  "cons-bag-as-append"  0  THENA  Auto)
  THEN  (InstLemma  `bag-append-comm`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\{u\}\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0
              THENA  (Auto
                            THEN  Repeat  ((RWO  "cons-bag-as-append"  0  THENA  Auto))
                            THEN  (RWO  "bag-append-assoc<"  0  THENA  Auto)
                            THEN  (MemCD  THEN  Auto)
                            THEN  BLemma  `bag-append-comm`
                            THEN  Auto)
              )
  THEN  RepUR  ``bag-accum  bag-append``  0
  THEN  (RWO  "list\_accum\_append"  0  THENA  (Auto  THEN  Unfold  `single-bag`  0  THEN  Auto))
  THEN  Try  (Folds  ``bag-accum  bag-append``  0))

---

Home Index