Changeset 2426 for src/joint


Ignore:
Timestamp:
Oct 31, 2012, 5:36:51 PM (7 years ago)
Author:
boender
Message:
  • updated stacksize to reflect new developments, completed proof
  • removed my versions of files
Location:
src/joint
Files:
1 deleted
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/stacksize.ma

    r2417 r2426  
    22include "joint/semantics.ma".
    33include "common/Executions.ma".
     4include "common/StructuredTraces.ma".
    45
    56inductive call_ud (p: params) (globals: list ident): Type [0] ≝
     
    4748  [ tal_base_not_return s1 s2 ex cl co ⇒ res
    4849  | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res
    49   | tal_base_call s1p s1s s2 ex cl f ca ar tlr co ⇒
    50     extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res)
    51   | tal_step_call end s1p s1s s1a s2 ex cl f ca ar tlr co tal ⇒
    52     let res' ≝ extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res) in
     50  | tal_base_call s1p s1s s2 ex cl ar tlr co ⇒
     51    extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
     52      (up ?? (lg (as_call_ident ? «s1p,cl»))::res)
     53  | tal_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒
     54    let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
     55      (up ?? (lg (as_call_ident ? «s1p,cl»))::res) in
    5356    extract_list_from_tal … lg top_f … tal res'
    5457  | tal_step_default end s1p s1i s1e ex tal cl co ⇒
     
    8487  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
    8588  | tal_base_return st1 st1' ex cl ⇒ ?
    86   | tal_base_call st1p st1s st1' ex cl f ca ar tlr1 co ⇒ ?
    87   | tal_step_call end st1p st1s st1 st1' ex cl f ca ar tlr1 co tal1 ⇒ ?
     89  | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
     90  | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
    8891  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
    8992  ].
     
    103106  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
    104107  | #st2 #st2' #ex' #cl' * #abs destruct (abs)
    105   | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
     108  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
    106109    #taa * #H * #G * #K inversion taa in ⊢ ?;
    107110    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     
    109112      normalize #abs destruct (abs)
    110113    ]
    111   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 normalize *
     114  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize *
    112115    #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
    113116    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     
    119122    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    120123    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    121       destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)
     124      destruct normalize #Hsim destruct (Hsim) (* getting somewhere. Use Hind? *)
     125      cases daemon
    122126    ]
    123127  ]
     
    125129  [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
    126130  | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res %
    127   | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #abs destruct (abs)
    128   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
     131  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs)
     132  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
    129133    normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
    130134    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     
    136140    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    137141    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    138       destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *) 
    139     ]
    140   ]
    141 | cases t2
    142   [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #taa
    143     * #st2mid' * #H * * [2: #st2mid'' *] #J * #f' * #G * #K * #tlr2 * #L * #H1
     142      destruct normalize #Hsim destruct (Hsim)
     143      cases daemon (* use Hind again? *) 
     144    ]
     145  ]
     146| cases t2
     147  [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #G * #ident_eq * #taa
     148    * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2 * #L * #H1
    144149    [ * * #H3 #H2 #H4 | #H2 ]
    145150    inversion taa in ⊢ ?;
     
    152157    ]
    153158  | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
    154   | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #_ * #st2mid *
    155     #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f'' * #G * #K * #tlr2' * #L
    156     inversion taa in ⊢ ?;
    157     [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #tal2 * * #H1 destruct (H1)
     159  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid * #G
     160    * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2' * #L
     161    [* #tl2]
     162    inversion taa in ⊢ ?;
     163    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    158164    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    159       destruct normalize * #tal2 * * #H1 destruct (H1)
     165      destruct normalize * * #abs destruct (abs)
    160166    | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
    161       >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *)
     167      >(tlr_rel_extract_equal p g lg … H2) destruct (H1)
     168      >ident_eq %
    162169    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    163170      destruct normalize * #abs destruct (abs)
    164171    ]
    165   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
    166     normalize * #H1 * #st2mid * #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f
    167     * #G * #K * #tlr2' * #L
    168     inversion taa in ⊢ ?;
    169     [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 #H2 #H3 #res
    170       cases daemon
    171     | #st2p' #st2p'' #st2mid'; #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    172       destruct normalize * #tal2' * * #H1 destruct (H1)
    173     | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
    174     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    175       destruct normalize * #abs destruct (abs)
     172  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize
     173    * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *]
     174    #K * #tlr2' * #L [* #tl2]
     175    inversion taa in ⊢ ?;
     176    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res
     177      destruct (H1) >(tlr_rel_extract_equal … H2) >ident_eq
     178      (* to do here: destruct tl2: 3 cases by contradiction, 1 by equality and 1 by
     179       * not sure yet *) cases daemon
     180    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     181      destruct normalize * * [#abs destruct (abs)] #H2 #res <ident_eq
     182      >(tlr_rel_extract_equal … H2) cases daemon (* stumped here *)
    176183    ]
    177184  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
    178     #taa * #st2mid' * #H * * [2: #stmid'' * ] #J * #f * #G * #K * #tlr2 * #L
    179     inversion taa in ⊢ ?;
    180     [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 destruct (H1)
    181     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    182       destruct normalize * #tal2' * * #H1 #H2 #H3 #res cases daemon
    183     | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
    184     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    185       destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *)
    186     ]
    187   ]
    188 | cases t2
    189   [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun *
    190     #st2_after_fun * * [#H | #st2mid'] * #J * #f' * #G * #K * #tlr2 * #L [2: * #tl2]
    191     inversion taa in ⊢ ?;
    192     [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1)
    193     | #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    194       normalize * * #H1 destruct (H1)
    195     | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    196     | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     185    #G * #ident_eq * #taa * #st2mid' * #H * * [2: #stmid'' * ] #K * #tlr2 * #L
     186    [* #tl2]
     187    inversion taa in ⊢ ?;
     188    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res
     189      destruct (H1)
     190    |2,4: #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     191      destruct normalize * [*] #H1 #H2 [#H3] #res destruct (H1) <ident_eq
     192      >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *)
     193    ]
     194  ]
     195| cases t2
     196  [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa *
     197    #st2mid' * #H * * [#_ | #st2mid''] * #K * #tlr2 * #L [2: * #tl2]
     198    inversion taa in ⊢ ?;
     199    [1,3: #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1)
     200    |2,4: #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     201      destruct normalize * * #H1 destruct (H1)
     202    ]
     203  | #st2 #st2' #ex' #cl' normalize * #st2mid * #G * #ident_eq * #taa * #st2mid'
     204    * #H * * [#abs destruct (abs)] #st2mid' * #K * #tlr2 * #L * #tl2
     205    inversion taa in ⊢ ?;
     206    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
     207    | #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    197208      normalize * * #abs destruct (abs)
    198209    ]
    199   | #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2mid' * #H *
    200     [ * #abs destruct (abs) | * #st2mid'' * #J * #f' * #G * #K * #tlr2 * #L * #tl2
    201       inversion taa in ⊢ ?;
    202       [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    203       | #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    204         normalize * * #abs destruct (abs)
     210  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #st2mid * #G *
     211    #ident_eq * #taa * #st2mid' * #H * * [ #_ | #st2mid'' ] * #K * #tlr2' * #L
     212    [2: * #tl2]
     213    inversion taa in ⊢ ?;
     214    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
     215      destruct (H1) >ident_eq >(tlr_rel_extract_equal … H3)
     216      cases tal1 in H2;
     217      [ #ss #sf #ex'' #cl'' #co'' normalize #_ %
     218      | #ss #sf #ex'' #cl'' normalize #abs cases abs
     219      | #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs
     220      | #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1'
     221        normalize #abs cases abs
     222      | #end' #st1p' #st1i #st1e #ex'' #tal1' #cl'' #co'' normalize
     223        cases daemon (* use induction here, but no *)
    205224      ]
    206     ]
    207   | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #st2mid * #taa
    208     * #st2mid' * #H * * [ #_ | #st2mid'' ] * #J * #f'' * #G * #K * #tlr2' * #L [2: * #tl2]
    209     inversion taa in ⊢ ?;
    210     [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    211     | #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     225    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    212226      destruct normalize * * #abs destruct (abs)
    213     | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 cases daemon
    214     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     227    ]
     228  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
     229    normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * *
     230    [ #H1 | #st2mid''] * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?;
     231    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
     232      destruct (H1) >ident_eq >(tal_rel_extract_equal … H2)
     233      >(tlr_rel_extract_equal … H3) %
     234    |2,4: #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    215235      destruct normalize * * #abs destruct (abs)
    216236    ]
    217   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
    218     normalize * #st2mid * #taa * #st2mid' * #ex'' * * [ #_ | #st2mid''] * #J *
    219     #f'' * #G * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?;
    220     [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
    221       cases daemon (* injectivity needed again *)
    222     | #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    223       destruct normalize * * #abs destruct (abs)
    224     | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) cases daemon
    225       (* huh? *)
    226     | #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    227       destruct normalize * * #abs destruct (abs) cases daemon (* huh2? *)
    228     ]
    229   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa *
    230     #st2mid' * #H * * [ #He | #st2mid'' ] * #J * #f' * #G * #K * #tlr2' * #L
     237  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #G *
     238    #ident_eq * #taa * #st2mid' * #H * * [ #He | #st2mid'' ] * #K * #tlr2' * #L
    231239    [2: * #tl2] inversion taa in ⊢ ?;
    232     [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    233     | #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    234       destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *)
    235     | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    236     | #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    237       destruct normalize * * #H1 #H2 #H3 #res cases daemon
    238     ]
    239   ]
    240 | cases t2
    241   [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res
    242     @(tal_rel_extract_equal p g lg top_f … Hsim)
    243   | #ss #fs #ex' #cl' normalize #Hsim #res
    244     @(tal_rel_extract_equal p g lg top_f … Hsim)
    245   | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize #Hsim #res
    246     @(tal_rel_extract_equal p g lg top_f … Hsim)
    247   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
    248     normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
    249   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res
    250     @(tal_rel_extract_equal p g lg top_f … Hsim)
    251   ]
     240    [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
     241    |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     242      destruct normalize * * #H1 #H2 #H3 #res destruct (H1)
     243      >(tlr_rel_extract_equal … H3) <ident_eq normalize cases daemon
     244      (* look further here *)
     245    ]
     246  ]
     247| cases t2
     248  [ #st2 #st2' #ex' #cl' #co'
     249  | #ss #fs #ex' #cl'
     250  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co'
     251  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
     252  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co'
     253  ]
     254  normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
    252255]
    253256qed.
     
    263266  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
    264267  ]
    265 and tll_rel_extract_equal (p: params) (g: list ident)
     268and tll_rel_max_equal (p: params) (g: list ident)
    266269  (lg: ident → joint_internal_function p g) (top_f: ident)
    267270  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
     
    272275  [ tll_base ends st1 st1' tal1 co ⇒ ?
    273276  ]
    274 and tal_rel_extract_equal (p: params) (g: list ident)
     277and tal_rel_max_equal (p: params) (g: list ident)
    275278  (lg: ident → joint_internal_function p g) (top_f: ident)
    276279  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
Note: See TracChangeset for help on using the changeset viewer.