hungry functionにいくら自然数を食わせてもhungryなままであることを証明

gistfile1.v

Section HungryIsImmutable.

CoInductive hungry := h : (nat -> hungry) -> hungry.

CoFixpoint f := h (fun _ => f).

Definition unH x :=
  match x with
  | h f => f 
  end.

Infix "$" := unH (at level 120).

Fixpoint mkHungry n :=
  match n with
  | O => f $ O
  | S m => mkHungry m $ S m
  end.

Theorem hungryIsImmutable : forall n, mkHungry n = f.
Proof.
induction n; [ | simpl; rewrite IHn ]; reflexivity.
Qed.

End HungryIsImmutable.