Library Size

Require Export Encoding.

Internalized size of terms


Definition Size := R (.\ "Size", "t"; "t" (.\"n"; !(enc 1))
                                          (.\"t1", "t2"; !Add ("Size" "t1") ("Size" "t2"))
                                          (.\"t"; !Add !(enc 1) ("Size" "t")) ).

Lemma Size_correct s : Size (tenc s) == enc (size s).
Proof.
  induction s.
  - crush.
  - transitivity ((Add ((lam (Size #0)) (tenc s1)) ((lam (Size #0)) (tenc s2)))).
    crush.
    now rewrite !Eta, IHs1, IHs2, Add_correct; value.
  - transitivity (Add (enc 1) ((lam (Size #0)) (tenc s))). crush.
    now rewrite !Eta, IHs, Add_correct; value.
Qed.

Lemma size_surj n : exists t, size t = S n.
Proof.
  induction n.
  - exists 0. reflexivity.
  - destruct IHn as [t H]. exists (lam t). simpl; congruence.
Qed.