(* G54DTP Dependently Typed Programming.
   The minimization function.
    Venanzio Capretta, March 2011.
*)


(* Minimization function:

    min : (nat -> nat) -> nat
    min f = if (f 0 = 0) 
            then 0 
            else min (\n -> f (S n)) + 1

  This function cannot be programmed directly.
*)


(* Inductive definition of the domain. *)

Inductive Dom_min: (nat->nat) -> Set :=
  dminO: forall f:nat->nat, (f O)=O -> Dom_min f
| dminS: forall f:nat->nat, (f O)<>O -> Dom_min (fun x => f (S x))
                     -> Dom_min f.

(* The formalization of min has an extra argument: a proof of Dom_min
   and it is defined by recursion on it.
*)

Fixpoint min (f:nat->nat)(h:Dom_min f): nat :=
match h with
  dminO f p => O
| dminS f q h' => S (min (fun x => f (S x)) h')
end.

(* A family of functions that we are going to use as examples. *)

Definition down (k:nat): nat -> nat:=
  fun x => k-x.

Eval compute in (down 5 4).
Eval compute in (down 10 2).
Eval compute in (down 3 5).

Definition ddown5: Dom_min (down 5).
repeat (apply dminS; [simpl; discriminate | simpl]).
apply dminO.
trivial.
Defined.

Eval compute in (min (down 5) ddown5).

(* A general proof that works for all parameters. *)

Definition ddown: forall n, Dom_min (down n).
intro n; elim n.
apply dminO; trivial.
intros n' H; apply dminS.
simpl.
auto.
simpl.
exact H.
Defined.

Eval compute in (min (down 10) (ddown 10)).

(* Another example. *)

Definition myfun: nat -> nat := fun x => 2*x + 7 - x*x*x.

Eval compute in (myfun 0).
Eval compute in (myfun 2).
Eval compute in (myfun 3).

(* The proof is exactly the same as for (down 5). *)

Definition dmyfun: Dom_min myfun.
repeat (apply dminS; [simpl; discriminate | simpl]).
apply dminO.
trivial.
Defined.

Eval compute in (min myfun dmyfun).

(* The minimization function for streams instead of functions:
   find the first position where a stream of naturals is zero.
*)

Require Import Streams.

Check hd.
Check tl.

Inductive Dom_smin: Stream nat -> Set :=
  dmin_head: forall (s:Stream nat), hd s = 0 -> Dom_smin s
| dmin_tail: forall (s:Stream nat), hd s <> 0 -> Dom_smin (tl s) ->
                  Dom_smin s.

Fixpoint smin (s:Stream nat)(h:Dom_smin s): nat :=
match h with
  dmin_head s p => O
| dmin_tail s q h' => S (smin (tl s) h')
end.

Set Implicit Arguments.

(* Constant streams *)

CoFixpoint consts (A:Set)(a:A): Stream A := Cons a (consts a).

(* Decreasing streams starting from a given parameter. *)

Fixpoint decs (n:nat): Stream nat :=
match n with
  O => consts O
| S n' => Cons n (decs n')
end.

Eval simpl in (decs 10).

(* Recall the operator that unfolds a stream many times. *)

Fixpoint sunf (A:Set)(s:Stream A)(n:nat): Stream A :=
match n with
  O => s
| S n' => match s with
            Cons a s' => Cons a (sunf s' n')
          end
end.

Eval simpl in (sunf (decs 10) 20).

Lemma dmin_decs10: Dom_smin (decs 10).
repeat (apply dmin_tail; [discriminate | simpl]).
apply dmin_head.
simpl.
trivial.
Defined.

Eval simpl in (smin (decs 10) dmin_decs10).