Require Import Arith. From mathcomp Require Import ssreflect. Section Vec. Variable A : Type. Inductive vec : nat -> Type := | Vnil : vec 0 | Vcons : forall (a : A) {n} (v : vec n), vec (S n). Inductive index : nat -> Type := | I0 : forall n, index (S n) | IS : forall n, index n -> index (S n). Definition index_is_succ {n} : index n -> {m | n = S m}. by case => m; exists m. Defined. Lemma test n m : index n -> n = S m -> index (S m). move => i H. by rewrite -H. Qed. Print test. Lemma index0_empty : index 0 -> False. Proof. move=> i; inversion i. Qed. Lemma index_S_pred {n} : index n -> S (pred n) = n. by case => m. Defined. Fixpoint remove {n} (lst : vec n) (j : index n) : vec (pred n) := match lst in (vec n) return index n -> vec (pred n) with | Vcons a m l => (fun j1 => match j1 in (index (S m)) return vec m -> vec m with | I0 n1 => (fun l => l) | IS n1 j2 => (fun l => eq_rect _ vec (Vcons a (remove l j2)) n1 (index_S_pred j2)) end l) | Vnil => (fun j1 => False_rect _ (index0_empty j1)) end j. Fixpoint get_nth {n} (sz : vec n) (i : index n) : A := match sz in (vec n) return index n -> A with | Vcons a m l => (fun i1 => match i1 in (index (S m)) return vec m -> A with | I0 n1 => (fun l => a) | IS n1 j2 => (fun l => get_nth l j2) end l) | Vnil => (fun i1 => False_rect _ (index0_empty i1)) end i. Fixpoint get_nth' {n} (sz : vec n) : index n -> A := match sz with | Vcons a m l => (fun i1 => match i1 in (index (S m)) return (index m -> A) -> A with | I0 n1 => (fun _ => a) | IS n1 j2 => (fun f => f j2) end (get_nth' l)) | Vnil => (fun i1 => False_rect _ (index0_empty i1)) end. End Vec. Section Table. Variable A : Type. Inductive table : forall {n}, vec nat n -> Type := | Tnil : table (Vnil nat) | Tcons : forall {m n} (h : vec A m) (sz : vec nat n), table sz -> table (Vcons nat m sz). Fixpoint decr_nth {n} (sz : vec nat n) (i : index n) : vec nat n := match sz in (vec _ n) return index n -> vec nat n with | Vcons a m l => (fun i1 => match i1 in (index (S m)) return vec nat m -> vec nat (S m) with | I0 n1 => Vcons _ (pred a) | IS n1 j2 => (fun l => Vcons _ a (decr_nth l j2)) end l) | Vnil => (fun j => False_rect _ (index0_empty j)) end i. Fixpoint remove_table {n} {sz : vec nat n} (tbl : table sz) (i : index n) (j : index (get_nth _ sz i)) : table (decr_nth sz i) := match tbl as tbl1 in (@table n1 sz1) return forall i : index n1, index (get_nth _ sz1 i) -> table (decr_nth sz1 i) with | Tnil => (fun i1 _ => False_rect _ (index0_empty i1)) | Tcons m n2 h szt t => (fun i1 j1 => match i1 as i2 in (index (S n2)) return forall szt : vec nat n2, index (get_nth nat (Vcons nat m szt) i2) -> vec A m -> table szt -> table (decr_nth (Vcons nat m szt) i2) with | I0 n3 => (fun szt j h t => Tcons (remove A h j) szt t) | IS n3 i4 => (fun szt j h t => Tcons h _ (remove_table t i4 j)) end szt j1 h t) end i j. End Table. Require Import String. Open Scope string_scope. Definition mkc x {n} (v : vec string n) := Vcons _ x v. Definition mk1 x := mkc x (Vnil _). Definition mk2 x y := mkc x (mk1 y). Definition mk3 x y z := mkc x (mk2 y z). Definition mk4 x y z t := mkc x (mk3 y z t). Definition tbl := Tcons _ (mk3 "X" "Y" "Z") _ (Tcons _ (mk2 "U" "V") _ (Tcons _ (mk4 "A" "B" "C" "D") _ (Tnil _))). Eval compute in remove_table _ tbl (I0 _) (I0 _). Eval compute in remove_table _ tbl (I0 _) (IS _ (I0 _)). Eval compute in remove_table _ tbl (I0 _) (IS _ (IS _ (I0 _))). Eval compute in remove_table _ tbl (IS _ (I0 _)) (I0 _). Eval compute in remove_table _ tbl (IS _ (IS _ (I0 _))) (IS _ (I0 _)).