## Refinement Reflection

Reflect function definition into its result refined type.

## Refinement Types

Types + Logical Predicates

Used for Specification

## Specification & Termination & Verification

We user refinement types for specification & termination

## Propositions

Propositions are refined unit types

```
type Proof = ()
```

with SMT-automated proofs

## Universal & Existential Propositions

Function arguments for universals## Refinement Reflection

How do we talk about user defined functions e.g., `fib`

?

## Step 1: Definition

In the logic, `fib`

is an uninterpreted function

## Step 2: Reflection

The Haskell definition of `fib`

is reflected into the type

```
fib :: i:Nat -> { v:Nat | v = fib i && fibP i }
```

where
```
fibP i = if i <= 1 then fib i = i
else fib i = fib (i-1) + fib (i-2)
```

## Step 3: Application

To prove that `fib 2 == 1`

we call `fib`

on `0`

, `1`

, and `2`

.

This does not look good ...

## Proof structure is not important ...

... as long as it has proper applications.

Still does not look good ...

## Equational Proofs

ProofCombinators library to structure proof terms.

```
data QED = QED
(***) :: a -> QED -> Proof
_ *** QED = ()
```

```
(==.) :: x:a -> a -> {v:a | v == x }
```

## Equational Proofs in Practice

We rewrite the `fib2`

proof using ProofCombinators.

Finally, looks like a proof!

## “Because” Combinators

We extend `(==.)`

to take an optional proof argument and ...

... define a dollar like `(?)`

combinator.

## Arithmetic and Ordering

Similarly, we use arithmetic proof combinators for arithmetic proofs.

## Induction

Since`fib`

increases locally, it is also monotonic.
## Higher Order Reasoning

Every function that increases locally, is also monotonic.## Instantiation of Higher Order Theorems

We get back monotonicity of `fib`

...

... by application of the general `fMono`

theorem.

## What about automation?

**Observation:** Since all reflected functions are terminating, ...

... their unfoldings are also termining,

... so unfolding can be **predictably** automated.

## Proof by Logical Evaluation (*PLE*)

**In theory:**Repeatedly unfold each function that statically unfolds.**In practise:**

## Summary:

Refinement Reflection and Proof by Logical Evaluation combined ...

... allow for complete verification with SMT-automation!

- Case Study:
**MapReduce Equivalence**