Library Fminor_well

Relation of well_bound of Fminor terms

Author: Zaynah Dargaye

Created: 29th April 2009




Require Import List.

Require Import Coqlib.

Require Import Coqlib2.

Require Import AST.

Require Import Globalenvs.

Require Import Maps.

Require Import Mml.

Require Import Mml_pre.

Require Import FSets.

Require Import FSetAVL.

Require Import Ordered.

Require Import Compare_dec.

Require Import Fminor.

Require Import M2Fminor.

Require Import M2Fminor_proof.




Definition bound_test (n q:nat) := 

  Zle (8+Z_of_nat n*4+4) (8+(Z_of_nat q)*4+4).




Inductive list_param_bound :nat-> list Param->Prop :=

 | bnil : forall z ,list_param_bound z nil 

  | vcons : forall id z l , list_param_bound z l -> 

     list_param_bound z (VR id::l) 

 | scons: forall n z l , bound_test n z -> 

                   list_param_bound z l -> 

     list_param_bound z (SL n::l).




Lemma list_param_bound_in : 

 forall z l , list_param_bound z l -> 

 (forall n , In (SL n) l -> bound_test n z).







Inductive well_atom_bound :nat->catom->Prop:=

 | wVar: forall id z , well_atom_bound z (Cvar id) 

 | wField : forall n a z, well_atom_bound z a -> 

        well_atom_bound z (Cfield n a) 

 | wSlot: forall n z, 

         bound_test n z  ->

        well_atom_bound z (Cslot n).




Inductive well_atomlist_bound : nat->list catom->Prop:= 

 |wAnil : forall z, well_atomlist_bound z nil 

 |wAcons: forall z hd tl , well_atom_bound z hd -> 

        well_atomlist_bound z tl -> well_atomlist_bound z (hd::tl).




Inductive well_bound : nat -> Cterm->Prop:= 

 | wCat : forall a z,

        well_atom_bound z a -> well_bound z (Catom a)

 | wCa :  forall fid a al z0 z ,

        le z0 z ->

        well_atom_bound z a -> 

        well_atomlist_bound z al ->

        well_bound z (Capp fid a al z0)

 | wCc : forall f al z0 z, 

         le z0 z -> 

         well_atomlist_bound z al -> 

         well_bound z (Cclos f al z0) 

 | wCcn : forall n al z0 z,

         le z0 z -> 

          well_atomlist_bound z al -> 

         well_bound z (Ccon n al z0)  

 | wCl  :  forall id c1 c2 z, 

          well_bound z c1  -> well_bound z c2 -> 

          well_bound z (Clet id c1 c2) 

 | wCp : forall n c1 c2 z,

         bound_test n z -> 

        well_bound z c1 -> well_bound z c2 -> 

        well_bound z (Cpush n c1 c2)          

 | wCm: forall a pl z , 

        well_atom_bound z a -> 

        well_plist_bound z pl  -> 

        well_bound z (Cmatch a pl)  

with well_pat_bound :nat->cpat->Prop := 

  |wPat : forall lp c z, 

          list_param_bound z lp -> 

          well_bound z c -> 

          well_pat_bound z (CPatc lp c)

with well_plist_bound :nat->list cpat->Prop:= 

 | wPnil : forall z , well_plist_bound z nil 

 | wPcons : forall hd tl z , well_pat_bound z hd -> 

        well_plist_bound z tl -> well_plist_bound z (hd::tl).




Scheme well_bound_ind6 := Minimality for well_bound Sort Prop

 with well_pat_ind6:= Minimality for well_pat_bound Sort Prop 

 with well_ptlist_ind6 := Minimality for well_plist_bound Sort Prop.




Definition well_bound_func (f:cfunction) := 

    well_bound  (cn_stackspace f) (cn_body f).




Definition well_bound_program (p:cprogram) := 

 (forall id f, In (id,f) (cprog_funct p) -> well_bound_func f) /\

 well_bound (cn_stackspace (cprog_main p)) 

                     (cn_body (cprog_main p)) .




Section correct_cterm_ind2.




Variable 

   (P: Cterm ->Prop) 

   (Pp: cpat ->Prop) 

   (Ppl: list cpat ->Prop).




Hypotheses 

  (Hca : forall a, P (Catom a)) 

  (Happ: forall fid ca cal z,  P (Capp fid ca cal z) ) 

  (Hclos: forall fid cal z,  P (Cclos fid cal z)) 

  (Hcon: forall n cal z,  P(Ccon n cal z))

  (Hlet: forall id c1 c2, P c1 ->P c2 -> P (Clet id c1 c2))

  (Hpush: forall n c1 c2, P c1 ->P c2 -> P (Cpush n c1 c2))

  (Hmat: forall ca pl,  Ppl pl -> P (Cmatch ca pl))

  (Hp: forall xl c, P c ->Pp (CPatc xl c)) 

  (Hcpn: Ppl nil) (Hcpc:  forall ph pt, Pp ph->Ppl pt ->Ppl (ph::pt)) .




Fixpoint cterm_ind2 (c:Cterm): P c:= 

 match c as x return P x with 

 | Catom a => Hca a 

 | Capp fid ca cal z => Happ fid ca cal z  

 | Cclos fid cal z => Hclos fid cal z 

 |Ccon n cal z => Hcon n cal z  

 |Clet id c1 c2=> Hlet id c1 c2 (cterm_ind2 c1) (cterm_ind2 c2) 

 |Cpush n c1 c2=> Hpush n c1 c2 (cterm_ind2 c1) (cterm_ind2 c2) 

 |Cmatch ca pl => Hmat ca pl  

  ( (fix fpl_ind2 (pl:list cpat ){struct pl}: Ppl pl:= 

        match pl as x return Ppl x with 

        | nil => Hcpn 

        | p::l => Hcpc p l (pat_ind2 p) (fpl_ind2 l) end) pl) 

end

with pat_ind2 (p:cpat) {struct p}:Pp p:= 

 match p as x return Pp x with 

 |CPatc xl c => Hp xl c (cterm_ind2 c) 

end.




End  correct_cterm_ind2.




Lemma max_commut: 

 forall z x , max z x = max x z.




Lemma bound_test_ge: 

   forall n z x, bound_test n z -> ge  x z -> 

   bound_test n x.




Lemma list_param_bound_ge: 

 forall l z , list_param_bound z l -> forall x, ge x z -> 

                 list_param_bound x l.




Lemma well_atom_bound_ge: 

 forall  z a , well_atom_bound z a -> 

  forall x, ge x z -> 

         well_atom_bound x a.




Lemma well_atlist_bound_ge: 

 forall  z a , well_atomlist_bound z a -> 

  forall x, ge x z -> 

         well_atomlist_bound x a.




Lemma well_bound_ge: 

  forall z c , well_bound  z c -> 

     forall x, ge x z -> well_bound x c.




Lemma max_ge_left: 

 forall x z, ge  (max x z) x.




Lemma max_ge_right: 

 forall x z, ge (max x z) z.




Lemma well_bound_max_left: 

 forall z c x, well_bound z c -> well_bound (max z x) c.




Lemma well_bound_max_right: 

 forall z c x, well_bound x c -> well_bound (max z x) c.




Lemma well_atom_bound_max_left:

   forall z c x, well_atom_bound z c -> well_atom_bound (max z x) c.




Lemma well_atom_bound_max_right: 

 forall z c x, well_atom_bound x c -> well_atom_bound (max z x) c.




Lemma well_atomlist_bound_max_left:

   forall z c x, well_atomlist_bound z c -> 

                       well_atomlist_bound (max z x) c.




Lemma well_atomlist_bound_max_right: 

 forall z c x, well_atomlist_bound x c -> well_atomlist_bound (max z x) c.




Lemma well_pat_bound_ge: 

  forall z a , well_pat_bound  z a -> 

     forall x, ge x z -> well_pat_bound x a.




Lemma well_pat_bound_max_left:

   forall z c x, well_pat_bound z c -> well_pat_bound (max z x) c.




Lemma well_pat_bound_max_right: 

 forall z c x, well_pat_bound x c -> well_pat_bound (max z x) c.




Lemma well_plist_bound_ge: 

  forall z a , well_plist_bound  z a -> 

     forall x, ge x z -> well_plist_bound x a.




Lemma well_plist_bound_max_left:

   forall z c x, well_plist_bound z c -> 

                       well_plist_bound (max z x) c.




Lemma well_plist_bound_max_right: 

 forall z c x, well_plist_bound x c -> well_plist_bound (max z x) c.




Lemma max_refl: 

 forall n , max n n = n .




Lemma max_trans : 

 forall n n1  n0, n <= n1 -> n <= n0 -> n <= (max n1 n0).




Lemma list_param_stack_monotone:

 forall xl n1 k, 

  list_param_stack xl n1 = Some k ->

  n1 <= k<= n1+length xl.







Lemma stack_term_monotone: 

 forall t n1 n2, stack_term t n1 = Some n2 -> n1 <= n2.













Lemma stack_case_monotone: 

 forall t n1 n2, stack_case t n1 = Some n2 -> n1 <= n2.




 Lemma stack_cases_monotone: 

 forall t n1 n2, stack_cases t n1 = Some n2 -> n1 <= n2.




Lemma well_atom_bound_germ_atom: 

 forall a ce ca  

   (GE: germ_atom a ce = Some ca )

    (SSz:stack_atom ca (cenv_height ce) = true), 

    well_atom_bound (cenv_height ce) ca.




Lemma  well_atomlist_bound_germ_atomlist: 

 forall al ce ca  

   (GE: germ_atomlist al ce = Some ca )

    (SSz:stack_atomlist ca (cenv_height ce) = true), 

    well_atomlist_bound (cenv_height ce) ca.







Lemma l1: 

forall l n k, 

 list_param_stack l n = Some k->

 list_param_bound k l.




Lemma binds_1 : 

 forall xl ce r  l c1 l0 

      (BD: bind_vars xl ce r l0 = Some (l,c1)) , 

      exists l3, l = l0++l3 /\ length l3 = length xl /\

      list_param_stack l3 (cenv_height ce) = Some (cenv_height c1).










Lemma well_bound_germ:

 forall t ce c n (GE: germ t ce = Some c) 

   (SSz : stack_term c (cenv_height ce) = Some n) , 

    well_bound n c.

























Lemma bind_pars_monotone: 

 forall l ce r l0 l2 c0, 

   bind_pars l ce r l0 = Some (l2,c0) ->  

   cenv_height ce <= cenv_height c0.




Lemma bind_pars_bound: 

 forall l ce r l0 l2 c0, 

   bind_pars l ce r l0 = Some (l2,c0) -> 

   exists l3, l2 = l0++l3 /\ 

   (forall n id , In (n,id) l3 -> n <= cenv_height c0).










Lemma cpush_bound: 

 forall l k c

     (W:well_bound k c) 

     (I:forall n id , In (n,id) l -> n <= k), 

     well_bound k (Cpush_list l c).




Lemma  well_bound_germ_cfunction: 

  forall t c (GE: germ_cfunction t  = Some c),  

    well_bound_func  c.




 Lemma  well_bound_germ_cfunctions: 

  forall t c (GE: germ_cfunctions t  = Some c),  

     (forall id f, In (id,f) c -> 

                   well_bound_func f).




Theorem well_bound_germ_cprogram: 

 forall p cp (GP: germ_cprogram p = Some cp), 

  well_bound_program cp.