Require Import VST.floyd.base2.
Require Import VST.floyd.type_induction.
Require Export VST.floyd.compact_prod_sum.
Require Import VST.floyd.fieldlist.
Require Import VST.floyd.sublist.

Definition
map_map: forall {A B C : Type} (f : A -> B) (g : B -> C) (l : list A),
       map g (map f l) = map (fun x : A => g (f x)) l :=
fun (A B C : Type) (f : A -> B) (g : B -> C) (l : list A) =>
list_ind
  (fun l0 : list A => map g (map f l0) = map (fun x : A => g (f x)) l0)
  eq_refl
  (fun (a : A) (l0 : list A)
     (IHl : map g (map f l0) = map (fun x : A => g (f x)) l0) =>
   eq_ind_r
     (fun l1 : list C =>
      g (f a) :: l1 = g (f a) :: map (fun x : A => g (f x)) l0) eq_refl IHl)
  l.

(******************************************

Definition of reptype.

******************************************)

Notation sigTT P := (fun tv => match tv with existT t v => P t end).

Definition compact_prod_sigT_type {A} {P: A -> Type} (l: list (sigT P)): Type :=
  compact_prod (map (sigTT P) l).

Definition compact_prod_sigT_value: forall {A} {P: A -> Type} (l: list (sigT P)), compact_prod (map (sigTT P) l).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: compact_sum (@map (@sigT A P) Type (fun tv : @sigT A P => let (t, _) := tv in P t) l) *)
  destruct l as [| [t0 v0] l]; [exact tt |].
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  revert t0 v0; induction l as [| [t v] l]; intros.
  + exact v0.
  + exact (v0, IHl t v).
Defined.

Definition compact_sum_sigT_type {A} {P: A -> Type} (l: list (sigT P)): Type :=
  compact_sum (map (sigTT P) l).

Definition compact_sum_sigT_value: forall {A} {P: A -> Type} (l: list (sigT P)), compact_sum (map (sigTT P) l).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: compact_sum (@map (@sigT A P) Type (fun tv : @sigT A P => let (t, _) := tv in P t) l) *)
  destruct l as [| [t0 v0] l]; [exact tt |].
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  revert t0 v0; destruct l as [| [t v] l]; intros.
  + exact v0.
  + exact (inl v0).
Defined.

Definition compact_prod_map {X: Type} {F F0: X -> Type} (l: list X)
  (f: ListType (map (fun x => F x -> F0 x) l)): compact_prod (map F l) -> compact_prod (map F0 l).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: compact_sum (@map X Type F0 l) *)
  destruct l; [exact tt |].
(* Goal: compact_sum (@map X Type F0 (@cons X x l)) *)
  revert x f X0; induction l; intros; simpl in *.
  + inversion f; subst.
(* Goal: F0 x *)
    exact (a X0).
  + remember ((F a -> F0 a) :: map (fun x0 : X => F x0 -> F0 x0) l) as L;
(* Goal: F0 x *)
    inversion f; subst.
(* Goal: prod (F0 x) match @map X Type F0 l with | nil => F0 a | cons T l0 => prod (F0 a) (compact_prod (@map X Type F0 l)) end *)
    exact (a0 (fst X0), IHl a b (snd X0)).
Defined.

Lemma compact_prod_map_nil: forall {X: Type} {F F0: X -> Type},
  @compact_prod_map X F F0 nil Nil tt = tt.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
  reflexivity.
Qed.

Lemma compact_prod_map_single: forall {X: Type} {F F0: X -> Type} (x: X)
  (f: F x -> F0 x) (v: F x),
  compact_prod_map (x :: nil) (Cons f Nil) v = f v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
  reflexivity.
Qed.

Lemma compact_prod_map_cons: forall {X: Type} {F F0: X -> Type} (x x0: X) (l: list X)
  (f: F x -> F0 x) (fl: ListType (map (fun x => F x -> F0 x) (x0 :: l)))
  (v: F x) (vl: compact_prod (map F (x0 :: l))),
  compact_prod_map (x :: x0 :: l) (Cons f fl) (v, vl) = (f v, compact_prod_map _ fl vl).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
  reflexivity.
Qed.

Definition compact_sum_map {X: Type} {F F0: X -> Type} (l: list X)
  (f: ListType (map (fun x => F x -> F0 x) l)): compact_sum (map F l) -> compact_sum (map F0 l).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: compact_sum (@map X Type F0 l) *)
  destruct l; [exact tt |].
(* Goal: compact_sum (@map X Type F0 (@cons X x l)) *)
  revert x f X0; induction l; intros; simpl in *.
  + inversion f; subst.
(* Goal: F0 x *)
    exact (a X0).
  + remember ((F a -> F0 a) :: map (fun x0 : X => F x0 -> F0 x0) l) as L;
(* Goal: F0 x *)
    inversion f; subst.
    exact match X0 with
          | inl X0_l => inl (a0 X0_l)
          | inr X0_r => inr (IHl a b X0_r)
          end.
Defined.

Lemma compact_sum_map_nil: forall {X: Type} {F F0: X -> Type},
  @compact_sum_map X F F0 nil Nil tt = tt.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
  reflexivity.
Qed.

Lemma compact_sum_map_single: forall {X: Type} {F F0: X -> Type} (x: X)
  (f: F x -> F0 x) (v: F x),
  compact_sum_map (x :: nil) (Cons f Nil) v = f v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
  reflexivity.
Qed.

Lemma compact_sum_map_cons_inl: forall {X: Type} {F F0: X -> Type} (x x0: X) (l: list X)
  (f: F x -> F0 x) (fl: ListType (map (fun x => F x -> F0 x) (x0 :: l)))
  (v: F x),
  compact_sum_map (x :: x0 :: l) (Cons f fl) (inl v) = inl (f v).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
  reflexivity.
Qed.

Lemma compact_sum_map_cons_inr: forall {X: Type} {F F0: X -> Type} (x x0: X) (l: list X)
  (f: F x -> F0 x) (fl: ListType (map (fun x => F x -> F0 x) (x0 :: l)))
  (vl: compact_sum (map F (x0 :: l))),
  compact_sum_map (x :: x0 :: l) (Cons f fl) (inr vl) = inr (compact_sum_map _ fl vl).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
  reflexivity.
Qed.



Definition reptype_gen {cs: compspecs} : type -> (sigT (fun x => x)) :=
  type_func (fun _ => (sigT (fun x => x)))
  (fun t =>
     if (type_is_by_value t)
     then existT (fun x => x) val Vundef
     else existT (fun x => x) unit tt)
  (fun t n a TV => existT (fun x => x) (list (projT1 TV)) (list_repeat (Z.to_nat n) (projT2 TV)))
  (fun id a TVs => existT (fun x => x) (compact_prod_sigT_type (decay TVs)) (compact_prod_sigT_value (decay TVs)))
  (fun id a TVs => existT (fun x => x) (compact_sum_sigT_type (decay TVs)) (compact_sum_sigT_value (decay TVs))).

Definition reptype {cs: compspecs} t: Type := match reptype_gen t with existT t _ => t end.

Definition default_val {cs: compspecs} t: reptype t :=
  match reptype_gen t as tv
    return match tv with existT t _ => t end
  with existT t v => v end.

Instance Inhabitant_reptype {cs: compspecs} (t: type) : Inhabitant (reptype t) := default_val t.

Section CENV.
Context {cs: compspecs}.

Lemma reptype_gen_eq: forall t,
  reptype_gen t =
  match t with
  | Tarray t0 n _ => existT (fun x => x) (list (projT1 (reptype_gen t0))) (list_repeat (Z.to_nat n) (projT2 (reptype_gen t0)))
  | Tstruct id _ => existT (fun x => x)
                     (compact_prod_sigT_type (map reptype_gen (map (fun it => field_type (fst it) (co_members (get_co id))) (co_members (get_co id)))))
                     (compact_prod_sigT_value (map reptype_gen (map (fun it => field_type (fst it) (co_members (get_co id))) (co_members (get_co id)))))
  | Tunion id _ => existT (fun x => x)
                     (compact_sum_sigT_type (map reptype_gen (map (fun it => field_type (fst it) (co_members (get_co id))) (co_members (get_co id)))))
                     (compact_sum_sigT_value (map reptype_gen (map (fun it => field_type (fst it) (co_members (get_co id))) (co_members (get_co id)))))
  | _ => if (type_is_by_value t)
         then existT (fun x => x) val Vundef
         else existT (fun x => x) unit tt
  end.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (@sigT Type (fun x : Type => x)) (@reptype_gen cs t) match t with | Tvoid => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt | Tint i s a => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt | Tlong s a => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt | Tfloat f a => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt | Tpointer t0 a => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt | Tarray t0 n a => @existT Type (fun x : Type => x) (list (@projT1 Type (fun x : Type => x) (@reptype_gen cs t0))) (@list_repeat (@projT1 Type (fun x : Type => x) (@reptype_gen cs t0)) (Z.to_nat n) (@projT2 Type (fun x : Type => x) (@reptype_gen cs t0))) | Tfunction t0 t1 c => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt | Tstruct id a => @existT Type (fun x : Type => x) (@compact_prod_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs id))) (co_members (@get_co cs id))))) (@compact_prod_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs id))) (co_members (@get_co cs id))))) | Tunion id a => @existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs id))) (co_members (@get_co cs id))))) (@compact_sum_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs id))) (co_members (@get_co cs id))))) end *)
  unfold reptype_gen at 1.
(* Goal: @eq (@reptype cs t) (@type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a)) => @fold_reptype (Tarray t n a) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a) v))) repinj_aux_s repinj_aux_u t v) (@fold_reptype t (match t as t' return (forall _ : match t' with | Tvoid => unit | Tint i s a => Int.int | Tlong s a => Int64.int | Tfloat f a => float | Tpointer t a => pointer_val | Tarray t0 z a => list (reptype' t0) | Tfunction t t0 c => unit | Tstruct id a => compact_prod (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => compact_sum (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end, match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end) with | Tvoid => @id unit | Tint i s a => Vint | Tlong s a => Vlong | Tfloat f a => Vfloat | Tpointer t a => pointer_val_val | Tarray t0 z a => @map (reptype' t0) (@reptype cs t0) (@type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u t0) | Tfunction t t0 c => @id unit | Tstruct id a => @compact_prod_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => @compact_sum_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end (@unfold_reptype' t v))) *)
  rewrite type_func_eq.
(* Goal: @eq (@reptype cs t) (match t as t0 return (forall _ : reptype' t0, @reptype cs t0) with | Tvoid => repinj_bv Tvoid | Tint i s a => repinj_bv (Tint i s a) | Tlong s a => repinj_bv (Tlong s a) | Tfloat f a => repinj_bv (Tfloat f a) | Tpointer t a => repinj_bv (Tpointer t a) | Tarray t0 n a => fun v : reptype' (Tarray t0 n a) => @fold_reptype (Tarray t0 n a) (@map (reptype' t0) (@reptype cs t0) (@type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n0 : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v0 : reptype' (Tarray t n0 a0)) => @fold_reptype (Tarray t n0 a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n0 a0) v0))) repinj_aux_s repinj_aux_u t0) (@unfold_reptype' (Tarray t0 n a) v)) | Tfunction t t0 c => repinj_bv (Tfunction t t0 c) | Tstruct id a => repinj_aux_s id a (@FTI_aux cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u id) | Tunion id a => repinj_aux_u id a (@FTI_aux cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u id) end v) (@fold_reptype t (match t as t' return (forall _ : match t' with | Tvoid => unit | Tint i s a => Int.int | Tlong s a => Int64.int | Tfloat f a => float | Tpointer t a => pointer_val | Tarray t0 z a => list (reptype' t0) | Tfunction t t0 c => unit | Tstruct id a => compact_prod (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => compact_sum (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end, match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end) with | Tvoid => @id unit | Tint i s a => Vint | Tlong s a => Vlong | Tfloat f a => Vfloat | Tpointer t a => pointer_val_val | Tarray t0 z a => @map (reptype' t0) (@reptype cs t0) (@type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u t0) | Tfunction t t0 c => @id unit | Tstruct id a => @compact_prod_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => @compact_sum_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end (@unfold_reptype' t v))) *)
  destruct t; auto.
  +  unfold FTI_aux; rewrite decay_spec.
(* Goal: @JMeq (@compact_sum_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (@compact_sum_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (reptype_unionlist (co_members (@get_co cs i))) (@compact_sum_gen (prod ident type) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun _ : prod ident type => true) (fun it : prod ident type => @default_val cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (co_members (@get_co cs i))) *)
    rewrite map_map.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    reflexivity.
  + unfold FTI_aux; rewrite decay_spec.
(* Goal: @JMeq (@compact_sum_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (@compact_sum_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (reptype_unionlist (co_members (@get_co cs i))) (@compact_sum_gen (prod ident type) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun _ : prod ident type => true) (fun it : prod ident type => @default_val cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (co_members (@get_co cs i))) *)
    rewrite map_map.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    reflexivity.
Defined.

Definition reptype_structlist (m: members) := compact_prod (map (fun it => reptype (field_type (fst it) m)) m).
Definition reptype_unionlist (m: members) := compact_sum (map (fun it => reptype (field_type (fst it) m)) m).

Notation REPTYPE t :=
  match t return Type with
  | Tvoid
  | Tfunction _ _ _ => unit
  | Tint _ _ _
  | Tlong _ _
  | Tfloat _ _
  | Tpointer _ _ => val
  | Tarray t0 _ _ => list (reptype t0)
  | Tstruct id _ => reptype_structlist (co_members (get_co id))
  | Tunion id _ => reptype_unionlist (co_members (get_co id))
  end.

Lemma reptype_eq: forall t,
  reptype t = REPTYPE t.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq Type (@reptype cs t) match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end *)
  unfold reptype.
(* Goal: @JMeq (let (t, _) := @reptype_gen cs t in t) (let (t, v) as tv return (let (t, _) := tv in t) := @reptype_gen cs t in v) match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end match t as t' return match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end with | Tvoid => tt | Tint i s a => Vundef | Tlong s a => Vundef | Tfloat f a => Vundef | Tpointer t a => Vundef | Tarray t0 n a => @list_repeat (@reptype cs t0) (Z.to_nat n) (let (t, v) as tv return (let (t, _) := tv in t) := @reptype_gen cs t0 in v) | Tfunction t t0 c => tt | Tstruct id a => struct_default_val (co_members (@get_co cs id)) | Tunion id a => union_default_val (co_members (@get_co cs id)) end *)
  rewrite reptype_gen_eq.
(* Goal: @eq Type (let (t, _) := match t with | Tvoid => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt | Tint i s a => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt | Tlong s a => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt | Tfloat f a => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt | Tpointer t0 a => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt | Tarray t0 n a => @existT Type (fun x : Type => x) (list (@projT1 Type (fun x : Type => x) (@reptype_gen cs t0))) (@list_repeat (@projT1 Type (fun x : Type => x) (@reptype_gen cs t0)) (Z.to_nat n) (@projT2 Type (fun x : Type => x) (@reptype_gen cs t0))) | Tfunction t0 t1 c => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt | Tstruct id a => @existT Type (fun x : Type => x) (@compact_prod_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs id))) (co_members (@get_co cs id))))) (@compact_prod_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs id))) (co_members (@get_co cs id))))) | Tunion id a => @existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs id))) (co_members (@get_co cs id))))) (@compact_sum_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs id))) (co_members (@get_co cs id))))) end in t) match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (let (t, _) := @reptype_gen cs t0 in t) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end *)
  destruct t as [| | | | | | | id ? | id ?]; auto.
  + unfold compact_prod_sigT_type.
(* Goal: @eq Type (compact_sum (@map (@sigT Type (fun x : Type => x)) Type (fun tv : @sigT Type (fun x : Type => x) => let (t, _) := tv in t) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs id))) (co_members (@get_co cs id)))))) (reptype_unionlist (co_members (@get_co cs id))) *)
    pose proof get_co_members_no_replicate id.
(* Goal: @eq Type (compact_sum (@map (@sigT Type (fun x : Type => x)) Type (fun tv : @sigT Type (fun x : Type => x) => let (t, _) := tv in t) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs id))) (co_members (@get_co cs id)))))) (reptype_unionlist (co_members (@get_co cs id))) *)
    forget (co_members (get_co id)) as m.
(* Goal: @JMeq (@compact_sum_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (@compact_sum_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (reptype_unionlist (co_members (@get_co cs i))) (@compact_sum_gen (prod ident type) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun _ : prod ident type => true) (fun it : prod ident type => @default_val cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (co_members (@get_co cs i))) *)
    rewrite map_map.
(* Goal: @JMeq (@compact_sum_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (@compact_sum_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (reptype_unionlist (co_members (@get_co cs i))) (@compact_sum_gen (prod ident type) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun _ : prod ident type => true) (fun it : prod ident type => @default_val cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (co_members (@get_co cs i))) *)
    rewrite map_map.
(* Goal: @eq Type (compact_prod (@map (prod ident type) Type (fun x : prod ident type => let (t, _) := @reptype_gen cs (field_type (@fst ident type x) m) in t) m)) (reptype_structlist m) *)
    unfold reptype_structlist.
(* Goal: @eq nat (Z.to_nat (Z.of_nat (@Datatypes.length (@reptype cs t) (@replist cs t lo hi al)))) (Z.to_nat (Z.sub hi lo)) *)
    f_equal.
  + unfold compact_sum_sigT_type.
(* Goal: @eq Type (compact_sum (@map (@sigT Type (fun x : Type => x)) Type (fun tv : @sigT Type (fun x : Type => x) => let (t, _) := tv in t) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs id))) (co_members (@get_co cs id)))))) (reptype_unionlist (co_members (@get_co cs id))) *)
    pose proof get_co_members_no_replicate id.
(* Goal: @eq Type (compact_sum (@map (@sigT Type (fun x : Type => x)) Type (fun tv : @sigT Type (fun x : Type => x) => let (t, _) := tv in t) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs id))) (co_members (@get_co cs id)))))) (reptype_unionlist (co_members (@get_co cs id))) *)
    forget (co_members (get_co id)) as m.
(* Goal: @JMeq (@compact_sum_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (@compact_sum_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (reptype_unionlist (co_members (@get_co cs i))) (@compact_sum_gen (prod ident type) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun _ : prod ident type => true) (fun it : prod ident type => @default_val cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (co_members (@get_co cs i))) *)
    rewrite map_map.
(* Goal: @JMeq (@compact_sum_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (@compact_sum_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (reptype_unionlist (co_members (@get_co cs i))) (@compact_sum_gen (prod ident type) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun _ : prod ident type => true) (fun it : prod ident type => @default_val cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (co_members (@get_co cs i))) *)
    rewrite map_map.
(* Goal: @eq Type (compact_sum (@map (prod ident type) Type (fun x : prod ident type => let (t, _) := @reptype_gen cs (field_type (@fst ident type x) m) in t) m)) (reptype_unionlist m) *)
    unfold reptype_unionlist.
(* Goal: @eq nat (Z.to_nat (Z.of_nat (@Datatypes.length (@reptype cs t) (@replist cs t lo hi al)))) (Z.to_nat (Z.sub hi lo)) *)
    f_equal.
Defined.

Definition unfold_reptype {t} (v: reptype t): REPTYPE t :=
  @eq_rect Type (reptype t) (fun x: Type => x) v (REPTYPE t) (reptype_eq t).

Definition fold_reptype {t} (v: REPTYPE t): reptype t :=
  @eq_rect_r Type (REPTYPE t) (fun x: Type => x) v (reptype t) (reptype_eq t).

Lemma fold_unfold_reptype: forall t (v: reptype t),
  fold_reptype (unfold_reptype v) = v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end (@unfold_reptype t (@fold_reptype t v)) v *)
  unfold fold_reptype, unfold_reptype.
(* Goal: @eq t' (@eq_rect Type (@reptype cs t) (fun x : Type => x) v t' (@reptype_eq cs t)) v' *)
  apply JMeq_eq.
  match goal with
  | |- JMeq (@eq_rect_r ?A ?x ?F ?v ?y ?H) _ =>
    eapply @JMeq_trans; [apply (eq_rect_r_JMeq A x y F v H) |]
  end.
  match goal with
  | |- JMeq (@eq_rect ?A ?x ?F ?v ?y ?H) _ =>
    apply (eq_rect_JMeq A x y F v H)
  end.
Defined.

Lemma unfold_fold_reptype: forall t (v: REPTYPE t),
  unfold_reptype (fold_reptype v) = v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end (@unfold_reptype t (@fold_reptype t v)) v *)
  unfold fold_reptype, unfold_reptype.
(* Goal: @eq t' (@eq_rect Type (@reptype cs t) (fun x : Type => x) v t' (@reptype_eq cs t)) v' *)
  apply JMeq_eq.
  match goal with
  | |- JMeq (@eq_rect ?A ?x ?F ?v ?y ?H) _ =>
    eapply @JMeq_trans; [apply (eq_rect_JMeq A x y F v H) |]
  end.
  match goal with
  | |- JMeq (@eq_rect_r ?A ?x ?F ?v ?y ?H) _ =>
    apply (eq_rect_r_JMeq A x y F v H)
  end.
Defined.

Lemma unfold_reptype_JMeq: forall t (v: reptype t),
  JMeq (unfold_reptype v) v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  unfold unfold_reptype.
  match goal with
  | |- JMeq (@eq_rect ?A ?x ?F ?v ?y ?H) _ =>
    apply (eq_rect_JMeq A x y F v H)
  end.
Qed.

Lemma fold_reptype_JMeq: forall t v,
  JMeq (fold_reptype v : reptype t) v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (@reptype cs t) (@default_val cs t) (@fold_reptype t match t as t' return match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end with | Tvoid => tt | Tint i s a => Vundef | Tlong s a => Vundef | Tfloat f a => Vundef | Tpointer t a => Vundef | Tarray t0 n a => @list_repeat (@reptype cs t0) (Z.to_nat n) (@default_val cs t0) | Tfunction t t0 c => tt | Tstruct id a => struct_default_val (co_members (@get_co cs id)) | Tunion id a => union_default_val (co_members (@get_co cs id)) end) *)
  unfold fold_reptype.
  match goal with
  | |- JMeq (@eq_rect_r ?A ?x ?F ?v ?y ?H) _ =>
    apply (eq_rect_r_JMeq A x y F v H)
  end.
Qed.

Definition union_default_filter m :=
  match m with
  | nil => fun _ => false
  | hd :: _ => fun m => if member_dec hd m then true else false
  end.

Definition is_default_filter {A} f (l: list A) :=
  match l with
  | nil => True
  | hd :: _ => f hd = true
  end.

Lemma union_default_filter_is_default_filter: forall m, is_default_filter (union_default_filter m) m.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @is_default_filter (prod ident type) (fun _ : prod ident type => true) m *)
  destruct m; simpl; auto.
(* Goal: @eq bool (if member_dec p p then true else false) true *)
  destruct (member_dec p p); auto.
Qed.

Lemma const_true_is_default_filter: forall m, is_default_filter (fun _: ident * type => true) m.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @is_default_filter (prod ident type) (fun _ : prod ident type => true) m *)
  destruct m; simpl; auto.
Qed.

(*
Lemma union_default_filter_legal: forall m, m <> nil ->
  legal_compact_sum_filter (union_default_filter m) m = true.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
  destruct m; auto.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) lo (S n) al)) (Z.succ (Z.of_nat n)) *)
  simpl.
  destruct (member_dec p p); [| congruence].
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
  auto.
Qed.
*)

Definition struct_default_val (m : members) := compact_prod_gen (fun it => default_val (field_type (fst it) m)) m.
Definition union_default_val (m : members) := compact_sum_gen (fun it => true) (fun it => default_val (field_type (fst it) m)) m.

Lemma compact_prod_sigT_compact_prod_gen:
  forall {A B} {P: A -> Type} (genT: B -> A) (genV: forall b: B, P (genT b)) (gen: B -> sigT P) (l: list B),
    (forall b, gen b = existT P (genT b) (genV b)) ->
    JMeq (compact_prod_sigT_value (map gen l)) (compact_prod_gen genV l).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @JMeq (compact_prod (@map (@sigT A P) Type (fun tv : @sigT A P => let (t, _) := tv in P t) (@map B (@sigT A P) gen l))) (@compact_prod_sigT_value A P (@map B (@sigT A P) gen l)) (compact_prod (@map B Type (fun b : B => P (genT b)) l)) (@compact_prod_gen B (fun b : B => P (genT b)) genV l) *)
  assert (gen = fun b => existT P (genT b) (genV b)) by (extensionality; apply H).
(* Goal: @JMeq (compact_prod (@map (@sigT A P) Type (fun tv : @sigT A P => let (t, _) := tv in P t) (@map B (@sigT A P) gen l))) (@compact_prod_sigT_value A P (@map B (@sigT A P) gen l)) (compact_prod (@map B Type (fun b : B => P (genT b)) l)) (@compact_prod_gen B (fun b : B => P (genT b)) genV l) *)
  rewrite H0; clear H H0 gen.
(* Goal: @JMeq (compact_prod (@map (@sigT A P) Type (fun tv : @sigT A P => let (t, _) := tv in P t) (@map B (@sigT A P) (fun b : B => @existT A P (genT b) (genV b)) l))) (@compact_prod_sigT_value A P (@map B (@sigT A P) (fun b : B => @existT A P (genT b) (genV b)) l)) (compact_prod (@map B Type (fun b : B => P (genT b)) l)) (@compact_prod_gen B (fun b : B => P (genT b)) genV l) *)
  destruct l; [apply JMeq_refl |].
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  revert b; induction l; intros.
  + apply JMeq_refl.
  + simpl map.
(* Goal: @JMeq (compact_prod (@cons Type (P (genT b)) (@cons Type (P (genT a)) (@map (@sigT A P) Type (fun tv : @sigT A P => let (t, _) := tv in P t) (@map B (@sigT A P) (fun b : B => @existT A P (genT b) (genV b)) l))))) (@compact_prod_sigT_value A P (@cons (@sigT A P) (@existT A P (genT b) (genV b)) (@cons (@sigT A P) (@existT A P (genT a) (genV a)) (@map B (@sigT A P) (fun b : B => @existT A P (genT b) (genV b)) l)))) (compact_prod (@cons Type (P (genT b)) (@cons Type (P (genT a)) (@map B Type (fun b : B => P (genT b)) l)))) (@compact_prod_gen B (fun b : B => P (genT b)) genV (@cons B b (@cons B a l))) *)
    change (compact_prod_gen genV (b :: a :: l)) with (genV b, compact_prod_gen genV (a :: l)).
    change (compact_prod_sigT_value
        (existT P (genT b) (genV b)
         :: existT P (genT a) (genV a)
            :: map (fun b0 : B => existT P (genT b0) (genV b0)) l)) with
      (genV b, compact_prod_sigT_value (existT P (genT a) (genV a) :: map (fun b0 : B => existT P (genT b0) (genV b0)) l)).
(* Goal: @JMeq (compact_prod (@cons Type (P (genT b)) (@cons Type (P (genT a)) (@map (@sigT A P) Type (fun tv : @sigT A P => let (t, _) := tv in P t) (@map B (@sigT A P) (fun b : B => @existT A P (genT b) (genV b)) l))))) (@pair (P (genT b)) (compact_prod (@map (@sigT A P) Type (fun tv : @sigT A P => let (t, _) := tv in P t) (@cons (@sigT A P) (@existT A P (genT a) (genV a)) (@map B (@sigT A P) (fun b0 : B => @existT A P (genT b0) (genV b0)) l)))) (genV b) (@compact_prod_sigT_value A P (@cons (@sigT A P) (@existT A P (genT a) (genV a)) (@map B (@sigT A P) (fun b0 : B => @existT A P (genT b0) (genV b0)) l)))) (compact_prod (@cons Type (P (genT b)) (@cons Type (P (genT a)) (@map B Type (fun b : B => P (genT b)) l)))) (@pair (P (genT b)) (compact_prod (@map B Type (fun b : B => P (genT b)) (@cons B a l))) (genV b) (@compact_prod_gen B (fun b : B => P (genT b)) genV (@cons B a l))) *)
    apply JMeq_pair; [auto |].
(* Goal: @JMeq (compact_prod (@map (@sigT A P) Type (fun tv : @sigT A P => let (t, _) := tv in P t) (@cons (@sigT A P) (@existT A P (genT a) (genV a)) (@map B (@sigT A P) (fun b0 : B => @existT A P (genT b0) (genV b0)) l)))) (@compact_prod_sigT_value A P (@cons (@sigT A P) (@existT A P (genT a) (genV a)) (@map B (@sigT A P) (fun b0 : B => @existT A P (genT b0) (genV b0)) l))) (compact_prod (@map B Type (fun b : B => P (genT b)) (@cons B a l))) (@compact_prod_gen B (fun b : B => P (genT b)) genV (@cons B a l)) *)
    exact (IHl a).
Qed.

Lemma compact_sum_sigT_compact_sum_gen:
  forall {A B} {P: A -> Type} (genT: B -> A) (genV: forall b: B, P (genT b)) (filter: B -> bool) (gen: B -> sigT P) (l: list B),
    (forall b, gen b = existT P (genT b) (genV b)) ->
    is_default_filter filter l ->
    JMeq (compact_sum_sigT_value (map gen l)) (compact_sum_gen filter genV l).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @JMeq (compact_prod (@map (@sigT A P) Type (fun tv : @sigT A P => let (t, _) := tv in P t) (@map B (@sigT A P) gen l))) (@compact_prod_sigT_value A P (@map B (@sigT A P) gen l)) (compact_prod (@map B Type (fun b : B => P (genT b)) l)) (@compact_prod_gen B (fun b : B => P (genT b)) genV l) *)
  assert (gen = fun b => existT P (genT b) (genV b)) by (extensionality; apply H).
  rewrite H1; clear H H1 gen.
(* Goal: @JMeq (compact_prod (@map (@sigT A P) Type (fun tv : @sigT A P => let (t, _) := tv in P t) (@map B (@sigT A P) (fun b : B => @existT A P (genT b) (genV b)) l))) (@compact_prod_sigT_value A P (@map B (@sigT A P) (fun b : B => @existT A P (genT b) (genV b)) l)) (compact_prod (@map B Type (fun b : B => P (genT b)) l)) (@compact_prod_gen B (fun b : B => P (genT b)) genV l) *)
  destruct l; [apply JMeq_refl |].
  destruct l.
  + apply JMeq_refl.
  + change (compact_sum_sigT_value
        (map (fun b1 : B => existT P (genT b1) (genV b1)) (b :: b0 :: l))) with
  (@inl (P (genT b)) (compact_sum (map (fun tv => match tv with existT t _ => P t end) (map (fun b1 : B => @existT A P (genT b1) (genV b1)) (b0 :: l)))) (genV b)).
    change (compact_sum (map (fun tv => match _ with existT t _ => P t end) (map (fun b1 : B => @existT A P (genT b1) (genV b1)) (b :: b0 :: l)))) with
      (P (genT b) + compact_sum (map (fun tv => match tv with existT t _ => P t end) (map (fun b1 : B => @existT A P (genT b1) (genV b1)) (b0 :: l))))%type.
    replace (compact_sum_gen filter genV (b :: b0 :: l)) with
      (@inl (P (genT b)) (compact_sum (map (fun b1 : B => P (genT b1)) (b0 :: l))) (genV b)).
    2:{
      simpl in H0 |- *.
      rewrite H0.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
      auto.
    }
    match goal with
    | |- @JMeq _ (@inl _ ?A _) _ (@inl _ ?B _) =>
         replace A with B; [auto |]
    end.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    rewrite map_map; reflexivity.
Qed.

Lemma default_val_eq: forall t,
  default_val t =
  fold_reptype
  match t as t' return REPTYPE t'
  with
  | Tvoid
  | Tfunction _ _ _ => tt
  | Tint _ _ _
  | Tlong _ _
  | Tfloat _ _
  | Tpointer _ _ => Vundef
  | Tarray t0 n _ => list_repeat (Z.to_nat n) (default_val t0)
  | Tstruct id _ => struct_default_val (co_members (get_co id))
  | Tunion id _ => union_default_val (co_members (get_co id))
  end.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (@reptype cs t) (@default_val cs t) (@fold_reptype t match t as t' return match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end with | Tvoid => tt | Tint i s a => Vundef | Tlong s a => Vundef | Tfloat f a => Vundef | Tpointer t a => Vundef | Tarray t0 n a => @list_repeat (@reptype cs t0) (Z.to_nat n) (@default_val cs t0) | Tfunction t t0 c => tt | Tstruct id a => struct_default_val (co_members (@get_co cs id)) | Tunion id a => union_default_val (co_members (@get_co cs id)) end) *)
  unfold fold_reptype.
(* Goal: @eq t' (@eq_rect Type (@reptype cs t) (fun x : Type => x) v t' (@reptype_eq cs t)) v' *)
  apply JMeq_eq.
  match goal with
  | |- JMeq _ (@eq_rect_r ?A ?x ?F ?v ?y ?H) =>
    eapply JMeq_trans; [| apply @JMeq_sym; apply (@eq_rect_r_JMeq A x y F v H)]
  end.
(* Goal: @JMeq (@reptype cs t) (@default_val cs t) match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end match t as t' return match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end with | Tvoid => tt | Tint i s a => Vundef | Tlong s a => Vundef | Tfloat f a => Vundef | Tpointer t a => Vundef | Tarray t0 n a => @list_repeat (@reptype cs t0) (Z.to_nat n) (@default_val cs t0) | Tfunction t t0 c => tt | Tstruct id a => struct_default_val (co_members (@get_co cs id)) | Tunion id a => union_default_val (co_members (@get_co cs id)) end *)
  unfold default_val.
(* Goal: @JMeq (@reptype cs t) (let (t, v) as tv return (let (t, _) := tv in t) := @reptype_gen cs t in v) match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end match t as t' return match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end with | Tvoid => tt | Tint i s a => Vundef | Tlong s a => Vundef | Tfloat f a => Vundef | Tpointer t a => Vundef | Tarray t0 n a => @list_repeat (@reptype cs t0) (Z.to_nat n) (let (t, v) as tv return (let (t, _) := tv in t) := @reptype_gen cs t0 in v) | Tfunction t t0 c => tt | Tstruct id a => struct_default_val (co_members (@get_co cs id)) | Tunion id a => union_default_val (co_members (@get_co cs id)) end *)
  unfold reptype at 1.
(* Goal: @JMeq (let (t, _) := @reptype_gen cs t in t) (let (t, v) as tv return (let (t, _) := tv in t) := @reptype_gen cs t in v) match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end match t as t' return match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end with | Tvoid => tt | Tint i s a => Vundef | Tlong s a => Vundef | Tfloat f a => Vundef | Tpointer t a => Vundef | Tarray t0 n a => @list_repeat (@reptype cs t0) (Z.to_nat n) (let (t, v) as tv return (let (t, _) := tv in t) := @reptype_gen cs t0 in v) | Tfunction t t0 c => tt | Tstruct id a => struct_default_val (co_members (@get_co cs id)) | Tunion id a => union_default_val (co_members (@get_co cs id)) end *)
  rewrite reptype_gen_eq.
(* Goal: @eq (@reptype cs t) (match t as t0 return (forall _ : reptype' t0, @reptype cs t0) with | Tvoid => repinj_bv Tvoid | Tint i s a => repinj_bv (Tint i s a) | Tlong s a => repinj_bv (Tlong s a) | Tfloat f a => repinj_bv (Tfloat f a) | Tpointer t a => repinj_bv (Tpointer t a) | Tarray t0 n a => fun v : reptype' (Tarray t0 n a) => @fold_reptype (Tarray t0 n a) (@map (reptype' t0) (@reptype cs t0) (@type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n0 : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v0 : reptype' (Tarray t n0 a0)) => @fold_reptype (Tarray t n0 a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n0 a0) v0))) repinj_aux_s repinj_aux_u t0) (@unfold_reptype' (Tarray t0 n a) v)) | Tfunction t t0 c => repinj_bv (Tfunction t t0 c) | Tstruct id a => repinj_aux_s id a (@FTI_aux cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u id) | Tunion id a => repinj_aux_u id a (@FTI_aux cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u id) end v) (@fold_reptype t (match t as t' return (forall _ : match t' with | Tvoid => unit | Tint i s a => Int.int | Tlong s a => Int64.int | Tfloat f a => float | Tpointer t a => pointer_val | Tarray t0 z a => list (reptype' t0) | Tfunction t t0 c => unit | Tstruct id a => compact_prod (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => compact_sum (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end, match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end) with | Tvoid => @id unit | Tint i s a => Vint | Tlong s a => Vlong | Tfloat f a => Vfloat | Tpointer t a => pointer_val_val | Tarray t0 z a => @map (reptype' t0) (@reptype cs t0) (@type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u t0) | Tfunction t t0 c => @id unit | Tstruct id a => @compact_prod_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => @compact_sum_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end (@unfold_reptype' t v))) *)
  destruct t; auto.
  + unfold struct_default_val.
(* Goal: @JMeq (@compact_sum_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (@compact_sum_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (reptype_unionlist (co_members (@get_co cs i))) (@compact_sum_gen (prod ident type) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun _ : prod ident type => true) (fun it : prod ident type => @default_val cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (co_members (@get_co cs i))) *)
    rewrite map_map.
    apply (compact_prod_sigT_compact_prod_gen
      (fun it => reptype (field_type (fst it) (co_members (get_co i))))
      (fun it => default_val (field_type (fst it) (co_members (get_co i))))
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
      (fun it => reptype_gen (field_type (fst it) (co_members (get_co i))))); intros.
(* Goal: @eq (@sigT Type (fun x : Type => x)) (@reptype_gen cs (field_type (@fst ident type b) (co_members (@get_co cs i)))) (@existT Type (fun x : Type => x) (@reptype cs (field_type (@fst ident type b) (co_members (@get_co cs i)))) (@default_val cs (field_type (@fst ident type b) (co_members (@get_co cs i))))) *)
(* Goal: @is_default_filter (prod ident type) (fun _ : prod ident type => true) (co_members (@get_co cs i)) *)
    unfold reptype, default_val.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    destruct (reptype_gen (field_type (fst b) (co_members (get_co i)))); reflexivity.
  + unfold union_default_val.
(* Goal: @JMeq (@compact_sum_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (@compact_sum_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (reptype_unionlist (co_members (@get_co cs i))) (@compact_sum_gen (prod ident type) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun _ : prod ident type => true) (fun it : prod ident type => @default_val cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (co_members (@get_co cs i))) *)
    rewrite map_map.
    apply (compact_sum_sigT_compact_sum_gen
      (fun it => reptype (field_type (fst it) (co_members (get_co i))))
      (fun it => default_val (field_type (fst it) (co_members (get_co i))))
      _
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
      (fun it => reptype_gen (field_type (fst it) (co_members (get_co i))))); intros.
(* Goal: @eq (@sigT Type (fun x : Type => x)) (@reptype_gen cs (field_type (@fst ident type b) (co_members (@get_co cs i)))) (@existT Type (fun x : Type => x) (@reptype cs (field_type (@fst ident type b) (co_members (@get_co cs i)))) (@default_val cs (field_type (@fst ident type b) (co_members (@get_co cs i))))) *)
(* Goal: @is_default_filter (prod ident type) (fun _ : prod ident type => true) (co_members (@get_co cs i)) *)
    unfold reptype, default_val.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    destruct (reptype_gen (field_type (fst b) (co_members (get_co i)))); reflexivity.
(* Goal: @is_default_filter (prod ident type) (fun _ : prod ident type => true) (co_members (@get_co cs i)) *)
    apply const_true_is_default_filter.
Qed.

Inductive pointer_val : Type :=
  | ValidPointer: block -> Ptrofs.int -> pointer_val
  | NullPointer.

Lemma PV_eq_dec: forall x y: pointer_val, {x = y} + {x <> y}.
Proof.
(* Goal: forall x y : pointer_val, sumbool (@eq pointer_val x y) (not (@eq pointer_val x y)) *)
  intros; destruct x, y; [| right | right | left]; try congruence.
(* Goal: sumbool (@eq pointer_val (ValidPointer b i) (ValidPointer b0 i0)) (not (@eq pointer_val (ValidPointer b i) (ValidPointer b0 i0))) *)
  destruct (block_eq_dec b b0), (Ptrofs.eq_dec i i0); [left | right | right | right]; congruence.
Qed.

Lemma zero_in_range : (-1 < 0 < Int.modulus)%Z.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
compute; split; auto.
Defined.
Definition Int_zero := Int.mkint 0 zero_in_range.

Definition pointer_val_val (pv: pointer_val): val :=
  match pv with
  | ValidPointer b i => Vptr b i
  | NullPointer => Vint Int.zero (* Vint Int_zero *)
  end.

Definition reptype': type -> Type :=
  type_func (fun _ => Type)
  (fun t =>
     if (type_is_by_value t)
     then match t with
          | Tint _ _ _ => int
          | Tlong _ _ => Int64.int
          | Tfloat _ _ => float
          | Tpointer _ _ => pointer_val
          | _ => val
          end
     else unit)
  (fun t n a T => list T)
  (fun id a T => compact_prod (decay T))
  (fun id a T => compact_sum (decay T)).

Notation REPTYPE' t :=
  match t return Type with
  | Tvoid
  | Tfunction _ _ _ => unit
  | Tint _ _ a => int
  | Tlong _ a => Int64.int
  | Tfloat _ a => float
  | Tpointer _ a => pointer_val
  | Tarray t0 _ _ => list (reptype' t0)
  | Tstruct id _ => compact_prod (map (fun it => reptype' (field_type (fst it) (co_members (get_co id)))) (co_members (get_co id)))
  | Tunion id _ => compact_sum (map (fun it => reptype' (field_type (fst it) (co_members (get_co id)))) (co_members (get_co id)))
  end.

Lemma reptype'_eq: forall t,
  reptype' t = REPTYPE' t.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
 unfold reptype'.
 etransitivity.
 apply (type_func_eq (fun _ => Type) _ _ _ _ t) .
(* Goal: @eq (@reptype cs t) (match t as t0 return (forall _ : reptype' t0, @reptype cs t0) with | Tvoid => repinj_bv Tvoid | Tint i s a => repinj_bv (Tint i s a) | Tlong s a => repinj_bv (Tlong s a) | Tfloat f a => repinj_bv (Tfloat f a) | Tpointer t a => repinj_bv (Tpointer t a) | Tarray t0 n a => fun v : reptype' (Tarray t0 n a) => @fold_reptype (Tarray t0 n a) (@map (reptype' t0) (@reptype cs t0) (@type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n0 : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v0 : reptype' (Tarray t n0 a0)) => @fold_reptype (Tarray t n0 a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n0 a0) v0))) repinj_aux_s repinj_aux_u t0) (@unfold_reptype' (Tarray t0 n a) v)) | Tfunction t t0 c => repinj_bv (Tfunction t t0 c) | Tstruct id a => repinj_aux_s id a (@FTI_aux cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u id) | Tunion id a => repinj_aux_u id a (@FTI_aux cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u id) end v) (@fold_reptype t (match t as t' return (forall _ : match t' with | Tvoid => unit | Tint i s a => Int.int | Tlong s a => Int64.int | Tfloat f a => float | Tpointer t a => pointer_val | Tarray t0 z a => list (reptype' t0) | Tfunction t t0 c => unit | Tstruct id a => compact_prod (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => compact_sum (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end, match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end) with | Tvoid => @id unit | Tint i s a => Vint | Tlong s a => Vlong | Tfloat f a => Vfloat | Tpointer t a => pointer_val_val | Tarray t0 z a => @map (reptype' t0) (@reptype cs t0) (@type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u t0) | Tfunction t t0 c => @id unit | Tstruct id a => @compact_prod_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => @compact_sum_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end (@unfold_reptype' t v))) *)
  destruct t; auto.
  + f_equal.
(* Goal: @eq (@sigT Type (fun x : Type => x)) (@existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs i)) (@FTI_aux cs (fun _ : type => @sigT Type (fun x : Type => x)) (fun t : type => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (fun (_ : type) (n : Z) (_ : attr) (TV : @sigT Type (fun x : Type => x)) => @existT Type (fun x : Type => x) (list (@projT1 Type (fun x : Type => x) TV)) (@list_repeat (@projT1 Type (fun x : Type => x) TV) (Z.to_nat n) (@projT2 Type (fun x : Type => x) TV))) (fun (id : positive) (_ : attr) (TVs : @FT_aux cs (fun _ : type => @sigT Type (fun x : Type => x)) id) => @existT Type (fun x : Type => x) (@compact_prod_sigT_type Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs)) (@compact_prod_sigT_value Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs))) (fun (id : positive) (_ : attr) (TVs : @FT_aux cs (fun _ : type => @sigT Type (fun x : Type => x)) id) => @existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs)) (@compact_sum_sigT_value Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs))) i))) (@compact_sum_sigT_value Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs i)) (@FTI_aux cs (fun _ : type => @sigT Type (fun x : Type => x)) (fun t : type => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (fun (_ : type) (n : Z) (_ : attr) (TV : @sigT Type (fun x : Type => x)) => @existT Type (fun x : Type => x) (list (@projT1 Type (fun x : Type => x) TV)) (@list_repeat (@projT1 Type (fun x : Type => x) TV) (Z.to_nat n) (@projT2 Type (fun x : Type => x) TV))) (fun (id : positive) (_ : attr) (TVs : @FT_aux cs (fun _ : type => @sigT Type (fun x : Type => x)) id) => @existT Type (fun x : Type => x) (@compact_prod_sigT_type Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs)) (@compact_prod_sigT_value Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs))) (fun (id : positive) (_ : attr) (TVs : @FT_aux cs (fun _ : type => @sigT Type (fun x : Type => x)) id) => @existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs)) (@compact_sum_sigT_value Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs))) i)))) (@existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (@compact_sum_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i)))))) *)
    unfold FTI_aux; rewrite decay_spec.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    reflexivity.
  + f_equal.
(* Goal: @eq (@sigT Type (fun x : Type => x)) (@existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs i)) (@FTI_aux cs (fun _ : type => @sigT Type (fun x : Type => x)) (fun t : type => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (fun (_ : type) (n : Z) (_ : attr) (TV : @sigT Type (fun x : Type => x)) => @existT Type (fun x : Type => x) (list (@projT1 Type (fun x : Type => x) TV)) (@list_repeat (@projT1 Type (fun x : Type => x) TV) (Z.to_nat n) (@projT2 Type (fun x : Type => x) TV))) (fun (id : positive) (_ : attr) (TVs : @FT_aux cs (fun _ : type => @sigT Type (fun x : Type => x)) id) => @existT Type (fun x : Type => x) (@compact_prod_sigT_type Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs)) (@compact_prod_sigT_value Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs))) (fun (id : positive) (_ : attr) (TVs : @FT_aux cs (fun _ : type => @sigT Type (fun x : Type => x)) id) => @existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs)) (@compact_sum_sigT_value Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs))) i))) (@compact_sum_sigT_value Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs i)) (@FTI_aux cs (fun _ : type => @sigT Type (fun x : Type => x)) (fun t : type => if type_is_by_value t then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (fun (_ : type) (n : Z) (_ : attr) (TV : @sigT Type (fun x : Type => x)) => @existT Type (fun x : Type => x) (list (@projT1 Type (fun x : Type => x) TV)) (@list_repeat (@projT1 Type (fun x : Type => x) TV) (Z.to_nat n) (@projT2 Type (fun x : Type => x) TV))) (fun (id : positive) (_ : attr) (TVs : @FT_aux cs (fun _ : type => @sigT Type (fun x : Type => x)) id) => @existT Type (fun x : Type => x) (@compact_prod_sigT_type Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs)) (@compact_prod_sigT_value Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs))) (fun (id : positive) (_ : attr) (TVs : @FT_aux cs (fun _ : type => @sigT Type (fun x : Type => x)) id) => @existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs)) (@compact_sum_sigT_value Type (fun x : Type => x) (@decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co cs id)) TVs))) i)))) (@existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i))))) (@compact_sum_sigT_value Type (fun x : Type => x) (@map type (@sigT Type (fun x : Type => x)) (@reptype_gen cs) (@map (prod ident type) type (fun it : prod ident type => field_type (@fst ident type it) (co_members (@get_co cs i))) (co_members (@get_co cs i)))))) *)
    unfold FTI_aux; rewrite decay_spec.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    reflexivity.
Defined.

Definition unfold_reptype' {t} (v: reptype' t): REPTYPE' t :=
  @eq_rect Type (reptype' t) (fun x: Type => x) v (REPTYPE' t) (reptype'_eq t).

Definition fold_reptype' {t} (v: REPTYPE' t): reptype' t :=
  @eq_rect_r Type (REPTYPE' t) (fun x: Type => x) v (reptype' t) (reptype'_eq t).

Lemma fold_unfold_reptype': forall t (v: reptype' t),
  fold_reptype' (unfold_reptype' v) = v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq match t with | Tvoid => unit | Tint i s a => Int.int | Tlong s a => Int64.int | Tfloat f a => float | Tpointer t a => pointer_val | Tarray t0 z a => list (reptype' t0) | Tfunction t t0 c => unit | Tstruct id a => compact_prod (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => compact_sum (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end (@unfold_reptype' t (@fold_reptype' t v)) v *)
  unfold fold_reptype', unfold_reptype'.
(* Goal: @eq t' (@eq_rect Type (@reptype cs t) (fun x : Type => x) v t' (@reptype_eq cs t)) v' *)
  apply JMeq_eq.
  match goal with
  | |- JMeq (@eq_rect_r ?A ?x ?F ?v ?y ?H) _ =>
    eapply JMeq_trans; [apply (eq_rect_r_JMeq A x y F v H) |]
  end.
  match goal with
  | |- JMeq (@eq_rect ?A ?x ?F ?v ?y ?H) _ =>
    apply (eq_rect_JMeq A x y F v H)
  end.
Defined.

Lemma unfold_fold_reptype': forall t (v: REPTYPE' t),
  unfold_reptype' (fold_reptype' v) = v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq match t with | Tvoid => unit | Tint i s a => Int.int | Tlong s a => Int64.int | Tfloat f a => float | Tpointer t a => pointer_val | Tarray t0 z a => list (reptype' t0) | Tfunction t t0 c => unit | Tstruct id a => compact_prod (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => compact_sum (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end (@unfold_reptype' t (@fold_reptype' t v)) v *)
  unfold fold_reptype', unfold_reptype'.
(* Goal: @eq t' (@eq_rect Type (@reptype cs t) (fun x : Type => x) v t' (@reptype_eq cs t)) v' *)
  apply JMeq_eq.
  match goal with
  | |- JMeq (@eq_rect ?A ?x ?F ?v ?y ?H) _ =>
    eapply JMeq_trans; [apply (eq_rect_JMeq A x y F v H) |]
  end.
  match goal with
  | |- JMeq (@eq_rect_r ?A ?x ?F ?v ?y ?H) _ =>
    apply (eq_rect_r_JMeq A x y F v H)
  end.
Defined.

Definition repinj_bv (t: type): reptype' t -> reptype t :=
  fun v =>
  fold_reptype
  (match t as t' return (REPTYPE' t' -> REPTYPE t': Type)
   with
   | Tvoid
   | Tfunction _ _ _ => @id unit
   | Tint _ _ a => Vint
   | Tlong _ a => Vlong
   | Tfloat _ a => Vfloat
   | Tpointer _ a => pointer_val_val
   | Tarray t0 n a => fun _ => nil
   | Tstruct id a => fun _ => struct_default_val _
   | Tunion id a => fun _ => union_default_val _
   end (unfold_reptype' v)).

Definition repinj_aux_s (id: ident) (a: attr) (F: ListType (map (fun it => reptype' (field_type (fst it) (co_members (get_co id))) -> reptype (field_type (fst it) (co_members (get_co id)))) (co_members (get_co id)))): reptype' (Tstruct id a) -> reptype (Tstruct id a) :=
  fun v => @fold_reptype (Tstruct id a) (compact_prod_map _ F (unfold_reptype' v)).

Definition repinj_aux_u (id: ident) (a: attr) (F: ListType (map (fun it => reptype' (field_type (fst it) (co_members (get_co id))) -> reptype (field_type (fst it) (co_members (get_co id)))) (co_members (get_co id)))): reptype' (Tunion id a) -> reptype (Tunion id a) :=
  fun v => @fold_reptype (Tunion id a) (compact_sum_map _ F (unfold_reptype' v)).

Definition repinj: forall t: type, reptype' t -> reptype t :=
  type_func (fun t => reptype' t -> reptype t)
  repinj_bv
  (fun t n a f v => @fold_reptype (Tarray t n a) (map f (unfold_reptype' v)))
  repinj_aux_s
  repinj_aux_u.

Lemma repinj_eq: forall t v,
  repinj t v =
  fold_reptype
  (match t as t' return REPTYPE' t' -> REPTYPE t' with
   | Tvoid
   | Tfunction _ _ _ => @id unit
   | Tint _ _ a => Vint
   | Tlong _ a => Vlong
   | Tfloat _ a => Vfloat
   | Tpointer _ a => pointer_val_val
   | Tarray t0 _ _ => map (repinj t0)
   | Tstruct id a => compact_prod_map _ (ListTypeGen (fun it => reptype' (field_type (fst it) (co_members (get_co id))) -> reptype (field_type (fst it) (co_members (get_co id)))) (fun it => repinj (field_type (fst it) (co_members (get_co id)))) (co_members (get_co id)))
   | Tunion id a => compact_sum_map _ (ListTypeGen (fun it => reptype' (field_type (fst it) (co_members (get_co id))) -> reptype (field_type (fst it) (co_members (get_co id)))) (fun it => repinj (field_type (fst it) (co_members (get_co id)))) (co_members (get_co id)))
   end (unfold_reptype' v)).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (@reptype cs t) (repinj t v) (@fold_reptype t (match t as t' return (forall _ : match t' with | Tvoid => unit | Tint i s a => Int.int | Tlong s a => Int64.int | Tfloat f a => float | Tpointer t a => pointer_val | Tarray t0 z a => list (reptype' t0) | Tfunction t t0 c => unit | Tstruct id a => compact_prod (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => compact_sum (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end, match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end) with | Tvoid => @id unit | Tint i s a => Vint | Tlong s a => Vlong | Tfloat f a => Vfloat | Tpointer t a => pointer_val_val | Tarray t0 z a => @map (reptype' t0) (@reptype cs t0) (repinj t0) | Tfunction t t0 c => @id unit | Tstruct id a => @compact_prod_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => repinj (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => @compact_sum_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => repinj (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end (@unfold_reptype' t v))) *)
  unfold repinj.
(* Goal: @eq (@reptype cs t) (@type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a)) => @fold_reptype (Tarray t n a) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a) v))) repinj_aux_s repinj_aux_u t v) (@fold_reptype t (match t as t' return (forall _ : match t' with | Tvoid => unit | Tint i s a => Int.int | Tlong s a => Int64.int | Tfloat f a => float | Tpointer t a => pointer_val | Tarray t0 z a => list (reptype' t0) | Tfunction t t0 c => unit | Tstruct id a => compact_prod (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => compact_sum (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end, match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end) with | Tvoid => @id unit | Tint i s a => Vint | Tlong s a => Vlong | Tfloat f a => Vfloat | Tpointer t a => pointer_val_val | Tarray t0 z a => @map (reptype' t0) (@reptype cs t0) (@type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u t0) | Tfunction t t0 c => @id unit | Tstruct id a => @compact_prod_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => @compact_sum_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end (@unfold_reptype' t v))) *)
  rewrite type_func_eq.
(* Goal: @eq (@reptype cs t) (match t as t0 return (forall _ : reptype' t0, @reptype cs t0) with | Tvoid => repinj_bv Tvoid | Tint i s a => repinj_bv (Tint i s a) | Tlong s a => repinj_bv (Tlong s a) | Tfloat f a => repinj_bv (Tfloat f a) | Tpointer t a => repinj_bv (Tpointer t a) | Tarray t0 n a => fun v : reptype' (Tarray t0 n a) => @fold_reptype (Tarray t0 n a) (@map (reptype' t0) (@reptype cs t0) (@type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n0 : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v0 : reptype' (Tarray t n0 a0)) => @fold_reptype (Tarray t n0 a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n0 a0) v0))) repinj_aux_s repinj_aux_u t0) (@unfold_reptype' (Tarray t0 n a) v)) | Tfunction t t0 c => repinj_bv (Tfunction t t0 c) | Tstruct id a => repinj_aux_s id a (@FTI_aux cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u id) | Tunion id a => repinj_aux_u id a (@FTI_aux cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u id) end v) (@fold_reptype t (match t as t' return (forall _ : match t' with | Tvoid => unit | Tint i s a => Int.int | Tlong s a => Int64.int | Tfloat f a => float | Tpointer t a => pointer_val | Tarray t0 z a => list (reptype' t0) | Tfunction t t0 c => unit | Tstruct id a => compact_prod (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => compact_sum (@map (prod ident type) Type (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end, match t' with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => reptype_structlist (co_members (@get_co cs id)) | Tunion id a => reptype_unionlist (co_members (@get_co cs id)) end) with | Tvoid => @id unit | Tint i s a => Vint | Tlong s a => Vlong | Tfloat f a => Vfloat | Tpointer t a => pointer_val_val | Tarray t0 z a => @map (reptype' t0) (@reptype cs t0) (@type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u t0) | Tfunction t t0 c => @id unit | Tstruct id a => @compact_prod_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) | Tunion id a => @compact_sum_map (prod ident type) (fun it : prod ident type => reptype' (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id)) (@ListTypeGen (prod ident type) (fun it : prod ident type => forall _ : reptype' (field_type (@fst ident type it) (co_members (@get_co cs id))), @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : reptype' t, @reptype cs t) repinj_bv (fun (t : type) (n : Z) (a0 : attr) (f : forall _ : reptype' t, @reptype cs t) (v : reptype' (Tarray t n a0)) => @fold_reptype (Tarray t n a0) (@map (reptype' t) (@reptype cs t) f (@unfold_reptype' (Tarray t n a0) v))) repinj_aux_s repinj_aux_u (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_members (@get_co cs id))) end (@unfold_reptype' t v))) *)
  destruct t; auto.
Defined.

Lemma int_add_repr_0_l: forall i, Int.add (Int.repr 0) i = i.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
Proof. intros. apply Int.add_zero_l. Qed.
Lemma int_add_repr_0_r: forall i, Int.add i (Int.repr 0) = i.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
Proof. intros. apply Int.add_zero. Qed.
Hint Rewrite int_add_repr_0_l int_add_repr_0_r : norm.

Lemma ptrofs_add_repr_0_l: forall i, Ptrofs.add (Ptrofs.repr 0) i = i.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
Proof. intros. apply Ptrofs.add_zero_l. Qed.
Lemma ptrofs_add_repr_0_r: forall i, Ptrofs.add i (Ptrofs.repr 0) = i.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
Proof. intros. apply Ptrofs.add_zero. Qed.
Hint Rewrite ptrofs_add_repr_0_l ptrofs_add_repr_0_r : norm.

Definition repinject (t: type) : reptype t -> val :=
  match t as t0 return reptype t0 -> val with
  | Tint _ _ _ => fun v => v
  | Tlong _ _ => fun v => v
  | Tfloat _ _ => fun v => v
  | Tpointer _ _ => fun v => v
  | _ => fun _ => Vundef
 end.

Definition valinject (t: type) : val -> reptype t :=
  match t as t0 return val -> reptype t0 with
  | Tint _ _ _ => fun v => v
  | Tlong _ _ => fun v => v
  | Tfloat _ _ => fun v => v
  | Tpointer _ _ => fun v => v
  | t => fun _ => default_val t
 end.

Lemma valinject_JMeq: forall t v, type_is_by_value t = true -> JMeq (valinject t v) v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @JMeq (@reptype cs_from (Tfunction t t0 c)) (@fold_reptype cs_from (Tfunction t t0 c) tt) (@reptype cs_to (Tfunction t t0 c)) (@fold_reptype cs_to (Tfunction t t0 c) tt) *)
  destruct t; simpl in *; try congruence; try tauto; apply JMeq_refl.
Qed.

Lemma repinject_JMeq: forall t v, type_is_by_value t = true -> JMeq (repinject t v) v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @JMeq (@reptype cs_from (Tfunction t t0 c)) (@fold_reptype cs_from (Tfunction t t0 c) tt) (@reptype cs_to (Tfunction t t0 c)) (@fold_reptype cs_to (Tfunction t t0 c) tt) *)
  destruct t; simpl in *; try congruence; try tauto; apply JMeq_refl.
Qed.

Lemma repinject_unfold_reptype: forall t v,
  match t as t' return REPTYPE t' -> Prop with
  | Tint _ _ _
  | Tfloat _ _
  | Tlong _ _
  | Tpointer _ _ => fun vv => repinject t v = vv
  | _ => fun _ => True
  end (unfold_reptype v).
Proof.
  intros; destruct t; auto;
  unfold repinject;
  unfold unfold_reptype;
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
  rewrite <- eq_rect_eq; auto.
Qed.

Lemma repinject_valinject:
  forall t v,
    type_is_by_value t = true -> repinject t (valinject t v) = v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
  destruct t; try inversion H; reflexivity.
Qed.

Lemma valinject_repinject: forall t v,
  type_is_by_value t = true ->
  (valinject t (repinject t v)) = v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
  destruct t; inversion H; reflexivity.
Qed.

Lemma repinject_default_val:
 forall t, repinject t (default_val t) = Vundef.
Proof.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
destruct t; reflexivity.
Qed.

End CENV.

Arguments reptype' {cs} t / .

Global Notation REPTYPE t :=
  match t return Type with
  | Tvoid
  | Tfunction _ _ _ => unit
  | Tint _ _ _
  | Tlong _ _
  | Tfloat _ _
  | Tpointer _ _ => val
  | Tarray t0 _ _ => list (reptype t0)
  | Tstruct id _ => reptype_structlist (co_members (get_co id))
  | Tunion id _ => reptype_unionlist (co_members (get_co id))
  end.

Tactic Notation "unfold_repinj" :=
repeat match goal with |- context [repinj ?T] =>
 let x := fresh "x" in set (x := repinj T);
    lazy beta iota zeta delta in x; subst x; lazy beta
end.

Tactic Notation "unfold_repinj" constr(T) :=
match goal with |- context [repinj T] =>
 let x := fresh "x" in set (x := repinj T);
    lazy beta iota zeta delta in x; subst x; lazy beta
end.

(* Too expensive to do "pattern (repinj T V)", this
  can blow up.
Tactic Notation "unfold_repinj" constr(T) constr(V) :=
   pattern (repinj T V);
  unfold_repinj' T.
*)

Lemma reptype_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall (t: type),
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  @reptype cs_from t = @reptype cs_to t.
Proof.
(* Goal: forall (t : type) (_ : @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) t) true), @JMeq (@reptype cs_from t) (@default_val cs_from t) (@reptype cs_to t) (@default_val cs_to t) *)
  intros t.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  type_induction t; intros.
  + rewrite !reptype_eq.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    reflexivity.
  + rewrite !reptype_eq.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    reflexivity.
  + rewrite !reptype_eq.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    reflexivity.
  + rewrite !reptype_eq.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    reflexivity.
  + rewrite !reptype_eq.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    reflexivity.
  + rewrite (@reptype_eq cs_from), (@reptype_eq cs_to).
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
    rewrite IH; auto.
  + rewrite !reptype_eq.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    reflexivity.
  + rewrite (@reptype_eq cs_from), (@reptype_eq cs_to).
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_from id))) (@union_default_val cs_from (co_members (@get_co cs_from id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    simpl in H.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
    rewrite co_members_get_co_change_composite by auto.
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_to id))) (@union_default_val cs_from (co_members (@get_co cs_to id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    apply members_spec_change_composite in H.
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_to id))) (@union_default_val cs_from (co_members (@get_co cs_to id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    cbv zeta in IH.
(* Goal: @Forall (prod ident type) (fun x : prod ident type => @JMeq (@reptype cs_from (field_type (@fst ident type x) (co_members (@get_co cs_to id)))) (@default_val cs_from (field_type (@fst ident type x) (co_members (@get_co cs_to id)))) (@reptype cs_to (field_type (@fst ident type x) (co_members (@get_co cs_to id)))) (@default_val cs_to (field_type (@fst ident type x) (co_members (@get_co cs_to id))))) (co_members (@get_co cs_to id)) *)
    revert H IH.
(* Goal: @eq Type (compact_prod (@map (prod ident type) Type (fun x : prod ident type => let (t, _) := @reptype_gen cs (field_type (@fst ident type x) m) in t) m)) (reptype_structlist m) *)
    unfold reptype_structlist.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
    generalize (co_members (get_co id)) at 1 3 4 5 7 9; intros.
(* Goal: @eq nat (Z.to_nat (Z.of_nat (@Datatypes.length (@reptype cs t) (@replist cs t lo hi al)))) (Z.to_nat (Z.sub hi lo)) *)
    f_equal.
    induction IH as [| [i t] ?].
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    - reflexivity.
    - Opaque field_type. simpl. Transparent field_type.
      inv H.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
      f_equal; auto.
  + rewrite (@reptype_eq cs_from), (@reptype_eq cs_to).
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_from id))) (@union_default_val cs_from (co_members (@get_co cs_from id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    simpl in H.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
    rewrite co_members_get_co_change_composite by auto.
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_to id))) (@union_default_val cs_from (co_members (@get_co cs_to id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    apply members_spec_change_composite in H.
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_to id))) (@union_default_val cs_from (co_members (@get_co cs_to id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    cbv zeta in IH.
(* Goal: @Forall (prod ident type) (fun x : prod ident type => @JMeq (@reptype cs_from (field_type (@fst ident type x) (co_members (@get_co cs_to id)))) (@default_val cs_from (field_type (@fst ident type x) (co_members (@get_co cs_to id)))) (@reptype cs_to (field_type (@fst ident type x) (co_members (@get_co cs_to id)))) (@default_val cs_to (field_type (@fst ident type x) (co_members (@get_co cs_to id))))) (co_members (@get_co cs_to id)) *)
    revert H IH.
(* Goal: @eq Type (compact_sum (@map (prod ident type) Type (fun x : prod ident type => let (t, _) := @reptype_gen cs (field_type (@fst ident type x) m) in t) m)) (reptype_unionlist m) *)
    unfold reptype_unionlist.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
    generalize (co_members (get_co id)) at 1 3 4 5 7 9; intros.
(* Goal: @eq nat (Z.to_nat (Z.of_nat (@Datatypes.length (@reptype cs t) (@replist cs t lo hi al)))) (Z.to_nat (Z.sub hi lo)) *)
    f_equal.
    induction IH as [| [i t] ?].
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    - reflexivity.
    - Opaque field_type. simpl. Transparent field_type.
      inv H.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
      f_equal; auto.
Qed.

Lemma default_val_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall (t: type),
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  JMeq (@default_val cs_from t) (@default_val cs_to t).
Proof.
(* Goal: forall (t : type) (_ : @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) t) true), @JMeq (@reptype cs_from t) (@default_val cs_from t) (@reptype cs_to t) (@default_val cs_to t) *)
  intros t.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  type_induction t; intros.
  + rewrite !default_val_eq.
(* Goal: @JMeq (@reptype cs_from (Tfunction t t0 c)) (@fold_reptype cs_from (Tfunction t t0 c) tt) (@reptype cs_to (Tfunction t t0 c)) (@fold_reptype cs_to (Tfunction t t0 c) tt) *)
    apply JMeq_refl.
  + rewrite !default_val_eq.
(* Goal: @JMeq (@reptype cs_from (Tfunction t t0 c)) (@fold_reptype cs_from (Tfunction t t0 c) tt) (@reptype cs_to (Tfunction t t0 c)) (@fold_reptype cs_to (Tfunction t t0 c) tt) *)
    apply JMeq_refl.
  + rewrite !default_val_eq.
(* Goal: @JMeq (@reptype cs_from (Tfunction t t0 c)) (@fold_reptype cs_from (Tfunction t t0 c) tt) (@reptype cs_to (Tfunction t t0 c)) (@fold_reptype cs_to (Tfunction t t0 c) tt) *)
    apply JMeq_refl.
  + rewrite !default_val_eq.
(* Goal: @JMeq (@reptype cs_from (Tfunction t t0 c)) (@fold_reptype cs_from (Tfunction t t0 c) tt) (@reptype cs_to (Tfunction t t0 c)) (@fold_reptype cs_to (Tfunction t t0 c) tt) *)
    apply JMeq_refl.
  + rewrite !default_val_eq.
(* Goal: @JMeq (@reptype cs_from (Tfunction t t0 c)) (@fold_reptype cs_from (Tfunction t t0 c) tt) (@reptype cs_to (Tfunction t t0 c)) (@fold_reptype cs_to (Tfunction t t0 c) tt) *)
    apply JMeq_refl.
  + rewrite (@default_val_eq cs_from), (@default_val_eq cs_to).
(* Goal: @JMeq (@reptype cs_from (Tunion id a)) (@fold_reptype cs_from (Tunion id a) (@union_default_val cs_from (co_members (@get_co cs_from id)))) (@reptype cs_to (Tunion id a)) (@fold_reptype cs_to (Tunion id a) (@union_default_val cs_to (co_members (@get_co cs_to id)))) *)
    eapply JMeq_trans; [| eapply JMeq_trans]; [apply fold_reptype_JMeq | | apply JMeq_sym, fold_reptype_JMeq].
(* Goal: @JMeq (list (@reptype cs_from t)) (@list_repeat (@reptype cs_from t) (Z.to_nat z) (@default_val cs_from t)) (list (@reptype cs_to t)) (@list_repeat (@reptype cs_to t) (Z.to_nat z) (@default_val cs_to t)) *)
    specialize (IH H).
(* Goal: @JMeq (list (@reptype cs_from t)) (@list_repeat (@reptype cs_from t) (Z.to_nat z) (@default_val cs_from t)) (list (@reptype cs_to t)) (@list_repeat (@reptype cs_to t) (Z.to_nat z) (@default_val cs_to t)) *)
    revert IH; generalize (@default_val cs_from t), (@default_val cs_to t).
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
    rewrite reptype_change_composite by auto.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
    intros.
(* Goal: @JMeq (list (@reptype cs_to t)) (@list_repeat (@reptype cs_to t) (Z.to_nat z) r) (list (@reptype cs_to t)) (@list_repeat (@reptype cs_to t) (Z.to_nat z) r0) *)
    apply JMeq_eq in IH; subst.
(* Goal: @JMeq (@reptype cs_from (Tfunction t t0 c)) (@fold_reptype cs_from (Tfunction t t0 c) tt) (@reptype cs_to (Tfunction t t0 c)) (@fold_reptype cs_to (Tfunction t t0 c) tt) *)
    apply JMeq_refl.
  + rewrite !default_val_eq.
(* Goal: @JMeq (@reptype cs_from (Tfunction t t0 c)) (@fold_reptype cs_from (Tfunction t t0 c) tt) (@reptype cs_to (Tfunction t t0 c)) (@fold_reptype cs_to (Tfunction t t0 c) tt) *)
    apply JMeq_refl.
  + rewrite (@default_val_eq cs_from), (@default_val_eq cs_to).
(* Goal: @JMeq (@reptype cs_from (Tunion id a)) (@fold_reptype cs_from (Tunion id a) (@union_default_val cs_from (co_members (@get_co cs_from id)))) (@reptype cs_to (Tunion id a)) (@fold_reptype cs_to (Tunion id a) (@union_default_val cs_to (co_members (@get_co cs_to id)))) *)
    eapply JMeq_trans; [| eapply JMeq_trans]; [apply fold_reptype_JMeq | | apply JMeq_sym, fold_reptype_JMeq].
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_from id))) (@union_default_val cs_from (co_members (@get_co cs_from id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    simpl in H.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
    rewrite co_members_get_co_change_composite by auto.
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_to id))) (@union_default_val cs_from (co_members (@get_co cs_to id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    apply members_spec_change_composite in H.
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_to id))) (@union_default_val cs_from (co_members (@get_co cs_to id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    cbv zeta in IH.
(* Goal: @JMeq (@reptype_structlist cs_from (co_members (@get_co cs_to id))) (@struct_default_val cs_from (co_members (@get_co cs_to id))) (@reptype_structlist cs_to (co_members (@get_co cs_to id))) (@struct_default_val cs_to (co_members (@get_co cs_to id))) *)
    unfold struct_default_val.
(* Goal: @JMeq (@reptype_structlist cs_from (co_members (@get_co cs_to id))) (@compact_prod_gen (prod ident type) (fun it : prod ident type => @reptype cs_from (field_type (@fst ident type it) (co_members (@get_co cs_to id)))) (fun it : prod ident type => @default_val cs_from (field_type (@fst ident type it) (co_members (@get_co cs_to id)))) (co_members (@get_co cs_to id))) (@reptype_structlist cs_to (co_members (@get_co cs_to id))) (@compact_prod_gen (prod ident type) (fun it : prod ident type => @reptype cs_to (field_type (@fst ident type it) (co_members (@get_co cs_to id)))) (fun it : prod ident type => @default_val cs_to (field_type (@fst ident type it) (co_members (@get_co cs_to id)))) (co_members (@get_co cs_to id))) *)
    apply compact_prod_gen_JMeq.
    rewrite <- Forall_forall.
(* Goal: @Forall (prod ident type) (fun x : prod ident type => @JMeq (@reptype cs_from (field_type (@fst ident type x) (co_members (@get_co cs_to id)))) (@default_val cs_from (field_type (@fst ident type x) (co_members (@get_co cs_to id)))) (@reptype cs_to (field_type (@fst ident type x) (co_members (@get_co cs_to id)))) (@default_val cs_to (field_type (@fst ident type x) (co_members (@get_co cs_to id))))) (co_members (@get_co cs_to id)) *)
    revert H IH.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
    generalize (co_members (get_co id)) at 1 3 4 5 6 7 9 10 11 12; intros.
(* Goal: @Forall (prod ident type) (fun x : prod ident type => @JMeq (@reptype cs_from (field_type (@fst ident type x) m)) (@default_val cs_from (field_type (@fst ident type x) m)) (@reptype cs_to (field_type (@fst ident type x) m)) (@default_val cs_to (field_type (@fst ident type x) m))) (co_members (@get_co cs_to id)) *)
    induction H as [| [i t] ?].
    - constructor.
    - inv IH.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
      constructor; auto.
  + rewrite (@default_val_eq cs_from), (@default_val_eq cs_to).
(* Goal: @JMeq (@reptype cs_from (Tunion id a)) (@fold_reptype cs_from (Tunion id a) (@union_default_val cs_from (co_members (@get_co cs_from id)))) (@reptype cs_to (Tunion id a)) (@fold_reptype cs_to (Tunion id a) (@union_default_val cs_to (co_members (@get_co cs_to id)))) *)
    eapply JMeq_trans; [| eapply JMeq_trans]; [apply fold_reptype_JMeq | | apply JMeq_sym, fold_reptype_JMeq].
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_from id))) (@union_default_val cs_from (co_members (@get_co cs_from id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    simpl in H.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
    rewrite co_members_get_co_change_composite by auto.
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_to id))) (@union_default_val cs_from (co_members (@get_co cs_to id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    apply members_spec_change_composite in H.
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_to id))) (@union_default_val cs_from (co_members (@get_co cs_to id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    cbv zeta in IH.
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_to id))) (@union_default_val cs_from (co_members (@get_co cs_to id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
    unfold union_default_val.
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_to id))) (@compact_sum_gen (prod ident type) (fun it : prod ident type => @reptype cs_from (field_type (@fst ident type it) (co_members (@get_co cs_to id)))) (fun _ : prod ident type => true) (fun it : prod ident type => @default_val cs_from (field_type (@fst ident type it) (co_members (@get_co cs_to id)))) (co_members (@get_co cs_to id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@compact_sum_gen (prod ident type) (fun it : prod ident type => @reptype cs_to (field_type (@fst ident type it) (co_members (@get_co cs_to id)))) (fun _ : prod ident type => true) (fun it : prod ident type => @default_val cs_to (field_type (@fst ident type it) (co_members (@get_co cs_to id)))) (co_members (@get_co cs_to id))) *)
    apply compact_sum_gen_JMeq.
    rewrite <- Forall_forall.
(* Goal: @Forall (prod ident type) (fun x : prod ident type => @JMeq (@reptype cs_from (field_type (@fst ident type x) (co_members (@get_co cs_to id)))) (@default_val cs_from (field_type (@fst ident type x) (co_members (@get_co cs_to id)))) (@reptype cs_to (field_type (@fst ident type x) (co_members (@get_co cs_to id)))) (@default_val cs_to (field_type (@fst ident type x) (co_members (@get_co cs_to id))))) (co_members (@get_co cs_to id)) *)
    revert H IH.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
    generalize (co_members (get_co id)) at 1 3 4 5 6 7 9 10 11 12; intros.
(* Goal: @Forall (prod ident type) (fun x : prod ident type => @JMeq (@reptype cs_from (field_type (@fst ident type x) m)) (@default_val cs_from (field_type (@fst ident type x) m)) (@reptype cs_to (field_type (@fst ident type x) m)) (@default_val cs_to (field_type (@fst ident type x) m))) (co_members (@get_co cs_to id)) *)
    induction H as [| [i t] ?].
    - constructor.
    - inv IH.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
      constructor; auto.
Qed.

Fixpoint force_lengthn {A} n (xs: list A) (default: A) :=
  match n, xs with
  | O, _ => nil
  | S n0, nil => default :: force_lengthn n0 nil default
  | S n0, hd :: tl => hd :: force_lengthn n0 tl default
  end.

Lemma force_lengthn_length_n: forall {A} n (xs : list A) (default: A),
  length (force_lengthn n xs default) = n.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  revert xs; induction n; intros.
  + reflexivity.
  + simpl.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    destruct xs; simpl; rewrite IHn; reflexivity.
Qed.

Lemma nth_force_lengthn_nil: forall {A} n i (default: A),
  nth i (force_lengthn n nil default) default = default.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  revert i; induction n; intros.
  + simpl. destruct i; reflexivity.
  + simpl. destruct i.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    - reflexivity.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    - rewrite IHn. reflexivity.
Qed.

Lemma nth_force_lengthn: forall {A} n i (xs : list A) (default: A),
  (0 <= i < n) %nat ->
  nth i (force_lengthn n xs default) default = nth i xs default.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  revert i H xs; induction n; intros.
  + omega.
  + simpl.
(* Goal: @eq A (@nth A i match xs with | nil => @cons A default (@force_lengthn A n (@nil A) default) | cons hd tl => @cons A hd (@force_lengthn A n tl default) end default) (@nth A i xs default) *)
    destruct xs.
    - simpl.
(* Goal: @eq A match i with | O => a | S m => @nth A m (@force_lengthn A n xs default) default end match i with | O => a | S m => @nth A m xs default end *)
      destruct i; [reflexivity |].
(* Goal: @eq A (@nth A i (@force_lengthn A n (@nil A) default) default) default *)
      apply nth_force_lengthn_nil.
    - simpl.
(* Goal: @eq A match i with | O => a | S m => @nth A m (@force_lengthn A n xs default) default end match i with | O => a | S m => @nth A m xs default end *)
      destruct i; [reflexivity |].
(* Goal: @eq (list A) (@replist' A d (Z.succ (Z.succ lo)) n (@cons A r al)) (@replist' A d (Z.succ lo) n al) *)
      apply IHn.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
      omega.
Qed.

Lemma force_lengthn_id: forall {A} n ct (d: A), length ct = n -> force_lengthn n ct d = ct.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  intros.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  revert ct H; induction n; intros.
  + destruct ct; try solve [inversion H].
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    reflexivity.
  + destruct ct; try solve [inversion H].
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) lo (S n) al)) (Z.succ (Z.of_nat n)) *)
    simpl.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
    rewrite IHn by auto.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
    reflexivity.
Qed.

(* "replist" is an alternative to zlist, avoids mysterious typeclass *)

Open Scope Z.

Fixpoint replist' {A: Type} {d: Inhabitant A} (lo: Z) (n: nat) (al: list A) :=
 match n with
 | O => nil
 | S n' =>  Znth lo al :: replist' (Z.succ lo) n' al
 end.

Definition replist {cs: compspecs} (t: type)  (lo hi: Z) (al: list (reptype t)) :=
  replist'  lo (Z.to_nat (hi-lo)) al.

(* replist t lo hi al *)

Lemma replist_replist {cs: compspecs}:
 forall t (lo hi lo' hi': Z) al,
   0 <= lo <= hi ->
   0 <= lo' <= hi' ->
   lo'+hi <= hi'  ->
 replist t lo hi (replist t lo' hi' al) =
   replist t (lo+lo') (hi+lo') al.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
intros.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist cs t lo hi al)) (Z.of_nat (Z.to_nat (Z.sub hi lo))) *)
 unfold replist.
 forget (default_val t) as d.
 replace (hi + lo' - (lo + lo')) with (hi-lo) by omega.
 remember (Z.to_nat (hi-lo)) as n.
 assert (hi = lo + Z.of_nat n).
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
  subst n. rewrite Z2Nat.id by omega. omega.
 subst hi.
 clear Heqn. destruct H as [? _].
 rewrite Z.add_assoc in H1.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) lo (S n) al)) (Z.succ (Z.of_nat n)) *)
  revert lo lo' H H0 H1; induction n; intros; simpl.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
   reflexivity.
(* Goal: @eq nat (Z.to_nat (Z.of_nat (@Datatypes.length (@reptype cs t) (@replist cs t lo hi al)))) (Z.to_nat (Z.sub hi lo)) *)
 f_equal.
+
  clear - H H0 H1. destruct H0 as [? _].
  remember (Z.to_nat (hi'-lo')) as k.
  rewrite inj_S in H1.
  replace hi' with (lo' + Z.of_nat k) in H1
    by (subst k; rewrite Z2Nat.id by omega; omega).
  clear hi' Heqk.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
  assert (lo < Z.of_nat k) by omega. clear H1.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
  revert lo lo' H H0 H2; induction k; intros. simpl in H2; omega.
  unfold replist'; fold @replist'.
  rewrite inj_S in H2.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) lo (S n) al)) (Z.succ (Z.of_nat n)) *)
  simpl.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
  assert (lo=0 \/ 0<lo) by omega.
  destruct H1. subst lo.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
  unfold Znth at 1. rewrite if_false by omega. simpl. auto.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) lo (Z.to_nat (Z.sub hi lo)) al)) (Z.of_nat (Z.to_nat (Z.sub hi lo))) *)
  clear H.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
  unfold Znth at 1. rewrite if_false by omega.
  destruct (Z.to_nat lo) eqn:?.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
  apply Z2Nat.inj_lt in H1; try omega.
  simpl nth.
  specialize (IHk (Z.of_nat n0) (Z.succ lo')).
  replace (lo+lo') with (Z.of_nat n0 + Z.succ lo').
2:{
(* Goal: @eq nat (S (Z.to_nat lo)) (Z.to_nat (Z.succ lo)) *)
(* Goal: @eq (list A) (@replist' A d (Z.succ (Z.succ lo)) n (@cons A r al)) (@replist' A d (Z.succ lo) n al) *)
  unfold Z.succ.
  transitivity (Z.of_nat n0 + 1 + lo'); [ omega |].
(* Goal: @eq nat (Z.to_nat (Z.of_nat (@Datatypes.length (@reptype cs t) (@replist cs t lo hi al)))) (Z.to_nat (Z.sub hi lo)) *)
  f_equal. apply Z2Nat.inj; try omega.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
  rewrite Z2Nat.inj_add; try omega. rewrite Nat2Z.id.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
 rewrite Heqn0. change (Z.to_nat 1) with 1%nat.  omega.
}
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
  etransitivity; [ | apply IHk]; try omega.
2:{
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
  assert (lo = Z.of_nat (S n0)).  apply Z2Nat.inj; try omega.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
  rewrite Nat2Z.id. auto.
   subst lo. clear - H2. rewrite inj_S in H2. omega.
}
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
  unfold Znth. rewrite if_false by omega. rewrite Nat2Z.id. auto.
+
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
  specialize (IHn (Z.succ lo) lo'). rewrite IHn; try omega.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
   f_equal; omega.
   rewrite inj_S in H1.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
  omega.
Qed.

Lemma replist'_succ:
 forall {A} {d:Inhabitant A} lo n r al,
   (lo>=0) -> replist' (Z.succ lo) n (r::al) = replist' lo n al.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
intros.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
revert lo al H; induction n; simpl; intros.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
auto.
(* Goal: @eq nat (Z.to_nat (Z.of_nat (@Datatypes.length (@reptype cs t) (@replist cs t lo hi al)))) (Z.to_nat (Z.sub hi lo)) *)
f_equal.
(* Goal: @eq A (@Znth A d (Z.succ lo) (@cons A r al)) (@Znth A d lo al) *)
(* Goal: @eq (list A) (@replist' A d (Z.succ (Z.succ lo)) n (@cons A r al)) (@replist' A d (Z.succ lo) n al) *)
unfold Znth.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
 do 2 rewrite if_false by omega.
(* Goal: @eq A (@nth A (Z.to_nat (Z.succ lo)) (@cons A r al) d) (@nth A (Z.to_nat lo) al d) *)
(* Goal: @eq (list A) (@replist' A d (Z.succ (Z.succ lo)) n (@cons A r al)) (@replist' A d (Z.succ lo) n al) *)
 replace (Z.to_nat (Z.succ lo)) with (S (Z.to_nat lo)).
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
 reflexivity. unfold Z.succ. rewrite Z2Nat.inj_add by omega.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
 change (Z.to_nat 1) with 1%nat; omega.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
 apply IHn. omega.
Qed.

Lemma replist_firstn_skipn {cs: compspecs}:
 forall t lo hi al,
  (lo <= hi <= length al)%nat ->
  replist t (Z.of_nat lo) (Z.of_nat hi) al = firstn (hi-lo) (skipn lo al).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
intros.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist cs t lo hi al)) (Z.of_nat (Z.to_nat (Z.sub hi lo))) *)
 unfold replist.
 rewrite <- Nat2Z.inj_sub by omega.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat lo) (Z.to_nat (Z.of_nat (Init.Nat.sub hi lo))) al) (@firstn (@reptype cs t) (Init.Nat.sub hi lo) (@skipn (@reptype cs t) lo al)) *)
 rewrite Nat2Z.id.
 assert (hi-lo <= length al - lo)%nat by omega.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) lo (Z.to_nat (Z.sub hi lo)) al)) (Z.of_nat (Z.to_nat (Z.sub hi lo))) *)
 clear H.
 forget (hi-lo)%nat as n. clear hi.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
 revert n al H0; induction lo; intros.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) lo (S n) al)) (Z.succ (Z.of_nat n)) *)
 simpl.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) Z0 n al) (@firstn (@reptype cs t) n al) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
 assert (n <= length al)%nat by omega; clear H0.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
 revert al H; induction n; simpl; intros; auto.
(* Goal: @JMeq (@reptype_unionlist cs_from (co_members (@get_co cs_from id))) (@union_default_val cs_from (co_members (@get_co cs_from id))) (@reptype_unionlist cs_to (co_members (@get_co cs_to id))) (@union_default_val cs_to (co_members (@get_co cs_to id))) *)
 destruct al; simpl in H. omega.
(* Goal: @eq nat (Z.to_nat (Z.of_nat (@Datatypes.length (@reptype cs t) (@replist cs t lo hi al)))) (Z.to_nat (Z.sub hi lo)) *)
 f_equal.
 rewrite <- (IHn al) by omega. clear IHn.
 rewrite <- (replist'_succ 0 n r al) by omega.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
 reflexivity.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) lo (S n) al)) (Z.of_nat (S n)) *)
 rewrite inj_S.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
  destruct al. simpl length in H0. assert (n=0)%nat by omega.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
  subst;   simpl. auto.
  simpl length in H0. simpl in H0. simpl. rewrite <- (IHlo _ _ H0).
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
  apply replist'_succ. omega.
Qed.

Lemma skipn_0:
 forall A (al: list A) n,
  (n=0)%nat -> skipn n al = al.
Proof.
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Zpos xH) n (@cons (@reptype cs t) r al)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.succ Z0) n (@cons (@reptype cs t) r al)) *)
(* Goal: @eq (list (@reptype cs t)) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) (Z.of_nat (S lo)) n al) (@firstn (@reptype cs t) n (@skipn (@reptype cs t) (S lo) al)) *)
intros; subst; reflexivity.
Qed.

Lemma replist_elim {cs: compspecs}:
  forall t lo hi al,
    lo = 0 -> hi = Zlength al ->
    replist t lo hi al = al.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
intros.
(* Goal: @eq (list (@reptype cs t)) (@replist cs t lo hi al) al *)
subst.
(* Goal: @eq (list (@reptype cs t)) (@replist cs t Z0 (@Zlength (@reptype cs t) al) al) al *)
change 0 with (Z.of_nat 0).
(* Goal: @eq (list (@reptype cs t)) (@replist cs t (Z.of_nat O) (@Zlength (@reptype cs t) al) al) al *)
rewrite Zlength_correct.
(* Goal: Z.ge (Z.of_nat lo) Z0 *)
rewrite replist_firstn_skipn by omega.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
rewrite skipn_0 by auto.
(* Goal: @eq (list (@reptype cs t)) (@firstn (@reptype cs t) (Init.Nat.sub (@Datatypes.length (@reptype cs t) al) O) al) al *)
rewrite NPeano.Nat.sub_0_r.
(* Goal: @eq (list (@reptype cs t)) (@firstn (@reptype cs t) (@Datatypes.length (@reptype cs t) al) al) al *)
apply firstn_exact_length.
Qed.

Lemma replist_Zlength {cs: compspecs}:
  forall t lo hi al,
    lo <= hi ->
   Zlength (replist t lo hi al) = hi-lo.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
intros.
rewrite <- (Z2Nat.id (hi-lo)) by omega.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist cs t lo hi al)) (Z.of_nat (Z.to_nat (Z.sub hi lo))) *)
unfold replist.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) lo (Z.to_nat (Z.sub hi lo)) al)) (Z.of_nat (Z.to_nat (Z.sub hi lo))) *)
clear H.
forget (Z.to_nat (hi-lo)) as n. clear hi.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
revert lo; induction n; intros.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
simpl. rewrite Zlength_nil. auto.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) lo (S n) al)) (Z.of_nat (S n)) *)
rewrite inj_S.
(* Goal: @eq Z (@Zlength (@reptype cs t) (@replist' (@reptype cs t) (@Inhabitant_reptype cs t) lo (S n) al)) (Z.succ (Z.of_nat n)) *)
simpl. rewrite Zlength_cons.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
rewrite IHn. auto.
Qed.

Lemma replist_length {cs: compspecs}:
  forall t lo hi al,
    lo <= hi ->
   length (replist t lo hi al) = Z.to_nat (hi-lo).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
intros.
rewrite <- (Nat2Z.id (length _)).
(* Goal: @eq nat (Z.to_nat (Z.of_nat (@Datatypes.length (@reptype cs t) (@replist cs t lo hi al)))) (Z.to_nat (Z.sub hi lo)) *)
f_equal.
rewrite <- Zlength_correct.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
apply replist_Zlength; auto.
Qed.


(* Hint Rewrite skipn_0 using computable : norm. *)

Lemma unfold_reptype_elim:
  forall cs t v v',
    JMeq v v' ->
   @unfold_reptype cs t v = v'.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (v' : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : @JMeq (@reptype cs t) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end v'), @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
intros.
(* Goal: @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) v' *)
unfold unfold_reptype.
(* Goal: @eq match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@eq_rect Type (@reptype cs t) (fun x : Type => x) v match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end (@reptype_eq cs t)) v' *)
match type of v' with ?t => set (t' := t) in * end.
(* Goal: @eq t' (@eq_rect Type (@reptype cs t) (fun x : Type => x) v t' (@reptype_eq cs t)) v' *)
pose proof (eq_rect_JMeq _ (reptype t) t' (fun x : Type => x) v (reptype_eq t)).
(* Goal: @eq t' (@eq_rect Type (@reptype cs t) (fun x : Type => x) v t' (@reptype_eq cs t)) v' *)
apply JMeq_eq.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.succ (Z.of_nat n)) *)
apply @JMeq_trans with (reptype t) v; auto.
Qed.


Lemma Zlength_default_val_Tarray_tuchar {cs} n a (N:0<=n): Zlength (@default_val cs (Tarray tuchar n a)) = n.
Proof. unfold default_val; simpl. rewrite Zlength_list_repeat; trivial. Qed.

