Changeset 1516 for src/common/Identifiers.ma
- Timestamp:
- Nov 19, 2011, 12:38:20 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Identifiers.ma
r1515 r1516 56 56 57 57 lemma eq_identifier_refl : ∀tag,id. eq_identifier tag id id = true. 58 #tag * #id whd in ⊢ (??%?) >eqb_n_n @refl58 #tag * #id whd in ⊢ (??%?); >eqb_n_n @refl 59 59 qed. 60 60 … … 64 64 65 65 definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y). 66 #tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %) 66 #tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %); 67 67 #E [ % | %2 ] 68 68 lapply E @eqb_elim … … 184 184 ] (refl ? u'). 185 185 cases l in p E; cases m; -l' -m' #m' #l' 186 whd in ⊢ (% → ?) 187 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?) 186 whd in ⊢ (% → ?); 187 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?); 188 188 #NL #U cases NL #H @H @(update_fail … U) 189 189 qed. … … 194 194 present tag A (update_present tag A m id' H' a) id. 195 195 #tag #A * #m * #id #a * #id' #H #H' 196 whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta196 whd whd in ⊢ (?(??(???(%??????)?)?)); normalize nodelta 197 197 cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id')) 198 [ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ????? U)198 [ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); >(update_lookup_opt_same ????? U) 199 199 % #E' destruct 200 | #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(??%%)?))200 | #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); whd in ⊢ (?(??(??%%)?)); 201 201 <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ] 202 202 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.