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

Add some notions of freshness, and start using them for temporary
generation (not yet complete).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1601 r1627  
    2020  λtag. mk_universe tag one.
    2121
    22 (* Fresh identifier generation uses delayed overflow checking.  To make sure
    23    that the identifiers really were fresh, use the check_universe_ok function
    24    below afterwards. *)
    25 definition fresh : ∀tag:String. universe tag → identifier tag × (universe tag) ≝
    26   λtag.
    27   λuniv: universe tag.
    28   let id ≝ next_identifier ? univ in
     22let rec fresh (tag:String) (u:universe tag) on u : identifier tag × (universe tag) ≝
     23  let id ≝ next_identifier ? u in
    2924  〈an_identifier tag id, mk_universe tag (succ id)〉.
     25
     26
     27let rec fresh_for_univ tag (id:identifier tag) (u:universe tag) on id : Prop ≝
     28  match id with [ an_identifier p ⇒ p < next_identifier … u ].
     29
     30
     31lemma fresh_is_fresh : ∀tag,id,u,u'.
     32  〈id,u〉 = fresh tag u' →
     33  fresh_for_univ tag id u.
     34#tag * #id * #u * #u' #E whd in E:(???%); destruct //
     35qed.
     36
     37lemma fresh_remains_fresh : ∀tag,id,id',u,u'.
     38  fresh_for_univ tag id u →
     39  〈id',u'〉 = fresh tag u →
     40  fresh_for_univ tag id u'.
     41#tag * #id * #id' * #u * #u' normalize #H #E destruct /2/
     42qed.
     43
     44lemma fresh_distinct : ∀tag,id,id',u,u'.
     45  fresh_for_univ tag id u →
     46  〈id',u'〉 = fresh tag u →
     47  id ≠ id'.
     48#tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2/
     49qed.
     50
     51
     52let rec env_fresh_for_univ tag A (env:list (identifier tag × A)) (u:universe tag) on u : Prop ≝
     53  All ? (λida. fresh_for_univ tag (\fst ida) u) env.
     54
     55lemma fresh_env_extend : ∀tag,A,env,u,u',id,a.
     56  env_fresh_for_univ tag A env u →
     57  〈id,u'〉 = fresh tag u →
     58  env_fresh_for_univ tag A (〈id,a〉::env) u'.
     59#tag #A #env * #u * #u' #id #a
     60#H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2/ ]
     61qed.
     62
    3063
    3164definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
     
    226259] qed.
    227260
     261
     262let rec fresh_for_map tag A (id:identifier tag) (m:identifier_map tag A) on id : Prop ≝
     263  lookup … m id = None A.
     264
     265definition fresh_map_for_univ ≝
     266λtag,A. λm:identifier_map tag A. λu:universe tag.
     267  ∀id. present tag A m id → fresh_for_univ tag id u.
     268
     269lemma fresh_fresh_for_map : ∀tag,A,m,id,u,u'.
     270  fresh_map_for_univ tag A m u →
     271  〈id,u'〉 = fresh tag u →
     272  fresh_for_map tag A id m.
     273#tag #A * #m * #id * #u * #u' whd in ⊢ (% → ???% → %);
     274#FMU #E destruct lapply (FMU (an_identifier tag u)) whd in ⊢ ((% → %) → ?);
     275generalize in ⊢ ((?(??%?) → ?) → ??%?); *
     276[ // | #a #H @False_ind lapply (H ?) /2/ % #E destruct
     277qed.
     278
     279lemma fresh_map_preserved : ∀tag,A,m,u,u',id.
     280  fresh_map_for_univ tag A m u →
     281  〈id,u'〉 = fresh tag u →
     282  fresh_map_for_univ tag A m u'.
     283#tag #A #m #u * #u' #id whd in ⊢ (% → ? → %); #H #E
     284#id' #PR @(fresh_remains_fresh … E) @H //
     285qed.
     286
     287lemma fresh_map_add : ∀tag,A,m,u,id,a.
     288  fresh_map_for_univ tag A m u →
     289  fresh_for_univ tag id u →
     290  fresh_map_for_univ tag A (add tag A m id a) u.
     291#tag #A * #m #u #id #a #Hm #Hi
     292#id' #PR cases (identifier_eq tag id' id)
     293[ #E >E @Hi
     294| #NE @Hm whd in PR;
     295  change with (add tag A (an_id_map tag A m) id a) in PR:(?(??(???%?)?));
     296  >lookup_add_miss in PR; //
     297] qed.
     298
     299lemma present_not_fresh : ∀tag,A,m,id,id'.
     300  present tag A m id →
     301  fresh_for_map tag A id' m →
     302  id ≠ id'.
     303#tag #A #m #id * #id' whd in ⊢ (% → % → ?);
     304* #NE #E % #E' destruct @(NE E)
     305qed.
     306
    228307(* Sets *)
    229308
Note: See TracChangeset for help on using the changeset viewer.