Changeset 2417 for src/joint


Ignore:
Timestamp:
Oct 25, 2012, 4:36:07 PM (7 years ago)
Author:
boender
Message:
  • reverted changes to StructuredTraces? (shouldn't have been committed yet)
  • updated _jaap files to remove function identifier from cl_call and add an as_call predicate
Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_jaap.ma

    r2398 r2417  
    175175  [ step_seq s ⇒
    176176    match s with
    177     [ CALL_ID l _ _ ⇒    cl_call l
    178     | extension_call _ ⇒ cl_call ? (* pointer stuff not yet implemented, it seems *)
     177    [ CALL_ID _ _ _ ⇒    cl_call
     178    | extension_call _ ⇒ cl_call
    179179    | _ ⇒ cl_other
    180180    ]
    181181  | COND _ _ ⇒ cl_jump
    182182  ].
    183  cases daemon
    184 qed.
    185183
    186184record stmt_params : Type[1] ≝
  • src/joint/stacksize.ma

    r2398 r2417  
    4747  [ tal_base_not_return s1 s2 ex cl co ⇒ res
    4848  | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res
    49   | tal_base_call s1p s1s s2 ex f cl ar tlr co ⇒
     49  | tal_base_call s1p s1s s2 ex cl f ca ar tlr co ⇒
    5050    extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res)
    51   | tal_step_call end s1p s1s s1a s2 ex f cl ar tlr co tal ⇒
     51  | tal_step_call end s1p s1s s1a s2 ex cl f ca ar tlr co tal ⇒
    5252    let res' ≝ extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res) in
    5353    extract_list_from_tal … lg top_f … tal res'
     
    8181  ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res =
    8282  extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝
     83  match t1 with
     84  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
     85  | 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 ⇒ ?
     88  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
     89  ].
     90[ cases t2
     91  [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
     92  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
     93  ]
     94| cases t2
     95  [ #st2 #st2' #tll2 normalize #abs cases abs
     96  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
     97    >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
     98    @(tlr_rel_extract_equal … (proj2 ?? Hsim))
     99  ]
     100| cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
     101  @(tal_rel_extract_equal … H2)
     102| cases t2
     103  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
     104  | #st2 #st2' #ex' #cl' * #abs destruct (abs)
     105  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
     106    #taa * #H * #G * #K inversion taa in ⊢ ?;
     107    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     108    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     109      normalize #abs destruct (abs)
     110    ]
     111  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 normalize *
     112    #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
     113    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     114    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     115      normalize #abs destruct (abs)
     116    ]
     117  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
     118    * #H * #G * #K inversion taa in ⊢ ?;
     119    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     120    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     121      destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)
     122    ]
     123  ]
     124| cases t2
     125  [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
     126  | #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
     129    normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
     130    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     131    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     132      normalize #abs destruct (abs)
     133    ]
     134  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
     135    * #taa * #H * #G inversion taa in ⊢ ?;
     136    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     137    | #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
     144    [ * * #H3 #H2 #H4 | #H2 ]
     145    inversion taa in ⊢ ?;
     146    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3)
     147    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     148      normalize in H3; destruct (H3)
     149    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
     150    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     151      normalize in H1; destruct (H1)
     152    ]
     153  | #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)
     158    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     159      destruct normalize * #tal2 * * #H1 destruct (H1)
     160    | #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? *)
     162    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     163      destruct normalize * #abs destruct (abs)
     164    ]
     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)
     176    ]
     177  | #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
     197      normalize * * #abs destruct (abs)
     198    ]
     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)
     205      ]
     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
     212      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
     215      destruct normalize * * #abs destruct (abs)
     216    ]
     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
     231    [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  ]
     252]
     253qed.
     254
     255(* let rec tlr_rel_max_equal (p: params) (g: list ident)
     256  (lg: ident → joint_internal_function p g) (top_f: ident)
     257  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
     258  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
     259  max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
     260  max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
     261  match t1 with
     262  [ tlr_base st1 st1' tll1 ⇒ ?
     263  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
     264  ]
     265and tll_rel_extract_equal (p: params) (g: list ident)
     266  (lg: ident → joint_internal_function p g) (top_f: ident)
     267  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
     268  t1 ≈ t2 →
     269  max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
     270  max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
     271  match t1 with
     272  [ tll_base ends st1 st1' tal1 co ⇒ ?
     273  ]
     274and tal_rel_extract_equal (p: params) (g: list ident)
     275  (lg: ident → joint_internal_function p g) (top_f: ident)
     276  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
     277  t1 ≈ t2 →
     278  max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
     279  max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
    83280  match t1 with
    84281  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
     
    88285  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
    89286  ].
    90 [ cases t2
    91   [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
    92   | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
    93   ]
    94 | cases t2
    95   [ #st2 #st2' #tll2 normalize #abs cases abs
    96   | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
    97     >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
    98     @(tlr_rel_extract_equal … (proj2 ?? Hsim))
    99   ]
    100 | cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
    101   @(tal_rel_extract_equal … H2)
    102 | cases t2
    103   [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
    104   | #st2 #st2' #ex' #cl' * #abs destruct (abs)
    105   | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
    106     #taa * #H * #G * #K inversion taa in ⊢ ?;
    107     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    108     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    109       normalize #abs destruct (abs)
    110     ]
    111   | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2 normalize *
    112     #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
    113     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    114     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    115       normalize #abs destruct (abs)
    116     ]
    117   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
    118     * #H * #G * #K inversion taa in ⊢ ?;
    119     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    120     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    121       destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)
    122     ]
    123   ]
    124 | cases t2
    125   [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
    126   | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res %
    127   | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs)
    128   | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
    129     normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
    130     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    131     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    132       normalize #abs destruct (abs)
    133     ]
    134   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
    135     * #taa * #H * #G inversion taa in ⊢ ?;
    136     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    137     | #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 * #f' * #G * #K * #tlr2 * #L * #H1 #H2 inversion taa in ⊢ ?;
    144     [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
    145     | #st2'' #st2''' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    146       normalize in H1; destruct (H1)
    147     ]
    148   | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
    149   | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid *
    150     #taa * #st2mid' * #H * #f'' * #G * #K * #tlr2' * #L inversion taa in ⊢ ?;
    151     [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
    152       >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *)
    153     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    154       destruct normalize * #abs destruct (abs)
    155     ]
    156   | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
    157     normalize * #H1 * #st2mid * #taa * #st2mid' * #H * #f * #G * #K * #tlr2' * #L
    158     inversion taa in ⊢ ?;
    159     [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
    160     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    161       destruct normalize * #abs destruct (abs)
    162     ]
    163   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
    164     #taa * #st2mid' * #H * #f * #G * #K * #tlr2 * #L inversion taa in ⊢ ?;
    165     [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
    166     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    167       destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *)
    168     ]
    169   ]
    170 | cases t2
    171   [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun
    172     * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?;
    173     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    174     | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    175       normalize * * #abs destruct (abs)
    176     ]
    177   | #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun
    178     * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?;
    179     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    180     | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    181       normalize * * #abs destruct (abs)
    182     ]
    183   | #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize * #st2mid * #taa
    184     * #st2_fun * #st2_after_fun * #H' * #f'' * #G * #K * #tlr2' * #L * #tl2
    185     inversion taa in ⊢ ?;
    186     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    187     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    188       destruct normalize * * #abs destruct (abs)
    189     ]
    190   | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
    191     normalize * #st2mid * #taa * #st2_fun * #st2_after_fun * #H * #f'' *
    192     #G * #K * #tlr2' * #L * #tl2 inversion taa in ⊢ ?;
    193     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
    194       >(tlr_rel_extract_equal … H2) cases daemon (* injectivity needed again *)
    195     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    196       destruct normalize * * #abs destruct (abs)
    197     ]
    198   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa *
    199     #st2_fun * #st2_after_fun * #H * #f' * #G * #K * #tlr2' * #L * #tl2
    200     inversion taa in ⊢ ?;
    201     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    202     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    203       destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *)
    204     ]
    205   ]
    206 | cases t2
    207   [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res
    208     @(tal_rel_extract_equal p g lg top_f … Hsim)
    209   | #ss #fs #ex' #cl' normalize #Hsim #res
    210     @(tal_rel_extract_equal p g lg top_f … Hsim)
    211   | #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize #Hsim #res
    212     @(tal_rel_extract_equal p g lg top_f … Hsim)
    213   | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
    214     normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
    215   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res
    216     @(tal_rel_extract_equal p g lg top_f … Hsim)
    217   ]
    218 ]
    219 qed.
    220 
    221 let rec tlr_rel_max_equal (p: params) (g: list ident)
    222   (lg: ident → joint_internal_function p g) (top_f: ident)
    223   S1 S2 s1 s1' s2 s2' t1 t2 on t1:
    224   tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
    225   max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
    226   max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
    227   match t1 with
    228   [ tlr_base st1 st1' tll1 ⇒ ?
    229   | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
    230   ]
    231 and tll_rel_extract_equal (p: params) (g: list ident)
    232   (lg: ident → joint_internal_function p g) (top_f: ident)
    233   S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
    234   t1 ≈ t2 →
    235   max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
    236   max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
    237   match t1 with
    238   [ tll_base ends st1 st1' tal1 co ⇒ ?
    239   ]
    240 and tal_rel_extract_equal (p: params) (g: list ident)
    241   (lg: ident → joint_internal_function p g) (top_f: ident)
    242   S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
    243   t1 ≈ t2 →
    244   max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
    245   max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
    246   match t1 with
    247   [ tal_base_not_return st1 st1' ex cl co ⇒ ?
    248   | tal_base_return st1 st1' ex cl ⇒ ?
    249   | tal_base_call st1p st1s st1' ex f cl ar tlr1 co ⇒ ?
    250   | tal_step_call end st1p st1s st1 st1' ex f cl ar tlr1 co tal1 ⇒ ?
    251   | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
    252   ].
    253287 cases daemon (* next proof *)
    254 qed.
     288qed. *)
    255289     
    256290     
Note: See TracChangeset for help on using the changeset viewer.