Abstract Refinements {#induction} ================================= Induction --------- Encoding *induction* with Abstract refinements <div class="hidden"> <pre><span class=hs-linenum>12: </span><span class='hs-keyword'>module</span> <span class='hs-conid'>Loop</span> <span class='hs-keyword'>where</span> <span class=hs-linenum>13: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Prelude</span> <span class='hs-varid'>hiding</span> <span class='hs-layout'>(</span><span class='hs-layout'>(</span><span class='hs-varop'>!!</span><span class='hs-layout'>)</span><span class='hs-layout'>,</span> <span class='hs-varid'>foldr</span><span class='hs-layout'>,</span> <span class='hs-varid'>length</span><span class='hs-layout'>,</span> <span class='hs-layout'>(</span><span class='hs-varop'>++</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <span class=hs-linenum>14: </span><span class='hs-comment'>-- import Measures</span> <span class=hs-linenum>15: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Language</span><span class='hs-varop'>.</span><span class='hs-conid'>Haskell</span><span class='hs-varop'>.</span><span class='hs-conid'>Liquid</span><span class='hs-varop'>.</span><span class='hs-conid'>Prelude</span> <span class=hs-linenum>16: </span><span class='hs-keyword'>{-@</span> <span class='hs-conid'>LIQUID</span> <span class='hs-str'>"--no-termination"</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>17: </span> <span class=hs-linenum>18: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>measure</span> <span class='hs-varid'>llen</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-conid'>L</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class=hs-linenum>19: </span> <span class='hs-varid'>llen</span> <span class='hs-layout'>(</span><span class='hs-conid'>N</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class='hs-num'>0</span> <span class=hs-linenum>20: </span> <span class='hs-varid'>llen</span> <span class='hs-layout'>(</span><span class='hs-conid'>C</span> <span class='hs-varid'>x</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class='hs-num'>1</span> <span class='hs-varop'>+</span> <span class='hs-layout'>(</span><span class='hs-varid'>llen</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>21: </span> <span class=hs-linenum>22: </span><span class='hs-definition'>size</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class=hs-linenum>23: </span><span class='hs-definition'>add</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class=hs-linenum>24: </span><span class='hs-definition'>loop</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>α</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>α</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>α</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>α</span> <span class=hs-linenum>25: </span><span class='hs-definition'>foldr</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span> </pre> </div> Induction ========= Example: `loop` redux --------------------- Recall the *higher-order* `loop` <br> <pre><span class=hs-linenum>40: </span><a class=annot href="#"><span class=annottext>forall a <p :: (GHC.Types.Int)-> a-> Bool>. lo:(Int) -> hi:{VV : (Int) | (lo <= VV)} -> {VV : a<p lo> | true} -> (i:(Int) -> {VV : a<p i> | true} -> forall [ex:{VV : (Int) | (VV == (i + 1))}].{VV : a<p ex> | true}) -> {VV : a<p hi> | true}</span><span class='hs-definition'>loop</span></a> <a class=annot href="#"><span class=annottext>(Int)</span><span class='hs-varid'>lo</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (lo <= VV)}</span><span class='hs-varid'>hi</span></a> <a class=annot href="#"><span class=annottext>{VV : a | ((papp2 p VV lo))}</span><span class='hs-varid'>base</span></a> <a class=annot href="#"><span class=annottext>i:(Int) -> {VV : a | ((papp2 p VV i))} -> forall [ex:{VV : (Int) | (VV == (i + 1))}].{VV : a | ((papp2 p VV ex))}</span><span class='hs-varid'>f</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{x4 : (Int) | (x4 >= lo) && (lo <= x4) && (x4 <= hi)} -> {VV : a | ((papp2 p VV x1))} -> {VV : a | ((papp2 p VV hi))}</span><span class='hs-varid'>go</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == lo)}</span><span class='hs-varid'>lo</span></a> <a class=annot href="#"><span class=annottext>{VV : a | ((papp2 p VV lo)) && (VV == base)}</span><span class='hs-varid'>base</span></a> <span class=hs-linenum>41: </span> <span class='hs-keyword'>where</span> <span class=hs-linenum>42: </span> <a class=annot href="#"><span class=annottext>i:{VV : (Int) | (VV >= lo) && (VV <= hi) && (lo <= VV)} -> {VV : a | ((papp2 p VV i))} -> {VV : a | ((papp2 p VV hi))}</span><span class='hs-varid'>go</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= lo) && (VV <= hi) && (lo <= VV)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>{VV : a | ((papp2 p VV i))}</span><span class='hs-varid'>acc</span></a> <span class=hs-linenum>43: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == i) && (x5 >= lo) && (lo <= x5) && (x5 <= hi)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>x1:{x14 : (Int) | (x14 >= i) && (x14 >= lo) && (i <= x14) && (lo <= x14) && (x14 <= hi)} -> x2:{x14 : (Int) | (x14 >= i) && (x14 >= lo) && (i <= x14) && (lo <= x14) && (x14 <= hi)} -> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}</span><span class='hs-varop'><</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == hi) && (lo <= x3)}</span><span class='hs-varid'>hi</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>i:{VV : (Int) | (VV >= lo) && (VV <= hi) && (lo <= VV)} -> {VV : a | ((papp2 p VV i))} -> {VV : a | ((papp2 p VV hi))}</span><span class='hs-varid'>go</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == i) && (x5 >= lo) && (lo <= x5) && (x5 <= hi)}</span><span class='hs-varid'>i</span></a><a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}</span><span class='hs-varop'>+</span></a><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>x1:(Int) -> {VV : a | ((papp2 p VV x1))} -> forall [ex:{VV : (Int) | (VV == (x1 + 1))}].{VV : a | ((papp2 p VV ex))}</span><span class='hs-varid'>f</span></a> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == i) && (x5 >= lo) && (lo <= x5) && (x5 <= hi)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>{VV : a | ((papp2 p VV i)) && (VV == acc)}</span><span class='hs-varid'>acc</span></a><span class='hs-layout'>)</span> <span class=hs-linenum>44: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : a | ((papp2 p VV i)) && (VV == acc)}</span><span class='hs-varid'>acc</span></a> </pre> Iteration Dependence -------------------- We used `loop` to write <br> <pre><span class=hs-linenum>53: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>add</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>n</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>m</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Nat</span><span class='hs-keyword'>|v=m+n}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>54: </span><span class='hs-definition'>add</span> <span class='hs-varid'>n</span> <span class='hs-varid'>m</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>loop</span> <span class='hs-num'>0</span> <span class='hs-varid'>m</span> <span class='hs-varid'>n</span> <span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-keyword'>_</span> <span class='hs-varid'>i</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>i</span> <span class='hs-varop'>+</span> <span class='hs-num'>1</span><span class='hs-layout'>)</span> </pre> <br> <div class="fragment"> **Problem** - As property only holds after *last* loop iteration... - ... cannot instantiate `α` with `{v:Int | v = n + m}` </div> Iteration Dependence -------------------- We used `loop` to write <br> <pre><span class=hs-linenum>75: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>add</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>n</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>m</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Nat</span><span class='hs-keyword'>|v=m+n}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>76: </span><span class='hs-definition'>add</span> <span class='hs-varid'>n</span> <span class='hs-varid'>m</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>loop</span> <span class='hs-num'>0</span> <span class='hs-varid'>m</span> <span class='hs-varid'>n</span> <span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-keyword'>_</span> <span class='hs-varid'>i</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>i</span> <span class='hs-varop'>+</span> <span class='hs-num'>1</span><span class='hs-layout'>)</span> </pre> <br> **Problem** Need invariant relating *iteration* `i` with *accumulator* `acc` Iteration Dependence -------------------- We used `loop` to write <br> <pre><span class=hs-linenum>92: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>add</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>n</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>m</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Nat</span><span class='hs-keyword'>|v=m+n}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>93: </span><span class='hs-definition'>add</span> <span class='hs-varid'>n</span> <span class='hs-varid'>m</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>loop</span> <span class='hs-num'>0</span> <span class='hs-varid'>m</span> <span class='hs-varid'>n</span> <span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-keyword'>_</span> <span class='hs-varid'>i</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>i</span> <span class='hs-varop'>+</span> <span class='hs-num'>1</span><span class='hs-layout'>)</span> </pre> <br> **Solution** - Abstract Refinement `p :: Int -> a -> Prop` - `(p i acc)` relates *iteration* `i` with *accumulator* `acc` Induction in `loop` (by hand) ----------------------------- <br> <pre><span class=hs-linenum>110: </span><span class='hs-definition'>loop</span> <span class='hs-varid'>lo</span> <span class='hs-varid'>hi</span> <span class='hs-varid'>base</span> <span class='hs-varid'>f</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>go</span> <span class='hs-varid'>lo</span> <span class='hs-varid'>base</span> <span class=hs-linenum>111: </span> <span class='hs-keyword'>where</span> <span class=hs-linenum>112: </span> <span class='hs-varid'>go</span> <span class='hs-varid'>i</span> <span class='hs-varid'>acc</span> <span class=hs-linenum>113: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>i</span> <span class='hs-varop'><</span> <span class='hs-varid'>hi</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>go</span> <span class='hs-layout'>(</span><span class='hs-varid'>i</span><span class='hs-varop'>+</span><span class='hs-num'>1</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>f</span> <span class='hs-varid'>i</span> <span class='hs-varid'>acc</span><span class='hs-layout'>)</span> <span class=hs-linenum>114: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>acc</span> </pre> <br> <div class="fragment"> <div align="center"> ------------ --- ---------------------------- **Assume** : `out = loop lo hi base f` **Prove** : `(p hi out)` ------------ --- ---------------------------- </div> </div> Induction in `loop` (by hand) ----------------------------- <br> <pre><span class=hs-linenum>136: </span><span class='hs-definition'>loop</span> <span class='hs-varid'>lo</span> <span class='hs-varid'>hi</span> <span class='hs-varid'>base</span> <span class='hs-varid'>f</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>go</span> <span class='hs-varid'>lo</span> <span class='hs-varid'>base</span> <span class=hs-linenum>137: </span> <span class='hs-keyword'>where</span> <span class=hs-linenum>138: </span> <span class='hs-varid'>go</span> <span class='hs-varid'>i</span> <span class='hs-varid'>acc</span> <span class=hs-linenum>139: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>i</span> <span class='hs-varop'><</span> <span class='hs-varid'>hi</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>go</span> <span class='hs-layout'>(</span><span class='hs-varid'>i</span><span class='hs-varop'>+</span><span class='hs-num'>1</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>f</span> <span class='hs-varid'>i</span> <span class='hs-varid'>acc</span><span class='hs-layout'>)</span> <span class=hs-linenum>140: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>acc</span> </pre> <br> **Base Case** Initial accumulator `base` satisfies invariant `(p base lo)` Induction in `loop` (by hand) ----------------------------- <br> <pre><span class=hs-linenum>155: </span><span class='hs-definition'>loop</span> <span class='hs-varid'>lo</span> <span class='hs-varid'>hi</span> <span class='hs-varid'>base</span> <span class='hs-varid'>f</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>go</span> <span class='hs-varid'>lo</span> <span class='hs-varid'>base</span> <span class=hs-linenum>156: </span> <span class='hs-keyword'>where</span> <span class=hs-linenum>157: </span> <span class='hs-varid'>go</span> <span class='hs-varid'>i</span> <span class='hs-varid'>acc</span> <span class=hs-linenum>158: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>i</span> <span class='hs-varop'><</span> <span class='hs-varid'>hi</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>go</span> <span class='hs-layout'>(</span><span class='hs-varid'>i</span><span class='hs-varop'>+</span><span class='hs-num'>1</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>f</span> <span class='hs-varid'>i</span> <span class='hs-varid'>acc</span><span class='hs-layout'>)</span> <span class=hs-linenum>159: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>acc</span> </pre> <br> **Inductive Step** `f` *preserves* invariant at `i` `(p acc i) => (p (f i acc) (i + 1))` Induction in `loop` (by hand) ----------------------------- <br> <pre><span class=hs-linenum>173: </span><span class='hs-definition'>loop</span> <span class='hs-varid'>lo</span> <span class='hs-varid'>hi</span> <span class='hs-varid'>base</span> <span class='hs-varid'>f</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>go</span> <span class='hs-varid'>lo</span> <span class='hs-varid'>base</span> <span class=hs-linenum>174: </span> <span class='hs-keyword'>where</span> <span class=hs-linenum>175: </span> <span class='hs-varid'>go</span> <span class='hs-varid'>i</span> <span class='hs-varid'>acc</span> <span class=hs-linenum>176: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>i</span> <span class='hs-varop'><</span> <span class='hs-varid'>hi</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>go</span> <span class='hs-layout'>(</span><span class='hs-varid'>i</span><span class='hs-varop'>+</span><span class='hs-num'>1</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>f</span> <span class='hs-varid'>i</span> <span class='hs-varid'>acc</span><span class='hs-layout'>)</span> <span class=hs-linenum>177: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>acc</span> </pre> <br> **"By Induction"** `out` satisfies invariant at `hi` `(p out hi)` Induction in `loop` (by type) ----------------------------- Induction is an **abstract refinement type** for `loop` <br> <pre><span class=hs-linenum>195: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>loop</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyword'>forall</span> <span class='hs-varid'>a</span> <span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span><span class='hs-varop'>>.</span> <span class=hs-linenum>196: </span> <span class='hs-varid'>lo</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class=hs-linenum>197: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>hi</span><span class='hs-conop'>:</span><span class='hs-keyword'>{v:</span><span class='hs-conid'>Int</span><span class='hs-keyword'>|lo <= v}</span> <span class=hs-linenum>198: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>base</span><span class='hs-conop'>:</span><span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>lo</span><span class='hs-varop'>></span> <span class=hs-linenum>199: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>f</span><span class='hs-conop'>:</span><span class='hs-layout'>(</span><span class='hs-varid'>i</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>i</span><span class='hs-varop'>></span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-layout'>(</span><span class='hs-varid'>i</span><span class='hs-varop'>+</span><span class='hs-num'>1</span><span class='hs-layout'>)</span><span class='hs-varop'>></span><span class='hs-layout'>)</span> <span class=hs-linenum>200: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>hi</span><span class='hs-varop'>></span> <span class='hs-keyword'>@-}</span> </pre> <br> Induction in `loop` (by type) ----------------------------- `p` is the *index dependent* invariant! <br> <pre><span class=hs-linenum>212: </span><span class='hs-definition'>p</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span> <span class='hs-comment'>-- invt </span> <span class=hs-linenum>213: </span><span class='hs-definition'>base</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>lo</span><span class='hs-varop'>></span> <span class='hs-comment'>-- base </span> <span class=hs-linenum>214: </span><span class='hs-definition'>f</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>i</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>i</span><span class='hs-varop'>></span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span><span class='hs-layout'>(</span><span class='hs-varid'>i</span><span class='hs-varop'>+</span><span class='hs-num'>1</span><span class='hs-layout'>)</span><span class='hs-varop'>></span> <span class='hs-comment'>-- step</span> <span class=hs-linenum>215: </span><span class='hs-definition'>out</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>hi</span><span class='hs-varop'>></span> <span class='hs-comment'>-- goal</span> </pre> Using Induction --------------- <pre><span class=hs-linenum>224: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>add</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>n</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>m</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Nat</span><span class='hs-keyword'>| v=m+n}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>225: </span><a class=annot href="#"><span class=annottext>n:{VV : (Int) | (VV >= 0)} -> m:{VV : (Int) | (VV >= 0)} -> {VV : (Int) | (VV == (m + n)) && (VV >= 0)}</span><span class='hs-definition'>add</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>m</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>. x1:(Int) -> x2:{x21 : (Int) | (x1 <= x21)} -> {x19 : (Int)<p x1> | (x19 >= 0) && (x19 >= n) && (n <= x19)} -> (i:(Int) -> {x19 : (Int)<p i> | (x19 >= 0) && (x19 >= n) && (n <= x19)} -> forall [ex:{VV : (Int) | (VV == (i + 1))}].{x19 : (Int)<p ex> | (x19 >= 0) && (x19 >= n) && (n <= x19)}) -> {x19 : (Int)<p x2> | (x19 >= 0) && (x19 >= n) && (n <= x19)}</span><span class='hs-varid'>loop</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == m) && (x3 >= 0)}</span><span class='hs-varid'>m</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == n) && (x3 >= 0)}</span><span class='hs-varid'>n</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>x1:(Int) -> x2:{x17 : (Int) | (x17 == (x1 + n)) && (x17 == (n + x1)) && (x17 >= 0) && (x17 >= x1) && (x17 >= n) && (x1 <= x17) && (n <= x17)} -> {x9 : (Int) | (x9 == (x2 + 1)) && (x9 > 0) && (x9 > x1) && (x9 > x2) && (x9 > n) && (x9 >= 0) && (x1 <= x9) && (n <= x9)}</span><span class='hs-keyglyph'>\</span></a><span class='hs-keyword'>_</span> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= n) && (n <= VV)}</span><span class='hs-varid'>z</span></a> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == z) && (x5 >= 0) && (x5 >= n) && (n <= x5)}</span><span class='hs-varid'>z</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}</span><span class='hs-varop'>+</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a><span class='hs-layout'>)</span> </pre> <br> **Verified** by instantiating the abstract refinement of `loop` `p := \i acc -> acc = i + n` Using Induction --------------- <div/> <pre><span class=hs-linenum>239: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>add</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>n</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>m</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Nat</span><span class='hs-keyword'>| v=m+n}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>240: </span><span class='hs-definition'>add</span> <span class='hs-varid'>n</span> <span class='hs-varid'>m</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>loop</span> <span class='hs-num'>0</span> <span class='hs-varid'>m</span> <span class='hs-varid'>n</span> <span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-keyword'>_</span> <span class='hs-varid'>z</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>z</span> <span class='hs-varop'>+</span> <span class='hs-num'>1</span><span class='hs-layout'>)</span> </pre> <br> Verified by instantiating `p := \i acc -> acc = i + n` - <div class="fragment">**Base:** `n = 0 + n`</div> - <div class="fragment">**Step:** `acc = i + n => acc + 1 = (i + 1) + n`</div> - <div class="fragment">**Goal:** `out = m + n`</div> Generalizes To Structures ------------------------- Same idea applies for induction over *structures* ... Structural Induction ==================== Example: Lists -------------- <br> <pre><span class=hs-linenum>269: </span><span class='hs-keyword'>data</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>N</span> <span class=hs-linenum>270: </span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>C</span> <span class='hs-varid'>a</span> <span class='hs-layout'>(</span><span class='hs-conid'>L</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> </pre> <br> <div class="fragment"> Lets write a generic loop over such lists ... </div> Example: `foldr` ---------------- <br> <pre><span class=hs-linenum>283: </span><span class='hs-definition'>foldr</span> <span class='hs-varid'>f</span> <span class='hs-varid'>b</span> <span class='hs-conid'>N</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>b</span> <span class=hs-linenum>284: </span><span class='hs-definition'>foldr</span> <span class='hs-varid'>f</span> <span class='hs-varid'>b</span> <span class='hs-layout'>(</span><span class='hs-conid'>C</span> <span class='hs-varid'>x</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>f</span> <span class='hs-varid'>xs</span> <span class='hs-varid'>x</span> <span class='hs-layout'>(</span><span class='hs-varid'>foldr</span> <span class='hs-varid'>f</span> <span class='hs-varid'>b</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span> </pre> <br> <div class="fragment"> Lets brace ourselves for the type... </div> Example: `foldr` ---------------- <pre><span class=hs-linenum>297: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>foldr</span> <span class='hs-keyglyph'>::</span> <span class=hs-linenum>298: </span> <span class='hs-keyword'>forall</span> <span class='hs-varid'>a</span> <span class='hs-varid'>b</span> <span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span><span class='hs-varop'>>.</span> <span class=hs-linenum>299: </span> <span class='hs-layout'>(</span><span class='hs-varid'>xs</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>xs</span><span class='hs-varop'>></span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span><span class='hs-layout'>(</span><span class='hs-conid'>C</span> <span class='hs-varid'>x</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span><span class='hs-varop'>></span><span class='hs-layout'>)</span> <span class=hs-linenum>300: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-conid'>N</span><span class='hs-varop'>></span> <span class=hs-linenum>301: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>ys</span><span class='hs-conop'>:</span><span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class=hs-linenum>302: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>ys</span><span class='hs-varop'>></span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>303: </span><a class=annot href="#"><span class=annottext>forall a b <p :: (Loop.L a)-> b-> Bool>. (xs:(L a) -> x:a -> {VV : b<p xs> | true} -> forall [ex:{VV : (L a) | (VV == (Loop.C x xs))}].{VV : b<p ex> | true}) -> forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : b<p ex> | true} -> ys:(L a) -> {VV : b<p ys> | true}</span><span class='hs-definition'>foldr</span></a> <a class=annot href="#"><span class=annottext>xs:(L a) -> x:a -> {VV : b | ((papp2 p VV xs))} -> forall [ex:{VV : (L a) | (VV == (Loop.C x xs))}].{VV : b | ((papp2 p VV ex))}</span><span class='hs-varid'>f</span></a> <a class=annot href="#"><span class=annottext>forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : a | ((papp2 p VV ex))}</span><span class='hs-varid'>b</span></a> <span class='hs-conid'>N</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : a | ((papp2 p VV ex))}</span><span class='hs-varid'>b</span></a> <span class=hs-linenum>304: </span><span class='hs-definition'>foldr</span> <span class='hs-varid'>f</span> <span class='hs-varid'>b</span> <span class='hs-layout'>(</span><span class='hs-conid'>C</span> <span class='hs-varid'>x</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:(L a) -> x2:a -> {VV : b | ((papp2 p VV x1))} -> forall [ex:{VV : (L a) | (VV == (Loop.C x2 x1))}].{VV : b | ((papp2 p VV ex))}</span><span class='hs-varid'>f</span></a> <a class=annot href="#"><span class=annottext>{x2 : (L a) | (x2 == xs)}</span><span class='hs-varid'>xs</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>forall <p :: (Loop.L a)-> b-> Bool>. (xs:(L a) -> x:a -> {VV : b<p xs> | true} -> forall [ex:{VV : (L a) | (VV == (Loop.C x xs))}].{VV : b<p ex> | true}) -> forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : b<p ex> | true} -> x4:(L a) -> {VV : b<p x4> | true}</span><span class='hs-varid'>foldr</span></a> <a class=annot href="#"><span class=annottext>x1:(L a) -> x2:a -> {VV : b | ((papp2 p VV x1))} -> forall [ex:{VV : (L a) | (VV == (Loop.C x2 x1))}].{VV : b | ((papp2 p VV ex))}</span><span class='hs-varid'>f</span></a> <a class=annot href="#"><span class=annottext>forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : a | ((papp2 p VV ex))}</span><span class='hs-varid'>b</span></a> <a class=annot href="#"><span class=annottext>{x2 : (L a) | (x2 == xs)}</span><span class='hs-varid'>xs</span></a><span class='hs-layout'>)</span> </pre> <br> <div class="fragment"> Lets step through the type... </div> `foldr`: Abstract Refinement ---------------------------- <div/> <pre><span class=hs-linenum>318: </span><span class='hs-definition'>p</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span> <span class=hs-linenum>319: </span><span class='hs-definition'>step</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>xs</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>xs</span><span class='hs-varop'>></span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span><span class='hs-layout'>(</span><span class='hs-conid'>C</span> <span class='hs-varid'>x</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span><span class='hs-varop'>></span> <span class=hs-linenum>320: </span><span class='hs-definition'>base</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-conid'>N</span><span class='hs-varop'>></span> <span class=hs-linenum>321: </span><span class='hs-definition'>ys</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class=hs-linenum>322: </span><span class='hs-definition'>out</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>ys</span><span class='hs-varop'>></span> </pre> <br> `(p xs b)` relates `b` with folded `xs` `p :: L a -> b -> Prop` `foldr`: Base Case ------------------ <div/> <pre><span class=hs-linenum>336: </span><span class='hs-definition'>p</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span> <span class=hs-linenum>337: </span><span class='hs-definition'>step</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>xs</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>xs</span><span class='hs-varop'>></span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span><span class='hs-layout'>(</span><span class='hs-conid'>C</span> <span class='hs-varid'>x</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span><span class='hs-varop'>></span> <span class=hs-linenum>338: </span><span class='hs-definition'>base</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-conid'>N</span><span class='hs-varop'>></span> <span class=hs-linenum>339: </span><span class='hs-definition'>ys</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class=hs-linenum>340: </span><span class='hs-definition'>out</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>ys</span><span class='hs-varop'>></span> </pre> <br> `base` is related to empty list `N` `base :: b<p N>` states `foldr`: Ind. Step ------------------ <div/> <pre><span class=hs-linenum>355: </span><span class='hs-definition'>p</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span> <span class=hs-linenum>356: </span><span class='hs-definition'>step</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>xs</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>xs</span><span class='hs-varop'>></span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span><span class='hs-layout'>(</span><span class='hs-conid'>C</span> <span class='hs-varid'>x</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span><span class='hs-varop'>></span> <span class=hs-linenum>357: </span><span class='hs-definition'>base</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-conid'>N</span><span class='hs-varop'>></span> <span class=hs-linenum>358: </span><span class='hs-definition'>ys</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class=hs-linenum>359: </span><span class='hs-definition'>out</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>ys</span><span class='hs-varop'>></span> </pre> <br> `step` extends relation from `xs` to `C x xs` `step :: xs:L a -> x:a -> b<p xs> -> b<p(C x xs)>` `foldr`: Output --------------- <div/> <pre><span class=hs-linenum>373: </span><span class='hs-definition'>p</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span> <span class=hs-linenum>374: </span><span class='hs-definition'>step</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>xs</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>xs</span><span class='hs-varop'>></span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span><span class='hs-layout'>(</span><span class='hs-conid'>C</span> <span class='hs-varid'>x</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span><span class='hs-varop'>></span> <span class=hs-linenum>375: </span><span class='hs-definition'>base</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-conid'>N</span><span class='hs-varop'>></span> <span class=hs-linenum>376: </span><span class='hs-definition'>ys</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class=hs-linenum>377: </span><span class='hs-definition'>out</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>b</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>ys</span><span class='hs-varop'>></span> </pre> <br> Relation holds between `out` and input list `ys` `out :: b<p ys>` Using `foldr`: Size ------------------- We can now verify <br> <pre><span class=hs-linenum>392: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>size</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>xs</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Int</span><span class='hs-keyword'>| v = (llen xs)}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>393: </span><a class=annot href="#"><span class=annottext>forall a. xs:(L a) -> {VV : (Int) | (VV == (llen xs))}</span><span class='hs-definition'>size</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall <p :: (Loop.L a)-> (GHC.Types.Int)-> Bool>. (xs:(L a) -> x:a -> {x12 : (Int)<p xs> | (x12 >= 0)} -> forall [ex:{VV : (L a) | (VV == (Loop.C x xs))}].{x12 : (Int)<p ex> | (x12 >= 0)}) -> forall [ex:{VV : (L a) | (VV == (Loop.N))}].{x12 : (Int)<p ex> | (x12 >= 0)} -> x4:(L a) -> {x12 : (Int)<p x4> | (x12 >= 0)}</span><span class='hs-varid'>foldr</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>x1:(L a) -> a -> x3:{x8 : (Int) | (x8 == (llen x1)) && (x8 >= 0)} -> {x5 : (Int) | (x5 == (x3 + 1)) && (x5 > 0) && (x5 > x3) && (x5 >= 0)}</span><span class='hs-keyglyph'>\</span></a><span class='hs-keyword'>_</span> <span class='hs-keyword'>_</span> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>n</span></a> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == n) && (x3 >= 0)}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}</span><span class='hs-varop'>+</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a> </pre> <br> <div class="fragment"> Verified by automatically instantiating `p := \xs acc -> acc = (llen xs)` </div> Using `foldr`: Append --------------------- <pre><span class=hs-linenum>408: </span><span class='hs-keyword'>{-@</span> <span class='hs-layout'>(</span><span class='hs-varop'>++</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>xs</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>ys</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-conid'>Cat</span> <span class='hs-varid'>a</span> <span class='hs-varid'>xs</span> <span class='hs-varid'>ys</span><span class='hs-layout'>)</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>409: </span><a class=annot href="#"><span class=annottext>(L a)</span><span class='hs-definition'>xs</span></a> <a class=annot href="#"><span class=annottext>forall a. xs:(L a) -> ys:(L a) -> {VV : (L a) | ((llen VV) == ((llen xs) + (llen ys)))}</span><span class='hs-varop'>++</span></a> <a class=annot href="#"><span class=annottext>(L a)</span><span class='hs-varid'>ys</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall <p :: (Loop.L a)-> (Loop.L a)-> Bool>. (xs:(L a) -> x:a -> {x8 : (L a)<p xs> | true} -> forall [ex:{VV : (L a) | (VV == (Loop.C x xs))}].{x8 : (L a)<p ex> | true}) -> forall [ex:{VV : (L a) | (VV == (Loop.N))}].{x8 : (L a)<p ex> | true} -> x4:(L a) -> {x8 : (L a)<p x4> | true}</span><span class='hs-varid'>foldr</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>(L a) -> a -> x3:(L a) -> {x2 : (L a) | ((llen x2) == (1 + (llen x3)))}</span><span class='hs-keyglyph'>\</span></a><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>a -> x2:(L a) -> {x2 : (L a) | ((llen x2) == (1 + (llen x2)))}</span><span class='hs-conid'>C</span></a><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>{x2 : (L a) | (x2 == ys)}</span><span class='hs-varid'>ys</span></a> <a class=annot href="#"><span class=annottext>{x2 : (L a) | (x2 == xs)}</span><span class='hs-varid'>xs</span></a> </pre> <br> <div class="fragment"> where the alias `Cat` is: <br> <pre><span class=hs-linenum>421: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>Cat</span> <span class='hs-varid'>a</span> <span class='hs-conid'>X</span> <span class='hs-conid'>Y</span> <span class='hs-keyglyph'>=</span> <span class=hs-linenum>422: </span> <span class='hs-layout'>{</span><span class='hs-varid'>v</span><span class='hs-conop'>:</span><span class='hs-conid'>L</span> <span class='hs-varid'>a</span><span class='hs-keyglyph'>|</span><span class='hs-layout'>(</span><span class='hs-varid'>llen</span> <span class='hs-varid'>v</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>(</span><span class='hs-varid'>llen</span> <span class='hs-conid'>X</span><span class='hs-layout'>)</span> <span class='hs-varop'>+</span> <span class='hs-layout'>(</span><span class='hs-varid'>llen</span> <span class='hs-conid'>Y</span><span class='hs-layout'>)</span><span class='hs-layout'>}</span> <span class='hs-keyword'>@-}</span> </pre> </div> Using `foldr`: Append --------------------- <div/> <pre><span class=hs-linenum>431: </span><span class='hs-keyword'>{-@</span> <span class='hs-layout'>(</span><span class='hs-varop'>++</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>xs</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>ys</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-conid'>Cat</span> <span class='hs-varid'>a</span> <span class='hs-varid'>xs</span> <span class='hs-varid'>ys</span><span class='hs-layout'>)</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>432: </span><span class='hs-definition'>xs</span> <span class='hs-varop'>++</span> <span class='hs-varid'>ys</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>foldr</span> <span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>C</span><span class='hs-layout'>)</span> <span class='hs-varid'>ys</span> <span class='hs-varid'>xs</span> </pre> <br> <div class="fragment"> Verified by automatically instantiating `p := \xs acc -> llen acc = llen xs + llen ys` </div> Recap ----- Abstract refinements decouple *invariant* from *traversal* <br> + <div class="fragment">*reusable* specifications for higher-order functions.</div> + <div class="fragment">*automatic* checking and instantiation by SMT.</div> Recap ----- 1. **Refinements:** Types + Predicates 2. **Subtyping:** SMT Implication 3. **Measures:** Strengthened Constructors 4. **Abstract:** Refinements over Type Signatures + *Dependencies* + <div class="fragment">*Induction*</div>