The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, May 15, 2012 at 2:28 PM, Andrej Bauer 
<andrej.bauer AT andrej.com>
 wrote:
> I am trying to formalize arguments in Coq which use arbitrarily nested
> identity types, i.e., I want to write things like:
>
>  forall (x0 y0 : A) (x1 y1 : x0 = y0) (x2 y2 : x1 = y1) ... (xn yn :
> x(n-1) = y(n-1), ....
>
> What is the best way to organize things here? Typically, I need access
> to the highest-level term xn yn, and typically I need to show
> something for every level n of nesting.

I whipped up a quick example of how you might define an "n-cell" type
consisting of data (x0 y0:A), (x1 y1:x0=y0), (x2 y2:x1=y1), ...,
(e:x(n-1)=y(n-1)), along with some "accessors" to get the various data
out of the n-cell.

Fixpoint ncell (A:Type) (n:nat) : Type :=
match n with
| 0 => A
| S m => { x:A & { y:A & ncell (x=y) m } }
end.

Inductive Fin : nat -> Set :=
| FinO : forall {n:nat}, Fin (S n)
| FinS : forall {n:nat}, Fin n -> Fin (S n).

Fixpoint ncell_src_dest_type {A:Type} {n:nat}
  (x:ncell A n) (i:Fin n) : Type :=
match i in (Fin m) return (ncell A m -> Type) with
| FinO _ => fun _ => A
| FinS _ i' => fun x => match x with
                        | existT _ (existT _ x') =>
                          ncell_src_dest_type x' i'
                        end
end x.

Fixpoint ncell_src {A:Type} {n:nat} (x:ncell A n) (i:Fin n) :
  ncell_src_dest_type x i :=
match i as i' in (Fin m) return (forall x:ncell A m,
                                 ncell_src_dest_type x i') with
| FinO _ => fun x => match x with
                     | existT src _ => src
                     end
| FinS _ i' => fun x => match x with
                        | existT _ (existT _ x') =>
                          ncell_src x' i'
                        end
end x.

Fixpoint ncell_dest {A:Type} {n:nat} (x:ncell A n) (i:Fin n) :
  ncell_src_dest_type x i :=
match i as i' in (Fin m) return (forall x:ncell A m,
                                 ncell_src_dest_type x i') with
| FinO _ => fun x => match x with
                     | existT _ (existT dest _) => dest
                     end
| FinS _ i' => fun x => match x with
                        | existT _ (existT _ x') =>
                          ncell_dest x' i'
                        end
end x.

Fixpoint Fin_max {n:nat} : Fin (S n) :=
match n with
| 0 => FinO
| S _ => FinS Fin_max
end.

Fixpoint ncell_final_eq {A:Type} {n:nat} (x:ncell A (S n)) :
  ncell_src x Fin_max = ncell_dest x Fin_max :=
match n as n' return
   (forall x:ncell A (S n'),
        ncell_src x Fin_max = ncell_dest x Fin_max) with
| 0 => fun x => match x with
                | existT _ (existT _ e) => e
                end
| S _ => fun x => match x with
                  | existT _ (existT _ e) =>
                      ncell_final_eq e
                  end
end x.
-- 
Daniel Schepler