Require Import Coq.Sorting.Permutation.
Require Import Coq.Sorting.Sorting.
Require Import Coq.Structures.Orders.
Require Import VST.veric.base.

Require Import compcert.cfrontend.Ctypes. 

(* TODO: This is obviously true. Ask Xavior to remove the definition list_norepet.*)
Axiom list_norepet_NoDup: forall {A: Type} (l: list A), list_norepet l <-> NoDup l.

(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
Lemma PTree_In_fst_elements {A: Type}: forall (T: PTree.t A) i,
  In i (map fst (PTree.elements T)) <-> exists a, PTree.get i T = Some a.
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  split; intros.
  + apply list_in_map_inv in H.
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i T) (@Some A a)) *)
    destruct H as [[i0 a] [? ?]].
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i T) (@Some A a)) *)
    simpl in H; subst i0.
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i T) (@Some A a)) *)
    apply PTree.elements_complete in H0.
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i T) (@Some A a)) *)
    eauto.
  + destruct H as [a ?].
(* Goal: @In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A T)) *)
    apply PTree.elements_correct in H.
(* Goal: @In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A T)) *)
    apply (in_map fst) in H.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    auto.
Qed.

(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
Lemma PTree_gs {A: Type}: forall (T: PTree.t A) i j x,
  (exists a, PTree.get i T= Some a) ->
  exists a, PTree.get i (PTree.set j x T) = Some a.
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i (@PTree.set A j x T)) (@Some A a)) *)
  destruct H.
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i (@PTree.set A j x T)) (@Some A a)) *)
  destruct (Pos.eq_dec i j).
  + subst.
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i T) (@Some A a)) *)
    rewrite PTree.gss; eauto.
  + rewrite PTree.gso; eauto.
Qed.

(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
Lemma PTree_gs_equiv {A: Type}: forall (T: PTree.t A) i j x,
  (exists a, PTree.get i T= Some a) \/ i = j <->
  exists a, PTree.get i (PTree.set j x T) = Some a.
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  split; intros.
  + destruct H; [apply PTree_gs; auto |].
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i T) (@Some A a)) *)
    subst; rewrite PTree.gss; eauto.
  + destruct (Pos.eq_dec i j); auto.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    rewrite PTree.gso in H by auto.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    auto.
Qed.

(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
Lemma PTree_set_In_fst_elements {A: Type}: forall (T: PTree.t A) i i' a',
  In i (map fst (PTree.elements T)) ->
  In i (map fst (PTree.elements (PTree.set i' a' T))).
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: @In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (@PTree.set A i' a' T))) *)
  rewrite PTree_In_fst_elements in H |- *.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
  apply PTree_gs; auto.
Qed.
  
(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
Fixpoint relative_defined_type {A: Type} (l: list (ident * A)) (t: type): Prop :=
  match t with
  | Tarray t' _ _ => relative_defined_type l t'
  | Tstruct id _ => In id (map fst l)
  | Tunion id _ => In id (map fst l)
  | _ => True
  end.

(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
Lemma relative_defined_type_mono: forall {A B: Type} (l1: list (ident * A)) (l2: list (ident * B)) (t: type),
  (forall i, In i (map fst l1) -> In i (map fst l2)) ->
  relative_defined_type l1 t ->
  relative_defined_type l2 t.
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
  induction t; auto.
  + simpl in *.
(* Goal: forall (i : ident) (_ : @In ident i (@map (prod ident composite) ident (@fst ident composite) l)), @In ident i (@map (prod ident A) ident (@fst ident A) (@PTree.elements A env)) *)
    firstorder.
  + simpl in *.
(* Goal: forall (i : ident) (_ : @In ident i (@map (prod ident composite) ident (@fst ident composite) l)), @In ident i (@map (prod ident A) ident (@fst ident A) (@PTree.elements A env)) *)
    firstorder.
Qed.

(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
Lemma relative_defined_type_equiv: forall {A B: Type} (l1: list (ident * A)) (l2: list (ident * B)) (t: type),
  (forall i, In i (map fst l1) <-> In i (map fst l2)) ->
  (relative_defined_type l1 t <-> relative_defined_type l2 t).
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
  split; apply relative_defined_type_mono;
(* Goal: forall (i : ident) (_ : @In ident i (@map (prod ident composite) ident (@fst ident composite) l)), @In ident i (@map (prod ident A) ident (@fst ident A) (@PTree.elements A env)) *)
  firstorder.
Qed.

Inductive ordered_composite: list (positive * composite) -> Prop :=
| ordered_composite_nil: ordered_composite nil
| ordered_composite_cons: forall i co l,
    Forall (relative_defined_type l) (map snd (co_members co)) ->
    ordered_composite l ->
    ordered_composite ((i, co) :: l).

Module composite_reorder.

(* Use merge sort instead *)
(* Sort rank from higher to lower *)
Module CompositeRankOrder <: TotalLeBool.
  Definition t := (positive * composite)%type.
  Definition leb (x y: t) := Nat.leb (co_rank (snd y)) (co_rank (snd x)).

  Theorem leb_total : forall a1 a2, leb a1 a2 = true \/ leb a2 a1 = true.
  Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
    intros.
(* Goal: or (@eq bool (leb a1 a2) true) (@eq bool (leb a2 a1) true) *)
    unfold leb.
(* Goal: or (@eq bool (Nat.leb (co_rank (@snd positive composite a2)) (co_rank (@snd positive composite a1))) true) (@eq bool (Nat.leb (co_rank (@snd positive composite a1)) (co_rank (@snd positive composite a2))) true) *)
    rewrite !Nat.leb_le.
(* Goal: le (co_rank (@snd positive composite z)) (co_rank (@snd positive composite x)) *)
    omega.
  Qed.

  Theorem leb_trans: Transitive (fun x y => is_true (leb x y)).
  Proof.
(* Goal: @Transitive t (fun x y : t => is_true (leb x y)) *)
    hnf; intros; unfold leb, is_true in *.
(* Goal: @eq bool (Nat.leb (co_rank (@snd positive composite z)) (co_rank (@snd positive composite x))) true *)
    rewrite !Nat.leb_le in *.
(* Goal: le (co_rank (@snd positive composite z)) (co_rank (@snd positive composite x)) *)
    omega.
  Qed.

End CompositeRankOrder.

Module CompositeRankSort := Sort CompositeRankOrder.

Section composite_reorder.

Context (cenv: composite_env)
        (cenv_consistent: composite_env_consistent cenv).

Definition rebuild_composite_elements := CompositeRankSort.sort (PTree.elements cenv).

Inductive ordered_and_complete: list (positive * composite) -> Prop :=
| ordered_and_complete_nil: ordered_and_complete nil
| ordered_and_complete_cons: forall i co l,
    (forall i' co',
        cenv ! i' = Some co' ->
        (co_rank co' < co_rank co)%nat ->
        In (i', co') l) ->
    ordered_and_complete l ->
    ordered_and_complete ((i, co) :: l).

Theorem RCT_Permutation: Permutation rebuild_composite_elements (PTree.elements cenv).
Proof.
(* Goal: @Permutation (prod positive composite) rebuild_composite_elements (@PTree.elements composite cenv) *)
  symmetry.
(* Goal: @Permutation (prod positive composite) (@PTree.elements composite cenv) rebuild_composite_elements *)
  apply CompositeRankSort.Permuted_sort.
Qed.

Lemma RCT_ordered_and_complete: ordered_and_complete rebuild_composite_elements.
Proof.
  pose proof RCT_Permutation.
  assert (forall i co, cenv ! i = Some co -> In (i, co) rebuild_composite_elements).
(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
  {
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
    intros.
    eapply Permutation_in.
    + symmetry; apply RCT_Permutation.
    + apply PTree.elements_correct; auto.
  } 
(* Goal: Consistent cenv (Env l) *)
  clear H.
  pose proof CompositeRankSort.StronglySorted_sort (PTree.elements cenv) CompositeRankOrder.leb_trans.
  pose proof app_nil_l rebuild_composite_elements.
  unfold rebuild_composite_elements in *.
  set (l := (CompositeRankSort.sort (PTree.elements cenv))) in H1 at 1 |- *.
  revert H1; generalize (@nil (positive * composite)).
  clearbody l.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  induction l; intros.
  + constructor.
  + specialize (IHl (l0 ++ a :: nil)).
    rewrite <- app_assoc in IHl.
    specialize (IHl H1).
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    destruct a as [i co]; constructor; auto.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
    intros.
    apply H0 in H2.
    rewrite <- H1 in H2, H.
    clear - H2 H3 H.
    induction l0.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    - destruct H2; auto.
      exfalso; inv H0.
(* Goal: le (co_rank (@snd positive composite z)) (co_rank (@snd positive composite x)) *)
      omega.
    - inv H.
      destruct H2.
      * exfalso.
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i (@PTree.set A j x T)) (@Some A a)) *)
        subst.
        rewrite Forall_forall in H5.
        specialize (H5 (i, co)).
        rewrite in_app in H5.
        specialize (H5 (or_intror (or_introl eq_refl))).
        unfold is_true in H5.
        rewrite Nat.leb_le in H5; simpl in H5.
(* Goal: le (co_rank (@snd positive composite z)) (co_rank (@snd positive composite x)) *)
        omega.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
      * apply IHl0; auto.
Qed.

Theorem RCT_ordered: ordered_composite rebuild_composite_elements.
Proof.
(* Goal: ordered_composite rebuild_composite_elements *)
  pose proof RCT_ordered_and_complete.
  assert (forall i co, In (i, co) rebuild_composite_elements -> complete_members cenv (co_members co) = true /\ co_rank co = rank_members cenv (co_members co)).
(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
  {
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
    intros.
(* Goal: and (@eq bool (complete_members cenv (co_members co)) true) (@eq nat (co_rank co) (rank_members cenv (co_members co))) *)
    eapply Permutation_in in H0; [| exact RCT_Permutation].
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    apply PTree.elements_complete in H0; auto.
(* Goal: and (@eq bool (complete_members cenv (co_members co)) true) (@eq nat (co_rank co) (rank_members cenv (co_members co))) *)
    split.
    + apply co_consistent_complete.
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i T) (@Some A a)) *)
      eapply cenv_consistent; eauto.
    + apply co_consistent_rank.
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i T) (@Some A a)) *)
      eapply cenv_consistent; eauto.
  }
(* Goal: ordered_composite rebuild_composite_elements *)
  induction H.
  + constructor.
  + specialize (IHordered_and_complete (fun i co HH => H0 i co (or_intror HH))).
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    constructor; auto.
(* Goal: @Forall type (@relative_defined_type composite l) (@map (prod ident type) type (@snd ident type) (co_members co)) *)
    clear IHordered_and_complete H1.
(* Goal: @Forall type (@relative_defined_type composite l) (@map (prod ident type) type (@snd ident type) (co_members co)) *)
    specialize (H0 _ _ (or_introl eq_refl)).
(* Goal: le (co_rank (@snd positive composite z)) (co_rank (@snd positive composite x)) *)
    assert (rank_members cenv (co_members co) <= co_rank co)%nat by omega.
(* Goal: @Forall type (@relative_defined_type composite l) (@map (prod ident type) type (@snd ident type) (co_members co)) *)
    destruct H0 as [? _].
(* Goal: @Forall type (@relative_defined_type composite l) (@map (prod ident type) type (@snd ident type) (co_members co)) *)
    induction (co_members co) as [| [i0 t0] ?].
(* Goal: @Forall type (@relative_defined_type composite l) (@map (prod ident type) type (@snd ident type) (@nil (prod ident type))) *)
    - constructor.
    - simpl in H0; rewrite andb_true_iff in H0; destruct H0.
(* Goal: @Forall type (@relative_defined_type composite l) (@map (prod ident type) type (@snd ident type) (@cons (prod ident type) (@pair ident type i0 t0) m)) *)
      simpl in H1; pose proof Max.max_lub_r _ _ _ H1.
(* Goal: @Forall type (@relative_defined_type composite l) (@map (prod ident type) type (@snd ident type) (@cons (prod ident type) (@pair ident type i0 t0) m)) *)
      apply Max.max_lub_l in H1.
(* Goal: @Forall type (@relative_defined_type composite l) (@map (prod ident type) type (@snd ident type) (@cons (prod ident type) (@pair ident type i0 t0) m)) *)
      constructor; auto; clear IHm H2 H3.
(* Goal: iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))))) *)
      simpl.
(* Goal: @relative_defined_type composite l t0 *)
      induction t0; try solve [simpl; auto].
      * (* array *)
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
        spec IHt0; auto.
(* Goal: @relative_defined_type composite l (Tarray t0 z a) *)
        spec IHt0; [simpl in H1; omega |].
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
        auto.
      * (* struct *)
        simpl in H0, H1 |- *.
(* Goal: @In ident i1 (@map (prod ident composite) ident (@fst ident composite) l) *)
        destruct (cenv ! i1) eqn:?H; [| inv H0].
(* Goal: @In ident i1 (@map (prod ident composite) ident (@fst ident composite) l) *)
        specialize (H _ _ H2).
(* Goal: @In ident i1 (@map (prod ident composite) ident (@fst ident composite) l) *)
        spec H; [omega |].
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
        apply (in_map fst) in H; auto.
      * (* union *)
        simpl in H0, H1 |- *.
(* Goal: @In ident i1 (@map (prod ident composite) ident (@fst ident composite) l) *)
        destruct (cenv ! i1) eqn:?H; [| inv H0].
(* Goal: @In ident i1 (@map (prod ident composite) ident (@fst ident composite) l) *)
        specialize (H _ _ H2).
(* Goal: @In ident i1 (@map (prod ident composite) ident (@fst ident composite) l) *)
        spec H; [omega |].
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
        apply (in_map fst) in H; auto.
Qed.

End composite_reorder.

End composite_reorder.

Module type_func.
Section type_func.

(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
Context {A: Type}
        (f_default: type -> A)
        (f_array: A -> type -> Z -> attr -> A)
        (f_struct: A -> ident -> attr -> A)
        (f_union: A -> ident -> attr -> A)
        (f_member: struct_or_union -> list (ident * type * A) -> A).

Fixpoint F (env: PTree.t A) (t: type): A :=
  match t with
  | Tarray t n a => f_array (F env t) t n a
  | Tstruct id a =>
      match env ! id with
      | Some v => f_struct v id a
      | None => f_default t
      end
  | Tunion id a =>
      match env ! id with
      | Some v => f_union v id a
      | None => f_default t
      end
  | _ => f_default t
  end.

Definition Complete (cenv: composite_env) (env: PTree.t A): Prop :=
  forall i,
    (exists co, PTree.get i cenv = Some co) <->
    (exists a, PTree.get i env = Some a).

Definition Consistent (cenv: composite_env) (env: PTree.t A): Prop :=
  forall i co a,
    PTree.get i cenv = Some co ->
    PTree.get i env = Some a ->
    a = f_member (co_su co) (map
                              (fun it0: positive * type =>
                                 let (i0, t0) := it0 in
                                 (i0, t0, F env t0))
                              (co_members co)).

Definition env_rec (i: positive) (co: composite) (env: PTree.t A): PTree.t A :=
  PTree.set i
    (f_member (co_su co) (map
                              (fun it0: positive * type =>
                                 let (i0, t0) := it0 in (i0, t0, F env t0))
                              (co_members co)))
    env.

Definition Env (l: list (positive * composite)): PTree.t A :=
  fold_right
    (fun (ic: positive * composite) =>
       let (i, co) := ic in env_rec i co)
    (PTree.empty A)
    l.

Lemma F_PTree_set: forall t env i a,
  ~ In i (map fst (PTree.elements env)) ->
  relative_defined_type (PTree.elements env) t ->
  F env t = F (PTree.set i a env) t.
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
  induction t; auto.
  + simpl.
(* Goal: @eq A (f_array (F env t) t z a0) (f_array (F (@PTree.set A i a env) t) t z a0) *)
    apply IHt in H0.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    rewrite H0; auto.
  + simpl in H0 |- *.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    rewrite PTree.gso; auto.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    intro; subst; tauto.
  + simpl in H0 |- *.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    rewrite PTree.gso; auto.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    intro; subst; tauto.
Qed.

Lemma relative_defined_type_PTree_set: forall t (env: PTree.t A) i a,
  relative_defined_type (PTree.elements env) t ->
  relative_defined_type (PTree.elements (PTree.set i a env)) t.
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: @relative_defined_type A (@PTree.elements A (@PTree.set A i a env)) t *)
  revert H; apply relative_defined_type_mono.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
  intros; apply PTree_set_In_fst_elements; auto.
Qed.

Section Consistency_Induction_Step.

Context (cenv: composite_env)
        (env: PTree.t A)
        (l: list (positive * composite))
        (i0: positive)
        (co0: composite).

Hypothesis NOT_IN_LIST: ~ In i0 (map fst l).

Hypothesis RDT_list: Forall (relative_defined_type l) (map snd (co_members co0)).

Hypothesis CENV0: PTree.get i0 cenv = Some co0.

Hypothesis IH_In_equiv: forall i, In i (map fst l) <-> In i (map fst (PTree.elements env)).

Hypothesis IH_RDT:
  forall i co a,
    PTree.get i cenv = Some co ->
    PTree.get i env = Some a ->
    Forall (relative_defined_type (PTree.elements env)) (map snd (co_members co)).

Hypothesis IH_main:
  Consistent cenv env.

Lemma NOT_IN: ~ In i0 (map fst (PTree.elements env)).
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
  rewrite <- IH_In_equiv; auto.
Qed.

Lemma RDT_PTree: Forall (relative_defined_type (PTree.elements env)) (map snd (co_members co0)).
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: @Forall type (@relative_defined_type A (@PTree.elements A env)) (@map (prod ident type) type (@snd ident type) (co_members co0)) *)
  revert RDT_list; apply Forall_impl.
(* Goal: forall (a : type) (_ : @relative_defined_type composite l a), @relative_defined_type A (@PTree.elements A env) a *)
  intros t.
(* Goal: forall _ : @relative_defined_type composite l t, @relative_defined_type A (@PTree.elements A env) t *)
  apply relative_defined_type_mono.
(* Goal: forall (i : ident) (_ : @In ident i (@map (prod ident composite) ident (@fst ident composite) l)), @In ident i (@map (prod ident A) ident (@fst ident A) (@PTree.elements A env)) *)
  firstorder.
Qed.

Lemma establish_In_equiv:
  forall i, In i (map fst ((i0, co0) :: l)) <-> In i (map fst (PTree.elements (env_rec i0 co0 env))).
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (env_rec i0 co0 env)))) *)
  specialize (IH_In_equiv i).
  rewrite PTree_In_fst_elements in IH_In_equiv |- *.
(* Goal: iff (or (@eq positive i0 i) (@In positive i (@map (prod positive composite) positive (@fst positive composite) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (env_rec i0 co0 (Env l))))) *)
  unfold env_rec.
  rewrite <- PTree_gs_equiv.
(* Goal: iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (or (@ex A (fun a : A => @eq (option A) (@PTree.get A i env) (@Some A a))) (@eq positive i i0)) *)
  simpl In.
  assert (i0 = i <-> i = i0) by (split; intros; congruence).
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
  tauto.
Qed.

Lemma establish_RDT:
  forall i co a,
    PTree.get i cenv = Some co ->
    PTree.get i (env_rec i0 co0 env) = Some a ->
    Forall (relative_defined_type (PTree.elements (env_rec i0 co0 env))) (map snd (co_members co)).
Proof.
(* Goal: Consistent cenv (env_rec i0 co0 env) *)
  pose proof RDT_PTree as RDT_PTree.
(* Goal: Consistent cenv (env_rec i0 co0 env) *)
  intros i co a CENV ENV.
(* Goal: @eq A a (f_member (co_su co) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i1, t0) := it0 in @pair (prod positive type) A (@pair positive type i1 t0) (F (env_rec i0 co0 env) t0)) (co_members co))) *)
  unfold env_rec in ENV.
(* Goal: @eq A a (f_member (co_su co) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i1, t0) := it0 in @pair (prod positive type) A (@pair positive type i1 t0) (F (env_rec i0 co0 env) t0)) (co_members co))) *)
  destruct (Pos.eq_dec i i0).
  + subst i0; rewrite CENV in CENV0; inversion CENV0; subst co0; clear CENV0.
(* Goal: @eq A a (f_member (co_su co) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co))) *)
    rewrite PTree.gss in ENV.
(* Goal: @eq A a (f_member (co_su co) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co))) *)
    inversion ENV; clear a ENV H0.
(* Goal: @Forall type (@relative_defined_type A (@PTree.elements A (env_rec i co env))) (@map (prod ident type) type (@snd ident type) (co_members co)) *)
    revert RDT_PTree.
(* Goal: forall (a : type) (_ : @relative_defined_type composite l a), @relative_defined_type A (@PTree.elements A env) a *)
    apply Forall_impl; intros t.
(* Goal: forall _ : @relative_defined_type A (@PTree.elements A env) t, @relative_defined_type A (@PTree.elements A (env_rec i0 co0 env)) t *)
    apply relative_defined_type_PTree_set.
  + rewrite PTree.gso in ENV by auto.
(* Goal: @relative_defined_type A (@PTree.elements A env) t1 *)
    specialize (IH_RDT _ _ _ CENV ENV).
(* Goal: @Forall type (@relative_defined_type A (@PTree.elements A (env_rec i0 co0 env))) (@map (prod ident type) type (@snd ident type) (co_members co)) *)
    revert IH_RDT.
(* Goal: forall (a : type) (_ : @relative_defined_type composite l a), @relative_defined_type A (@PTree.elements A env) a *)
    apply Forall_impl; intros t.
(* Goal: forall _ : @relative_defined_type A (@PTree.elements A env) t, @relative_defined_type A (@PTree.elements A (env_rec i0 co0 env)) t *)
    apply relative_defined_type_PTree_set.
Qed.

Lemma establish_main:
  Consistent cenv (env_rec i0 co0 env).
Proof.
(* Goal: Consistent cenv (env_rec i0 co0 env) *)
  pose proof NOT_IN as NOT_IN.
(* Goal: Consistent cenv (env_rec i0 co0 env) *)
  pose proof RDT_PTree as RDT_PTree.
(* Goal: Consistent cenv (env_rec i0 co0 env) *)
  intros i co a CENV ENV.
(* Goal: @eq A a (f_member (co_su co) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i1, t0) := it0 in @pair (prod positive type) A (@pair positive type i1 t0) (F (env_rec i0 co0 env) t0)) (co_members co))) *)
  unfold env_rec in ENV.
(* Goal: @eq A a (f_member (co_su co) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i1, t0) := it0 in @pair (prod positive type) A (@pair positive type i1 t0) (F (env_rec i0 co0 env) t0)) (co_members co))) *)
  destruct (Pos.eq_dec i i0).
  + subst i0; rewrite CENV in CENV0; inversion CENV0; subst co0; clear CENV0.
(* Goal: @eq A a (f_member (co_su co) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co))) *)
    rewrite PTree.gss in ENV.
(* Goal: @eq A a (f_member (co_su co) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co))) *)
    inversion ENV; clear a ENV H0.
(* Goal: @eq (prod (prod positive type) A) (@pair (prod positive type) A (@pair positive type i1 t1) (F env t1)) (@pair (prod positive type) A (@pair positive type i1 t1) (F (env_rec i0 co0 env) t1)) *)
    f_equal.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    auto.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i1, t0) := it0 in @pair (prod positive type) A (@pair positive type i1 t0) (F (env_rec i0 co0 env) t0)) (co_members co)) *)
    apply map_ext_in.
(* Goal: forall (a : prod positive type) (_ : @In (prod positive type) a (co_members co)), @eq (prod (prod positive type) A) (let (i0, t0) := a in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (let (i1, t0) := a in @pair (prod positive type) A (@pair positive type i1 t0) (F (env_rec i0 co0 env) t0)) *)
    intros (i1, t1) ?.
(* Goal: @eq (prod (prod positive type) A) (@pair (prod positive type) A (@pair positive type i1 t1) (F env t1)) (@pair (prod positive type) A (@pair positive type i1 t1) (F (env_rec i0 co0 env) t1)) *)
    f_equal.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    apply F_PTree_set; auto.
(* Goal: @relative_defined_type A (@PTree.elements A env) t1 *)
    rewrite Forall_forall in RDT_PTree; apply RDT_PTree.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    apply (in_map snd) in H; auto.
  + rewrite PTree.gso in ENV by auto.
(* Goal: @eq A a (f_member (co_su co) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i1, t0) := it0 in @pair (prod positive type) A (@pair positive type i1 t0) (F (env_rec i0 co0 env) t0)) (co_members co))) *)
    specialize (IH_main _ _ _ CENV ENV).
(* Goal: @eq A a (f_member (co_su co) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i1, t0) := it0 in @pair (prod positive type) A (@pair positive type i1 t0) (F (env_rec i0 co0 env) t0)) (co_members co))) *)
    subst a.
(* Goal: @eq (prod (prod positive type) A) (@pair (prod positive type) A (@pair positive type i1 t1) (F env t1)) (@pair (prod positive type) A (@pair positive type i1 t1) (F (env_rec i0 co0 env) t1)) *)
    f_equal.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i1, t0) := it0 in @pair (prod positive type) A (@pair positive type i1 t0) (F (env_rec i0 co0 env) t0)) (co_members co)) *)
    apply map_ext_in.
(* Goal: forall (a : prod positive type) (_ : @In (prod positive type) a (co_members co)), @eq (prod (prod positive type) A) (let (i0, t0) := a in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (let (i1, t0) := a in @pair (prod positive type) A (@pair positive type i1 t0) (F (env_rec i0 co0 env) t0)) *)
    intros (i1, t1) ?.
(* Goal: @eq (prod (prod positive type) A) (@pair (prod positive type) A (@pair positive type i1 t1) (F env t1)) (@pair (prod positive type) A (@pair positive type i1 t1) (F (env_rec i0 co0 env) t1)) *)
    f_equal.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    apply F_PTree_set; auto.
(* Goal: @relative_defined_type A (@PTree.elements A env) t1 *)
    specialize (IH_RDT _ _ _ CENV ENV).
(* Goal: @relative_defined_type A (@PTree.elements A env) t1 *)
    rewrite Forall_forall in IH_RDT; apply IH_RDT.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    apply (in_map snd) in H; auto.
Qed.

End Consistency_Induction_Step.

Lemma Consistency: forall cenv l,
  Permutation l (PTree.elements cenv) ->
  ordered_composite l ->
  Consistent cenv (Env l).
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
  assert (forall i co, In (i, co) l -> PTree.get i cenv = Some co).
(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
  {
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
    intros.
(* Goal: @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
    apply PTree.elements_complete.
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i T) (@Some A a)) *)
    eapply Permutation_in; eauto.
  }
(* Goal: Consistent cenv (Env l) *)
  assert (NoDup (map fst l)).
(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
  {
(* Goal: @NoDup positive (@map (prod positive composite) positive (@fst positive composite) l) *)
    eapply Permutation_NoDup; [symmetry; apply Permutation_map; eassumption |].
    rewrite <- list_norepet_NoDup.
(* Goal: @list_norepet positive (@map (prod positive composite) positive (@fst positive composite) (@PTree.elements composite cenv)) *)
    apply PTree.elements_keys_norepet.
  }
(* Goal: Consistent cenv (Env l) *)
  clear H.
  assert (
    (forall i, In i (map fst l) <-> In i (map fst (PTree.elements (Env l)))) /\
    (forall i co a,
      PTree.get i cenv = Some co ->
      PTree.get i (Env l) = Some a ->
      Forall (relative_defined_type (PTree.elements (Env l))) (map snd (co_members co))) /\
    Consistent cenv (Env l)); [| tauto].
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) l)) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env l))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env l)) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env l))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env l))) *)
  induction l as [| [i0 co0] l].
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  + split; [| split]; hnf; intros.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    - simpl; tauto.
    - unfold Env in H3; simpl in H3.
(* Goal: @eq A a (f_member (co_su co) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (Env (@nil (prod positive composite))) t0)) (co_members co))) *)
      rewrite PTree.gempty in H3; inv H3.
    - unfold Env in H3; simpl in H3.
(* Goal: @eq A a (f_member (co_su co) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (Env (@nil (prod positive composite))) t0)) (co_members co))) *)
      rewrite PTree.gempty in H3; inv H3.
  + inv H0.
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
    rename H4 into RDT_list; specialize (IHl H6); clear H6.
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
    assert (CENV0: PTree.get i0 cenv = Some co0).
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    { apply H1; left; auto. }
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
    spec IHl; [| clear H1].
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    { intros; apply H1; right; auto. } 
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
    inv H2.
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
    rename H1 into NOT_IN_LIST; specialize (IHl H3); clear H3.
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
    destruct IHl as [IH_In_equiv [IH_RDT IH_main]].
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
    split; [| split].
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    - apply establish_In_equiv; auto.
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i T) (@Some A a)) *)
    - eapply establish_RDT; eauto.
(* Goal: @ex A (fun a : A => @eq (option A) (@PTree.get A i T) (@Some A a)) *)
    - eapply establish_main; eauto.
Qed.

Lemma Completeness: forall cenv l,
  Permutation l (PTree.elements cenv) ->
  Complete cenv (Env l).
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: Complete cenv (Env l) *)
  intro.
  rewrite <- !PTree_In_fst_elements.
(* Goal: iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@PTree.elements composite cenv))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env l)))) *)
  pose proof PTree.elements_keys_norepet cenv.
(* Goal: iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@PTree.elements composite cenv))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env l)))) *)
  rewrite list_norepet_NoDup in H0.
(* Goal: Consistent cenv (Env l) *)
  rewrite <- H in H0 |- *; clear H.
(* Goal: iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) l)) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env l)))) *)
  induction l.
  + simpl; tauto.
  + destruct a as [i0 co0].
(* Goal: iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))))) *)
    inv H0.
(* Goal: iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))))) *)
    specialize (IHl H3).
(* Goal: iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))))) *)
    simpl.
(* Goal: iff (or (@eq positive i0 i) (@In positive i (@map (prod positive composite) positive (@fst positive composite) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (env_rec i0 co0 (Env l))))) *)
    unfold env_rec.
    rewrite PTree_In_fst_elements, <- PTree_gs_equiv, <- PTree_In_fst_elements.
    assert (i = i0 <-> i0 = i) by (split; intros; congruence).
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    tauto.
Qed.

End type_func.

End type_func.

(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
Corollary composite_reorder_consistent {A: Type}:
  forall cenv f_default f_array f_struct f_union f_members,
    composite_env_consistent cenv ->
    type_func.Consistent f_default f_array f_struct f_union f_members cenv (@type_func.Env A f_default f_array f_struct f_union f_members (composite_reorder.rebuild_composite_elements cenv)).
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: @type_func.Consistent A f_default f_array f_struct f_union f_members cenv (@type_func.Env A f_default f_array f_struct f_union f_members (composite_reorder.rebuild_composite_elements cenv)) *)
  apply type_func.Consistency.
  + apply composite_reorder.RCT_Permutation.
  + apply composite_reorder.RCT_ordered; auto.
Qed.

(* Goal: forall (i : positive) (co : composite) (_ : @In (prod positive composite) (@pair positive composite i co) l), @eq (option composite) (@PTree.get composite i cenv) (@Some composite co) *)
(* Goal: and (forall i : positive, iff (@In positive i (@map (prod positive composite) positive (@fst positive composite) (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@In positive i (@map (prod positive A) positive (@fst positive A) (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))))) (and (forall (i : positive) (co : composite) (a : A) (_ : @eq (option composite) (@PTree.get composite i cenv) (@Some composite co)) (_ : @eq (option A) (@PTree.get A i (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l))) (@Some A a)), @Forall type (@relative_defined_type A (@PTree.elements A (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) (@map (prod ident type) type (@snd ident type) (co_members co))) (Consistent cenv (Env (@cons (prod positive composite) (@pair positive composite i0 co0) l)))) *)
Corollary composite_reorder_complete {A: Type}:
  forall cenv f_default f_array f_struct f_union f_members,
    type_func.Complete cenv (@type_func.Env A f_default f_array f_struct f_union f_members (composite_reorder.rebuild_composite_elements cenv)).
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: @type_func.Complete A cenv (@type_func.Env A f_default f_array f_struct f_union f_members (composite_reorder.rebuild_composite_elements cenv)) *)
  apply type_func.Completeness.
(* Goal: @Permutation (prod positive composite) (composite_reorder.rebuild_composite_elements cenv) (@PTree.elements composite cenv) *)
  apply composite_reorder.RCT_Permutation.
Qed.

Section cuof.

Context (cenv: composite_env).

Fixpoint complete_legal_cosu_type t :=
  match t with
  | Tarray t' _ _ => complete_legal_cosu_type t'
  | Tstruct id _ => match cenv ! id with
                    | Some co => match co_su co with
                                 | Struct => true
                                 | Union => false
                                 end
                    | _ => false
                    end
  | Tunion id _ => match cenv ! id with
                   | Some co => match co_su co with
                                | Struct => false
                                | Union => true
                                end
                   | _ => false
                   end
  | Tfunction _ _ _
  | Tvoid => false
  | _ => true
  end.

Fixpoint composite_complete_legal_cosu_type (m: members): bool :=
  match m with
  | nil => true
  | (_, t) :: m' => complete_legal_cosu_type t && composite_complete_legal_cosu_type m'
  end.

Definition composite_env_complete_legal_cosu_type: Prop :=
  forall (id : positive) (co : composite),
    cenv ! id = Some co -> composite_complete_legal_cosu_type (co_members co) = true.
  
End cuof.

Lemma complete_legal_cosu_type_complete_type: forall cenv: composite_env,
  forall t,
    complete_legal_cosu_type cenv t = true ->
    complete_type cenv t = true.
Proof.
(* Goal: forall (cenv : composite_env) (t : type) (_ : @eq bool (complete_legal_cosu_type cenv t) true), @eq bool (complete_type cenv t) true *)
  intros.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
  induction t; auto.
  + simpl in *.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    destruct (cenv ! i); auto.
  + simpl in *.
(* Goal: @eq (list (prod (prod positive type) A)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F env t0)) (co_members co)) (@map (prod positive type) (prod (prod positive type) A) (fun it0 : prod positive type => let (i0, t0) := it0 in @pair (prod positive type) A (@pair positive type i0 t0) (F (env_rec i co env) t0)) (co_members co)) *)
    destruct (cenv ! i); auto.
Qed.

