---
title: "Mirror proof"
breaks: false
---

# Proof

**Claim.**
For any tree $t : \alpha \ \mathsf{tree}$, we have $\mathsf{mirror} (\mathsf{mirror} \ t) \cong t$.

graph btree {
    1 -- 2;
    1 -- 3;
    2 -- 4;
    2 -- 5;
    3 -- 6;
    3 -- 7;
    
}

## Idiomatic Structural Induction

Definition of Mirror:

let rec mirror (t : 'a tree) : 'a tree = match t with
  | Leaf -> Leaf
  | Node(a, x, b) -> Node((mirror b), x, (mirror a))
;;

**Proof.**
By structural induction, we will show that $\forall t$ where $t$ is an $\alpha \ tree$, it holds that $mirror(mirror(t)) \cong t$:

- If $t$ is a $Leaf$, it is clear that $mirror(t) \cong t$, by definition of $mirror$. Applying $mirror$ to $t$, we can see by substitution that $mirror(mirror(t)) \cong t$. Therefore, the base case holds.
- If $t$ is a $Node(L, x, R)$, when evaluating $mirror(t)$ we observe that $mirror$ is recursively applied to $L$ and $R$, yielding $Node(mirror(R), x, mirror(L))$.
Therefore, applying $mirror(mirror(Node(L,x,R)))$ gives us $Node(mirror(mirror(L)), x, mirror(mirror(R)))$. By Inductive Hypothesis, $mirror(mirror(L))$ and $mirror(mirror(R))$ give us $L$ and $R$, respectively. The expression then reduces to $Node(L,x,R)$.

Thus, the induction proceeds, so the claim holds for all $t : \alpha \ tree$.

We see that our claim is proven $\forall t$ where $t$ is an $\alpha \ tree$.

---

- If $t$ is a $Leaf$, it is clear that $mirror(Leaf) \cong Leaf$, by definition of $mirror$. Thus, $mirror(mirror(t)) = t$ as well, so the base case holds.
- If $t \cong Leaf$, then the claim holds trivially.

---

(* data type with two variants *)
type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree

type expr = Const of int | Sum of expr * expr | Mul of expr * expr

Sum (Mul (Const 3, Const 5), Const 7) (* (3 * 5) + 7)

val eval : expr -> int

show something about like $\mathsf{eval} \ x$ for all expressions $x$

*Proof.*
By structural induction on $x$:
- If $x \cong \mathsf{Const}(n)$ for some $n$, then ....
- If $x \cong \mathsf{Sum}(a, b)$ where $a, b: \mathsf{expr}$, thnen suppose inductively that ... and then ...
- If $x \cong \mathsf{Mul}(a, b)$ where $a, b: \mathsf{expr}$, thnen suppose inductively that ... and then ...

## Original Structural Induction

Definition of Mirror:

let rec mirror (t : 'a tree) : 'a tree = match t with
  | Leaf -> Leaf
  | Node(a, x, b) -> Node((mirror b), x, (mirror a))
;;

$Case: T = Leaf$.

Note that
\begin{align}
mirror(Leaf) = Leaf\\
\therefore \ mirror(mirror(Leaf)) = Leaf
\end{align}
$Case: T = Node(L, x, R)$ For some trees $L$ and $R$.

Note that
$$
\begin{align}
mirror(mirror(Node(L,x,R))) & = mirror(Node(mirror(R), x, mirror(L))) &&\text{Definition of mirror}\\
& = Node(mirror(mirror(L)), x, mirror(mirror(R)))) &&\text{Definition of mirror}\\
& = Node(L, x, R) &&\text{Inductive Hypothesis}
\end{align}
$$

Thus the assertion $mirror(mirror(T)) = T \ \forall \ T$ is proven by structural induction.

created with some help from: [University of Washington](https://courses.cs.washington.edu/courses/cse311/17au/sections/07/section07-solutions.pdf)

## Bad Mathematical Induction
Given a binary tree of nodes `1` to `n`, where `1` identifies the root node, it is possible to find the position of the node within a given level of the tree with the following relation:

$$
p(n) = n - 2^{floor(\log_2 n)} + 1
$$

where $p(4) = 1$, $p(7) = 4$, $p(3) = 2$ etc.

The maximum index of node n within it's current level can be defined as follows:

$$
i_{max}(n) = 2^{floor(\log_2n + 1)}
$$

where $i_{max}(4) = i_{max}(5) = i_{max}(6) = i_{max}(7) = 7$

A function that creates a mirror of an existing tree effectively translates all nodes across the tree's center axis. The length and direction of this translation can be calculated as a function of the max index at the current depth relative to the node's position:
$$
reverse(n) = i_{max}(n) - p(n)
$$

Put in terms of n and simplified, we get
$$
reverse(n) = 3*2^{floor(\log_2n)} - n - 1
$$

### Base Case
For a tree of a single leaf node
$$
reverse(1) = 1
$$
therefore
$$
reverse(reverse(1)) = 1
$$
for our base case.

## Structural-mathematical induction

### Covered

- $\forall a. \phi(a)$ is a "universal quantification"
- to prove a universal quantification, pick some arbitrary $a$ and show that $\phi(a)$ holds
- congruence, as distinct from equality
- "recursive proofs", "unwinding/unrolling"
- mathematical notation: lambdas, function types, "Currying" (functions of multiple arguments are the same thing as nested functions), $\mathbb Z$/$\mathbb R$
- structure of a proof
- we didn't really get to the different kinds of induction

**Theorem.**
For any tree $t : \alpha \ \mathsf{tree}$, it holds that $\mathsf{reverse}(\mathsf{reverse} \ t) \cong t$.

Let $(\cong)$ be the smallest relation such that:

- if $x$ and $y$ are numbers and $x = y$, then $x \cong y$
- likewise bool, str, array; types that have $(=)$
- let's ignore floats for now
- if $f : \alpha \to \beta$, and $x : \alpha$, then $f \ x \cong \text{the thing that you get when you evaluate \(f\) at \(x\)}$
- if $\alpha$ and $\beta$ are types, and $f, g : \alpha \to \beta$, and $f$ and $g$ are pure total functions, and (**for all** $a : \alpha$, it holds that $f \ a \cong g \ a$), then $f \cong g$.

**Claim:**
$(\lambda (x : \mathbb Z). x \cdot 2) \cong (\lambda (x : \mathbb Z). x + x)$

**Proof:**
Let $f = (\lambda (x : \mathbb Z). x \cdot 2)$, and $g = (\lambda (x : \mathbb Z). x + x)$.
Then $f, g : \mathbb Z \to \mathbb Z$. (`f : int -> int`, `g : int -> int`)
And $f$ and $g$ are pure and total.

Now, want to show: $\forall (a : \mathbb Z). \ f \ a = g \ a$.
(We want to prove this universal quantification.)
Let $a$ be any element of $\mathbb Z$.
Then show that $f \ a = g \ a$.
$f \ a = (\lambda (x : \mathbb Z). x \cdot 2) \ a = a \cdot 2$.
$g \ a = (\lambda (x : \mathbb Z). x + x) \ a = a + a$.

By arithmetic, $a \cdot 2 = a + a$.
So, $f \ a = g \ a$.
So, by the definition of universal quantification, $\forall (a : \mathbb Z). \ f \ a = g \ a$.

So, $f \cong g$, by definition of $\cong$.
'

---

Question:
$(\lambda x. (\lambda y. x + y)) \overset?\cong (\lambda x. \lambda y. y + x)$

let $f = (\lambda x. (\lambda y. x + y))$.
what's the type of $f$?
$f : \mathbb R \to (\mathbb R \to \mathbb R)$

> - if $\alpha$ and $\beta$ are types, and $f, g : \alpha \to \beta$, and $f$ and $g$ are pure total functions, and (**for all** $a : \alpha$, it holds that $f \ a = g \ a$), then $f \cong g$.

Define $\alpha = \mathbb R$, $\beta = (\mathbb R \to \mathbb R)$.
Then, $f : \alpha \to \beta$.
Assume pure, total.

Now, want to show: $\forall (a : \mathbb R). \ f \ a = g \ a$.
Pick some arbitrary $a : \mathbb R$.
$f \ a \cong (\lambda x. (\lambda y. x + y))a \cong (\lambda y.a + y)$
$g \ a \cong (\lambda x. (\lambda y. y + x))a \cong (\lambda y.y + a)$

Want to show: $f \ a \cong g \ a$.

How do we show that? Well, $f \ a$ is a function...
Want to show: $\forall (b: \mathbb R). f\ a\ b \cong g\ a\ b$.
For some arbitrary $b: \mathbb R$

$f \ a = (\lambda y.a + y)$
$(f \ a) \ b \cong (\lambda y.a + y) \ b \cong a + b$
$(g \ a) \ b \cong (\lambda y.y + a) \ b \cong b + a$

by arithmetic, $a+b = b+a$
$(f \ a) \ b \cong (g \ a) \ b$
so, by defn of congruence, $f \ a \cong g \ a$
Again, by defn of congruence, $f \cong g$

- "Is $f\ a = g\ a$?" Not well defined, since $f\ a$ and $g\ a$ are functions, which aren't equality types.
- "Is $f\ a \cong g\ a$?" Maybe! We have a defn. for that.

> proof sketch:
> "is `(x) => (y) => x + y` congruent to `x=>y=>y+x`?"
> well, for some fixed `a`, is `(y) => a+y` cong to `(y) => y+a`?
> well again, for some fixed `b`, is `a+b` cong to `b+a`?
> yes!
> so yes!
> so yes!

f = (x, y) => x + y
f = (x) => ((y) => x + y)

---

different proof

$\forall (x : \mathbf{Bool}). \ x = \lnot \lnot x$.
Let $b$ be any element of **Bool**.
Then we want to show that $b = \lnot \lnot b$.
Because **Bool** is a finite type, either $b = \top$ or $b = \bot$.
Proof by cases:
- if true, $\top = \lnot \bot = \lnot \lnot \top$. thus it holds for $b$
- if false, .... thus, it still holds for $b$
in any case, it holds that $b = \lnot\lnot b$.

Thus, $\forall (x : \mathbf{Bool}). \ x = \lnot \lnot x$.

## Take Home Proofs

**Claim 1:**

For all trees $t : \alpha \ \mathsf{tree}$

If $t : \alpha \ \mathsf{tree}$, then $$\mathsf{treeMap} \ \mathsf{id} \ t \cong t.$$

where

$$\mathsf{id} \cong (\lambda x.x)$$

$$\mathsf{id} : \forall \alpha. \alpha \to \alpha$$

and
<!-- $$\mathsf{treeMap} \cong (\lambda(\lambda x.y). (\lambda x \ tree.y \ tree))$$ -->

$$\mathsf{treeMap} : \forall \alpha. \forall \beta. (\alpha \to \beta) \to \alpha \ T \to \beta \ T$$

type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree;;

let rec treeMap (f : 'a -> 'b) (t : 'a tree) : 'b tree = match t with
  | Leaf -> Leaf
  | Node(x,a,y) -> Node((treeMap f x),f a, (treeMap f y))
;;

$\lambda \_. \square$: function, value, expression --- not a function interface, type, type family

$(\lambda y. y)$: second $y$ is the output, sometimes it's a simple math operation, sometimes it's an abstract symbol that may be different from the input. in general, this is an expression that may depend on the input parameter.

$\lambda x. \texttt{fetch("http://example.com/" + \(x\)).json().field}$

(f) => fetch("..." + x).json().field

f = (x) => x/2
g = () => 7

array.map(f)
array.map(g)
array.map((x) => x/2)

array.map( (x + 1) => 7 )

function f(x) { return 7 }

f = lambda (lambda y. y). 7

f(1)

$\lambda x. x \cong \lambda y. y$

thoughts:

- lambda defines a named input
- specific application of an abstract output
- $\lambda \alpha. \beta$: valid lambda, but we don't know much about what it does
- $\alpha$-substitution: "renaming"
- $\beta$-reduction: substitution
- $\alpha$ and $\beta$ represent classes of inputs (types?)
- substitute with concrete input to get a concrete output
- "$\lambda$-abstraction": something like $\lambda x. \text{something using \(x\)}$
- sub: take a $\lambda$-abstraction and a concrete value (argument), compute the output

$[v/x] e$ read as "substitute the value $v$ for occurrences of the name $x$ in the expression $e$"

function f(x) {
  const y = x + 1;
  return y * x;
}

f(7)  // let's perform beta-reduction here
=>
{
  const y = 7 + 1;
  return y * 7;
}

[7/x] { const y = x + 1; return y * x; }
=> { const y = 7 + 1; return y * 7; }

To evaluate an expression of the form $(\lambda x. e) v$, perform $[v/x]e$, and that's your result of the first step of evaluation.

STEPS FOR SUBSTITUTION/BETA-REDUCTION

1. "the function" and "the argument": `f(v)`
2. "the function" itself is like `lambda(x) { e }`: "the name" and "the body" (which is an expression)
3. DECLARATION: substition occurs given a **name** (a name), a **body** (expr), and an **argument** (value)
4. Take the body (discard the lambda skeleton), and replace occurrences of the name with the argument.

(\lambda x. 7 + x) 12
  function: \lambda x. 7 + x
  name: x
  body: 7 + x
  argument: 12
  result: 7 + 12

(\lambda (\lambda y. y). 7) 12
  function: \lambda (\lambda y. y). 7
  name: \lambda y. y, x + 1
  body: 7
  argument: 12
  result: 7

(function(function(y) { return y }) { return 7 })(12)

f = (\lambda x. x)
g = (\lambda y. y)

f(g)


[KIND OF THING: fn application] (\lambda x. x) (\lambda y. y)
[KIND OF THING: lambda expression (value)] (\lambda y. y)

 4. Take the body (discard the lambda skeleton), and replace occurrences of the name with the argument.


[KIND OF THING: fn application]
(\lambda f. f f) (\lambda g. g g)
(\lambda g. g g) (\lambda g. g g) 
  function: (\lambda g. g g)
  name: g
  body: g g 
  argument: \lambda g. g g
  result: (\lambda g. g g) (\lambda g. g g)
(\lambda g. g g) (\lambda g. g g)
(\lambda g. g g) (\lambda g. g g)
(\lambda g. g g) (\lambda g. g g)
(\lambda g. g g) (\lambda g. g g)
...

let foo = getTheFoo();
let foo = process(foo);
let foo = process2(foo);
let foo = frobnicate(foo);
return foo;

(function(foo) {
  return (function(foo) {
    return process2(foo);
  })(process(foo));
})

$\omega = \lambda x. \ x \ x$

k = (x) => ((x) => x);
function k(x) {
  function z(x) { return x; }
}

k(7)(12)
k(7)(12) = ((x) => x)(12) = 7


// friendGroups: [["kevin", "wc"], ["kevin", "dl"]]
function renderAllTheThings(friendGroups) {
  return friendsGroups.map((x) => {  // x: ["kevin", "wc"]
    const n = x.length;
    return <span>{n}{x.map((x2) => {
      <span> friend named {x2} </span>
    }
    )}</span>
  })
}


[]

Substitution that supports shadowing be like:
- "take the Body, traverse the expression, and replace any occurrence of the Name with the Argument, BUT if you ever enter a lambda expression whose parameter is ALSO the Name, then don't enter the lambda"

  

f1 = (x) => x + 1
f2 = (x) => x * 2

PI = 3.14
function() { return PI }


(\lambda \lambda \lambda . . . x y)

3.15 = 3.14
function(PI) { return PI }


\lambda y.7

(\lambda x. (\lambda y. (x))) 7 12
1. (\lambda y.7) 12
2. 7

(\lambda (\lambda y. y). 7) 12




\lambda z. (\lambda x. (\lambda y. (x)))

beta reduction returns an expression but it may or may not return a value

(\lambda x. x + 1)(7)
7 + 1 => 8

**Proof:** Let $t: \alpha \ tree$ and $\mathsf{id} = (\lambda x.x)$ and $f = \lambda\alpha.\beta$ $\mathsf{treeMap} = \lambda(\lambda a.b).(\lambda \ at.bt)$. In $\mathsf{treeMap}$, $\beta$ is an abstraction and $\alpha$ may intersect with $\beta$. We are free to apply $\mathsf{id}$ to $\mathsf{treeMap}$ by definition of $b$ as $a$ in this case. Through substitution, we get

let id (a) = a
let rec treeMap id (t : 'a tree): 'a tree = match t with
  | Leaf -> Leaf
  | Node(x,a,y) -> Node((treeMap id x),id a, (treeMap id y))
;;

Because $\mathsf{id}$ is substituted for $f$, the resultant $\mathsf{idMap}$ returns $a$ trees. This is due to the way treeMap is defined. The output of $f$ defines the type of tree that is returned from $\mathsf{treemap}$.

This leaves us with the task of walking through this function definition.

$Case: T = Leaf$.

by definition
\begin{align}
idMap(Leaf) & = Leaf
\end{align}
$Case: T = Node(L, x, R)$ For some trees $L$ and $R$.

Note that
$$
\begin{align}
idMap(Node(L,x,R))) & = Node(treeMap \ id \ L, id \ x, treeMap \ id \ R)) &&\text{Definition of treeMap}\\
& = Node( treeMap \ L, x, treeMap \ R )) &&\text{Definition of identity}\\
& = Node(L, x, R) &&\text{Inductive Hypothesis}
\end{align}
$$

Because both cases reduce to the inputs, we have shown that:

$$\mathsf{treeMap} \ \mathsf{id} \ t \cong t.$$

**Proof Plan:**

Let $t: \alpha \ tree$, any tree.
Plan:
- show what `treeMap id` looks like
- assume that `t` is a leaf
- reduce `(treeMap id) t` to show that it's congruent to `t`

(fn t -> (match t with
    Leaf -> Leaf
    Node(x,a,y) -> Node((treeMap id x),id a,(treeMap id y))
)) t

Consider cases:

axioms: if $a \cong b$ and $b \cong c$, then $a \cong c$ (transitivity)
symm

- *case 1*: if $t$ is `Leaf`. then the `match` expr enters the `Leaf ->` pattern, and evaluates to `Leaf`. so $\mathsf{treeMap} \ \mathsf{id} \ t \cong \mathsf{Leaf}$. and we also know that $t \cong \mathsf{Leaf}$, so $\mathsf{Leaf} \cong t$. therefore, by symemtry and transitivty of $\cong$, $\mathsf{treeMap} \ \mathsf{id} \ t \cong t$.
- *case 2*: if $t$ is `Node`, then the `match` expr enters the `Node(x,a,y) ->` pattern. Starting with the second element, we can apply `id` to `a`, which evaluates to `a`. For the first and third elements, we will inductively show that they evaluate to `x` and `y` respectively.

- what if neither of those? impossible, because we assumed that it's an $\alpha \ \mathsf{tree}$

If we apply $\mathsf{id}$ as an argument in $\mathsf{treeMap}$ and then apply that to $t$ we have
$$ \mathsf{treeMap \ id} \ t \cong (\lambda(\lambda x.x).(\lambda x \ tree.x \ tree))$$

let outer = treeMap  (* just the whole thing *)
let inner = treeMap id  (* application of outer function to our particular mapper *)
                        (* the actual function that operates on trees *)

We observe that that $\mathsf{treeMap}$ contains two functions that conform to the definition of the identity. We therefore are able to apply both functions and are left with
$$ \mathsf{treeMap \ id} \ t \cong \alpha \ tree $$
and therefore have
$$ \mathsf{treeMap \ id} \ t \cong t $$

---
**Claim 2:** If $f : \alpha \to \beta$ and $g : \beta \to \gamma$, and $t : \alpha \ \mathsf{tree}$, then $$\mathsf{cart} \ g \ (\mathsf{cart} \ f \ t) \cong \mathsf{cart} \ (\mathsf{swish} \ f \ g) \ t.$$

where
$$\mathsf{swish} = (\lambda((\lambda\alpha.\beta).(\lambda\beta.\gamma).(\lambda \alpha.\gamma)))$$

**Proof:**
Evaluating $\mathsf{cart} \ g \ (\mathsf{cart} \ f \ t)$ as a lambda yields
$$ \mathsf{cart} \ g \ (\mathsf{cart} \ f \ t) \cong $$