Changeset 1628
 Timestamp:
 Dec 19, 2011, 2:48:35 PM (8 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/fresh.ma
r1515 r1628 18 18 19 19 definition 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). 21 21 22 22 definition max_id_of_fundef : clight_fundef → ident ≝ … … 37 37 (max_id_of_globvars (prog_vars ?? p)). 38 38 39 definition universe_ for_program : clight_program→ universe SymbolTag ≝40 λ p. match max_id_of_program pwith [ an_identifier i ⇒39 definition universe_of_max : ident → universe SymbolTag ≝ 40 λmx. match mx with [ an_identifier i ⇒ 41 41 let next ≝ succ i in 42 42 mk_universe SymbolTag next 43 43 ]. 44 45 definition 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 51 definition 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 54 definition 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 61 definition 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 69 lemma uni_of_max_of : ∀i. fresh_for_univ ? i (universe_of_max i). 70 * #i normalize // 71 qed. 72 73 lemma 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 79 lemma 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)) 81 qed. 82 83 84 theorem 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 
src/utilities/binary/positive.ma
r1587 r1628 1161 1161 λn,m. match leb n m with [ true ⇒ m  _ ⇒ n]. 1162 1162 1163 lemma commutative_max : commutative Pos max. 1164 #n #m whd in ⊢ (??%%); 1165 lapply (pos_compare_to_Prop n m) 1166 cases (pos_compare n m) whd in ⊢ (% → ?); #H 1167 [ >(le_to_leb_true n m) >(not_le_to_leb_false m n) /2/ 1168  >H @refl 1169  >(le_to_leb_true m n) >(not_le_to_leb_false n m) /2/ 1170 ] qed. 1171 1172 lemma max_l : ∀m,n:Pos. m ≤ max m n. 1173 #m #n normalize @leb_elim // 1174 qed. 1175 1176 lemma max_r : ∀m,n:Pos. n ≤ max m n. 1177 #m #n >commutative_max // 1178 qed. 1163 1179 1164 1180 
src/utilities/lists.ma
r1626 r1628 1 1 include "basics/lists/list.ma". 2 3 (* An alternative form of All that can be easier to use sometimes. *) 4 lemma All_alt : ∀A,P,l. 5 (∀a,pre,post. l = pre@a::post → P a) → 6 All A P l. 7 #A #P #l #H lapply (refl ? l) change with ([ ] @ l) in ⊢ (???% → ?); 8 generalize in ⊢ (???(??%?) → ?); elim l in ⊢ (? → ???(???%) → %); 9 [ #pre #E % 10  #a #tl #IH #pre #E % 11 [ @(H a pre tl E) 12  @(IH (pre@[a])) >associative_append @E 13 ] 14 ] qed. 2 15 3 16 let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
Note: See TracChangeset
for help on using the changeset viewer.