The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

I'm trying to formalize the notion of a finite type as one that is equivalent 
to (fin n) for some n.
I'm using "t" from Vectors.Fin as "fin" in my code. The rest of this email is 
coq code with comments describing what I tried and where things go wrong.
The gist is I tried a fancy motive to get around an ill-typed term after 
destructing something, and since I apparently don't know quite well enough 
what I'm doing, explosion.

(* Here's where I started: *)
Definition Finite (A : Type) : Prop :=
  exists (n : nat) (f : A -> fin n), Bi_inv f. (* HoTT's Bi_inv with Prop 
equality *)

Remark bool_fin : Finite bool.
Proof.
exists 2, (fun a : bool => if a then F1 else FS F1).
apply Quasi_bi_inv.
exists (fun f : fin 2 => match f with F1 _ => true | FS _ _ => false end).
(* destructing b leads to ill-typed term. *)
Abort.

(*So I try the encode/decode method with two codes for the two fins I need to 
deal with:*)

Definition fin_code1 (b : fin 2) : Prop :=
  match b with
      F1 _=> b = F1
    | FS _ _ => False
  end.
Definition fin_code2 (b : fin 2) : Prop :=
  match b with
      F1 _=> False
    | FS _ _ => b = FS F1
  end.
Definition fin_encode1 (b : fin 2) (p : b = F1) : fin_code1 b.
unfold fin_code1; rewrite p; reflexivity.
Defined.
Definition fin_encode2 (b : fin 2) (p : b = FS F1) : fin_code2 b.
unfold fin_code1; rewrite p; reflexivity.
Defined.

(*All is well, so now I need decode functions.*)

(* How about this? Uncomment for the error. Basically, I can't have two 
different types for H without a fancy motive.

Definition fin_decode1 (b : fin 2) (c : fin_code1 b) : F1 = b :=
  (match b with
      F1 _ => (fun (H : F1 = b) (H0 : fin_code1 F1) =>
                 H)
    | FS _ _ => (fun (H : b = FS F1) (H0 : fin_code1 (FS F1)) =>
                   match H0 with end)
  end (eq_refl b) c)

*)

(* Let's try a fancy motive! I'm pretty sure this should work...

Definition fin_decode1 (b : fin 2) (c : fin_code1 b) : F1 = b :=
  (match b as b' in (fin n) return (match b' with
                                        F1 _ => F1 = b -> fin_code1 F1 -> F1 
= b
                                      | FS _ _ => b = FS F1 -> fin_code1 (FS 
F1) -> F1 = b
                                    end)
   with
      F1 _ => (fun (H : F1 = b) (H0 : fin_code1 F1) =>
                 H)
    | FS _ _ => (fun (H : b = FS F1) (H0 : fin_code1 (FS F1)) =>
                   match H0 with end)
  end (eq_refl b) c).

Nope, the return type is a match, and I thus can't apply it to (eq_refl b). 
What now?
Well, I wasn't sure whether to have b or b' in the return type, but it yelled 
at me when I put b',
since I didn't have the fin type's index figured out. Let's try to do 
something better about that.
*)

Definition fin_decode1 (b : fin 2) (c : fin_code1 b) : F1 = b :=
  (match b as b' in (fin n) return ((match n with
                                        0 => (fun H : n = 0 => False)
                                      | S n' =>
                                        (fun H : n = S n' =>
                                           (match b' with
                                                F1 _ => (@F1 n') = b' -> 
fin_code1 F1 -> F1 = b'
                                              | FS _ _ => b' = FS (@F1 1) -> 
fin_code1 (FS F1) -> F1 = b'
                                            end))
                                          end) (eq_refl n))
   with
      F1 _ => (fun (H : F1 = b) (H0 : fin_code1 F1) =>
                 H)
    | FS _ _ => (fun (H : b = FS F1) (H0 : fin_code1 (FS F1)) =>
                   match H0 with end)
  end (eq_refl b) c).

(* STACK OVERFLOW! Well, I'm out of ideas. Better go to coq-club. Any 
assistance is appreciated.

-Ian
*)