mymatch.v

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

Open Scope bool_scope.
Open Scope Z_scope.

Definition myMatch b A (e1: b = true -> A) (e2: b = false -> A): A.                    
  destruct b.
  - apply e1. reflexivity.
  - apply e2. reflexivity.
Defined.


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.

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

Next Obligation.
Admitted.

Lemma match_or:
  forall b A e1 e2,
    (exists p: b = true, myMatch b A e1 e2 = e1 p) \/
    (exists p: b = false, myMatch b A e1 e2 = e2 p).
Admitted.

Next Obligation.
  match goal with
  | H: context[myMatch ?b ?B ?e1 ?e2] |- _ => pose proof match_or b B e1 e2
  end.
  intuition; destruct H0.
  - admit.
  - rewrite H in h; intuition.
Admitted.