(see header comment)

nCk_Eq.v

(** Approximating decidable equality for the type nCk.
 
As with GlobSet and DeltaSet, we implement locally the needed homotopy theory (which is trivial);
 `Require Import Homotopy` will do as well, modulo some notation, some names. I'd also bet some
 disappointment that the rhyming staves at the end of `nCk_uniq` are encapsulated in some named
 Lemma in `Homotopy`. Since the path arguments to `trans` in the concluding Lemma are cases of
 `@path nat`, which is a proposition in the sense of Voevodsky, it should be straight-forward (if
 tedious) to produce decidable equality in `nCk` by using those in `(list bool)` and `nat`.
*)

Inductive path { A : Type } : A -> A -> Type :=
  idpath (a : A) : path a a.

Notation " a == b " := (path a b) (at level 70).

Definition pathdec (A : Type) : Type :=
  forall a b : A, sum (a == b) ( a == b -> False ).

Lemma cts { A B : Type } (f : A -> B) { x y : A } (p : x == y) :
  f x == f y.
Proof.
  destruct p.
  apply idpath.
Defined.

Lemma twocat { A : Type } { a b c : A } :
  a == b -> b == c -> a == c.
Proof.
  intros x y.
  destruct x; destruct y; apply idpath.
Defined.

Lemma trans { A : Type } ( P : A -> Type ) { x y : A } (p : P x) :
  x == y -> P y.
Proof.
  intro.
  destruct X. auto.
Defined.

Inductive nCk : nat -> nat -> Type :=
  | zz : nCk 0 0
  | incl { n k } : nCk n k -> nCk (S n) (S k)
  | excl { n k } : nCk n k -> nCk (S n) k.

Fixpoint size (l : list bool) : nat :=
  match l with
  | nil => 0
  | cons true ll => S (size ll)
  | cons false ll => size ll end.

Fixpoint length {A : Type} (l : list A) : nat :=
  match l with
  | nil => 0
  | cons _ ll => S (length ll) end.

Fixpoint codeClist {n m : nat} ( ct : nCk n m ) :
  { ll : list bool & n == length ll & m == size ll }.
Proof.
  destruct ct.
  exists nil; apply idpath.
  destruct (codeClist _ _ ct) as [ l' e1 e2 ].
  exists (cons true l');
  simpl; apply cts; auto.
  destruct (codeClist _ _ ct) as [ l' e1 e2 ].
  exists (cons false l'); simpl; try apply cts; auto.
Defined.

Fixpoint decodeClist (ll : list bool) : nCk (length ll) (size ll).
Proof.
  destruct ll.
  apply zz.
  destruct b; simpl.
  apply incl. apply decodeClist.
  apply excl. apply decodeClist.
Defined.

Definition my_equiv_type { n m : nat } (ct : nCk n m) : Type.
Proof.
  destruct (codeClist ct) as [ ll eq1 eq2 ].
  set  (ct' := trans (fun y => nCk (length ll) y) (trans (fun x => nCk x m) ct eq1) eq2).
  simpl in ct'.
  exact ( ct' == decodeClist ll ).
Defined.

Lemma nCk_uniq { n m : nat } ( ct : nCk n m ):
  my_equiv_type ct.
Proof.
  unfold my_equiv_type.
  induction ct; simpl.
  apply idpath.

  set (v := codeClist ct) in *.
  destruct v.
  simpl.
  refine ( twocat _ (cts incl IHct)).
  clear.
    revert p p0.
    generalize (length x); generalize (size x).
    clear. intros.
    destruct p.
    destruct p0.
    apply idpath.

  set ( v := codeClist ct ) in *.
  destruct v.
  refine ( twocat _ (cts excl IHct)).
  clear.
    revert p p0.
    simpl.
    generalize (length x); generalize (size x).
    clear. intros.
    destruct p.
    destruct p0.
    apply idpath.

Defined.

Of course, this raises the pointed question: why not use { ll : list bool & length ll == n & size ll = k } instead of nCk n k ?