Require Import VST.floyd.base2.
Require Import VST.floyd.fieldlist.
Require Import VST.floyd.computable_theorems.
Open Scope nat.

Inductive ListType: list Type -> Type :=
  | Nil: ListType nil
  | Cons: forall {A B} (a: A) (b: ListType B), ListType (A :: B).

Fixpoint ListTypeGen {A} (F: A -> Type) (f: forall A, F A) (l: list A) : ListType (map F l) :=
  match l with
  | nil => Nil
  | cons h t => Cons (f h) (ListTypeGen F f t)
  end.

Lemma ListTypeGen_preserve: forall A F f1 f2 (l: list A),
  (forall a, In a l -> f1 a = f2 a) ->
  ListTypeGen F f1 l = ListTypeGen F f2 l.
Proof.
(* Goal: forall t : type, @eq (A t) (type_func t) match t as t0 return (A t0) with | Tvoid => F_ByValue Tvoid | Tint i s a => F_ByValue (Tint i s a) | Tlong s a => F_ByValue (Tlong s a) | Tfloat f a => F_ByValue (Tfloat f a) | Tpointer t0 a => F_ByValue (Tpointer t0 a) | Tarray t0 n a => F_Tarray t0 n a (type_func t0) | Tfunction t0 t1 c => F_ByValue (Tfunction t0 t1 c) | Tstruct id a => F_Tstruct id a (FTI_aux id) | Tunion id a => F_Tunion id a (FTI_aux id) end *)
  intros.
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
  induction l.
  + reflexivity.
  + simpl.
(* Goal: @eq (ListType (@cons Type (F a) (@map A Type F l))) (@Cons (F a) (@map A Type F l) (f1 a) (@ListTypeGen A F f1 l)) (@Cons (F a) (@map A Type F l) (f2 a) (@ListTypeGen A F f2 l)) *)
    rewrite H, IHl.
(* Goal: @eq (ListType (@map (prod ident type) Type (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (co_default Struct)))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => F_ByValue match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (co_default Struct))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A (field_type (@fst ident type it) (co_members (co_default Struct)))) (fun it : prod ident type => type_func (field_type (@fst ident type it) (co_members (co_default Struct)))) (co_members (co_default Struct))) *)
    - reflexivity.
    - intros; apply H; simpl; tauto.
    - simpl; left; auto.
Defined.

Definition decay' {X} {F: Type} {l: list X} (v: ListType (map (fun _ => F) l)): list F.
(* Goal: list F *)
  remember (map (fun _ : X => F) l) eqn:E.
(* Goal: list F *)
  revert l E.
(* Goal: forall t : type, @eq (A t) (type_func t) match t as t0 return (A t0) with | Tvoid => F_ByValue Tvoid | Tint i s a => F_ByValue (Tint i s a) | Tlong s a => F_ByValue (Tlong s a) | Tfloat f a => F_ByValue (Tfloat f a) | Tpointer t0 a => F_ByValue (Tpointer t0 a) | Tarray t0 n a => F_Tarray t0 n a (type_func t0) | Tfunction t0 t1 c => F_ByValue (Tfunction t0 t1 c) | Tstruct id a => F_Tstruct id a (FTI_aux id) | Tunion id a => F_Tunion id a (FTI_aux id) end *)
  induction v; intros.
  + exact nil.
  + destruct l; inversion E.
(* Goal: list F *)
    specialize (IHv l H1).
(* Goal: list F *)
    rewrite H0 in a.
(* Goal: list F *)
    exact (a :: IHv).
Defined.

Fixpoint decay'' {X} {F: Type} (l0 : list Type) (v: ListType l0) :
  forall (l: list X), l0 = map (fun _ => F) l -> list F :=
  match v in ListType l1
    return forall l2, l1 = map (fun _ => F) l2 -> list F
  with
  | Nil => fun _ _ => nil
  | Cons A B a b =>
    fun (l1 : list X) (E0 : A :: B = map (fun _ : X => F) l1) =>
    match l1 as l2 return (A :: B = map (fun _ : X => F) l2 -> list F) with
    | nil => fun _ => nil (* impossible case *)
    | x :: l2 =>
       fun E1 : A :: B = map (fun _ : X => F) (x :: l2) =>
       (fun
          X0 : map (fun _ : X => F) (x :: l2) =
               map (fun _ : X => F) (x :: l2) -> list F =>
        X0 eq_refl)
         match
           E1 in (_ = y)
           return (y = map (fun _ : X => F) (x :: l2) -> list F)
         with
         | eq_refl =>
             fun H0 : A :: B = map (fun _ : X => F) (x :: l2) =>
              (fun (H3 : A = F) (H4 : B = map (fun _ : X => F) l2) =>
                  (eq_rect A (fun A0 : Type => A0) a F H3) :: (decay'' B b l2 H4))
                 (f_equal
                    (fun e : list Type =>
                     match e with
                     | nil => A
                     | T :: _ => T
                     end) H0)
                (f_equal
                   (fun e : list Type =>
                    match e with
                    | nil => B
                    | _ :: l3 => l3
                    end) H0)
         end
    end E0
  end.

Definition decay {X} {F: Type} {l: list X} (v: ListType (map (fun _ => F) l)): list F :=
  let l0 := map (fun _ => F) l in
  let E := @eq_refl _ (map (fun _ => F) l) : l0 = map (fun _ => F) l in
  decay'' l0 v l E.

Lemma decay_spec: forall A F f l,
  decay (ListTypeGen (fun _: A => F) f l) = map f l.
Proof.
(* Goal: forall t : type, @eq (A t) (type_func t) match t as t0 return (A t0) with | Tvoid => F_ByValue Tvoid | Tint i s a => F_ByValue (Tint i s a) | Tlong s a => F_ByValue (Tlong s a) | Tfloat f a => F_ByValue (Tfloat f a) | Tpointer t0 a => F_ByValue (Tpointer t0 a) | Tarray t0 n a => F_Tarray t0 n a (type_func t0) | Tfunction t0 t1 c => F_ByValue (Tfunction t0 t1 c) | Tstruct id a => F_Tstruct id a (FTI_aux id) | Tunion id a => F_Tunion id a (FTI_aux id) end *)
  intros.
(* Goal: @eq (list F) (@decay A F l (@ListTypeGen A (fun _ : A => F) f l)) (@map A F f l) *)
  unfold decay.
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
  induction l.
  + simpl.
(* Goal: @eq (ListType (@map (prod ident type) Type (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (co_default Struct)))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => F_ByValue match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (co_default Struct))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A (field_type (@fst ident type it) (co_members (co_default Struct)))) (fun it : prod ident type => type_func (field_type (@fst ident type it) (co_members (co_default Struct)))) (co_members (co_default Struct))) *)
    reflexivity.
  + simpl.
(* Goal: @eq (A (Tunion id a)) (F_Tunion id a (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => F_ByValue match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id)))) (F_Tunion id a (FTI_aux id)) *)
    f_equal.
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
    auto.
Defined.

Section COMPOSITE_ENV.
Context {cs: compspecs}.

Lemma type_ind: forall P : type -> Prop,
  (forall t,
  match t with
  | Tarray t0 _ _ => P t0
  | Tstruct id _ => let m := co_members (get_co id) in Forall (fun it => P (field_type (fst it) m)) m
  | Tunion id _ => let m := co_members (get_co id) in Forall (fun it => P (field_type (fst it) m)) m
  | _ => True
  end -> P t) ->
  forall t, P t.
Proof.
(* Goal: forall (P : forall _ : type, Prop) (_ : forall (t : type) (_ : match t with | Tvoid => True | Tint i s a => True | Tlong s a => True | Tfloat f a => True | Tpointer t0 a => True | Tarray t0 z a => P t0 | Tfunction t0 t1 c => True | Tstruct id a => let m := co_members (@get_co cs id) in @Forall (prod ident type) (fun it : prod ident type => P (field_type (@fst ident type it) m)) m | Tunion id a => let m := co_members (@get_co cs id) in @Forall (prod ident type) (fun it : prod ident type => P (field_type (@fst ident type it) m)) m end), P t) (t : type), P t *)
  intros P IH_TYPE.
(* Goal: forall t : type, @eq (A t) (type_func t) match t as t0 return (A t0) with | Tvoid => F_ByValue Tvoid | Tint i s a => F_ByValue (Tint i s a) | Tlong s a => F_ByValue (Tlong s a) | Tfloat f a => F_ByValue (Tfloat f a) | Tpointer t0 a => F_ByValue (Tpointer t0 a) | Tarray t0 n a => F_Tarray t0 n a (type_func t0) | Tfunction t0 t1 c => F_ByValue (Tfunction t0 t1 c) | Tstruct id a => F_Tstruct id a (FTI_aux id) | Tunion id a => F_Tunion id a (FTI_aux id) end *)
  intros.
(* Goal: P t *)
  remember (rank_type cenv_cs t) as n eqn: RANK'.
(* Goal: P t *)
  assert (rank_type cenv_cs t <= n)%nat as RANK.
(* Goal: le (rank_type (@cenv_cs cs) t) n *)
(* Goal: P t *)
  subst. apply le_n.
(* Goal: P t *)
  clear RANK'.
(* Goal: P t *)
  revert t RANK.
  induction n;
  intros;
  specialize (IH_TYPE t); destruct t;
  try solve [specialize (IH_TYPE I); auto].
  + (* Tarray level 0 *)
(* Goal: P (Tunion i a) *)
    simpl in RANK. inv RANK.
  + (* Tstruct level 0 *)
(* Goal: P (Tunion i a) *)
    simpl in RANK.
(* Goal: P (Tunion i a) *)
    unfold get_co in IH_TYPE.
(* Goal: P (Tstruct i a) *)
    destruct (cenv_cs ! i); [inv RANK | apply IH_TYPE; simpl; constructor].
  + (* Tunion level 0 *)
(* Goal: P (Tunion i a) *)
    simpl in RANK.
(* Goal: P (Tunion i a) *)
    unfold get_co in IH_TYPE.
(* Goal: P (Tunion i a) *)
    destruct (cenv_cs ! i); [inv RANK | apply IH_TYPE].
(* Goal: @Forall (prod ident type) (fun it : prod ident type => P (field_type (@fst ident type it) (co_members (co_default Struct)))) (co_members (co_default Struct)) *)
    simpl; constructor.
  + (* Tarray level positive *)
(* Goal: P (Tunion i a) *)
    simpl in RANK.
(* Goal: P (Tarray t z a) *)
    specialize (IHn t).
(* Goal: P (Tarray t z a) *)
    apply IH_TYPE, IHn.
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
    apply le_S_n; auto.
  + (* Tstruct level positive *)
(* Goal: P (Tunion i a) *)
    simpl in RANK.
(* Goal: P (Tunion i a) *)
    pose proof get_co_members_no_replicate i.
(* Goal: P (Tunion i a) *)
    unfold get_co in *.
(* Goal: P (Tunion i a) *)
    destruct (cenv_cs ! i) as [co |] eqn:CO; [| apply IH_TYPE; simpl; constructor].
(* Goal: P (Tunion i a) *)
    apply IH_TYPE; clear IH_TYPE.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => P (field_type (@fst ident type it) (co_members co))) (co_members co) *)
    apply Forall_forall.
(* Goal: @eq (A (Tunion id a)) (type_func_rec (S n) (Tunion id a)) (type_func_rec (S n0) (Tunion id a)) *)
    intros [i0 t0] ?; simpl.
(* Goal: P match Ctypes.field_type i0 (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end *)
    apply IHn.
(* Goal: le (rank_type (@cenv_cs cs) match Ctypes.field_type i0 (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) n *)
    pose proof In_field_type _ _ H H0.
(* Goal: le (rank_type (@cenv_cs cs) match Ctypes.field_type i0 (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) n *)
    simpl in H1; rewrite H1.
(* Goal: le (rank_type (@cenv_cs cs) t0) n *)
    apply rank_type_members with (ce := cenv_cs) in H0.
    rewrite <- co_consistent_rank in H0.
(* Goal: le (rank_type (@cenv_cs cs) t0) n *)
(* Goal: composite_consistent (@cenv_cs cs) co *)
    eapply le_trans; [eassumption |].
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
    apply le_S_n; auto.
(* Goal: composite_consistent (@cenv_cs cs) co *)
    exact (cenv_consistent i co CO).
  + (* Tunion level positive *)
(* Goal: P (Tunion i a) *)
    simpl in RANK.
(* Goal: P (Tunion i a) *)
    pose proof get_co_members_no_replicate i.
(* Goal: P (Tunion i a) *)
    unfold get_co in *.
(* Goal: P (Tunion i a) *)
    destruct (cenv_cs ! i) as [co |] eqn:CO; [| apply IH_TYPE; simpl; constructor].
(* Goal: P (Tunion i a) *)
    apply IH_TYPE; clear IH_TYPE.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => P (field_type (@fst ident type it) (co_members co))) (co_members co) *)
    apply Forall_forall.
(* Goal: @eq (A (Tunion id a)) (type_func_rec (S n) (Tunion id a)) (type_func_rec (S n0) (Tunion id a)) *)
    intros [i0 t0] ?; simpl.
(* Goal: P match Ctypes.field_type i0 (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end *)
    apply IHn.
(* Goal: le (rank_type (@cenv_cs cs) match Ctypes.field_type i0 (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) n *)
    pose proof In_field_type _ _ H H0.
(* Goal: le (rank_type (@cenv_cs cs) match Ctypes.field_type i0 (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) n *)
    simpl in H1; rewrite H1.
(* Goal: le (rank_type (@cenv_cs cs) t0) n *)
    apply rank_type_members with (ce := cenv_cs) in H0.
    rewrite <- co_consistent_rank in H0.
(* Goal: le (rank_type (@cenv_cs cs) t0) n *)
(* Goal: composite_consistent (@cenv_cs cs) co *)
    eapply le_trans; [eassumption |].
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
    apply le_S_n; auto.
(* Goal: composite_consistent (@cenv_cs cs) co *)
    exact (cenv_consistent i co CO).
Defined.

Ltac type_induction t :=
  pattern t;
  match goal with
  | |- ?P t =>
    apply type_ind; clear t;
    let t := fresh "t" in
    intros t IH;
    let id := fresh "id" in
    let a := fresh "a" in
    destruct t as [| | | | | | | id a | id a]
  end.

Variable A: type -> Type.

Definition FT_aux id :=
    let m := co_members (get_co id) in
    ListType (map (fun it => A (field_type (fst it) m)) m).

Variable F_ByValue: forall t: type, A t.
Variable F_Tarray: forall t n a, A t -> A (Tarray t n a).
Variable F_Tstruct: forall id a, FT_aux id -> A (Tstruct id a).
Variable F_Tunion: forall id a, FT_aux id -> A (Tunion id a).

Fixpoint type_func_rec (n: nat) (t: type): A t :=
  match n with
  | 0 =>
    match t as t0 return A t0 with
    | Tstruct id a =>
       match cenv_cs ! id with
       | None => let m := co_members (get_co id) in
                       F_Tstruct id a (ListTypeGen (fun it => A (field_type (fst it) m)) (fun it => F_ByValue (field_type (fst it) m)) m)
       | _ => F_ByValue (Tstruct id a)
       end
    | Tunion id a =>
       match cenv_cs ! id with
       | None => let m := co_members (get_co id) in
                      F_Tunion id a (ListTypeGen (fun it => A (field_type (fst it) m)) (fun it => F_ByValue (field_type (fst it) m)) m)
       | _ => F_ByValue (Tunion id a)
       end
    | t' => F_ByValue t'
    end
  | S n' =>
    match t as t0 return A t0 with
    | Tarray t0 n a => F_Tarray t0 n a (type_func_rec n' t0)
    | Tstruct id a =>  let m := co_members (get_co id) in
                            F_Tstruct id a (ListTypeGen (fun it => A (field_type (fst it) m)) (fun it => type_func_rec n' (field_type (fst it) m)) m)
    | Tunion id a =>  let m := co_members (get_co id) in
                            F_Tunion id a (ListTypeGen (fun it => A (field_type (fst it) m)) (fun it => type_func_rec n' (field_type (fst it) m)) m)
    | t' => F_ByValue t'
    end
  end.

Definition type_func t := type_func_rec (rank_type cenv_cs t) t.

Lemma rank_type_Tstruct: forall id a co, cenv_cs ! id = Some co ->
  rank_type cenv_cs (Tstruct id a) = S (co_rank (get_co id)).
Proof.
(* Goal: forall t : type, @eq (A t) (type_func t) match t as t0 return (A t0) with | Tvoid => F_ByValue Tvoid | Tint i s a => F_ByValue (Tint i s a) | Tlong s a => F_ByValue (Tlong s a) | Tfloat f a => F_ByValue (Tfloat f a) | Tpointer t0 a => F_ByValue (Tpointer t0 a) | Tarray t0 n a => F_Tarray t0 n a (type_func t0) | Tfunction t0 t1 c => F_ByValue (Tfunction t0 t1 c) | Tstruct id a => F_Tstruct id a (FTI_aux id) | Tunion id a => F_Tunion id a (FTI_aux id) end *)
  intros.
(* Goal: @eq (A (Tunion id a)) (type_func_rec (S n) (Tunion id a)) (type_func_rec (S n0) (Tunion id a)) *)
  unfold get_co; simpl.
(* Goal: @eq nat match @PTree.get composite id (@cenv_cs cs) with | Some co => S (co_rank co) | None => O end (S (co_rank match @PTree.get composite id (@cenv_cs cs) with | Some co => co | None => co_default Struct end)) *)
  destruct (cenv_cs ! id); auto; congruence.
Defined.

Lemma rank_type_Tunion: forall id a co, cenv_cs ! id = Some co ->
  rank_type cenv_cs (Tunion id a) = S (co_rank (get_co id)).
Proof.
(* Goal: forall t : type, @eq (A t) (type_func t) match t as t0 return (A t0) with | Tvoid => F_ByValue Tvoid | Tint i s a => F_ByValue (Tint i s a) | Tlong s a => F_ByValue (Tlong s a) | Tfloat f a => F_ByValue (Tfloat f a) | Tpointer t0 a => F_ByValue (Tpointer t0 a) | Tarray t0 n a => F_Tarray t0 n a (type_func t0) | Tfunction t0 t1 c => F_ByValue (Tfunction t0 t1 c) | Tstruct id a => F_Tstruct id a (FTI_aux id) | Tunion id a => F_Tunion id a (FTI_aux id) end *)
  intros.
(* Goal: @eq (A (Tunion id a)) (type_func_rec (S n) (Tunion id a)) (type_func_rec (S n0) (Tunion id a)) *)
  unfold get_co; simpl.
(* Goal: @eq nat match @PTree.get composite id (@cenv_cs cs) with | Some co => S (co_rank co) | None => O end (S (co_rank match @PTree.get composite id (@cenv_cs cs) with | Some co => co | None => co_default Struct end)) *)
  destruct (cenv_cs ! id); auto; congruence.
Defined.

Lemma type_func_rec_rank_irrelevent: forall t n n0,
  n >= rank_type cenv_cs t ->
  n0 >= rank_type cenv_cs t ->
  type_func_rec n t = type_func_rec n0 t.
Proof.
 (* DON'T USE omega IN THIS PROOF!
   We want the proof to compute reasonably efficiently.
*)
(* Goal: forall (t : type) (n n0 : nat) (_ : ge n (rank_type (@cenv_cs cs) t)) (_ : ge n0 (rank_type (@cenv_cs cs) t)), @eq (A t) (type_func_rec n t) (type_func_rec n0 t) *)
  intros t.
  type_induction t;
  intros;
  try solve [destruct n; simpl; auto; destruct n0; simpl; auto].
  + (* Tarray *)
(* Goal: @eq (A (Tunion id a)) (type_func_rec n (Tunion id a)) (type_func_rec n0 (Tunion id a)) *)
    destruct n; simpl in H; try solve [inv H].
(* Goal: @eq (A (Tunion id a)) (type_func_rec (S n) (Tunion id a)) (type_func_rec n0 (Tunion id a)) *)
    destruct n0; simpl in H; try solve [inv H0].
(* Goal: @eq (A (Tunion id a)) (type_func_rec (S n) (Tunion id a)) (type_func_rec (S n0) (Tunion id a)) *)
    simpl. f_equal.
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
    apply IH; apply le_S_n; auto.
  + (* Tstruct *)
(* Goal: @eq (A (Tunion id a)) (type_func_rec n (Tunion id a)) (type_func_rec n0 (Tunion id a)) *)
    destruct (cenv_cs ! id) as [co |] eqn: CO.
    - erewrite rank_type_Tstruct in H by eauto.
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
      erewrite rank_type_Tstruct in H0 by eauto.
(* Goal: @eq (A (Tunion id a)) (type_func_rec n (Tunion id a)) (type_func_rec n0 (Tunion id a)) *)
      clear co CO.
(* Goal: @eq (A (Tunion id a)) (type_func_rec n (Tunion id a)) (type_func_rec n0 (Tunion id a)) *)
    destruct n; simpl in H; try solve [inv H].
(* Goal: @eq (A (Tunion id a)) (type_func_rec (S n) (Tunion id a)) (type_func_rec n0 (Tunion id a)) *)
    destruct n0; simpl in H; try solve [inv H0].
(* Goal: @eq (A (Tunion id a)) (type_func_rec (S n) (Tunion id a)) (type_func_rec (S n0) (Tunion id a)) *)
      simpl.
(* Goal: @eq (A (Tunion id a)) (F_Tunion id a (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => F_ByValue match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id)))) (F_Tunion id a (FTI_aux id)) *)
      f_equal.
(* Goal: @eq (ListType (@map (prod ident type) Type (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id)))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => type_func_rec n match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => type_func_rec n0 match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id))) *)
      apply ListTypeGen_preserve.
(* Goal: forall (a : prod ident type) (_ : @In (prod ident type) a (co_members (@get_co cs id))), @eq (A match Ctypes.field_type (@fst ident type a) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type a) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type a) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      intros [i t] Hin.
(* Goal: @eq (A match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      simpl in IH.
(* Goal: @eq (A (field_type (@fst ident type (@pair ident type i t)) (co_members co))) (type_func_rec (co_rank co) match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
      generalize (Forall_forall1 _ _ IH); clear IH; intro IH.
(* Goal: @eq (A match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      specialize (IH (i, t) Hin n n0).
(* Goal: @eq (A match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      apply le_S_n in H; apply le_S_n in H0.
(* Goal: @eq (A match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      assert (H3 := rank_type_members cenv_cs i t _ Hin).
(* Goal: @eq (A match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      pose proof get_co_members_no_replicate id.
(* Goal: @eq (A match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      pose proof In_field_type (i, t) _ H1 Hin.
      rewrite <- (co_consistent_rank cenv_cs (get_co id) (get_co_consistent _)) in H3.
(* Goal: @eq (A match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      unfold field_type in H2.
      apply IH;
       (eapply le_trans; [ | eassumption]; rewrite H2; auto).
    - destruct n, n0; simpl;  unfold FT_aux in *;
      generalize (F_Tstruct id a) as FF; unfold get_co;
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
      rewrite CO; intros; auto.
  + (* Tunion *)
(* Goal: @eq (A (Tunion id a)) (type_func_rec n (Tunion id a)) (type_func_rec n0 (Tunion id a)) *)
    destruct (cenv_cs ! id) as [co |] eqn: CO.
    - erewrite rank_type_Tunion in H by eauto.
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
      erewrite rank_type_Tunion in H0 by eauto.
(* Goal: @eq (A (Tunion id a)) (type_func_rec n (Tunion id a)) (type_func_rec n0 (Tunion id a)) *)
      clear co CO.
(* Goal: @eq (A (Tunion id a)) (type_func_rec n (Tunion id a)) (type_func_rec n0 (Tunion id a)) *)
    destruct n; simpl in H; try solve [inv H].
(* Goal: @eq (A (Tunion id a)) (type_func_rec (S n) (Tunion id a)) (type_func_rec n0 (Tunion id a)) *)
    destruct n0; simpl in H; try solve [inv H0].
(* Goal: @eq (A (Tunion id a)) (type_func_rec (S n) (Tunion id a)) (type_func_rec (S n0) (Tunion id a)) *)
      simpl.
(* Goal: @eq (A (Tunion id a)) (F_Tunion id a (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => F_ByValue match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id)))) (F_Tunion id a (FTI_aux id)) *)
      f_equal.
(* Goal: @eq (ListType (@map (prod ident type) Type (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id)))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => type_func_rec n match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => type_func_rec n0 match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id))) *)
      apply ListTypeGen_preserve.
(* Goal: forall (a : prod ident type) (_ : @In (prod ident type) a (co_members (@get_co cs id))), @eq (A match Ctypes.field_type (@fst ident type a) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type a) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type a) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      intros [i t] Hin.
(* Goal: @eq (A (field_type (@fst ident type (@pair ident type i t)) (co_members co))) (type_func_rec (co_rank co) match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
      generalize (Forall_forall1 _ _ IH); clear IH; intro IH.
(* Goal: @eq (A match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      specialize (IH (i, t) Hin n n0).
(* Goal: @eq (A match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      apply le_S_n in H; apply le_S_n in H0.
(* Goal: @eq (A match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      assert (H3 := rank_type_members cenv_cs i t _ Hin).
(* Goal: @eq (A match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      pose proof get_co_members_no_replicate id.
(* Goal: @eq (A match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func_rec n0 match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      pose proof In_field_type (i, t) _ H1 Hin.
      rewrite <- (co_consistent_rank cenv_cs (get_co id) (get_co_consistent _)) in H3.
      apply IH;
       (eapply le_trans; [ | eassumption]; rewrite H2; auto).
    - destruct n, n0; simpl;  unfold FT_aux in *;
      generalize (F_Tunion id a) as FF; unfold get_co;
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
      rewrite CO; intros; auto.
Defined.

Definition FTI_aux id :=
    let m := co_members (get_co id) in
    (ListTypeGen (fun it => A (field_type (fst it) m)) (fun it => type_func (field_type (fst it) m)) m).


Lemma type_func_eq: forall t,
  type_func t =
  match t as t0 return A t0 with
  | Tarray t0 n a => F_Tarray t0 n a (type_func t0)
  | Tstruct id a => F_Tstruct id a (FTI_aux id)
  | Tunion id a => F_Tunion id a (FTI_aux id)
  | t' => F_ByValue t'
  end.
Proof.
(* Goal: forall t : type, @eq (A t) (type_func t) match t as t0 return (A t0) with | Tvoid => F_ByValue Tvoid | Tint i s a => F_ByValue (Tint i s a) | Tlong s a => F_ByValue (Tlong s a) | Tfloat f a => F_ByValue (Tfloat f a) | Tpointer t0 a => F_ByValue (Tpointer t0 a) | Tarray t0 n a => F_Tarray t0 n a (type_func t0) | Tfunction t0 t1 c => F_ByValue (Tfunction t0 t1 c) | Tstruct id a => F_Tstruct id a (FTI_aux id) | Tunion id a => F_Tunion id a (FTI_aux id) end *)
  intros.
(* Goal: @eq (ListType (@map (prod ident type) Type (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (co_default Struct)))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => F_ByValue match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (co_default Struct))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A (field_type (@fst ident type it) (co_members (co_default Struct)))) (fun it : prod ident type => type_func (field_type (@fst ident type it) (co_members (co_default Struct)))) (co_members (co_default Struct))) *)
  type_induction t; try reflexivity.
  + (* Tstruct *)
(* Goal: @eq (A (Tunion id a)) (type_func (Tunion id a)) (F_Tunion id a (FTI_aux id)) *)
    unfold type_func in *.
(* Goal: @eq (A (Tunion id a)) (type_func_rec (rank_type (@cenv_cs cs) (Tunion id a)) (Tunion id a)) (F_Tunion id a (FTI_aux id)) *)
    simpl type_func_rec.
(* Goal: @eq (A (Tunion id a)) (type_func_rec (S n) (Tunion id a)) (type_func_rec (S n0) (Tunion id a)) *)
    destruct (cenv_cs ! id) as [co |] eqn:CO; simpl.
    - f_equal.
(* Goal: @eq (ListType (@map (prod ident type) Type (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id)))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => type_func_rec (co_rank co) match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id))) (FTI_aux id) *)
      apply ListTypeGen_preserve; intros [i t].
(* Goal: forall _ : @In (prod ident type) (@pair ident type i t) (co_members (@get_co cs id)), @eq (A (field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)))) (type_func_rec (co_rank co) match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func (field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)))) *)
      unfold get_co; rewrite CO.
(* Goal: forall _ : @In (prod ident type) (@pair ident type i t) (co_members co), @eq (A (field_type (@fst ident type (@pair ident type i t)) (co_members co))) (type_func_rec (co_rank co) match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
      intro Hin.
(* Goal: @eq (A (field_type (@fst ident type (@pair ident type i t)) (co_members co))) (type_func_rec (co_rank co) match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
      generalize (Forall_forall1 _ _ IH); clear IH; intro IH.
(* Goal: @eq (A (field_type (@fst ident type (@pair ident type i t)) (co_members co))) (type_func_rec (co_rank co) match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
      apply type_func_rec_rank_irrelevent.
      * assert (H0 := get_co_members_no_replicate id).
(* Goal: ge (co_rank co) (rank_type (@cenv_cs cs) (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
        unfold get_co in H0; rewrite CO in H0.
(* Goal: ge (co_rank co) (rank_type (@cenv_cs cs) (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
        rewrite (In_field_type _ _ H0 Hin).
        rewrite (co_consistent_rank cenv_cs _
                           (cenv_consistent id co CO)).
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
        eapply rank_type_members; eauto.
(* Goal: ge (rank_type (@cenv_cs cs) (field_type (@fst ident type (@pair ident type i t)) (co_members co))) (rank_type (@cenv_cs cs) (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
      * apply le_n.
    - rewrite CO.
(* Goal: @eq (A (Tunion id a)) (F_Tunion id a (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => F_ByValue match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id)))) (F_Tunion id a (FTI_aux id)) *)
      f_equal.
(* Goal: @eq (A (Tunion id a)) match @PTree.get composite id (@cenv_cs cs) with | Some c => F_ByValue (Tunion id a) | None => F_Tunion id a (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => F_ByValue match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id))) end (F_Tunion id a (FTI_aux id)) *)
      unfold FTI_aux, get_co; rewrite CO.
(* Goal: @eq (ListType (@map (prod ident type) Type (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (co_default Struct)))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => F_ByValue match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (co_default Struct))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A (field_type (@fst ident type it) (co_members (co_default Struct)))) (fun it : prod ident type => type_func (field_type (@fst ident type it) (co_members (co_default Struct)))) (co_members (co_default Struct))) *)
      reflexivity.
  + (* Tunion *)
(* Goal: @eq (A (Tunion id a)) (type_func (Tunion id a)) (F_Tunion id a (FTI_aux id)) *)
    unfold type_func in *.
(* Goal: @eq (A (Tunion id a)) (type_func_rec (rank_type (@cenv_cs cs) (Tunion id a)) (Tunion id a)) (F_Tunion id a (FTI_aux id)) *)
    simpl type_func_rec.
(* Goal: @eq (A (Tunion id a)) (type_func_rec (S n) (Tunion id a)) (type_func_rec (S n0) (Tunion id a)) *)
    destruct (cenv_cs ! id) as [co |] eqn:CO; simpl.
    - f_equal.
(* Goal: @eq (ListType (@map (prod ident type) Type (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id)))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => type_func_rec (co_rank co) match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id))) (FTI_aux id) *)
      apply ListTypeGen_preserve; intros [i t].
(* Goal: forall _ : @In (prod ident type) (@pair ident type i t) (co_members (@get_co cs id)), @eq (A (field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)))) (type_func_rec (co_rank co) match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func (field_type (@fst ident type (@pair ident type i t)) (co_members (@get_co cs id)))) *)
      unfold get_co; rewrite CO.
(* Goal: forall _ : @In (prod ident type) (@pair ident type i t) (co_members co), @eq (A (field_type (@fst ident type (@pair ident type i t)) (co_members co))) (type_func_rec (co_rank co) match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
      intro Hin.
(* Goal: @eq (A (field_type (@fst ident type (@pair ident type i t)) (co_members co))) (type_func_rec (co_rank co) match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
      generalize (Forall_forall1 _ _ IH); clear IH; intro IH.
(* Goal: @eq (A (field_type (@fst ident type (@pair ident type i t)) (co_members co))) (type_func_rec (co_rank co) match Ctypes.field_type (@fst ident type (@pair ident type i t)) (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) (type_func (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
      apply type_func_rec_rank_irrelevent.
      * assert (H0 := get_co_members_no_replicate id).
(* Goal: ge (co_rank co) (rank_type (@cenv_cs cs) (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
        unfold get_co in H0; rewrite CO in H0.
(* Goal: ge (co_rank co) (rank_type (@cenv_cs cs) (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
        rewrite (In_field_type _ _ H0 Hin).
        rewrite (co_consistent_rank cenv_cs _
                           (cenv_consistent id co CO)).
(* Goal: @eq (list F) (@decay'' A F (@map A Type (fun _ : A => F) l) (@ListTypeGen A (fun _ : A => F) f l) l (@eq_refl (list Type) (@map A Type (fun _ : A => F) l))) (@map A F f l) *)
        eapply rank_type_members; eauto.
(* Goal: ge (rank_type (@cenv_cs cs) (field_type (@fst ident type (@pair ident type i t)) (co_members co))) (rank_type (@cenv_cs cs) (field_type (@fst ident type (@pair ident type i t)) (co_members co))) *)
      * apply le_n.
    - rewrite CO.
(* Goal: @eq (A (Tunion id a)) (F_Tunion id a (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => F_ByValue match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id)))) (F_Tunion id a (FTI_aux id)) *)
      f_equal.
(* Goal: @eq (A (Tunion id a)) match @PTree.get composite id (@cenv_cs cs) with | Some c => F_ByValue (Tunion id a) | None => F_Tunion id a (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => F_ByValue match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (@get_co cs id))) end (F_Tunion id a (FTI_aux id)) *)
      unfold FTI_aux, get_co; rewrite CO.
(* Goal: @eq (ListType (@map (prod ident type) Type (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (co_default Struct)))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => F_ByValue match Ctypes.field_type (@fst ident type it) (co_members (co_default Struct)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (co_members (co_default Struct))) (@ListTypeGen (prod ident type) (fun it : prod ident type => A (field_type (@fst ident type it) (co_members (co_default Struct)))) (fun it : prod ident type => type_func (field_type (@fst ident type it) (co_members (co_default Struct)))) (co_members (co_default Struct))) *)
      reflexivity.
Defined.

End COMPOSITE_ENV.

Arguments type_func {cs} A F_ByValue F_Tarray F_Tstruct F_Tunion t / .

Ltac type_induction t :=
  pattern t;
  match goal with
  | |- ?P t =>
    apply type_ind; clear t;
    let t := fresh "t" in
    intros t IH;
    let id := fresh "id" in
    let a := fresh "a" in
    destruct t as [| | | | | | | id a | id a]
  end.
