---

Step * 1 2 of Lemma bag-mapfilter-fast-eq


1. A : Type
2. B : Type
3. P : A ⟶ 𝔹
4. f : {x:A| ↑P[x]}  ⟶ B
5. u : A
6. v : A List
7. bag-accum(b,x.if P[x] then f[x].b else b fi ;{};v)
= bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};v))
∈ bag(B)
⊢ bag-accum(b,x.if P[x] then f[x].b else b fi ;{};[u / v])
= bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};[u / v]))
∈ bag(B)
BY
{ (Try (Fold `cons-bag` 0)
   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 Try ((Repeat (AutoSplit)
                           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))
                )
         )) }

1
.....debug..... 
1. A : Type
2. B : Type
3. P : A ⟶ 𝔹
4. f : {x:A| ↑P[x]}  ⟶ B
5. u : A
6. v : A List
7. bag-accum(b,x.if P[x] then f[x].b else b fi ;{};v)
= bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};v))
∈ bag(B)
8. ({u} + v) = (v + {u}) ∈ bag(A)
⊢ ...EqCDAux1... bag-accum(b,x.{f[x]} + b;{};bag-accum(b,x.if P[x] then {x} + b else b fi ;{};{u} + v))
= bag-accum(b,x.{f[x]} + b;{};bag-accum(b,x.if P[x] then {x} + b else b fi ;{};v + {u}))
∈ bag(B)

2
1. A : Type
2. B : Type
3. P : A ⟶ 𝔹
4. f : {x:A| ↑P[x]}  ⟶ B
5. u : A
6. v : A List
7. bag-accum(b,x.if P[x] then f[x].b else b fi ;{};v)
= bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};v))
∈ bag(B)
8. ({u} + v) = (v + {u}) ∈ bag(A)
⊢ bag-accum(b,x.if P[x] then {f[x]} + b else b fi ;{};v + {u})
= bag-accum(b,x.{f[x]} + b;{};bag-accum(b,x.if P[x] then {x} + b else b fi ;{};v + {u}))
∈ bag(B)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  P  :  A  {}\mrightarrow{}  \mBbbB{}
4.  f  :  \{x:A|  \muparrow{}P[x]\}    {}\mrightarrow{}  B
5.  u  :  A
6.  v  :  A  List
7.  bag-accum(b,x.if  P[x]  then  f[x].b  else  b  fi  ;\{\};v)
=  bag-accum(b,x.f[x].b;\{\};bag-accum(b,x.if  P[x]  then  x.b  else  b  fi  ;\{\};v))
\mvdash{}  bag-accum(b,x.if  P[x]  then  f[x].b  else  b  fi  ;\{\};[u  /  v])
=  bag-accum(b,x.f[x].b;\{\};bag-accum(b,x.if  P[x]  then  x.b  else  b  fi  ;\{\};[u  /  v]))


By

---

Latex:
(Try  (Fold  `cons-bag`  0)
  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  Try  ((Repeat  (AutoSplit)
                                                  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))
                            )
              ))

---

Home Index