tables.v

Require Import List.
Import ListNotations.
Require Import Coq.Program.Basics. 

Set Implicit Arguments.

(******************)
(* standard hlist *)
(******************)

Inductive hlist (A : Type) (B : A -> Type) : list A -> Type :=
| hnil : hlist B []
| hcons : forall a (b : B a) l (h : hlist B l), hlist B (a :: l).

Inductive member (A : Type) (x : A) : list A -> Type :=
| here : forall l, member x (x :: l)
| there : forall y l, member x l -> member x (y :: l).

Fixpoint hget A (B : A -> Type) (x : A) (l : list A) (m : member x l) : hlist B l -> B x :=
  match m with
  | here _ _ =>
    fun h => match h with
          | hnil _ => I
          | hcons _ b _ => b
          end
  | there y m =>
    fun h => match h with
          | hnil _ => I
          | hcons _ _ h => fun rec => rec h
          end (hget m)
  end.


(**********)
(* tables *)
(* the ' variants of the definitions are generalized for cell types that depend on the labels *)
(**********)

Definition table (A R C : Type) (r : list R) (c : list C) : Type :=
  hlist (fun _ => hlist (fun _ => A) c) r.

Definition table' (R C : Type) (r : list R) (c : list C)(celltype: R -> C -> Type) : Type :=
  hlist (fun r => hlist (fun c => celltype r c) c) r.

Definition lookup A R C (r : list R) (c : list C) (t : table A r c) x y
           (mx : member x r) (my : member y c) : A :=
  hget my (hget mx t).


Definition lookup' R C (r : list R) (c : list C) ct (t : table' r c ct) x y
           (mx : member x r) (my : member y c) : ct x y :=
  hget my (hget mx t).

(* auxiliary function to map over homogenous heterogenous lists :-) *)
Definition maph : forall A B lt (labels : list lt), hlist (fun _ => A) labels -> (A -> B) -> hlist (fun _ => B) labels.
intros. induction labels.
- exact (hnil _).
- inversion X ; subst. exact (hcons a (X0 b)(IHlabels h)).
Defined.

Definition maph' : forall lt (labels : list lt) ct ct' (t: forall A, ct A -> ct' A), hlist ct labels ->  hlist ct' labels.
intros. induction labels.
- exact (hnil _).
- inversion X ; subst. exact (hcons a (t _ b)(IHlabels h)).
Defined.

Definition destructColumns : forall {a cl rl c} (rows : list rl) (columns : (list cl)),
  table a (c :: columns) rows -> hlist (fun _ => a) rows * table a columns rows.
intros. inversion X; subst. exact (b,h). Defined.


Definition destructColumns' : forall {cl rl c} (rows : list rl) (columns : (list cl)) ct,
  table' (c :: columns) rows ct -> hlist (ct c) rows * table' columns rows ct.
intros. inversion X; subst. exact (b,h). Defined.

Definition destructhcons : forall {A B a} {l : list A}, hlist B (a :: l) ->  B a * hlist B l.
intros. inversion X; subst. exact (b,h). Defined.


Definition destructRows : forall {a cl rl r} (rows : list rl) (columns : (list cl)),
  table a columns (r :: rows) -> hlist (fun _ => a) columns * table a columns rows.
intros. 
exact( maph X ( compose fst destructhcons), maph X ( compose snd destructhcons)).
Defined.

Definition destructRows' : forall {cl rl r} (rows : list rl) (columns : (list cl)) ct,
  table' columns (r :: rows) ct -> hlist (fun c => ct c r) columns * table' columns rows ct.
intros. unfold table' in *.
pose proof (@maph' cl 
             columns 
             (fun r0 : cl => @hlist rl (fun c : rl => ct r0 c) (r :: rows)) 
             (fun r0 : cl => (ct r0 r) ) 
             (fun A : cl => compose fst (@destructhcons rl (fun c : rl => ct A c) r rows)) 
              X) as P.
pose proof (@maph' cl 
             columns 
             (fun r0 : cl => @hlist rl (fun c : rl => ct r0 c) (r :: rows)) 
             (fun r0 : cl => (@hlist rl (fun c : rl => ct r0 c) rows)) 
             (fun A : cl => compose snd (@destructhcons rl (fun c : rl => ct A c) r rows)) 
              X) as P'.
exact(P,P').
Defined.

Definition consRows : forall {a cl rl r} (rows : list rl) (columns : (list cl)),
  hlist (fun _ => a) columns -> table a columns rows -> table a columns (r :: rows).
intros. induction columns.  
- exact (hnil _).
- destruct (destructhcons X). destruct (destructColumns X0).
  pose proof (IHcolumns h t) as almostthere.
  pose proof (hcons r a1 h0) as q.
  exact (hcons _ q almostthere).
Defined.

Definition consRows' : forall {cl rl r} (rows : list rl) (columns : (list cl)) ct,
  hlist (fun c => ct c r) columns -> table' columns rows ct -> table' columns (r :: rows) ct.
intros. induction columns.  
- exact (hnil _).
- destruct (destructhcons X). destruct (destructColumns' X0).
  pose proof (IHcolumns h t) as almostthere.
  pose proof (hcons r c h0) as q.
  exact (hcons _ q almostthere).
Defined.

Definition transpose : forall {a cl rl} (rows : list rl) (columns : (list cl)),
   table a columns rows -> table a rows columns.
induction rows.
- intros. exact (hnil _).
- induction columns.
  * intros. exact( hcons a0 (hnil _) (IHrows _ (hnil _))).
  * intros. inversion X ; subst. fold (table a columns (a0 :: rows)) in *.
    pose proof (IHcolumns h) as firststep.
    pose proof (fst (destructColumns X)) as secondstep.
    exact(consRows  secondstep firststep).
Defined.

Definition transpose' : forall {cl rl} (rows : list rl) (columns : (list cl)) ct,
   table' columns rows ct -> table' rows columns (flip ct).
induction rows.
- intros. exact (hnil _).
- induction columns.
  * intros. exact( hcons _ (hnil _) (IHrows _ ct (hnil _))).
  * intros. inversion X ; subst. fold (table' columns (a :: rows) ct) in *.
    pose proof (IHcolumns ct h) as firststep.
    pose proof (fst (destructColumns' X)) as secondstep.
    exact(consRows'  secondstep firststep).
Defined.


Lemma transpose_correct:
  forall {a cl rl} (rows : list rl) (columns : (list cl)) (t: table a columns rows) x y (mx : member x columns) (my: member y rows), 
   lookup t mx my = lookup (transpose t) my mx.
(* TODO! *)
Admitted.

Lemma transpose_correct':
  forall {cl rl} (rows : list rl) (columns : (list cl)) ct (t: table' columns rows ct ) x y (mx : member x columns) (my: member y rows), 
   lookup' t mx my = lookup' (transpose' t) my mx.
(* TODO! *)
Admitted.