Step
*
of Lemma
bag-drop-commutes
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x,y:T].
(bag-drop(eq;bag-drop(eq;bs;x);y) = bag-drop(eq;bag-drop(eq;bs;y);x) ∈ bag(T))
BY
{ TACTIC:(Auto
THEN (Assert ∀x,y:T. Dec(x = y ∈ T) BY
Auto)
THEN (TACTIC: Decide ⌜x = y ∈ T⌝⋅⋅ THENA Auto)
THEN Try ((HypSubst (-1) 0 THEN Auto))
THEN Unfold `bag-drop` 0
THEN (InstLemma `bag-remove1-property` [⌜T⌝;⌜eq⌝]⋅ THENA Auto)
THEN (InstHyp [⌜x⌝;⌜bs⌝] 8⋅ THENA Auto)
THEN D -1
THEN ExRepD
THEN ((HypSubst (-1) 0 THENA (D (-1) THEN Reduce 0 THEN Auto))
THEN Reduce 0
THEN ((InstHyp [⌜y⌝;⌜bs⌝] 8⋅ THENA Auto)
THEN D -1
THEN ExRepD
THEN ((HypSubst (-1) 0 THENA (D (-1) THEN Reduce 0 THEN Auto)) THEN Reduce 0)⋅)⋅)⋅) }
1
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
5. y : T
6. ∀x,y:T. Dec(x = y ∈ T)
7. ¬(x = y ∈ T)
8. ∀x:T. ∀bs:bag(T).
((∃as:bag(T). ((bs = ({x} + as) ∈ bag(T)) ∧ (bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?))))
∨ ((¬x ↓∈ bs) ∧ (bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?))))
9. as : bag(T)
10. bs = ({x} + as) ∈ bag(T)
11. bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?)
12. a1 : bag(T)
13. bs = ({y} + a1) ∈ bag(T)
14. bag-remove1(eq;bs;y) = (inl a1) ∈ (bag(T)?)
⊢ case bag-remove1(eq;as;y) of inl(as) => as | inr(_) => as
= case bag-remove1(eq;a1;x) of inl(as) => as | inr(_) => a1
∈ bag(T)
2
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
5. y : T
6. ∀x,y:T. Dec(x = y ∈ T)
7. ¬(x = y ∈ T)
8. ∀x:T. ∀bs:bag(T).
((∃as:bag(T). ((bs = ({x} + as) ∈ bag(T)) ∧ (bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?))))
∨ ((¬x ↓∈ bs) ∧ (bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?))))
9. as : bag(T)
10. bs = ({x} + as) ∈ bag(T)
11. bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?)
12. ¬y ↓∈ bs
13. bag-remove1(eq;bs;y) = (inr ⋅ ) ∈ (bag(T)?)
⊢ case bag-remove1(eq;as;y) of inl(as) => as | inr(_) => as
= case bag-remove1(eq;bs;x) of inl(as) => as | inr(_) => bs
∈ bag(T)
3
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
5. y : T
6. ∀x,y:T. Dec(x = y ∈ T)
7. ¬(x = y ∈ T)
8. ∀x:T. ∀bs:bag(T).
((∃as:bag(T). ((bs = ({x} + as) ∈ bag(T)) ∧ (bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?))))
∨ ((¬x ↓∈ bs) ∧ (bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?))))
9. ¬x ↓∈ bs
10. bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?)
11. as : bag(T)
12. bs = ({y} + as) ∈ bag(T)
13. bag-remove1(eq;bs;y) = (inl as) ∈ (bag(T)?)
⊢ as = case bag-remove1(eq;as;x) of inl(as) => as | inr(_) => as ∈ bag(T)
4
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
5. y : T
6. ∀x,y:T. Dec(x = y ∈ T)
7. ¬(x = y ∈ T)
8. ∀x:T. ∀bs:bag(T).
((∃as:bag(T). ((bs = ({x} + as) ∈ bag(T)) ∧ (bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?))))
∨ ((¬x ↓∈ bs) ∧ (bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?))))
9. ¬x ↓∈ bs
10. bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?)
11. ¬y ↓∈ bs
12. bag-remove1(eq;bs;y) = (inr ⋅ ) ∈ (bag(T)?)
⊢ bs = case bag-remove1(eq;bs;x) of inl(as) => as | inr(_) => bs ∈ bag(T)
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[bs:bag(T)]. \mforall{}[x,y:T].
(bag-drop(eq;bag-drop(eq;bs;x);y) = bag-drop(eq;bag-drop(eq;bs;y);x))
By
Latex:
TACTIC:(Auto
THEN (Assert \mforall{}x,y:T. Dec(x = y) BY
Auto)
THEN (TACTIC: Decide \mkleeneopen{}x = y\mkleeneclose{}\mcdot{}\mcdot{} THENA Auto)
THEN Try ((HypSubst (-1) 0 THEN Auto))
THEN Unfold `bag-drop` 0
THEN (InstLemma `bag-remove1-property` [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstHyp [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}] 8\mcdot{} THENA Auto)
THEN D -1
THEN ExRepD
THEN ((HypSubst (-1) 0 THENA (D (-1) THEN Reduce 0 THEN Auto))
THEN Reduce 0
THEN ((InstHyp [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}] 8\mcdot{} THENA Auto)
THEN D -1
THEN ExRepD
THEN ((HypSubst (-1) 0 THENA (D (-1) THEN Reduce 0 THEN Auto)) THEN Reduce 0)\mcdot{})
\mcdot{})\mcdot{})
Home
Index