Lazy Nat

This s a lazified version of the natural number that allow one to delay computation until demanded. This is useful for large natural numbers (often upper bounds) where only a small number of terms are actually need for compuation.

Inductive LazyNat : Set :=
| LazyO : LazyNat
| LazyS : (unit -> LazyNat) -> LazyNat.

Successor

Definition lazyS (n:LazyNat) : LazyNat := LazyS (fun _ => n).

Convert a nat to a lazy nat

Fixpoint LazifyNat (n : N) {struct n} : LazyNat :=
  match n with
  | O => LazyO
  | S p => LazyS (fun _ => (LazifyNat p))
  end.

Predecessor

Definition LazyPred (n:LazyNat) : LazyNat :=
match n with
| LazyO => LazyO
| LazyS n' => (n' tt)
end.

Lemma LazifyPred : forall n, LazifyNat (pred n) = LazyPred (LazifyNat n).

Addition

Fixpoint LazyPlus (n m : LazyNat) {struct n} : LazyNat :=
  match n with
  | LazyO => m
  | LazyS p => LazyS (fun _ => LazyPlus (p tt) m)
  end.

Lemma LazifyPlus : forall n m, (LazifyNat (n + m) = LazyPlus (LazifyNat n) (LazifyNat m))%nat.

Multiplication

Fixpoint Pmult_LazyNat (x:positive) (pow2:LazyNat) {struct x} : LazyNat :=
  match x with
    | xI x' => (LazyPlus pow2 (Pmult_LazyNat x' (LazyPlus pow2 pow2)))%nat
    | xO x' => Pmult_LazyNat x' (LazyPlus pow2 pow2)%nat
    | xH => pow2
  end.

Lemma LazifyPmult_LazyNat : forall x pow2, LazifyNat (Pmult_nat x pow2) = Pmult_LazyNat x (LazifyNat pow2).

Convert a positive to a lazy nat. This is the most common way of generating lazy nats.

Definition LazyNat_of_P (x:positive) := Pmult_LazyNat x (LazyS (fun _ => LazyO)).

Lemma LazifyNat_of_P : forall x, LazifyNat (nat_of_P x) = LazyNat_of_P x.

Fixpoint Pplus_LazyNat (p:positive)(n:LazyNat) {struct n} : positive :=
match n with
| LazyO => p
| (LazyS n') => (Pplus_LazyNat (Psucc p) (n' tt))
end.