Require Import VST.floyd.base2.
Require Import VST.floyd.client_lemmas.

Arguments align !n !amount / .
Arguments Z.max !n !m / .

Definition field_type i m :=
  match Ctypes.field_type i m with
  | Errors.OK t => t
  | _ => Tvoid
  end.

Definition field_offset env i m :=
  match Ctypes.field_offset env i m with
  | Errors.OK ofs => ofs
  | _ => 0
  end.

Fixpoint field_offset_next_rec env i m ofs sz :=
  match m with
  | nil => 0
  | (i0, t0) :: m0 =>
    match m0 with
    | nil => sz
    | (_, t1) :: _ =>
      if ident_eq i i0
      then align (ofs + @sizeof env t0) (@alignof env t1)
      else field_offset_next_rec env i m0 (align (ofs + @sizeof env t0) (@alignof env t1)) sz
    end
  end.

Definition field_offset_next env i m sz := field_offset_next_rec env i m 0 sz.

Lemma in_members_field_type: forall i m,
  in_members i m ->
  In (i, field_type i m) m.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (field_type i (co_members (@get_co cs_to id)))) true *)
  unfold field_type.
(* Goal: @eq type match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end Tvoid *)
  induction m as [|[i0 t0] m].
  + inversion H.
  + unfold in_members in H; simpl in H.
(* Goal: @eq type match (if ident_eq i0 i then @Errors.OK type t else Ctypes.field_type i0 m) with | Errors.OK t => t | Errors.Error e => Tvoid end t0 *)
    destruct (ident_eq i0 i).
    - subst.
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) *)
      simpl.
(* Goal: @eq Z (@sizeof env match (if ident_eq i i0 then @Errors.OK type t0 else Ctypes.field_type i m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
      if_tac; [| congruence].
(* Goal: or (@eq (prod ident type) (@pair ident type i t0) (@pair ident type i t0)) (@In (prod ident type) (@pair ident type i t0) m) *)
      left. auto.
    - simpl.
(* Goal: or (@eq (prod ident type) (@pair ident type i0 t0) (@pair ident type i match (if ident_eq i i0 then @Errors.OK type t0 else Ctypes.field_type i m) with | Errors.OK t => t | Errors.Error e => Tvoid end)) (@In (prod ident type) (@pair ident type i match (if ident_eq i i0 then @Errors.OK type t0 else Ctypes.field_type i m) with | Errors.OK t => t | Errors.Error e => Tvoid end) m) *)
      right.
(* Goal: @In (prod ident type) (@pair ident type i match (if ident_eq i i0 then @Errors.OK type t0 else Ctypes.field_type i m) with | Errors.OK t => t | Errors.Error e => Tvoid end) m *)
      destruct H; [congruence |].
(* Goal: Z.le (@sizeof (@cenv_cs cs) match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end) (Z.max (@sizeof (@cenv_cs cs) t0) (sizeof_union (@cenv_cs cs) m)) *)
      specialize (IHm H).
(* Goal: @eq Z (@sizeof env match (if ident_eq i i0 then @Errors.OK type t0 else Ctypes.field_type i m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
      if_tac; [congruence |].
(* Goal: @In (prod ident type) (@pair ident type i match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end) m *)
      exact IHm.
Qed.

Lemma field_offset_field_type_match: forall cenv i m,
  match Ctypes.field_offset cenv i m, Ctypes.field_type i m with
  | Errors.OK _, Errors.OK _ => True
  | Errors.Error _, Errors.Error _ => True
  | _, _ => False
  end.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: match Ctypes.field_offset cenv i m with | Errors.OK z => match Ctypes.field_type i m with | Errors.OK t => True | Errors.Error e => False end | Errors.Error e => match Ctypes.field_type i m with | Errors.OK t => False | Errors.Error e0 => True end end *)
  unfold Ctypes.field_offset.
(* Goal: match field_offset_rec cenv i m Z0 with | Errors.OK z => match Ctypes.field_type i m with | Errors.OK t => True | Errors.Error e => False end | Errors.Error e => match Ctypes.field_type i m with | Errors.OK t => False | Errors.Error e0 => True end end *)
  remember 0 as pos; clear Heqpos.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  revert pos; induction m as [| [? ?] ?]; intros.
  + simpl. auto.
  + simpl. destruct (ident_eq i i0) eqn:HH.
    - auto.
    - apply IHm.
Defined.

Lemma field_type_in_members: forall i m,
  match Ctypes.field_type i m with
  | Errors.Error _ => ~ in_members i m
  | _ => in_members i m
  end.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: match Ctypes.field_type i m with | Errors.OK t => in_members i m | Errors.Error e => not (in_members i m) end *)
  unfold in_members.
(* Goal: @eq type match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end Tvoid *)
  induction m as [| [i0 t0] m].
  + simpl; tauto.
  + simpl.
(* Goal: @eq Z (@sizeof env match Ctypes.field_type i (@cons (prod ident type) (@pair ident type i0 t0) m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
    destruct (ident_eq i i0).
    - left; subst; auto.
    - destruct (Ctypes.field_type i m).
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      * right; auto.
      * intro HH; destruct HH; [congruence | tauto].
Qed.

Section COMPOSITE_ENV.
Context {cs: compspecs}.

Ltac solve_field_offset_type i m :=
  let H := fresh "H" in
  let Hty := fresh "H" in
  let Hofs := fresh "H" in
  let t := fresh "t" in
  let ofs := fresh "ofs" in
  pose proof field_offset_field_type_match cenv_cs i m;
  destruct (Ctypes.field_offset cenv_cs i m) as [ofs|?] eqn:Hofs, (Ctypes.field_type i m) as [t|?] eqn:Hty;
    [clear H | inversion H | inversion H | clear H].

Lemma complete_legal_cosu_member: forall (cenv : composite_env) (id : ident) (t : type) (m : list (ident * type)),
  In (id, t) m -> @composite_complete_legal_cosu_type cenv m = true -> @complete_legal_cosu_type cenv t = true.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq bool (@complete_legal_cosu_type cenv t) true *)
  induction m as [| [i0 t0] ?].
  + inv H.
  + destruct H.
    - inv H.
(* Goal: @eq type t t0 *)
      simpl in H0.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      rewrite andb_true_iff in H0; tauto.
    - apply IHm; auto.
(* Goal: @eq type t t0 *)
      simpl in H0.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      rewrite andb_true_iff in H0; tauto.
Qed.         

Lemma complete_legal_cosu_type_field_type: forall id i,
  in_members i (co_members (get_co id)) ->
  complete_legal_cosu_type (field_type i (co_members (get_co id))) = true.
Proof.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
  unfold get_co.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: align_compatible_rec (@cenv_cs cs) (field_type i (co_members match @PTree.get composite id (@cenv_cs cs) with | Some co => co | None => co_default Struct end)) ofs *)
  destruct (cenv_cs ! id) as [co |] eqn:CO.
  + apply in_members_field_type in H.
(* Goal: @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (field_type i (co_members co))) true *)
    pose proof cenv_legal_su _ _ CO.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
    eapply complete_legal_cosu_member; eauto.
  + inversion H.
Qed.

Lemma align_compatible_rec_Tstruct_inv': forall id a ofs,
  align_compatible_rec cenv_cs (Tstruct id a) ofs ->
  forall i,
  in_members i (co_members (get_co id)) ->
  align_compatible_rec cenv_cs (field_type i (co_members (get_co id)))
    (ofs + field_offset cenv_cs i (co_members (get_co id))).
Proof.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
  unfold get_co.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: align_compatible_rec (@cenv_cs cs) (field_type i (co_members match @PTree.get composite id (@cenv_cs cs) with | Some co => co | None => co_default Struct end)) ofs *)
  destruct (cenv_cs ! id) as [co |] eqn:CO.
  + eapply align_compatible_rec_Tstruct_inv with (i0 := i); try eassumption.
(* Goal: @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (field_type i (co_members (@get_co cs_to id)))) true *)
    - unfold field_type.
(* Goal: @eq (Errors.res type) (Ctypes.field_type i (co_members co)) (@Errors.OK type match Ctypes.field_type i (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
      induction (co_members co) as [| [i0 t0] ?].
      * inv H0.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      * simpl; if_tac; auto.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
        apply IHm.
(* Goal: in_members i m *)
        destruct H0; [simpl in H0; congruence | auto].
    - unfold field_offset, Ctypes.field_offset.
(* Goal: @eq (Errors.res Z) (field_offset_rec (@cenv_cs cs) i (co_members co) Z0) (@Errors.OK Z match field_offset_rec (@cenv_cs cs) i (co_members co) Z0 with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) *)
      generalize 0 at 1 2.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
      induction (co_members co) as [| [i0 t0] ?]; intros.
      * inv H0.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      * simpl; if_tac; auto.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
        apply IHm.
(* Goal: in_members i m *)
        destruct H0; [simpl in H0; congruence | auto].
  + inv H0.
Qed.

Lemma align_compatible_rec_Tunion_inv': forall id a ofs,
  align_compatible_rec cenv_cs (Tunion id a) ofs ->
  forall i,
  in_members i (co_members (get_co id)) ->
  align_compatible_rec cenv_cs (field_type i (co_members (get_co id))) ofs.
Proof.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
  unfold get_co.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: align_compatible_rec (@cenv_cs cs) (field_type i (co_members match @PTree.get composite id (@cenv_cs cs) with | Some co => co | None => co_default Struct end)) ofs *)
  destruct (cenv_cs ! id) as [co |] eqn:CO.
  + eapply align_compatible_rec_Tunion_inv with (i0 := i); try eassumption.
(* Goal: @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (field_type i (co_members (@get_co cs_to id)))) true *)
    unfold field_type.
(* Goal: @eq (Errors.res type) (Ctypes.field_type i (co_members co)) (@Errors.OK type match Ctypes.field_type i (co_members co) with | Errors.OK t => t | Errors.Error e => Tvoid end) *)
    induction (co_members co) as [| [i0 t0] ?].
    - inv H0.
    - simpl; if_tac; auto.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      apply IHm.
(* Goal: in_members i m *)
      destruct H0; [simpl in H0; congruence | auto].
  + inv H0.
Qed.

Lemma field_offset_aligned: forall i m,
  (alignof (field_type i m) | field_offset cenv_cs i m).
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: Z.divide (@alignof (@cenv_cs cs) (field_type i m)) (field_offset (@cenv_cs cs) i m) *)
  unfold field_type, field_offset.
(* Goal: and (Z.le Z0 match Ctypes.field_offset (@cenv_cs cs) i m with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) (Z.le (Z.add match Ctypes.field_offset (@cenv_cs cs) i m with | Errors.OK ofs => ofs | Errors.Error e => Z0 end (@sizeof (@cenv_cs cs) match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end)) (sizeof_struct (@cenv_cs cs) Z0 m)) *)
  solve_field_offset_type i m.
  + eapply field_offset_aligned; eauto.
  + apply Z.divide_0_r.
Qed.

Lemma alignof_composite_hd_divide: forall i t m, (alignof t | alignof_composite cenv_cs ((i, t) :: m)).
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: Z.divide (@alignof (@cenv_cs cs) t) (alignof_composite (@cenv_cs cs) (@cons (prod ident type) (@pair ident type i t) m)) *)
  destruct (alignof_two_p t) as [N ?].
(* Goal: Z.divide (alignof_composite (@cenv_cs cs) m) (alignof_composite (@cenv_cs cs) (@cons (prod ident type) (@pair ident type i t) m)) *)
  destruct (alignof_composite_two_p cenv_cs ((i, t) :: m)) as [M ?].
(* Goal: Z.divide (@alignof (@cenv_cs cs) t) (alignof_composite (@cenv_cs cs) (@cons (prod ident type) (@pair ident type i t) m)) *)
  assert (alignof t <= alignof_composite cenv_cs ((i,t)::m)) by (apply Z.le_max_l).
  rewrite H in *.
  rewrite H0 in *.
(* Goal: Z.divide (two_power_nat N) (two_power_nat M) *)
  exact (power_nat_divide N M H1).
Qed.

Lemma alignof_composite_tl_divide: forall i t m, (alignof_composite cenv_cs m | alignof_composite cenv_cs ((i, t) :: m)).
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: Z.divide (alignof_composite (@cenv_cs cs) m) (alignof_composite (@cenv_cs cs) (@cons (prod ident type) (@pair ident type i t) m)) *)
  destruct (alignof_composite_two_p cenv_cs m) as [N ?].
(* Goal: Z.divide (alignof_composite (@cenv_cs cs) m) (alignof_composite (@cenv_cs cs) (@cons (prod ident type) (@pair ident type i t) m)) *)
  destruct (alignof_composite_two_p cenv_cs ((i, t) :: m)) as [M ?].
(* Goal: Z.divide (alignof_composite (@cenv_cs cs) m) (alignof_composite (@cenv_cs cs) (@cons (prod ident type) (@pair ident type i t) m)) *)
  assert (alignof_composite cenv_cs m <= alignof_composite cenv_cs ((i, t) :: m)) by (apply Z.le_max_r).
  rewrite H in *.
  rewrite H0 in *.
(* Goal: Z.divide (two_power_nat N) (two_power_nat M) *)
  exact (power_nat_divide N M H1).
Qed.

Lemma alignof_field_type_divide_alignof: forall i m,
  in_members i m ->
  (alignof (field_type i m) | alignof_composite cenv_cs m).
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (field_type i (co_members (@get_co cs_to id)))) true *)
  unfold field_type.
(* Goal: @eq type match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end Tvoid *)
  induction m as [| [i0 t0] m].
  + inversion H.
  + unfold in_members in H; simpl in H.
    simpl Ctypes.field_type.
(* Goal: @eq Z match (if ident_eq i i0 then @Errors.OK Z (align z (@alignof (@cenv_cs cs_from) t0)) else field_offset_rec (@cenv_cs cs_from) i m (Z.add (align z (@alignof (@cenv_cs cs_from) t0)) (@sizeof (@cenv_cs cs_from) t0))) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match (if ident_eq i i0 then @Errors.OK Z (align z (@alignof (@cenv_cs cs_to) t0)) else field_offset_rec (@cenv_cs cs_to) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0))) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
    if_tac.
    - apply alignof_composite_hd_divide.
    - eapply Z.divide_trans.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      * apply IHm.
        destruct H; [congruence | auto].
      * apply alignof_composite_tl_divide.
Qed.

(* if sizeof Tvoid = 0, this lemma can be nicer. *)
Lemma field_offset_in_range: forall i m,
  in_members i m ->
  0 <= field_offset cenv_cs i m /\ field_offset cenv_cs i m + sizeof (field_type i m) <= sizeof_struct cenv_cs 0 m.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: or (Z.le (Z.add (field_offset (@cenv_cs cs) i1 m) (@sizeof (@cenv_cs cs) (field_type i1 m))) (field_offset (@cenv_cs cs) i2 m)) (Z.le (Z.add (field_offset (@cenv_cs cs) i2 m) (@sizeof (@cenv_cs cs) (field_type i2 m))) (field_offset (@cenv_cs cs) i1 m)) *)
  unfold field_offset, field_type.
(* Goal: and (Z.le Z0 match Ctypes.field_offset (@cenv_cs cs) i m with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) (Z.le (Z.add match Ctypes.field_offset (@cenv_cs cs) i m with | Errors.OK ofs => ofs | Errors.Error e => Z0 end (@sizeof (@cenv_cs cs) match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end)) (sizeof_struct (@cenv_cs cs) Z0 m)) *)
  solve_field_offset_type i m.
  + eapply field_offset_in_range; eauto.
  + pose proof field_type_in_members i m.
(* Goal: and (Z.le Z0 Z0) (Z.le (Z.add Z0 (@sizeof (@cenv_cs cs) Tvoid)) (sizeof_struct (@cenv_cs cs) Z0 m)) *)
    rewrite H1 in H0.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
    tauto.
Qed.

(* if sizeof Tvoid = 0, this lemma can be nicer. *)
Lemma sizeof_union_in_members: forall i m,
  in_members i m ->
  sizeof (field_type i m) <= sizeof_union cenv_cs m.
(* field_offset2_in_range union's version *)
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: Z.le (@sizeof (@cenv_cs cs) (field_type i m)) (sizeof_union (@cenv_cs cs) m) *)
  unfold in_members in H.
(* Goal: @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (field_type i (co_members (@get_co cs_to id)))) true *)
  unfold field_type.
(* Goal: @eq type match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end Tvoid *)
  induction m as [|[i0 t0] m].
  + inversion H.
  + simpl.
(* Goal: @eq Z (@sizeof env match Ctypes.field_type i (@cons (prod ident type) (@pair ident type i0 t0) m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
    destruct (ident_eq i i0).
    - apply Z.le_max_l.
    - simpl in H; destruct H; [congruence |].
(* Goal: Z.le (@sizeof (@cenv_cs cs) match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end) (Z.max (@sizeof (@cenv_cs cs) t0) (sizeof_union (@cenv_cs cs) m)) *)
     specialize (IHm H).
(* Goal: Z.le (@sizeof (@cenv_cs cs) match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end) (Z.max (@sizeof (@cenv_cs cs) t0) (sizeof_union (@cenv_cs cs) m)) *)
     fold (sizeof t0).
(* Goal: Z.le (@sizeof (@cenv_cs cs) match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end) (Z.max (@sizeof (@cenv_cs cs) t0) (sizeof_union (@cenv_cs cs) m)) *)
     pose proof Z.le_max_r (sizeof t0) (sizeof_union cenv_cs m).
(* Goal: @eq Z (sizeof_union env m) Z0 *)
     omega.
Qed.

(* if sizeof Tvoid = 0, this lemma can be nicer. *)
Lemma field_offset_no_overlap:
  forall i1 i2 m,
  i1 <> i2 ->
  in_members i1 m ->
  in_members i2 m ->
  field_offset cenv_cs i1 m + sizeof (field_type i1 m) <= field_offset cenv_cs i2 m \/
  field_offset cenv_cs i2 m + sizeof (field_type i2 m) <= field_offset cenv_cs i1 m.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: or (Z.le (Z.add (field_offset (@cenv_cs cs) i1 m) (@sizeof (@cenv_cs cs) (field_type i1 m))) (field_offset (@cenv_cs cs) i2 m)) (Z.le (Z.add (field_offset (@cenv_cs cs) i2 m) (@sizeof (@cenv_cs cs) (field_type i2 m))) (field_offset (@cenv_cs cs) i1 m)) *)
  unfold field_offset, field_type.
(* Goal: or (Z.le (Z.add match Ctypes.field_offset (@cenv_cs cs) i1 m with | Errors.OK ofs => ofs | Errors.Error e => Z0 end (@sizeof (@cenv_cs cs) match Ctypes.field_type i1 m with | Errors.OK t => t | Errors.Error e => Tvoid end)) match Ctypes.field_offset (@cenv_cs cs) i2 m with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) (Z.le (Z.add match Ctypes.field_offset (@cenv_cs cs) i2 m with | Errors.OK ofs => ofs | Errors.Error e => Z0 end (@sizeof (@cenv_cs cs) match Ctypes.field_type i2 m with | Errors.OK t => t | Errors.Error e => Tvoid end)) match Ctypes.field_offset (@cenv_cs cs) i1 m with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) *)
  pose proof field_type_in_members i1 m.
(* Goal: or (Z.le (Z.add match Ctypes.field_offset (@cenv_cs cs) i1 m with | Errors.OK ofs => ofs | Errors.Error e => Z0 end (@sizeof (@cenv_cs cs) match Ctypes.field_type i1 m with | Errors.OK t => t | Errors.Error e => Tvoid end)) match Ctypes.field_offset (@cenv_cs cs) i2 m with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) (Z.le (Z.add match Ctypes.field_offset (@cenv_cs cs) i2 m with | Errors.OK ofs => ofs | Errors.Error e => Z0 end (@sizeof (@cenv_cs cs) match Ctypes.field_type i2 m with | Errors.OK t => t | Errors.Error e => Tvoid end)) match Ctypes.field_offset (@cenv_cs cs) i1 m with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) *)
  pose proof field_type_in_members i2 m.
  solve_field_offset_type i1 m;
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
  solve_field_offset_type i2 m; try tauto.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
  eapply field_offset_no_overlap; eauto.
Qed.

Lemma not_in_members_field_type: forall i m,
  ~ in_members i m ->
  field_type i m = Tvoid.
Proof.
(* Goal: forall (i : ident) (m : members) (_ : not (in_members i m)), @eq type (field_type i m) Tvoid *)
  unfold in_members, field_type.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq type match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end Tvoid *)
  induction m as [| [i0 t0] m].
  + reflexivity.
  + simpl in H.
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) *)
    simpl.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
    destruct (ident_eq i i0) as [HH | HH]; pose proof (@eq_sym ident i i0); tauto.
Qed.

Lemma not_in_members_field_offset: forall i m,
  ~ in_members i m ->
  field_offset cenv_cs i m = 0.
Proof.
(* Goal: forall (i : ident) (m : members) (_ : not (in_members i m)), @eq Z (field_offset (@cenv_cs cs) i m) Z0 *)
  unfold in_members, field_offset, Ctypes.field_offset.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs) i m Z0 with | Errors.OK ofs => ofs | Errors.Error e => Z0 end Z0 *)
  generalize 0 at 1.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  induction m as [| [i0 t0] m]; intros.
  + reflexivity.
  + simpl in H.
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) *)
    simpl.
(* Goal: @eq Z match (if ident_eq i i0 then @Errors.OK Z (align z (@alignof (@cenv_cs cs) t0)) else field_offset_rec (@cenv_cs cs) i m (Z.add (align z (@alignof (@cenv_cs cs) t0)) (@sizeof (@cenv_cs cs) t0))) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end Z0 *)
    destruct (ident_eq i i0) as [HH | HH]; pose proof (@eq_sym ident i i0); [tauto |].
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
    apply IHm. tauto.
Qed.

Lemma field_offset_next_in_range: forall i m sz,
  in_members i m ->
  sizeof_struct cenv_cs 0 m <= sz ->
  field_offset cenv_cs i m + sizeof (field_type i m) <=
  field_offset_next cenv_cs i m sz <= sz.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: and (Z.le (Z.add (field_offset (@cenv_cs cs) i m) (@sizeof (@cenv_cs cs) (field_type i m))) (field_offset_next (@cenv_cs cs) i m sz)) (Z.le (field_offset_next (@cenv_cs cs) i m sz) sz) *)
  destruct m as [| [i0 t0] m]; [inversion H |].
(* Goal: and (Z.le (Z.add (field_offset (@cenv_cs cs) i (@cons (prod ident type) (@pair ident type i0 t0) m)) (@sizeof (@cenv_cs cs) (field_type i (@cons (prod ident type) (@pair ident type i0 t0) m)))) (field_offset_next (@cenv_cs cs) i (@cons (prod ident type) (@pair ident type i0 t0) m) sz)) (Z.le (field_offset_next (@cenv_cs cs) i (@cons (prod ident type) (@pair ident type i0 t0) m) sz) sz) *)
  unfold field_offset, Ctypes.field_offset, field_offset_next, field_type.
(* Goal: and (Z.le (Z.add match field_offset_rec (@cenv_cs cs) i (@cons (prod ident type) (@pair ident type i0 t0) m) Z0 with | Errors.OK ofs => ofs | Errors.Error e => Z0 end (@sizeof (@cenv_cs cs) match Ctypes.field_type i (@cons (prod ident type) (@pair ident type i0 t0) m) with | Errors.OK t => t | Errors.Error e => Tvoid end)) (field_offset_next_rec (@cenv_cs cs) i (@cons (prod ident type) (@pair ident type i0 t0) m) Z0 sz)) (Z.le (field_offset_next_rec (@cenv_cs cs) i (@cons (prod ident type) (@pair ident type i0 t0) m) Z0 sz) sz) *)
  pattern 0 at 3 4; replace 0 with (align 0 (alignof t0)) by (apply align_0, alignof_pos).
  match goal with
  | |- ?A => assert (A /\
                     match field_offset_rec cenv_cs i ((i0, t0) :: m) 0 with
                     | Errors.OK _ => True
                     | _ => False
                     end /\
                     match Ctypes.field_type i ((i0, t0) :: m) with
                     | Errors.OK _ => True
                     | _ => False
                     end); [| tauto]
  end.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  revert i0 t0 H H0; generalize 0; induction m as [| [i1 t1] m]; intros.
  + destruct (ident_eq i i0); [| destruct H; simpl in H; try congruence; tauto].
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) *)
    subst; simpl.
(* Goal: @eq Z (@sizeof env match (if ident_eq i i0 then @Errors.OK type t0 else Ctypes.field_type i m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
    if_tac; [| congruence].
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
    split; [| split]; auto.
(* Goal: @eq type t t0 *)
    simpl in H0.
   fold (sizeof t0) in *.
(* Goal: @eq Z (sizeof_union env m) Z0 *)
    omega.
  + remember ((i1, t1) :: m) as m0. simpl in H0 |- *. subst m0.
(* Goal: @eq Z (@sizeof env match Ctypes.field_type i (@cons (prod ident type) (@pair ident type i0 t0) m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
    destruct (ident_eq i i0).
    - split; [| split]; auto.
(* Goal: iff (@eq bool (Pos.eqb p q) true) (@eq positive p q) *)
      split.
      * apply align_le, alignof_pos.
      * pose proof sizeof_struct_incr cenv_cs m (align (align z (alignof t0) + sizeof t0)
            (alignof t1) + sizeof t1).
(* Goal: Z.le (align (Z.add (align z (@alignof (@cenv_cs cs) t0)) (@sizeof (@cenv_cs cs) t0)) (@alignof (@cenv_cs cs) t1)) sz *)
        pose proof sizeof_pos t1.
(* Goal: @eq Z (sizeof_union env m) Z0 *)
        simpl in H0; omega.
    - destruct H as [H | H]; [simpl in H; congruence |].
      specialize (IHm (align z (alignof t0) + sizeof t0) i1 t1 H H0).
      destruct (field_offset_rec cenv_cs i ((i1, t1) :: m) (align z (alignof t0) + sizeof t0)),
               (field_type i ((i1, t1) :: m));
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      try tauto.
Qed.

Lemma Pos_eqb_eq: forall p q: positive, iff (eq (Pos.eqb p q) true) (eq p q).
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
intros.
(* Goal: iff (@eq bool (Pos.eqb p q) true) (@eq positive p q) *)
split.
(* Goal: forall _ : @eq bool (Pos.eqb p q) true, @eq positive p q *)
(* Goal: forall _ : @eq positive p q, @eq bool (Pos.eqb p q) true *)
revert q; induction p; destruct q; simpl; intros; auto; try discriminate.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
apply f_equal. apply IHp; auto.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
apply f_equal. apply IHp; auto.
(* Goal: False *)
intros; subst.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
induction q; simpl; auto.
Defined.


(* copied from veric/Clight_lemmas.v; but here Defined instead of Qed  *)
Lemma id_in_list_true: forall i ids, id_in_list i ids = true -> In i ids.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
 induction ids; simpl; intros. inv H.
(* Goal: or (@eq ident a i) (@In ident i ids) *)
 destruct (i =? a)%positive eqn:?.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
 apply Pos_eqb_eq in Heqb. left; auto.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
 auto.
Defined.


Lemma id_in_list_false: forall i ids, id_in_list i ids = false -> ~In i ids.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
 intros.
(* Goal: False *)
(* Goal: False *)
 intro. induction ids. inv H0.
 simpl in *. destruct H0. subst i.
(* Goal: False *)
(* Goal: False *)
 assert (a =? a = true)%positive.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
 apply Pos_eqb_eq. auto. rewrite H0 in H. simpl in H. inv H.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
 destruct (i =? a)%positive. simpl in H. inv H.   auto.
Defined.

Lemma members_no_replicate_ind: forall m,
  (members_no_replicate m = true) <->
  match m with
  | nil => True
  | (i0, _) :: m0 => ~ in_members i0 m0 /\ members_no_replicate m0 = true
  end.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: iff (@eq bool (members_no_replicate m) true) match m with | nil => True | cons (pair i0 t as p) m0 => and (not (in_members i0 m0)) (@eq bool (members_no_replicate m0) true) end *)
  unfold members_no_replicate.
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) *)
  destruct m as [| [i t] m]; simpl.
  + assert (true = true) by auto; tauto.
  + destruct (id_in_list i (map fst m)) eqn:HH.
    - apply id_in_list_true in HH.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
       split; intros. inv H.  destruct H. elimtype False; apply H.
(* Goal: in_members i m *)
      apply HH.
    - apply id_in_list_false in HH.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
      split; intros. split; auto. destruct H; auto.
Defined.

Lemma map_members_ext: forall A (f f':ident * type -> A) (m: members),
  members_no_replicate m = true ->
  (forall i, in_members i m -> f (i, field_type i m) = f' (i, field_type i m)) ->
  map f m = map f' m.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq Z (@sizeof env match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
  induction m as [| (i0, t0) m].
  + reflexivity.
  + simpl.
(* Goal: @eq (list A) (@cons A (f (@pair ident type i0 t0)) (@map (prod ident type) A f m)) (@cons A (f' (@pair ident type i0 t0)) (@map (prod ident type) A f' m)) *)
    rewrite members_no_replicate_ind in H.
(* Goal: @eq Z (align z (@alignof (@cenv_cs cs_from) t0)) (align z (@alignof (@cenv_cs cs_to) t0)) *)
    f_equal.
    - specialize (H0 i0).
(* Goal: @eq A (f (@pair ident type i (field_type i m))) (f' (@pair ident type i (field_type i m))) *)
      unfold field_type, in_members in H0.
(* Goal: @eq A (f (@pair ident type i0 t0)) (f' (@pair ident type i0 t0)) *)
      simpl in H0; if_tac in H0; [| congruence].
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      apply H0; auto.
    - apply IHm; [tauto |].
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
      intros.
(* Goal: @eq A (f (@pair ident type i (field_type i m))) (f' (@pair ident type i (field_type i m))) *)
      specialize (H0 i).
(* Goal: @eq A (f (@pair ident type i (field_type i m))) (f' (@pair ident type i (field_type i m))) *)
      unfold field_type, in_members in H0.
(* Goal: @eq A (f (@pair ident type i (field_type i m))) (f' (@pair ident type i (field_type i m))) *)
      simpl in H0; if_tac in H0; [subst; tauto |].
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      apply H0; auto.
Defined.

Lemma in_members_tail_no_replicate: forall i i0 t0 m,
  members_no_replicate ((i0, t0) :: m) = true ->
  in_members i m ->
  i <> i0.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: not (@eq ident i i0) *)
 destruct (members_no_replicate_ind ((i0,t0)::m)) as [? _].
(* Goal: not (@eq ident i i0) *)
 apply H1 in H. clear H1.
(* Goal: not (@eq ident i i0) *)
  intro.
(* Goal: False *)
  subst. destruct H. auto.
Defined.

Lemma neq_field_offset_rec_cons: forall env i i0 t0 m z,
  i <> i0 ->
  field_offset_rec env i ((i0, t0) :: m) z =
  field_offset_rec env i m (align z (alignof t0) + sizeof t0).
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) *)
  simpl.
(* Goal: @eq Z (@sizeof env match (if ident_eq i i0 then @Errors.OK type t0 else Ctypes.field_type i m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
  if_tac; [congruence |].
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
  auto.
Qed.

Lemma neq_field_offset_next_rec_cons: forall env i i0 t0 i1 t1 m z sz,
  i <> i0 ->
  field_offset_next_rec env i ((i0, t0) :: (i1, t1) :: m) z sz =
  field_offset_next_rec env i ((i1, t1) :: m) (align (z +  sizeof t0) (alignof t1)) sz.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) *)
  simpl.
(* Goal: @eq Z (@sizeof env match (if ident_eq i i0 then @Errors.OK type t0 else Ctypes.field_type i m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
  if_tac; [congruence |].
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
  auto.
Qed.

Lemma sizeof_struct_0: forall env i m,
  sizeof_struct env 0 m = 0 ->
  in_members i m ->
  sizeof (field_type i m) = 0 /\
  field_offset_next env i m 0 - (field_offset env i m + sizeof (field_type i m)) = 0.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: and (@eq Z (@sizeof env (field_type i m)) Z0) (@eq Z (Z.sub (field_offset_next env i m Z0) (Z.add (field_offset env i m) (@sizeof env (field_type i m)))) Z0) *)
  unfold field_type, field_offset, Ctypes.field_offset, field_offset_next.
(* Goal: @eq Z (@sizeof env match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
  induction m as [| (i0, t0) m].
  + inversion H0.
  + simpl in H.
    pose proof sizeof_struct_incr env m (align 0 (alignof t0) + sizeof t0).
(* Goal: and (@eq Z (@sizeof env match Ctypes.field_type i (@cons (prod ident type) (@pair ident type i0 t0) m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0) (@eq Z (Z.sub (field_offset_next_rec env i (@cons (prod ident type) (@pair ident type i0 t0) m) Z0 Z0) (Z.add match field_offset_rec env i (@cons (prod ident type) (@pair ident type i0 t0) m) Z0 with | Errors.OK ofs => ofs | Errors.Error e => Z0 end (@sizeof env match Ctypes.field_type i (@cons (prod ident type) (@pair ident type i0 t0) m) with | Errors.OK t => t | Errors.Error e => Tvoid end))) Z0) *)
    pose proof align_le 0 (alignof t0) (alignof_pos _).
(* Goal: @eq Z (@sizeof env t0) Z0 *)
    pose proof sizeof_pos t0.
(* Goal: @eq Z (@sizeof env match Ctypes.field_type i (@cons (prod ident type) (@pair ident type i0 t0) m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
    destruct (ident_eq i i0).
    - simpl in *.
(* Goal: @eq Z (@sizeof env match (if ident_eq i i0 then @Errors.OK type t0 else Ctypes.field_type i m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
      if_tac; [| congruence].
(* Goal: @eq Z (sizeof_union env m) Z0 *)
      replace (sizeof t0) with 0 by omega.
      destruct m as [| (?, ?) m];
      rewrite !align_0 by apply alignof_pos;
(* Goal: @eq Z (sizeof_union env m) Z0 *)
      omega.
    - destruct H0; [simpl in H0; congruence |].
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) *)
      simpl.
(* Goal: @eq Z (@sizeof env match (if ident_eq i i0 then @Errors.OK type t0 else Ctypes.field_type i m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
      if_tac; [congruence |].
(* Goal: @eq Z (sizeof_union env m) Z0 *)
      replace (sizeof t0) with 0 by omega.
(* Goal: and (@eq Z (@sizeof env match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0) (@eq Z (Z.sub match m with | nil => Z0 | cons (pair y t1 as p) l => field_offset_next_rec env i m (align Z0 (@alignof env t1)) Z0 end (Z.add match field_offset_rec env i m (Z.add (align Z0 (@alignof env t0)) Z0) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end (@sizeof env match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end))) Z0) *)
      destruct m as [| (?, ?) m]; [inversion H0 |].
(* Goal: and (@eq Z (@sizeof env match Ctypes.field_type i (@cons (prod ident type) (@pair ident type i1 t) m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0) (@eq Z (Z.sub (field_offset_next_rec env i (@cons (prod ident type) (@pair ident type i1 t) m) (align Z0 (@alignof env t)) Z0) (Z.add match field_offset_rec env i (@cons (prod ident type) (@pair ident type i1 t) m) (Z.add (align Z0 (@alignof env t0)) Z0) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end (@sizeof env match Ctypes.field_type i (@cons (prod ident type) (@pair ident type i1 t) m) with | Errors.OK t => t | Errors.Error e => Tvoid end))) Z0) *)
      rewrite !align_0 by apply alignof_pos.
(* Goal: @eq Z (@sizeof env match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
      apply IHm; [| auto].
      replace (align 0 (alignof t0) + sizeof t0) with 0 in * by omega.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      auto.
Qed.

Lemma sizeof_union_0: forall env i m,
  sizeof_union env m = 0 ->
  in_members i m ->
  sizeof (field_type i m) = 0.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (field_type i (co_members (@get_co cs_to id)))) true *)
  unfold field_type.
(* Goal: @eq Z (@sizeof env match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
  induction m as [| (i0, t0) m].
  + inversion H0.
  + simpl in H.
(* Goal: @eq Z (@sizeof env match Ctypes.field_type i (@cons (prod ident type) (@pair ident type i0 t0) m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
    destruct (ident_eq i i0).
    - simpl in *.
(* Goal: @eq Z (@sizeof env match (if ident_eq i i0 then @Errors.OK type t0 else Ctypes.field_type i m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
      if_tac; [| congruence].
(* Goal: @eq Z (@sizeof env t0) Z0 *)
      pose proof sizeof_pos t0.
(* Goal: @eq Z (@sizeof env t0) Z0 *)
      pose proof Z.le_max_l (sizeof t0) (sizeof_union env m).
(* Goal: @eq Z (sizeof_union env m) Z0 *)
      omega.
    - destruct H0; [simpl in H0; congruence |].
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) *)
      simpl.
(* Goal: @eq Z (@sizeof env match (if ident_eq i i0 then @Errors.OK type t0 else Ctypes.field_type i m) with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
      if_tac; [congruence |].
(* Goal: @eq Z (@sizeof env match Ctypes.field_type i m with | Errors.OK t => t | Errors.Error e => Tvoid end) Z0 *)
      apply IHm; [| auto].
(* Goal: @eq Z (sizeof_union env m) Z0 *)
      pose proof sizeof_union_pos env m.
(* Goal: @eq Z (sizeof_union env m) Z0 *)
      pose proof Z.le_max_r (sizeof t0) (sizeof_union env m).
(* Goal: @eq Z (sizeof_union env m) Z0 *)
      omega.
Qed.

Definition in_map: forall {A B : Type} (f : A -> B) (l : list A) (x : A),
       In x l -> In (f x) (map f l) :=
fun (A B : Type) (f : A -> B) (l : list A) =>
list_ind (fun l0 : list A => forall x : A, In x l0 -> In (f x) (map f l0))
  (fun (x : A) (H : In x nil) => H)
  (fun (a : A) (l0 : list A)
     (IHl : forall x : A, In x l0 -> In (f x) (map f l0)) (x : A)
     (H : In x (a :: l0)) =>
   or_ind
     (fun H0 : a = x =>
      or_introl (eq_ind_r (fun a0 : A => f a0 = f x) eq_refl H0))
     (fun H0 : In x l0 =>
      or_intror
        ((fun H1 : In x l0 -> In (f x) (map f l0) =>
          (fun H2 : In (f x) (map f l0) => H2) (H1 H0)) (IHl x))) H) l.

Lemma In_field_type: forall it m,
  members_no_replicate m = true ->
  In it m ->
  field_type (fst it) m = snd it.
Proof.
(* Goal: @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (field_type i (co_members (@get_co cs_to id)))) true *)
  unfold field_type.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq type match Ctypes.field_type (@fst ident type it) m with | Errors.OK t => t | Errors.Error e => Tvoid end (@snd ident type it) *)
  induction m.
  + inversion H0.
  + destruct a, it.
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) *)
    simpl.
(* Goal: @eq type match (if ident_eq i0 i then @Errors.OK type t else Ctypes.field_type i0 m) with | Errors.OK t => t | Errors.Error e => Tvoid end t0 *)
    destruct (ident_eq i0 i).
    - destruct H0; [inversion H0; auto |].
(* Goal: @eq type t t0 *)
      apply in_map with (f := fst) in H0.
(* Goal: @eq type t t0 *)
      simpl in H0.
(* Goal: @eq type t t0 *)
      pose proof in_members_tail_no_replicate _ _ _ _ H H0.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      subst i0. contradiction H1; auto.
    - apply IHm.
(* Goal: @eq bool (members_no_replicate m) true *)
(* Goal: @In (prod ident type) (@pair ident type i0 t0) m *)
       destruct (members_no_replicate_ind ((i,t)::m)) as [? _].
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
       destruct (H1 H); auto.
      * inversion H0; [| auto].
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
        inversion H1. subst i0 t0.  contradiction n; auto.
Defined.

End COMPOSITE_ENV.

Lemma members_spec_change_composite' {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall id,
  match (coeq cs_from cs_to) ! id with
  | Some b => test_aux cs_from cs_to b id
  | None => false
  end = true ->
  Forall (fun it => cs_preserve_type cs_from cs_to (coeq _ _) (snd it) = true) (co_members (get_co id)).
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
  destruct ((@cenv_cs cs_to) ! id) eqn:?H.
  + pose proof proj1 (coeq_complete _ _ id) (ex_intro _ c H0) as [b ?].
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
    rewrite H1 in H.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
    apply (coeq_consistent _ _ id _ _ H0) in H1.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
    unfold test_aux in H.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
    destruct b; [| inv H].
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
    rewrite !H0 in H.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
    destruct ((@cenv_cs cs_from) ! id) eqn:?H; [| inv H].
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
    simpl in H.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
    rewrite !andb_true_iff in H.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
    unfold get_co.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members match @PTree.get composite id (@cenv_cs cs_to) with | Some co => co | None => co_default Struct end) *)
    rewrite H0.
    clear - H1.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members c) *)
    symmetry in H1.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members c) *)
    induction (co_members c) as [| [i t] ?].
    - constructor.
    - simpl in H1; rewrite andb_true_iff in H1; destruct H1.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      constructor; auto.
  + destruct ((coeq cs_from cs_to) ! id) eqn:?H.
    - pose proof proj2 (coeq_complete _ _ id) (ex_intro _ b H1) as [co ?].
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (co_members (@get_co cs_to id)) *)
      congruence.
    - inv H.
Qed.

Lemma members_spec_change_composite'' {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall id,
  match (coeq cs_from cs_to) ! id with
  | Some b => test_aux cs_from cs_to b id
  | None => false
  end = true ->
  forall i, cs_preserve_type cs_from cs_to (coeq _ _) (field_type i (co_members (get_co id))) = true.
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (field_type i (co_members (@get_co cs_to id)))) true *)
  unfold field_type.
(* Goal: @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  apply members_spec_change_composite' in H.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
  induction H as [| [i0 t0] ?]; auto.
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) (@cons (prod ident type) (@pair ident type i1 t1) l)) z (co_sizeof (@get_co cs_to id))) *)
  simpl.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
  if_tac; auto.
Qed.

Lemma members_spec_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall id,
  match (coeq cs_from cs_to) ! id with
  | Some b => test_aux cs_from cs_to b id
  | None => false
  end = true ->
  Forall (fun it => cs_preserve_type cs_from cs_to (coeq _ _) (field_type (fst it) (co_members (get_co id))) = true) (co_members (get_co id)).
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  apply members_spec_change_composite' in H.
  assert (Forall (fun it: ident * type => field_type (fst it) (co_members (get_co id)) = snd it) (co_members (get_co id))).
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq type (field_type (@fst ident type it) (co_members (@get_co cs_to id))) (@snd ident type it)) (co_members (@get_co cs_to id)) *)
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (field_type (@fst ident type it) (co_members (@get_co cs_to id)))) true) (co_members (@get_co cs_to id)) *)
  1:{
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq type (field_type (@fst ident type it) (co_members (@get_co cs_to id))) (@snd ident type it)) (co_members (@get_co cs_to id)) *)
    rewrite Forall_forall.
(* Goal: forall (x : prod ident type) (_ : @In (prod ident type) x (co_members (@get_co cs_to id))), @eq type (field_type (@fst ident type x) (co_members (@get_co cs_to id))) (@snd ident type x) *)
    intros it ?.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
    apply In_field_type; auto.
(* Goal: @eq bool (members_no_replicate (co_members (@get_co cs_to id))) true *)
    apply get_co_members_no_replicate.
  }
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (field_type (@fst ident type it) (co_members (@get_co cs_to id)))) true) (co_members (@get_co cs_to id)) *)
  revert H0; generalize (co_members (get_co id)) at 1 3.
(* Goal: @Forall (prod ident type) (fun it : prod ident type => @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@snd ident type it)) true) (@nil (prod ident type)) *)
  induction H as [| [i t] ?]; constructor.
  + inv H1.
    simpl in *.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
    rewrite H4; auto.
  + inv H1.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
    auto.
Qed.

(* TODO: we have already proved a related field_offset lemma in veric/change_compspecs.v. But it seems not clear how to use that in an elegant way. *)
Lemma field_offset_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall id i,
  match (coeq cs_from cs_to) ! id with
  | Some b => test_aux cs_from cs_to b id
  | None => false
  end = true ->
  field_offset (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) =
  field_offset (@cenv_cs cs_to) i (co_members (@get_co cs_to id)).
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  apply members_spec_change_composite' in H.
(* Goal: @eq Z (field_offset (@cenv_cs cs_from) i (co_members (@get_co cs_to id))) (field_offset (@cenv_cs cs_to) i (co_members (@get_co cs_to id))) *)
  unfold field_offset, Ctypes.field_offset.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) Z0 with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) Z0 with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
  generalize 0 at 1 3.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  induction (co_members (get_co id)) as [| [i0 t0] ?]; intros.
  + auto.
  + simpl.
(* Goal: @eq Z match (if ident_eq i i0 then @Errors.OK Z (align z (@alignof (@cenv_cs cs_from) t0)) else field_offset_rec (@cenv_cs cs_from) i m (Z.add (align z (@alignof (@cenv_cs cs_from) t0)) (@sizeof (@cenv_cs cs_from) t0))) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match (if ident_eq i i0 then @Errors.OK Z (align z (@alignof (@cenv_cs cs_to) t0)) else field_offset_rec (@cenv_cs cs_to) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0))) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
    inv H.
(* Goal: @eq Z match (if ident_eq i i0 then @Errors.OK Z (align z (@alignof (@cenv_cs cs_from) t0)) else field_offset_rec (@cenv_cs cs_from) i m (Z.add (align z (@alignof (@cenv_cs cs_from) t0)) (@sizeof (@cenv_cs cs_from) t0))) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match (if ident_eq i i0 then @Errors.OK Z (align z (@alignof (@cenv_cs cs_to) t0)) else field_offset_rec (@cenv_cs cs_to) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0))) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
    if_tac.
    - f_equal.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      apply alignof_change_composite; auto.
    - specialize (IHm H3).
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      rewrite alignof_change_composite, sizeof_change_composite by auto.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i m (Z.add (align z (@alignof (@cenv_cs cs_to) t0)) (@sizeof (@cenv_cs cs_to) t0)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      apply IHm.
Qed.

Lemma field_offset_next_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall id i,
  match (coeq cs_from cs_to) ! id with
  | Some b => test_aux cs_from cs_to b id
  | None => false
  end = true ->
  field_offset_next (@cenv_cs cs_from) i (co_members (get_co id)) (co_sizeof (@get_co cs_from id)) =
field_offset_next (@cenv_cs cs_to) i (co_members (get_co id)) (co_sizeof (@get_co cs_to id)).
Proof.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  intros.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
  rewrite co_sizeof_get_co_change_composite by auto.
(* Goal: @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  apply members_spec_change_composite' in H.
(* Goal: @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  unfold field_offset_next.
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) Z0 (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) Z0 (co_sizeof (@get_co cs_to id))) *)
  generalize 0.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
  destruct H as [| [i0 t0] ? ]; intros; auto.
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) l) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) l) z (co_sizeof (@get_co cs_to id))) *)
  simpl in H, H0.
(* Goal: @eq Z (field_offset_next_rec (@cenv_cs cs_from) i (@cons (prod ident type) (@pair ident type i0 t0) l) z (co_sizeof (@get_co cs_to id))) (field_offset_next_rec (@cenv_cs cs_to) i (@cons (prod ident type) (@pair ident type i0 t0) l) z (co_sizeof (@get_co cs_to id))) *)
  revert i0 t0 H z.
(* Goal: forall (id i : positive) (_ : @eq bool match @PTree.get bool id (@coeq cs_from cs_to CCE) with | Some b => test_aux cs_from cs_to b id | None => false end true), @eq Z (field_offset_next (@cenv_cs cs_from) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_from id))) (field_offset_next (@cenv_cs cs_to) i (co_members (@get_co cs_to id)) (co_sizeof (@get_co cs_to id))) *)
  induction H0 as [| [i1 t1] ? ]; intros.
  + reflexivity.
  + simpl.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
    if_tac; auto.
    - f_equal; [f_equal |].
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      * apply sizeof_change_composite; auto.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      * apply alignof_change_composite; auto.
    - specialize (IHForall i1 t1 H (align (z + sizeof t0) (alignof t1))); simpl in IHForall.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      rewrite (sizeof_change_composite t0) by auto.
(* Goal: @eq Z match field_offset_rec (@cenv_cs cs_from) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end match field_offset_rec (@cenv_cs cs_to) i (@nil (prod ident type)) z with | Errors.OK ofs => ofs | Errors.Error e => Z0 end *)
      rewrite (alignof_change_composite t1) by auto.
(* Goal: @eq Z match l with | nil => co_sizeof (@get_co cs_to id) | cons (pair y t2 as p) l0 => if ident_eq i i1 then align (Z.add (align (Z.add z (@sizeof (@cenv_cs cs_to) t0)) (@alignof (@cenv_cs cs_to) t1)) (@sizeof (@cenv_cs cs_from) t1)) (@alignof (@cenv_cs cs_from) t2) else field_offset_next_rec (@cenv_cs cs_from) i l (align (Z.add (align (Z.add z (@sizeof (@cenv_cs cs_to) t0)) (@alignof (@cenv_cs cs_to) t1)) (@sizeof (@cenv_cs cs_from) t1)) (@alignof (@cenv_cs cs_from) t2)) (co_sizeof (@get_co cs_to id)) end match l with | nil => co_sizeof (@get_co cs_to id) | cons (pair y t2 as p) l0 => if ident_eq i i1 then align (Z.add (align (Z.add z (@sizeof (@cenv_cs cs_to) t0)) (@alignof (@cenv_cs cs_to) t1)) (@sizeof (@cenv_cs cs_to) t1)) (@alignof (@cenv_cs cs_to) t2) else field_offset_next_rec (@cenv_cs cs_to) i l (align (Z.add (align (Z.add z (@sizeof (@cenv_cs cs_to) t0)) (@alignof (@cenv_cs cs_to) t1)) (@sizeof (@cenv_cs cs_to) t1)) (@alignof (@cenv_cs cs_to) t2)) (co_sizeof (@get_co cs_to id)) end *)
      apply IHForall.
Qed.

Arguments field_type i m / .
Arguments field_offset env i m / .

