Require Import Arith.

Inductive Fin : nat -> Set :=
  F1 : forall n : nat, Fin (S n)
| FS : forall n : nat, Fin n -> Fin (S n).

Definition cardinality (n : nat) (A : Type) : Prop :=
  exists (f : A -> Fin n) (g : Fin n -> A),
      (forall x, g (f x) = x) /\
      (forall y, f (g y) = y).

Definition bool_to_Fin_2 (x : bool) : Fin 2 :=
  if x then FS _ (F1 _) else F1 _.

Definition Fin_2_to_bool (y : Fin 2) : bool :=
  match y with
    | F1 _ => false
    | FS _ (F1 _) => true
    | _ => false (* bogus! *)
  end.

Theorem bool_cardinality_2 :
  cardinality 2 bool.
Proof.
  unfold cardinality.
  exists bool_to_Fin_2.
  exists Fin_2_to_bool.
  split; intros.
  - destruct x; auto.
  - 
    Require Import Program.
    dependent destruction y.
    + reflexivity.
    + 
      dependent destruction y.
      * reflexivity.
      * inversion y.
Qed.

Print Assumptions bool_cardinality_2. 

Lemma bool_to_Fin_2__Fin_2_to_bool__id :
  forall y,
    bool_to_Fin_2 (Fin_2_to_bool y) = y.
Proof.
  intros.

  refine (match y with
            | F1 _ => _
            | FS _ _ => _
          end).
  

  Undo.

  refine (match y as y' return bool_to_Fin_2 (Fin_2_to_bool y) = y with
            | F1 _ => _
            | FS _ _ => _
          end).
  

  Undo.

  refine (match y as y'
                return y = y' ->
                       bool_to_Fin_2 (Fin_2_to_bool y) = y with
            | F1 _ => _
            | FS _ _ => _
          end _).
end code*)

  refine (match y as y' in Fin n
                return forall pf : n = 2,
                         eq_rect n Fin y' 2 pf = y ->
                         bool_to_Fin_2 (Fin_2_to_bool y) = y with
            | F1 _ => _
            | FS _ _ => _
          end eq_refl _).
  

  - intros.
    inversion pf.
    subst.
    rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec.
    reflexivity.
  - intros.
    inversion pf.
    subst.
    rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec.
    simpl.
Abort.

Lemma fin_case :
  forall n (P : Fin (S n) -> Type),
    (P (F1 _)) ->
    (forall x, P (FS _ x)) ->
    (forall x, P x).

Proof.
  intros.
  refine (match x as x' in Fin n'
                return forall pf : n' = S n,
                         eq_rect n' Fin x' (S n) pf = x ->
                         P x with
            | F1 _ => _
            | FS _ _ => _
          end eq_refl _).
  - intros.
    inversion pf.
    subst.
    rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec.
    auto.
  - intros.
    inversion pf.
    subst.
    rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec.
    auto.
  - rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec.
    reflexivity.
Qed.

Lemma bool_to_Fin_2__Fin_2_to_bool__id :
  forall y,
    bool_to_Fin_2 (Fin_2_to_bool y) = y.
Proof.
  intros.

  apply fin_case.

  Undo.

  pattern y.
  apply fin_case.
  - reflexivity.
  - intros.
    pattern x.
    apply fin_case.
    + reflexivity.
    + intros.
      inversion x0.
Qed.

Ltac fin_dep_destruct v :=
  pattern v; apply fin_case; clear v; intros.

Lemma bool_to_Fin_2__Fin_2_to_bool__id' :
  forall y,
    bool_to_Fin_2 (Fin_2_to_bool y) = y.
Proof.
  intros.
  fin_dep_destruct y.
  - reflexivity.
  - fin_dep_destruct x.
    + reflexivity.
    + inversion x.
Qed.

Print Assumptions bool_to_Fin_2__Fin_2_to_bool__id'.

Set Implicit Arguments.
Inductive type : Type :=  Nat : type | Func : type -> type -> type.

Require Import List.
Import ListNotations.

Inductive member (A : Type) (elm : A) : list A -> Type :=
    HFirst : forall ls : list A, member elm (elm :: ls)
  | HNext : forall (x : A) (ls : list A),
            member elm ls -> member elm (x :: ls).

Inductive term : list type -> type -> Type :=
  Var : forall (G : list type) (t : type), member t G -> term G t
| Const : forall G : list type, nat -> term G Nat
| Plus : forall G : list type, term G Nat -> term G Nat -> term G Nat
| Abs : forall (G : list type) (dom ran : type),
          term (dom :: G) ran -> term G (Func dom ran)
| App : forall (G : list type) (dom ran : type),
          term G (Func dom ran) -> term G dom -> term G ran
| Let : forall (G : list type) (t1 t2 : type),
          term G t1 -> term (t1 :: G) t2 -> term G t2.

Fixpoint cfold G t (e : term G t) : term G t :=
  match e with
    | Plus G e1 e2 =>
      let e1' := cfold e1 in
      let e2' := cfold e2 in
      let maybeOpt := match e1'  with
                        | Const _ n1 =>
                          match e2' with
                            | Const _ n2 => Some (Const _ (n1 + n2))
                            | _ => None
                          end
                        | _ => None
                      end in
      match maybeOpt with
        | None => Plus e1' e2'
        | Some e' => e'
      end

    | Abs _ _ _ e1 => Abs (cfold e1)
    | App _ _ _ e1 e2 => App (cfold e1) (cfold e2)

    | Let _ _ _ e1 e2 => Let (cfold e1) (cfold e2)

    | e => e
  end.

Lemma ty_eq_dec :
  forall x y : type, {x = y} + {x <> y}.
Proof.
  decide equality.
Qed.
Lemma term_case :
  forall G t (P : term G t -> Type),
    (forall p, P (Var p)) ->
    (forall n (pf : t = Nat), P (eq_rect Nat _ (Const G n) t (eq_sym pf))) ->
    (forall e1 e2 (pf : t = Nat), P (eq_rect Nat _ (Plus e1 e2) t (eq_sym pf))) ->
    (forall dom ran (pf : t = Func dom ran) b, P (eq_rect (Func dom ran) _ (Abs b) _ (eq_sym pf))) ->
    (forall dom e1 e2, P (App (dom:=dom) e1 e2)) ->
    (forall ty1 e1 e2, P (Let (t1:=ty1) e1 e2)) ->
    forall e, P e.
Proof.
  intros.
  destruct e eqn:?; auto.
  - specialize (X0 n eq_refl).
    rewrite <- Eqdep_dec.eq_rect_eq_dec in * by exact ty_eq_dec.
    auto.
  - specialize (X1 t0_1 t0_2 eq_refl).
    rewrite <- Eqdep_dec.eq_rect_eq_dec in * by exact ty_eq_dec.
    auto.
  - specialize (X2 dom ran eq_refl t0).
    rewrite <- Eqdep_dec.eq_rect_eq_dec in * by exact ty_eq_dec.
    auto.
Qed.