Require Import VST.floyd.base2.
Require Import VST.floyd.client_lemmas.
Require Import VST.floyd.type_induction.
Require Import VST.floyd.fieldlist.
Open Scope Z.

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

Definition, lemmas and useful samples of nested_pred

nested_pred only ensure the specific property to be true on nested types with
memory assigned, i.e. inside structure of pointer, function, empty array are
not included.

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

Lemma fold_right_map: forall {A B C} (f: B -> A -> A) (g: C -> B) (e: A) (l: list C),
  fold_right f e (map g l) = fold_right (fun c a => f (g c) a) e l.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: @eq A (@fold_right A B f e (@map C B g l)) (@fold_right A C (fun (c : C) (a : A) => f (g c) a) e l) *)
  induction l.
  + reflexivity.
  + simpl.
(* Goal: @eq A (f (g a) (@fold_right A B f e (@map C B g l))) (f (g a) (@fold_right A C (fun (c : C) (a : A) => f (g c) a) e l)) *)
    rewrite IHl.
(* Goal: @eq bool (@fold_right bool (prod ident type) (fun (c : prod ident type) (a : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a0 : attr) (b : bool) => andb (atom_pred (Tarray t n a0)) b) (fun (id : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type c) (co_members (@get_co cs i)))) a) true (co_members (@get_co cs i))) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a : attr) (b0 : bool) => andb (atom_pred (Tarray t n a)) b0) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs i)))) b) true (co_members (@get_co cs i))) *)
    reflexivity.
Qed.

Section NESTED_PRED.
Context {cs: compspecs}.

Definition nested_pred (atom_pred: type -> bool): type -> bool :=
  type_func
    (fun _ => bool)
    (fun t => atom_pred t)
    (fun t n a b => (atom_pred (Tarray t n a) && b)%bool)
    (fun id a bl => (atom_pred (Tstruct id a) && fold_right andb true (decay bl))%bool)
    (fun id a bl => (atom_pred (Tunion id a) && fold_right andb true (decay bl))%bool).

Definition nested_fields_pred (atom_pred: type -> bool) (m: members) : bool :=
  fold_right (fun it b => (nested_pred atom_pred (field_type (fst it) m) && b)%bool) true m.

Lemma nested_pred_eq: forall atom_pred t,
  nested_pred atom_pred t =
  match t with
  | Tarray t0 _ _ => (atom_pred t && nested_pred atom_pred t0)%bool
  | Tstruct id _
  | Tunion id _ => (atom_pred t && nested_fields_pred atom_pred (co_members (get_co id)))%bool
  | _ => atom_pred t
  end.
Proof.
(* Goal: forall (atom_pred : forall _ : type, bool) (t : type), @eq bool (nested_pred atom_pred t) match t with | Tvoid => atom_pred t | Tint i s a => atom_pred t | Tlong s a => atom_pred t | Tfloat f a => atom_pred t | Tpointer t0 a => atom_pred t | Tarray t0 z a => andb (atom_pred t) (nested_pred atom_pred t0) | Tfunction t0 t1 c => atom_pred t | Tstruct id a => andb (atom_pred t) (nested_fields_pred atom_pred (co_members (@get_co cs id))) | Tunion id a => andb (atom_pred t) (nested_fields_pred atom_pred (co_members (@get_co cs id))) end *)
  unfold nested_fields_pred.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: @eq bool (nested_pred atom_pred t) match t with | Tvoid => atom_pred t | Tint i s a => atom_pred t | Tlong s a => atom_pred t | Tfloat f a => atom_pred t | Tpointer t0 a => atom_pred t | Tarray t0 z a => andb (atom_pred t) (nested_pred atom_pred t0) | Tfunction t0 t1 c => atom_pred t | Tstruct id a => andb (atom_pred t) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (nested_pred atom_pred (field_type (@fst ident type it) (co_members (@get_co cs id)))) b) true (co_members (@get_co cs id))) | Tunion id a => andb (atom_pred t) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (nested_pred atom_pred (field_type (@fst ident type it) (co_members (@get_co cs id)))) b) true (co_members (@get_co cs id))) end *)
  unfold nested_pred.
(* Goal: @eq bool (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a : attr) (b : bool) => andb (atom_pred (Tarray t n a)) b) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) t) match t with | Tvoid => atom_pred t | Tint i s a => atom_pred t | Tlong s a => atom_pred t | Tfloat f a => atom_pred t | Tpointer t0 a => atom_pred t | Tarray t0 z a => andb (atom_pred t) (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a0 : attr) (b : bool) => andb (atom_pred (Tarray t n a0)) b) (fun (id : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) t0) | Tfunction t0 t1 c => atom_pred t | Tstruct id a => andb (atom_pred t) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a0 : attr) (b0 : bool) => andb (atom_pred (Tarray t n a0)) b0) (fun (id0 : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id0) => andb (atom_pred (Tstruct id0 a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id0)) bl))) (fun (id0 : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id0) => andb (atom_pred (Tunion id0 a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id0)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs id)))) b) true (co_members (@get_co cs id))) | Tunion id a => andb (atom_pred t) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a0 : attr) (b0 : bool) => andb (atom_pred (Tarray t n a0)) b0) (fun (id0 : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id0) => andb (atom_pred (Tstruct id0 a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id0)) bl))) (fun (id0 : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id0) => andb (atom_pred (Tunion id0 a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id0)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs id)))) b) true (co_members (@get_co cs id))) end *)
  rewrite type_func_eq with (t0 := t) (A := (fun _ => bool)) at 1 by auto.
(* Goal: @eq bool match t with | Tvoid => atom_pred Tvoid | Tint i s a => atom_pred (Tint i s a) | Tlong s a => atom_pred (Tlong s a) | Tfloat f a => atom_pred (Tfloat f a) | Tpointer t a => atom_pred (Tpointer t a) | Tarray t0 n a => andb (atom_pred (Tarray t0 n a)) (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n0 : Z) (a0 : attr) (b : bool) => andb (atom_pred (Tarray t n0 a0)) b) (fun (id : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) t0) | Tfunction t t0 c => atom_pred (Tfunction t t0 c) | Tstruct id a => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) (@FTI_aux cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a0 : attr) (b : bool) => andb (atom_pred (Tarray t n a0)) b) (fun (id0 : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id0) => andb (atom_pred (Tstruct id0 a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id0)) bl))) (fun (id0 : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id0) => andb (atom_pred (Tunion id0 a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id0)) bl))) id))) | Tunion id a => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) (@FTI_aux cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a0 : attr) (b : bool) => andb (atom_pred (Tarray t n a0)) b) (fun (id0 : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id0) => andb (atom_pred (Tstruct id0 a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id0)) bl))) (fun (id0 : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id0) => andb (atom_pred (Tunion id0 a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id0)) bl))) id))) end match t with | Tvoid => atom_pred t | Tint i s a => atom_pred t | Tlong s a => atom_pred t | Tfloat f a => atom_pred t | Tpointer t0 a => atom_pred t | Tarray t0 z a => andb (atom_pred t) (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a0 : attr) (b : bool) => andb (atom_pred (Tarray t n a0)) b) (fun (id : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) t0) | Tfunction t0 t1 c => atom_pred t | Tstruct id a => andb (atom_pred t) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a0 : attr) (b0 : bool) => andb (atom_pred (Tarray t n a0)) b0) (fun (id0 : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id0) => andb (atom_pred (Tstruct id0 a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id0)) bl))) (fun (id0 : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id0) => andb (atom_pred (Tunion id0 a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id0)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs id)))) b) true (co_members (@get_co cs id))) | Tunion id a => andb (atom_pred t) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a0 : attr) (b0 : bool) => andb (atom_pred (Tarray t n a0)) b0) (fun (id0 : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id0) => andb (atom_pred (Tstruct id0 a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id0)) bl))) (fun (id0 : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id0) => andb (atom_pred (Tunion id0 a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id0)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs id)))) b) true (co_members (@get_co cs id))) end *)
  destruct t; auto.
  + f_equal. unfold FTI_aux.
(* Goal: @eq bool (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs i)) (@ListTypeGen (prod ident type) (fun _ : prod ident type => bool) (fun it : prod ident type => @type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a : attr) (b : bool) => andb (atom_pred (Tarray t n a)) b) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs i)))) (co_members (@get_co cs i))))) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a : attr) (b0 : bool) => andb (atom_pred (Tarray t n a)) b0) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs i)))) b) true (co_members (@get_co cs i))) *)
    rewrite decay_spec.
(* Goal: @eq bool (@fold_right bool bool andb true (@map (prod ident type) bool (fun it : prod ident type => @type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a : attr) (b : bool) => andb (atom_pred (Tarray t n a)) b) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs i)))) (co_members (@get_co cs i)))) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a : attr) (b0 : bool) => andb (atom_pred (Tarray t n a)) b0) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs i)))) b) true (co_members (@get_co cs i))) *)
    rewrite fold_right_map.
(* Goal: @eq bool (@fold_right bool (prod ident type) (fun (c : prod ident type) (a : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a0 : attr) (b : bool) => andb (atom_pred (Tarray t n a0)) b) (fun (id : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type c) (co_members (@get_co cs i)))) a) true (co_members (@get_co cs i))) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a : attr) (b0 : bool) => andb (atom_pred (Tarray t n a)) b0) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs i)))) b) true (co_members (@get_co cs i))) *)
    reflexivity.
  + f_equal. unfold FTI_aux.
(* Goal: @eq bool (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs i)) (@ListTypeGen (prod ident type) (fun _ : prod ident type => bool) (fun it : prod ident type => @type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a : attr) (b : bool) => andb (atom_pred (Tarray t n a)) b) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs i)))) (co_members (@get_co cs i))))) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a : attr) (b0 : bool) => andb (atom_pred (Tarray t n a)) b0) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs i)))) b) true (co_members (@get_co cs i))) *)
    rewrite decay_spec.
(* Goal: @eq bool (@fold_right bool bool andb true (@map (prod ident type) bool (fun it : prod ident type => @type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a : attr) (b : bool) => andb (atom_pred (Tarray t n a)) b) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs i)))) (co_members (@get_co cs i)))) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a : attr) (b0 : bool) => andb (atom_pred (Tarray t n a)) b0) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs i)))) b) true (co_members (@get_co cs i))) *)
    rewrite fold_right_map.
(* Goal: @eq bool (@fold_right bool (prod ident type) (fun (c : prod ident type) (a : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a0 : attr) (b : bool) => andb (atom_pred (Tarray t n a0)) b) (fun (id : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a0 : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a0)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type c) (co_members (@get_co cs i)))) a) true (co_members (@get_co cs i))) (@fold_right bool (prod ident type) (fun (it : prod ident type) (b : bool) => andb (@type_func cs (fun _ : type => bool) (fun t : type => atom_pred t) (fun (t : type) (n : Z) (a : attr) (b0 : bool) => andb (atom_pred (Tarray t n a)) b0) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tstruct id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (fun (id : positive) (a : attr) (bl : @FT_aux cs (fun _ : type => bool) id) => andb (atom_pred (Tunion id a)) (@fold_right bool bool andb true (@decay (prod ident type) bool (co_members (@get_co cs id)) bl))) (field_type (@fst ident type it) (co_members (@get_co cs i)))) b) true (co_members (@get_co cs i))) *)
    reflexivity.
Defined.

Lemma nested_pred_atom_pred: forall (atom_pred: type -> bool) (t: type),
  nested_pred atom_pred t = true -> atom_pred t = true.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: @eq bool (nested_fields_pred atom_pred (co_members (@get_co cs id))) true *)
  rewrite nested_pred_eq in H by auto.
  destruct t; simpl in *;
(* Goal: in_members i m *)
  try apply andb_true_iff in H; try tauto.
Defined.

Lemma nested_fields_pred_nested_pred: forall (atom_pred: type -> bool) i m, in_members i m -> nested_fields_pred atom_pred m = true -> nested_pred atom_pred (field_type i m) = true.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: @eq bool (nested_pred atom_pred (field_type i m)) true *)
  unfold nested_fields_pred in H0.
(* Goal: @eq bool (nested_pred atom_pred (field_type i m)) true *)
  rewrite <- fold_right_map in H0.
(* Goal: @eq bool (nested_pred atom_pred (field_type i m)) true *)
  eapply fold_right_andb; [exact H0 |].
(* Goal: @In bool (nested_pred atom_pred (field_type i m)) (@map (prod ident type) bool (fun c : prod ident type => nested_pred atom_pred (field_type (@fst ident type c) m)) m) *)
  clear - H.
(* Goal: @In bool (nested_pred atom_pred (field_type i m)) (@map (prod ident type) bool (fun c : prod ident type => nested_pred atom_pred (field_type (@fst ident type c) m)) m) *)
  rewrite <- map_map.
(* Goal: @In type ((fun it : prod ident type => field_type (@fst ident type it) m) (@pair ident type i (field_type i m))) (@map (prod ident type) type (fun x : prod ident type => field_type (@fst ident type x) m) m) *)
  apply in_map.
(* Goal: @In type (field_type i m) (@map (prod ident type) type (fun x : prod ident type => field_type (@fst ident type x) m) m) *)
  change (field_type i m) with ((fun it => field_type (fst it) m) (i, field_type i m)).
(* Goal: @In type ((fun it : prod ident type => field_type (@fst ident type it) m) (@pair ident type i (field_type i m))) (@map (prod ident type) type (fun x : prod ident type => field_type (@fst ident type x) m) m) *)
  apply in_map.
(* Goal: @In (prod ident type) (@pair ident type i (field_type i m)) m *)
  apply in_members_field_type.
(* Goal: in_members i m *)
  auto.
Defined.

Lemma nested_pred_Tarray: forall (atom_pred: type -> bool) t n a,
  nested_pred atom_pred (Tarray t n a) = true -> nested_pred atom_pred t = true.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: @eq bool (nested_fields_pred atom_pred (co_members (@get_co cs id))) true *)
  rewrite nested_pred_eq in H by auto.
(* Goal: @eq bool (nested_pred atom_pred t) true *)
  apply andb_true_iff in H.
(* Goal: in_members i m *)
  tauto.
Defined.

Lemma nested_pred_Tstruct: forall (atom_pred: type -> bool) id a,
  nested_pred atom_pred (Tstruct id a) = true -> nested_fields_pred atom_pred (co_members (get_co id)) = true.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: @eq bool (nested_fields_pred atom_pred (co_members (@get_co cs id))) true *)
  rewrite nested_pred_eq in H by auto.
(* Goal: in_members i m *)
  apply andb_true_iff in H; tauto.
Defined.

Lemma nested_pred_Tstruct2: forall (atom_pred: type -> bool) id a i,
  nested_pred atom_pred (Tstruct id a) = true ->
  in_members i (co_members (get_co id)) ->
  nested_pred atom_pred (field_type i (co_members (get_co id))) = true.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: @eq bool (nested_pred atom_pred (field_type i (co_members (@get_co cs id)))) true *)
  apply nested_pred_Tstruct in H.
(* Goal: in_members i m *)
  apply nested_fields_pred_nested_pred; auto.
Qed.

Lemma nested_pred_Tunion: forall (atom_pred: type -> bool) id a,
  nested_pred atom_pred (Tunion id a) = true -> nested_fields_pred atom_pred (co_members (get_co id)) = true.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: @eq bool (nested_fields_pred atom_pred (co_members (@get_co cs id))) true *)
  rewrite nested_pred_eq in H by auto.
(* Goal: in_members i m *)
  apply andb_true_iff in H; tauto.
Defined.

Lemma nested_pred_Tunion2: forall (atom_pred: type -> bool) id a i,
  nested_pred atom_pred (Tunion id a) = true ->
  in_members i (co_members (get_co id)) ->
  nested_pred atom_pred (field_type i (co_members (get_co id))) = true.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: @eq bool (nested_pred atom_pred (field_type i (co_members (@get_co cs id)))) true *)
  apply nested_pred_Tunion in H.
(* Goal: in_members i m *)
  apply nested_fields_pred_nested_pred; auto.
Qed.

Lemma complete_legal_cosu_type_Tstruct: forall id a,
  complete_legal_cosu_type (Tstruct id a) = true ->
  co_su (get_co id) = Struct.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: or (@eq Z (@sizeof (@cenv_cs cs) t) Z0) (Z.le n Z0) *)
  simpl in H.
(* Goal: @eq struct_or_union (co_su (@get_co cs id)) Union *)
  unfold get_co.
(* Goal: in_members i m *)
  destruct (cenv_cs ! id); auto.
(* Goal: @eq struct_or_union (co_su c) Union *)
  destruct (co_su c); congruence.
Qed.

Lemma complete_legal_cosu_type_Tunion: forall id a,
  complete_legal_cosu_type (Tunion id a) = true ->
  co_su (get_co id) = Union.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: or (@eq Z (@sizeof (@cenv_cs cs) t) Z0) (Z.le n Z0) *)
  simpl in H.
(* Goal: @eq struct_or_union (co_su (@get_co cs id)) Union *)
  unfold get_co.
(* Goal: @eq struct_or_union (co_su match @PTree.get composite id (@cenv_cs cs) with | Some co => co | None => co_default Struct end) Union *)
  destruct (cenv_cs ! id); auto; try congruence.
(* Goal: @eq struct_or_union (co_su c) Union *)
  destruct (co_su c); congruence.
Qed.

Lemma Tarray_sizeof_0: forall t n a,
  sizeof (Tarray t n a) = 0 ->
  sizeof t = 0 \/ n <= 0.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: or (@eq Z (@sizeof (@cenv_cs cs) t) Z0) (Z.le n Z0) *)
  simpl in H.
(* Goal: or (@eq Z (@sizeof (@cenv_cs cs) t) Z0) (Z.le n Z0) *)
  apply Z.eq_mul_0 in H.
(* Goal: in_members i m *)
  destruct H; auto.
(* Goal: or (@eq Z (@sizeof (@cenv_cs cs) t) Z0) (Z.le n Z0) *)
  right.
(* Goal: Z.le n Z0 *)
  destruct (zlt 0 n); [| omega].
(* Goal: Z.le n Z0 *)
  rewrite Z.max_r in H by omega.
(* Goal: @eq Z (sizeof_union (@cenv_cs cs) (co_members (@get_co cs id))) Z0 *)
  omega.
Qed.

Lemma Tstruct_sizeof_0: forall id a,
  complete_legal_cosu_type (Tstruct id a) = true ->
  sizeof (Tstruct id a) = 0 ->
  forall i, in_members i (co_members (get_co id)) ->
  sizeof (field_type i (co_members (get_co id))) = 0 /\
  field_offset_next cenv_cs i (co_members (get_co id)) (co_sizeof (get_co id)) -
   (field_offset cenv_cs i (co_members (get_co id)) +
      sizeof (field_type i (co_members (get_co id)))) = 0.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: and (@eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0) (@eq Z (Z.sub (field_offset_next (@cenv_cs cs) i (co_members (@get_co cs id)) (co_sizeof (@get_co cs id))) (Z.add (field_offset (@cenv_cs cs) i (co_members (@get_co cs id))) (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))))) Z0) *)
  rewrite sizeof_Tstruct in H0.
(* Goal: and (@eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0) (@eq Z (Z.sub (field_offset_next (@cenv_cs cs) i (co_members (@get_co cs id)) (co_sizeof (@get_co cs id))) (Z.add (field_offset (@cenv_cs cs) i (co_members (@get_co cs id))) (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))))) Z0) *)
  rewrite H0.
(* Goal: in_members i m *)
  apply sizeof_struct_0; auto.
(* Goal: @eq Z (sizeof_union (@cenv_cs cs) (co_members (@get_co cs id))) Z0 *)
  pose proof co_consistent_sizeof cenv_cs (get_co id) (get_co_consistent id).
(* Goal: in_members i m *)
  erewrite complete_legal_cosu_type_Tstruct in H2 by eauto.
(* Goal: @eq Z (sizeof_union (@cenv_cs cs) (co_members (@get_co cs id))) Z0 *)
  simpl in H2.
  pose proof align_le (sizeof_struct cenv_cs 0 (co_members (get_co id)))
     (co_alignof (get_co id)) (co_alignof_pos _).
(* Goal: @eq Z (sizeof_struct (@cenv_cs cs) Z0 (co_members (@get_co cs id))) Z0 *)
  pose proof sizeof_struct_incr cenv_cs (co_members (get_co id)) 0.
(* Goal: @eq Z (sizeof_union (@cenv_cs cs) (co_members (@get_co cs id))) Z0 *)
  omega.
Qed.

Lemma Tunion_sizeof_0: forall id a,
  complete_legal_cosu_type (Tunion id a) = true ->
  sizeof (Tunion id a) = 0 ->
  forall i, in_members i (co_members (get_co id)) ->
  sizeof (field_type i (co_members (get_co id))) = 0.
Proof.
(* Goal: forall (id : ident) (a : attr) (_ : @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (Tunion id a)) true) (_ : @eq Z (@sizeof (@cenv_cs cs) (Tunion id a)) Z0) (i : ident) (_ : in_members i (co_members (@get_co cs id))), @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  intros.
(* Goal: @eq Z (@sizeof (@cenv_cs cs) (field_type i (co_members (@get_co cs id)))) Z0 *)
  rewrite sizeof_Tunion in H0.
(* Goal: in_members i m *)
  apply sizeof_union_0; auto.
(* Goal: @eq Z (sizeof_union (@cenv_cs cs) (co_members (@get_co cs id))) Z0 *)
  pose proof co_consistent_sizeof cenv_cs (get_co id) (get_co_consistent id).
(* Goal: in_members i m *)
  erewrite complete_legal_cosu_type_Tunion in H2 by eauto.
(* Goal: @eq Z (sizeof_union (@cenv_cs cs) (co_members (@get_co cs id))) Z0 *)
  simpl in H2.
  pose proof align_le (sizeof_union cenv_cs (co_members (get_co id)))
     (co_alignof (get_co id)) (co_alignof_pos _).
(* Goal: @eq Z (sizeof_union (@cenv_cs cs) (co_members (@get_co cs id))) Z0 *)
  pose proof sizeof_union_pos cenv_cs (co_members (get_co id)).
(* Goal: @eq Z (sizeof_union (@cenv_cs cs) (co_members (@get_co cs id))) Z0 *)
  omega.
Qed.

End NESTED_PRED.

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

Arithmetic properties with nested_pred assumption.

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

Ltac pose_mod_le A :=
  let H := fresh "H" in
  pose proof Z.mod_le A Ptrofs.modulus;
  spec H; [try omega | spec H; [pose Ptrofs.modulus_pos; omega |]].

Ltac pose_mul_distr_l l r :=
  match r with
  | (?A + ?B)%Z => pose proof Z.mul_add_distr_l l A B;
                   pose_mul_distr_l l A;
                   pose_mul_distr_l l B
  | Z.succ ?A => let H := fresh "H" in
                 pose proof Z.mul_add_distr_l l A 1 as H;
                 replace (A + 1) with (Z.succ A) in H by omega;
                 pose_mul_distr_l l A
  | (?A - ?B)%Z => pose proof Z.mul_sub_distr_l l A B;
                   pose_mul_distr_l l A;
                   pose_mul_distr_l l B
  | _ => idtac
  end.


Ltac pose_size_mult' env t l :=
  match l with
  | nil => idtac
  | ?z :: ?l0 =>
    match l0 with
    | nil => pose_mul_distr_l (@sizeof env t) z
    | ?z0 :: _ => pose_mul_distr_l (@sizeof env t) z;
                  assert (@sizeof env t * z <= @sizeof env t * z0) by
                    (pose proof @sizeof_pos env t; apply Zmult_le_compat_l; omega);
                  pose_size_mult' env t l0
    end
  end.

Ltac pose_size_mult env t l :=
  pose_size_mult' env t l;
  try rewrite !Z.mul_0_r in *;
  try rewrite !Z.mul_1_r in *.

Definition align_alignof a b := align a b.

Definition sizeof_struct_le := sizeof_struct.

Ltac pose_align_le :=
  repeat
  match goal with
  | |- context [align ?A (@alignof ?env ?t)] =>
         assert (A <= align A (@alignof env t)) by (apply align_le, @alignof_pos);
         change (align A (@alignof env t)) with (align_alignof A (@alignof env t))
  | |- context [align ?A (co_alignof ?co)] =>
         let x := fresh "x" in
         assert (A <= align A (co_alignof co)) by (apply align_le; destruct (co_alignof_two_p co) as [x ?];
           pose proof two_power_nat_pos x; omega);
         change (align A (co_alignof co)) with (align_alignof A (co_alignof co))
  | |- context [sizeof_struct ?env ?A ?m] =>
         pose proof sizeof_struct_incr env m A;
         change (sizeof_struct env A m) with (sizeof_struct_le env A m)
  end;
  try unfold align_alignof in *;
  try unfold sizeof_struct_le in *.

Definition sizeofp := @sizeof.

Ltac pose_sizeof_pos :=
  repeat
  match goal with
  | |- context [@sizeof ?env ?t] =>
         pose proof @sizeof_pos env t;
         change (@sizeof env t) with (sizeofp env t)
  end;
  unfold sizeofp in *.

Ltac pose_sizeof_co t :=
  match t with
  | Tstruct ?id ?a =>
    pose proof sizeof_Tstruct id a;
    assert (sizeof_struct cenv_cs 0 (co_members (get_co id)) <= co_sizeof (get_co id)); [
      rewrite co_consistent_sizeof with (env := cenv_cs) by (apply get_co_consistent);
      rewrite complete_legal_cosu_type_Tstruct with (a0 := a) by auto;
      apply align_le, co_alignof_pos
       |]
  | Tunion ?id ?a =>
    pose proof sizeof_Tunion id a;
    assert (sizeof_union cenv_cs (co_members (get_co id)) <= co_sizeof (get_co id)); [
      rewrite co_consistent_sizeof with (env := cenv_cs) by (apply get_co_consistent);
      rewrite complete_legal_cosu_type_Tunion with (a0 := a) by auto;
      apply align_le, co_alignof_pos
       |]
  end.

Ltac pose_field :=
  match goal with
  | _ : complete_legal_cosu_type (Tstruct ?id ?a) = true |-
    context [@sizeof cenv_cs (field_type ?i (co_members (get_co ?id)))] =>
      pose_sizeof_co (Tstruct id a);
      let H := fresh "H" in
      pose proof field_offset_in_range i (co_members (get_co id)) as H;
      spec H; [solve [auto] |];
      pose proof @sizeof_pos cenv_cs (field_type i (co_members (get_co id)))
  | _ : complete_legal_cosu_type (Tunion ?id ?a) = true |-
    context [@sizeof cenv_cs (field_type ?i (co_members (get_co ?id)))] =>
      pose_sizeof_co (Tunion id a);
      let H := fresh "H" in
      pose proof sizeof_union_in_members i (co_members (get_co id)) as H;
      spec H; [solve [auto] |];
      pose proof @sizeof_pos cenv_cs (field_type i (co_members (get_co id)))
  | _ => idtac
  end;
  match goal with
  | _ : complete_legal_cosu_type (Tstruct ?id ?a) = true |-
    context [field_offset_next cenv_cs ?i (co_members (get_co ?id)) (co_sizeof (get_co ?id))] =>
      let H := fresh "H" in
      pose proof field_offset_next_in_range i (co_members (get_co id)) (co_sizeof (get_co id));
      spec H; [solve [auto] |];
      spec H; [solve [auto | pose_sizeof_co (Tstruct id a); auto] |]
  | _ => idtac
  end
.
