Forall_dec.v

Require Import
        List
        Arith_base.

Inductive Exp : Set :=
| EConst : nat -> Exp
| EVar   : nat -> Exp
| EFun   : nat -> list Exp -> Exp.

Definition Env := list nat.

Inductive WF (env : Env) : Exp -> Prop :=
| WFConst : forall n, WF env (EConst n)
| WFVar   : forall n, In n env -> WF env (EVar n)
| WFFun   : forall n es, In n env ->
                         Forall (WF env) es ->
                         WF env (EFun n es).
Hint Constructors WF.

Definition Forall_dec :=
fun (A : Type) (P : A -> Prop) (Pdec : forall x : A, {P x} + {~ P x}) (l : list A) =>
list_rec (fun l0 : list A => {Forall P l0} + {~ Forall P l0}) (left (Forall_nil P))
  (fun (a : A) (l' : list A) (Hrec : {Forall P l'} + {~ Forall P l'}) =>
   match Hrec with
   | left Hl' =>
       let s := Pdec a in
       match s with
       | left Ha => left (Forall_cons a Ha Hl')
       | right Ha =>
           right
             (fun H : Forall P (a :: l') =>
              let H0 :=
                match H in (Forall _ l0) return (l0 = a :: l' -> False) with
                | Forall_nil _ =>
                    fun H0 : nil = a :: l' =>
                    (fun H1 : nil = a :: l' =>
                     let H2 :=
                       eq_ind nil (fun e : list A => match e with
                                                     | nil => True
                                                     | _ :: _ => False
                                                     end) I (a :: l') H1
                       :
                       False in
                     False_ind False H2) H0
                | @Forall_cons _ _ x l0 H0 H1 =>
                    fun H2 : x :: l0 = a :: l' =>
                    (fun H3 : x :: l0 = a :: l' =>
                     let H4 := f_equal (fun e : list A => match e with
                                                          | nil => l0
                                                          | _ :: l1 => l1
                                                          end) H3 : l0 = l' in
                     (let H5 := f_equal (fun e : list A => match e with
                                                           | nil => x
                                                           | a0 :: _ => a0
                                                           end) H3 : x = a in
                      (fun H6 : x = a =>
                       let H7 := H6 : x = a in
                       eq_ind_r (fun a0 : A => l0 = l' -> P a0 -> Forall P l0 -> False)
                         (fun H8 : l0 = l' =>
                          let H9 := H8 : l0 = l' in
                          eq_ind_r (fun l1 : list A => P a -> Forall P l1 -> False)
                            (fun (H10 : P a) (_ : Forall P l') => False_ind False (Ha H10)) H9) H7) H5) H4) H2 H0 H1
                end
                :
                a :: l' = a :: l' -> False in
              H0 eq_refl)
       end
   | right Hl' =>
       right
         (fun H : Forall P (a :: l') =>
          let H0 :=
            match H in (Forall _ l0) return (l0 = a :: l' -> False) with
            | Forall_nil _ =>
                fun H0 : nil = a :: l' =>
                (fun H1 : nil = a :: l' =>
                 let H2 :=
                   eq_ind nil (fun e : list A => match e with
                                                 | nil => True
                                                 | _ :: _ => False
                                                 end) I (a :: l') H1
                   :
                   False in
                 False_ind False H2) H0
            | @Forall_cons _ _ x l0 H0 H1 =>
                fun H2 : x :: l0 = a :: l' =>
                (fun H3 : x :: l0 = a :: l' =>
                 let H4 := f_equal (fun e : list A => match e with
                                                      | nil => l0
                                                      | _ :: l1 => l1
                                                      end) H3 : l0 = l' in
                 (let H5 := f_equal (fun e : list A => match e with
                                                       | nil => x
                                                       | a0 :: _ => a0
                                                       end) H3 : x = a in
                  (fun H6 : x = a =>
                   let H7 := H6 : x = a in
                   eq_ind_r (fun a0 : A => l0 = l' -> P a0 -> Forall P l0 -> False)
                     (fun H8 : l0 = l' =>
                      let H9 := H8 : l0 = l' in
                      eq_ind_r (fun l1 : list A => P a -> Forall P l1 -> False)
                        (fun (_ : P a) (H11 : Forall P l') => False_ind False (Hl' H11)) H9) H7) H5) H4) H2 H0 H1
            end
            :
            a :: l' = a :: l' -> False in
          H0 eq_refl)
   end) l.

Definition WFDec (env : Env) : forall e, {WF env e} + {~ WF env e}.
  refine (fix wfdec e : {WF env e} + {~ WF env e} :=
            match e as e' return e = e' -> {WF env e'} + {~ WF env e'} with
            | EConst n => fun _ => left _ _
            | EVar n => fun _ =>
                          match in_dec eq_nat_dec n env with
                          | left _ _ => left _ _
                          | right _ _ => right _ _
                          end
            | EFun n es => fun _ =>
                          match in_dec eq_nat_dec n env with
                          | left _ _ =>
                            match Forall_dec _ (WF env) wfdec es with
                            | left _ _ => _
                            | right _ _ => _
                            end
                          | right _ _ => right _ _
                          end
            end (eq_refl e)); clear wfdec ; subst ; eauto.
- intros H. inversion H. tauto.
- right. intros H. inversion H. tauto.
- intros H. inversion H. tauto.
Qed.