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.