Require Import VST.veric.base.
Require Import compcert.cfrontend.Ctypes.

Section COMPOSITE_ENV.

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

Lemma type_ind: forall P : type -> Prop,
  (forall t,
  match t with
  | Tarray t0 _ _ => P t0
  | Tstruct id _ 
  | Tunion id _ => match cenv ! id with
                    | Some co => Forall (Basics.compose P snd) (co_members co)
                    | _ => True
                    end
  | _ => True
  end -> P t) ->
  forall t, P t.
Proof.
(* Goal: forall (P : forall _ : type, Prop) (_ : forall (t : type) (_ : match t with | Tvoid => True | Tint i s a => True | Tlong s a => True | Tfloat f a => True | Tpointer t0 a => True | Tarray t0 z a => P t0 | Tfunction t0 t1 c => True | Tstruct id a => match @PTree.get composite id cenv with | Some co => @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (co_members co) | None => True end | Tunion id a => match @PTree.get composite id cenv with | Some co => @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (co_members co) | None => True end end), P t) (t : type), P t *)
  intros P IH_TYPE.
(* Goal: forall t : type, P t *)
  intros.
(* Goal: P t *)
  remember (rank_type cenv t) as n eqn: RANK'.
(* Goal: P t *)
  assert (rank_type cenv t <= n)%nat as RANK.
(* Goal: le (rank_type cenv t) n *)
(* Goal: P t *)
  subst. apply le_n.
(* Goal: P t *)
  clear RANK'.
(* Goal: P t *)
  revert t RANK.
  induction n;
  intros;
  specialize (IH_TYPE t); destruct t;
  try solve [specialize (IH_TYPE I); auto].
  + (* Tarray level 0 *)
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    simpl in RANK. inv RANK.
  + (* Tstruct level 0 *)
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    simpl in RANK.
(* Goal: P (Tstruct i a) *)
    destruct (cenv ! i); [inv RANK | apply IH_TYPE; simpl; constructor].
  + (* Tunion level 0 *)
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    simpl in RANK.
(* Goal: P (Tunion i a) *)
    destruct (cenv ! i); [inv RANK | apply IH_TYPE].
(* Goal: True *)
    simpl; constructor.
  + (* Tarray level positive *)
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    simpl in RANK.
(* Goal: P (Tarray t z a) *)
    specialize (IHn t).
(* Goal: P (Tarray t z a) *)
    apply IH_TYPE, IHn.
(* Goal: le (rank_type cenv t) n *)
    apply le_S_n; auto.
  + (* Tstruct level positive *)
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    simpl in RANK.
(* Goal: P (Tunion i a) *)
    destruct (cenv ! i) as [co |] eqn:CO; auto.
(* Goal: P (Tunion i a) *)
    apply IH_TYPE; clear IH_TYPE.
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (co_members co) *)
    erewrite co_consistent_rank in RANK by (eapply cenv_consistent; eauto).
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (co_members co) *)
    clear - RANK IHn; induction (co_members co) as [| [i t] ?]; auto.
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    simpl in RANK.
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    pose proof Max.le_max_l (rank_type cenv t) (rank_members cenv m).
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    pose proof Max.le_max_r (rank_type cenv t) (rank_members cenv m).
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    constructor.
    - apply IHn; simpl; omega.
    - apply IHm; omega.
  + (* Tunion level positive *)
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    simpl in RANK.
(* Goal: P (Tunion i a) *)
    destruct (cenv ! i) as [co |] eqn:CO; auto.
(* Goal: P (Tunion i a) *)
    apply IH_TYPE; clear IH_TYPE.
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (co_members co) *)
    erewrite co_consistent_rank in RANK by (eapply cenv_consistent; eauto).
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (co_members co) *)
    clear - RANK IHn; induction (co_members co) as [| [i t] ?]; auto.
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    simpl in RANK.
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    pose proof Max.le_max_l (rank_type cenv t) (rank_members cenv m).
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    pose proof Max.le_max_r (rank_type cenv t) (rank_members cenv m).
(* Goal: @Forall (prod ident type) (@Basics.compose (prod ident type) type Prop P (@snd ident type)) (@cons (prod ident type) (@pair ident type i t) m) *)
    constructor.
    - apply IHn; simpl; omega.
    - apply IHm; omega.
Defined.

End COMPOSITE_ENV.

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