Test.v

Require Import Arith Bool Eqdep.


Section NotAsEasy.
    
  Inductive type : Set :=
    | Nat : type
    | Bool : type.

  Inductive exp : type -> Set :=
    | NConst : nat -> exp Nat
    | Inc   : exp Nat -> exp Nat.

  Fixpoint typeDenote (t: type) : Set :=
    match t with
      | Nat  => nat
      | Bool => bool
    end%type.


  Fixpoint expDenote t (e: exp t): typeDenote t :=
    match e in (exp t) return (typeDenote t) with
      | NConst n       => n
      | Inc e          => S (expDenote _ e)
    end.

  Fixpoint expOpt t (e: exp t) : exp t :=
    match e in (exp t) return (exp t) with
      | NConst n => NConst n
      | Inc e =>
          let e' := expOpt _ e in
            match e' return exp Nat with
              | NConst n => NConst (S n)
              | _ => Inc e'
            end
      end.

Theorem dep_destruct:
  forall (T: Type)
         (T': T -> Type)
         (x: T)
         (v: T' x)
         (P: T' x -> Prop),
    (forall (x': T)
           (v': T' x')
           (H: x' = x),
      P match H in (_ = x0) return (T' x0) with
          | eq_refl => v'
        end) -> P v.
Proof.
  intros.
  exact (match (H x v eq_refl) with
  | x => x
  end). Qed.


  Lemma lem:
    forall (expr: exp Nat),
      expDenote _ expr = expDenote _ (expOpt _ expr).
  Proof.
    destruct expr; auto.