Changeset 1628 for src/Clight/fresh.ma


Ignore:
Timestamp:
Dec 19, 2011, 2:48:35 PM (8 years ago)
Author:
campbell
Message:

Show that the universe generated by Clight/fresh.ma is good.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/fresh.ma

    r1515 r1628  
    1818
    1919definition max_id_of_fn : function → ident ≝
    20 λf. max_id (max_id_of_env (fn_params f)) (max_id_of_env (fn_vars f)).
     20λf. max_id_of_env (fn_params f @ fn_vars f).
    2121
    2222definition max_id_of_fundef : clight_fundef → ident ≝
     
    3737           (max_id_of_globvars (prog_vars ?? p)).
    3838
    39 definition universe_for_program : clight_program → universe SymbolTag ≝
    40 λp. match max_id_of_program p with [ an_identifier i ⇒
     39definition universe_of_max : ident → universe SymbolTag ≝
     40λmx. match mx with [ an_identifier i ⇒
    4141      let next ≝ succ i in
    4242      mk_universe SymbolTag next
    4343    ].
     44
     45definition universe_for_program : clight_program → universe SymbolTag ≝
     46λp. universe_of_max (max_id_of_program p).
     47
     48
     49(* A specification for the result *)
     50
     51definition fn_fresh_for_univ : function → universe SymbolTag → Prop ≝
     52λf,u. All ? (λit. fresh_for_univ ? (\fst it) u) (fn_params f @ fn_vars f).
     53
     54definition fd_fresh_for_univ : clight_fundef → universe SymbolTag → Prop ≝
     55λfd,u.
     56  match fd with
     57  [ CL_Internal f ⇒ fn_fresh_for_univ f u
     58  | CL_External id _ _ ⇒ fresh_for_univ ? id u
     59  ].
     60
     61definition prog_fresh_for_univ : clight_program → universe SymbolTag → Prop ≝
     62λp,u.
     63  All ? (λifd. fresh_for_univ ? (\fst ifd) u ∧ fd_fresh_for_univ (\snd ifd) u) (prog_funct ?? p) ∧
     64  fresh_for_univ ? (prog_main ?? p) u ∧
     65  All ? (λv. fresh_for_univ ? (\fst (\fst v)) u) (prog_vars ?? p).
     66
     67(* And they match up. *)
     68
     69lemma uni_of_max_of : ∀i. fresh_for_univ ? i (universe_of_max i).
     70* #i normalize //
     71qed.
     72
     73lemma uni_max_l : ∀i,j,k. fresh_for_univ ? i (universe_of_max j) → fresh_for_univ ? i (universe_of_max (max_id j k)).
     74* #i * #j * #k normalize @leb_elim normalize
     75[ #H #H' @(transitive_le … (succ j)) /2/
     76| /2/
     77] qed.
     78
     79lemma uni_max_r : ∀i,j,k. fresh_for_univ ? i (universe_of_max k) → fresh_for_univ ? i (universe_of_max (max_id j k)).
     80* #i * #j * #k whd in ⊢ (? → ???(?%)); >commutative_max @(uni_max_l ? (an_identifier ? k) (an_identifier ? j))
     81qed.
     82
     83
     84theorem prog_fresh : ∀p. prog_fresh_for_univ p (universe_for_program p).
     85* #vars #fns #main
     86%
     87[ %
     88  [ @All_alt * #id #fd #pre #post #Efns %
     89    [ @uni_max_l @uni_max_l >Efns elim pre
     90      [ @uni_max_l @uni_max_l //
     91      | #x #y #H @uni_max_r @H
     92      ]
     93    | cases fd in Efns ⊢ %;
     94      [ #fn #Efns @All_alt >Efns * #id' #ty #envpre #envpost #Eenv
     95        @uni_max_l @uni_max_l elim pre
     96        [ @uni_max_l @uni_max_r
     97          whd in ⊢ (???(?%)); >Eenv elim envpre
     98          [ @uni_max_l //
     99          | #x #y #H @uni_max_r //
     100          ]
     101        | #x #y #H @uni_max_r @H
     102        ]
     103      | #id' #tys #ty #Efn >Efn
     104        @uni_max_l @uni_max_l elim pre
     105        [ @uni_max_l @uni_max_r //
     106        | #x #y #H @uni_max_r @H
     107        ]
     108      ]
     109    ]
     110  | @uni_max_l @uni_max_r //
     111  ]
     112| @All_alt * * #id #r #init #pre #post #E @uni_max_r >E elim pre
     113  [ @uni_max_l //
     114  | #x #y #H @uni_max_r @H
     115  ]
     116] qed.
     117
     118   
Note: See TracChangeset for help on using the changeset viewer.