elimbool.v

Require Import Coq.Program.Tactics.
Require Import Coq.Program.Program.
Require Import Omega.

Open Scope bool_scope.
Open Scope Z_scope.

Program Definition g (i: Z) (h: (Z.gtb i 0 = true)) : {holds: bool | (holds = true)} :=
  Z.geb i (-1).

Admit Obligations.

Program Definition f (i: Z) (h: (Z.geb i 0 = true)) : bool :=
  Z.gtb i 0.

Admit Obligations.

Lemma elimBool:
  forall (b: bool) (A: bool -> Type) (b1: b = true -> A true) (b2: b = false -> A false),
    A b.
  intros.
  destruct b; intuition.
Qed.

Program Definition h
        (i: Z)
        (h: elimBool
              (Z.gtb i 0)
              (fun _ => bool)
              (fun _ => f (Z.sub i 1) _)
              (fun _ => false) = true):  {res: Z | g (Z.add i 1) _ = true } := Z.add i 1.

Next Obligation.
Admitted.

Next Obligation.
  destruct (i >? 0).