---

Step * of Lemma cpsquicksort-quicksort

∀[T:Type]
  ∀[A:Type]. ∀[cmp:comparison(T)].  ∀L:T List. ∀[k:(T List) ⟶ A]. (cpsquicksort(cmp;L;k) ~ k quicksort(cmp;L)) 
  supposing valueall-type(T)
BY
{ (InductionOnLength
   THEN Auto
   THEN (RecUnfold `cpsquicksort` 0 THEN RecUnfold `quicksort` 0)
   THEN OldAutoSplit
   THEN (Auto THENA (DVar `L' THEN Reduce 0 THEN Auto THEN D -1 THEN Auto))
   THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
   THEN RepeatFor 4 (((GenConclAtAddr [1;1] THENA (Auto THEN Auto)) THEN RW (AddrC [1] UnfoldTopAbC) 0 THEN Reduce 0))
   THEN (Assert ||filter(λz.0 <z cmp z v;L)|| < ||L|| ∧ ||filter(λz.0 <z cmp v z;L)|| < ||L|| BY
               (RevHypSubst' -7 0
                THEN Auto
                THEN ((BLemma `length-filter-decreases` THEN Auto THEN Reduce 0)
                      THEN (With ⌜0⌝ (D 0)⋅ THEN Reduce 0)
                      THEN Auto
                      THEN RWO "select0" 0
                      THEN Auto
                      THEN Subst' cmp hd(L) hd(L) ~ 0 0
                      THEN Reduce 0
                      THEN Auto
                      THEN (InstLemma `comparison-equiv` [⌜T⌝;⌜cmp⌝]⋅ THENA Auto)
                      THEN D -1
                      THEN Auto)⋅))) }

1
1. T : Type
2. valueall-type(T)
3. A : Type
4. cmp : comparison(T)
5. n : ℕ
6. L : T List
7. ∀L1:T List. (||L1|| < ||L|| ⇒ (∀[k:(T List) ⟶ A]. (cpsquicksort(cmp;L1;k) ~ k quicksort(cmp;L1))))
8. k : (T List) ⟶ A
9. ¬(L = [] ∈ (T List))
10. v : T
11. hd(L) = v ∈ T
12. v1 : T List
13. filter(λz.0 <z cmp z v;L) = v1 ∈ (T List)
14. v2 : T List
15. filter(λz.(0 =z cmp v z);L) = v2 ∈ (T List)
16. v3 : T List
17. filter(λz.0 <z cmp v z;L) = v3 ∈ (T List)
18. ||filter(λz.0 <z cmp z v;L)|| < ||L|| ∧ ||filter(λz.0 <z cmp v z;L)|| < ||L||
⊢ cpsquicksort(cmp;v1;λS1.cpsquicksort(cmp;v3;λS3.(k (S1 @ v2 @ S3)))) ~ k 
                                                                         let L3 ⟵ v2
                                                                         in quicksort(cmp;v1) @ L3 @ quicksort(cmp;v3)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[A:Type].  \mforall{}[cmp:comparison(T)].
        \mforall{}L:T  List.  \mforall{}[k:(T  List)  {}\mrightarrow{}  A].  (cpsquicksort(cmp;L;k)  \msim{}  k  quicksort(cmp;L)) 
    supposing  valueall-type(T)


By

---

Latex:
(InductionOnLength
  THEN  Auto
  THEN  (RecUnfold  `cpsquicksort`  0  THEN  RecUnfold  `quicksort`  0)
  THEN  OldAutoSplit
  THEN  (Auto  THENA  (DVar  `L'  THEN  Reduce  0  THEN  Auto  THEN  D  -1  THEN  Auto))
  THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto))
  THEN  RepeatFor  4  (((GenConclAtAddr  [1;1]  THENA  (Auto  THEN  Auto))
                                        THEN  RW  (AddrC  [1]  UnfoldTopAbC)  0
                                        THEN  Reduce  0))
  THEN  (Assert  ||filter(\mlambda{}z.0  <z  cmp  z  v;L)||  <  ||L||  \mwedge{}  ||filter(\mlambda{}z.0  <z  cmp  v  z;L)||  <  ||L||  BY
                          (RevHypSubst'  -7  0
                            THEN  Auto
                            THEN  ((BLemma  `length-filter-decreases`  THEN  Auto  THEN  Reduce  0)
                                        THEN  (With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0)
                                        THEN  Auto
                                        THEN  RWO  "select0"  0
                                        THEN  Auto
                                        THEN  Subst'  cmp  hd(L)  hd(L)  \msim{}  0  0
                                        THEN  Reduce  0
                                        THEN  Auto
                                        THEN  (InstLemma  `comparison-equiv`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}cmp\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                        THEN  D  -1
                                        THEN  Auto)\mcdot{})))

---

Home Index