- Timestamp:
- Apr 8, 2011, 2:06:46 PM (10 years ago)
- Location:
- src
- Files:
-
- 1 deleted
- 8 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Csyntax.ma
r744 r747 17 17 18 18 (*include "Integers.ma".*) 19 include " Clight/AST.ma".19 include "common/AST.ma". 20 20 include "utilities/Coqlib.ma". 21 21 include "common/Errors.ma". -
src/RTLabs/RTLabs-syntax.ma
r738 r747 2 2 include "basics/logic.ma". 3 3 4 include " Clight/AST.ma".4 include "common/AST.ma". 5 5 include "common/CostLabel.ma". 6 6 include "common/FrontEndOps.ma". -
src/common/AST.ma
r722 r747 1 include "arithmetics/nat.ma". 2 3 include "ASM/String.ma". 1 (* *********************************************************************) 2 (* *) 3 (* The Compcert verified compiler *) 4 (* *) 5 (* Xavier Leroy, INRIA Paris-Rocquencourt *) 6 (* *) 7 (* Copyright Institut National de Recherche en Informatique et en *) 8 (* Automatique. All rights reserved. This file is distributed *) 9 (* under the terms of the GNU General Public License as published by *) 10 (* the Free Software Foundation, either version 2 of the License, or *) 11 (* (at your option) any later version. This file is also distributed *) 12 (* under the terms of the INRIA Non-Commercial License Agreement. *) 13 (* *) 14 (* *********************************************************************) 15 16 (* * This file defines a number of data types and operations used in 17 the abstract syntax trees of many of the intermediate languages. *) 18 19 include "basics/types.ma". 20 include "common/Integers.ma". 21 include "common/Floats.ma". 4 22 include "ASM/BitVector.ma". 5 include "utilities/Compare.ma". 6 23 include "common/Identifiers.ma". 24 25 26 (* * * Syntactic elements *) 27 28 (* Global variables and functions are represented by identifiers with the 29 tag for symbols. Note that Clight also uses them for locals due to 30 the ambiguous syntax. *) 31 32 axiom SymbolTag : String. 33 34 definition ident ≝ identifier SymbolTag. 35 36 definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?. 37 38 definition ident_of_nat : nat → ident ≝ identifier_of_nat ?. 39 40 (* XXX backend is currently using untagged words as identifiers. *) 7 41 definition Identifier ≝ Word. 8 definition Immediate ≝ nat. 42 43 definition Immediate ≝ nat. (* XXX is this the best place to put this? *) 44 45 (* Memory spaces *) 46 47 inductive region : Type[0] ≝ 48 | Any : region 49 | Data : region 50 | IData : region 51 | PData : region 52 | XData : region 53 | Code : region. 54 55 definition eq_region : region → region → bool ≝ 56 λr1,r2. 57 match r1 with 58 [ Any ⇒ match r2 with [ Any ⇒ true | _ ⇒ false ] 59 | Data ⇒ match r2 with [ Data ⇒ true | _ ⇒ false ] 60 | IData ⇒ match r2 with [ IData ⇒ true | _ ⇒ false ] 61 | PData ⇒ match r2 with [ PData ⇒ true | _ ⇒ false ] 62 | XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ] 63 | Code ⇒ match r2 with [ Code ⇒ true | _ ⇒ false ] 64 ]. 65 66 lemma eq_region_elim : ∀P:bool → Type[0]. ∀r1,r2. 67 (r1 = r2 → P true) → (r1 ≠ r2 → P false) → 68 P (eq_region r1 r2). 69 #P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse 70 try ( @Ptrue // ) 71 @Pfalse % #E destruct; 72 qed. 73 74 definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2). 75 #r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed. 76 77 definition size_pointer : region → nat ≝ 78 λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ]. 79 80 (* * The intermediate languages are weakly typed, using only three types: 81 [ASTint] for integers, [ASTptr] for pointers, and [ASTfloat] for floating-point 82 numbers. *) 83 84 inductive typ : Type[0] ≝ 85 | ASTint : typ 86 | ASTptr : region → typ 87 | ASTfloat : typ. 88 89 (* XXX aliases *) 90 definition SigType ≝ typ. 91 definition SigType_Int ≝ ASTint. 92 (* 93 | SigType_Float: SigType 94 *) 95 definition SigType_Ptr ≝ ASTptr Any. 96 97 98 (* FIXME: ASTint size is not 1 for Clight32 *) 99 definition typesize : typ → nat ≝ λty. 100 match ty with [ ASTint ⇒ 1 | ASTptr r ⇒ size_pointer r | ASTfloat ⇒ 8 ]. 101 102 lemma typesize_pos: ∀ty. typesize ty > 0. 103 #ty cases ty [ 2: * ] /2/ qed. 104 105 lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2). 106 #t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct; qed. 107 108 lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2). 109 #t1 #t2 cases t1 cases t2 110 [ %1 @refl 111 | 2,3: #ty %2 % #H destruct 112 | #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/ 113 ] 114 qed. 115 116 (* * Additionally, function definitions and function calls are annotated 117 by function signatures indicating the number and types of arguments, 118 as well as the type of the returned value if any. These signatures 119 are used in particular to determine appropriate calling conventions 120 for the function. *) 121 122 record signature : Type[0] ≝ { 123 sig_args: list typ; 124 sig_res: option typ 125 }. 126 127 (* XXX aliases *) 128 definition Signature ≝ signature. 129 definition signature_args ≝ sig_args. 130 definition signature_return ≝ sig_res. 131 132 definition proj_sig_res : signature → typ ≝ λs. 133 match sig_res s with 134 [ None ⇒ ASTint 135 | Some t ⇒ t 136 ]. 137 138 (* * Memory accesses (load and store instructions) are annotated by 139 a ``memory chunk'' indicating the type, size and signedness of the 140 chunk of memory being accessed. *) 141 142 inductive memory_chunk : Type[0] ≝ 143 | Mint8signed : memory_chunk (*r 8-bit signed integer *) 144 | Mint8unsigned : memory_chunk (*r 8-bit unsigned integer *) 145 | Mint16signed : memory_chunk (*r 16-bit signed integer *) 146 | Mint16unsigned : memory_chunk (*r 16-bit unsigned integer *) 147 | Mint32 : memory_chunk (*r 32-bit integer, or pointer *) 148 | Mfloat32 : memory_chunk (*r 32-bit single-precision float *) 149 | Mfloat64 : memory_chunk (*r 64-bit double-precision float *) 150 | Mpointer : region → memory_chunk. (* pointer addressing given region *) 151 152 (* * Initialization data for global variables. *) 153 154 inductive init_data: Type[0] ≝ 155 | Init_int8: int → init_data 156 | Init_int16: int → init_data 157 | Init_int32: int → init_data 158 | Init_float32: float → init_data 159 | Init_float64: float → init_data 160 | Init_space: nat → init_data 161 | Init_null: region → init_data 162 | Init_addrof: region → ident → int → init_data. (*r address of symbol + offset *) 163 164 (* * Whole programs consist of: 165 - a collection of function definitions (name and description); 166 - the name of the ``main'' function that serves as entry point in the program; 167 - a collection of global variable declarations, consisting of 168 a name, initialization data, and additional information. 169 170 The type of function descriptions and that of additional information 171 for variables vary among the various intermediate languages and are 172 taken as parameters to the [program] type. The other parts of whole 173 programs are common to all languages. *) 174 175 record program (F,V: Type[0]) : Type[0] := { 176 prog_funct: list (ident × F); 177 prog_main: ident; 178 prog_vars: list (ident × (list init_data) × region × V) 179 }. 180 181 definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V. 182 map ?? (fst ident F) (prog_funct ?? p). 183 184 definition prog_var_names ≝ λF,V: Type[0]. λp: program F V. 185 map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p). 186 (* 187 (** * Generic transformations over programs *) 188 189 (** We now define a general iterator over programs that applies a given 190 code transformation function to all function descriptions and leaves 191 the other parts of the program unchanged. *) 192 193 Section TRANSF_PROGRAM. 194 195 Variable A B V: Type. 196 Variable transf: A -> B. 197 *) 198 199 definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝ 200 λA,B,transf,l. 201 map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l. 202 203 definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝ 204 λA,B,V,transf,p. 205 mk_program B V 206 (transf_program ?? transf (prog_funct A V p)) 207 (prog_main A V p) 208 (prog_vars A V p). 209 (* 210 lemma transform_program_function: 211 ∀A,B,V,transf,p,i,tf. 212 in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) → 213 ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf. 214 normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H); 215 #x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/; 216 qed. 217 *) 218 (* 219 End TRANSF_PROGRAM. 220 221 (** The following is a variant of [transform_program] where the 222 code transformation function can fail and therefore returns an 223 option type. *) 224 225 Open Local Scope error_monad_scope. 226 Open Local Scope string_scope. 227 228 Section MAP_PARTIAL. 229 230 Variable A B C: Type. 231 Variable prefix_errmsg: A -> errmsg. 232 Variable f: B -> res C. 233 234 Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) := 235 match l with 236 | nil => OK nil 237 | (a, b) :: rem => 238 match f b with 239 | Error msg => Error (prefix_errmsg a ++ msg)%list 240 | OK c => 241 do rem' <- map_partial rem; 242 OK ((a, c) :: rem') 243 end 244 end. 245 246 Remark In_map_partial: 247 forall l l' a c, 248 map_partial l = OK l' -> 249 In (a, c) l' -> 250 exists b, In (a, b) l /\ f b = OK c. 251 Proof. 252 induction l; simpl. 253 intros. inv H. elim H0. 254 intros until c. destruct a as [a1 b1]. 255 caseEq (f b1); try congruence. 256 intro c1; intros. monadInv H0. 257 elim H1; intro. inv H0. exists b1; auto. 258 exploit IHl; eauto. intros [b [P Q]]. exists b; auto. 259 Qed. 260 261 Remark map_partial_forall2: 262 forall l l', 263 map_partial l = OK l' -> 264 list_forall2 265 (fun (a_b: A * B) (a_c: A * C) => 266 fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c)) 267 l l'. 268 Proof. 269 induction l; simpl. 270 intros. inv H. constructor. 271 intro l'. destruct a as [a b]. 272 caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 273 constructor. simpl. auto. auto. 274 Qed. 275 276 End MAP_PARTIAL. 277 278 Remark map_partial_total: 279 forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)), 280 map_partial prefix (fun b => OK (f b)) l = 281 OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l). 282 Proof. 283 induction l; simpl. 284 auto. 285 destruct a as [a1 b1]. rewrite IHl. reflexivity. 286 Qed. 287 288 Remark map_partial_identity: 289 forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)), 290 map_partial prefix (fun b => OK b) l = OK l. 291 Proof. 292 induction l; simpl. 293 auto. 294 destruct a as [a1 b1]. rewrite IHl. reflexivity. 295 Qed. 296 297 Section TRANSF_PARTIAL_PROGRAM. 298 299 Variable A B V: Type. 300 Variable transf_partial: A -> res B. 301 302 Definition prefix_funct_name (id: ident) : errmsg := 303 MSG "In function " :: CTX id :: MSG ": " :: nil. 304 305 Definition transform_partial_program (p: program A V) : res (program B V) := 306 do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct); 307 OK (mkprogram fl p.(prog_main) p.(prog_vars)). 308 309 Lemma transform_partial_program_function: 310 forall p tp i tf, 311 transform_partial_program p = OK tp -> 312 In (i, tf) tp.(prog_funct) -> 313 exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf. 314 Proof. 315 intros. monadInv H. simpl in H0. 316 eapply In_map_partial; eauto. 317 Qed. 318 319 Lemma transform_partial_program_main: 320 forall p tp, 321 transform_partial_program p = OK tp -> 322 tp.(prog_main) = p.(prog_main). 323 Proof. 324 intros. monadInv H. reflexivity. 325 Qed. 326 327 Lemma transform_partial_program_vars: 328 forall p tp, 329 transform_partial_program p = OK tp -> 330 tp.(prog_vars) = p.(prog_vars). 331 Proof. 332 intros. monadInv H. reflexivity. 333 Qed. 334 335 End TRANSF_PARTIAL_PROGRAM. 336 337 (** The following is a variant of [transform_program_partial] where 338 both the program functions and the additional variable information 339 are transformed by functions that can fail. *) 340 341 Section TRANSF_PARTIAL_PROGRAM2. 342 343 Variable A B V W: Type. 344 Variable transf_partial_function: A -> res B. 345 Variable transf_partial_variable: V -> res W. 346 347 Definition prefix_var_name (id_init: ident * list init_data) : errmsg := 348 MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil. 349 350 Definition transform_partial_program2 (p: program A V) : res (program B W) := 351 do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct); 352 do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars); 353 OK (mkprogram fl p.(prog_main) vl). 354 355 Lemma transform_partial_program2_function: 356 forall p tp i tf, 357 transform_partial_program2 p = OK tp -> 358 In (i, tf) tp.(prog_funct) -> 359 exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf. 360 Proof. 361 intros. monadInv H. 362 eapply In_map_partial; eauto. 363 Qed. 364 365 Lemma transform_partial_program2_variable: 366 forall p tp i tv, 367 transform_partial_program2 p = OK tp -> 368 In (i, tv) tp.(prog_vars) -> 369 exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv. 370 Proof. 371 intros. monadInv H. 372 eapply In_map_partial; eauto. 373 Qed. 374 375 Lemma transform_partial_program2_main: 376 forall p tp, 377 transform_partial_program2 p = OK tp -> 378 tp.(prog_main) = p.(prog_main). 379 Proof. 380 intros. monadInv H. reflexivity. 381 Qed. 382 383 End TRANSF_PARTIAL_PROGRAM2. 384 385 (** The following is a relational presentation of 386 [transform_program_partial2]. Given relations between function 387 definitions and between variable information, it defines a relation 388 between programs stating that the two programs have the same shape 389 (same global names, etc) and that identically-named function definitions 390 are variable information are related. *) 391 392 Section MATCH_PROGRAM. 393 394 Variable A B V W: Type. 395 Variable match_fundef: A -> B -> Prop. 396 Variable match_varinfo: V -> W -> Prop. 397 398 Definition match_funct_entry (x1: ident * A) (x2: ident * B) := 399 match x1, x2 with 400 | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2 401 end. 402 403 Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) := 404 match x1, x2 with 405 | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2 406 end. 407 408 Definition match_program (p1: program A V) (p2: program B W) : Prop := 409 list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct) 410 /\ p1.(prog_main) = p2.(prog_main) 411 /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars). 412 413 End MATCH_PROGRAM. 414 415 Remark transform_partial_program2_match: 416 forall (A B V W: Type) 417 (transf_partial_function: A -> res B) 418 (transf_partial_variable: V -> res W) 419 (p: program A V) (tp: program B W), 420 transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp -> 421 match_program 422 (fun fd tfd => transf_partial_function fd = OK tfd) 423 (fun info tinfo => transf_partial_variable info = OK tinfo) 424 p tp. 425 Proof. 426 intros. monadInv H. split. 427 apply list_forall2_imply with 428 (fun (ab: ident * A) (ac: ident * B) => 429 fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)). 430 eapply map_partial_forall2. eauto. 431 intros. destruct v1; destruct v2; simpl in *. auto. 432 split. auto. 433 apply list_forall2_imply with 434 (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) => 435 fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)). 436 eapply map_partial_forall2. eauto. 437 intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence. 438 Qed. 439 *) 440 (* * * External functions *) 441 442 (* * For most languages, the functions composing the program are either 443 internal functions, defined within the language, or external functions 444 (a.k.a. system calls) that emit an event when applied. We define 445 a type for such functions and some generic transformation functions. *) 446 447 record external_function : Type[0] ≝ { 448 ef_id: ident; 449 ef_sig: signature 450 }. 451 452 definition ExternalFunction ≝ external_function. 453 definition external_function_tag ≝ ef_id. 454 definition external_function_sig ≝ ef_sig. 455 456 inductive fundef (F: Type[0]): Type[0] ≝ 457 | Internal: F → fundef F 458 | External: external_function → fundef F. 459 (* 460 (* Implicit Arguments External [F]. *) 461 (* 462 Section TRANSF_FUNDEF. 463 464 Variable A B: Type. 465 Variable transf: A -> B. 466 *) 467 definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝ 468 λA,B,transf,fd. 469 match fd with 470 [ Internal f ⇒ Internal ? (transf f) 471 | External ef ⇒ External ? ef 472 ]. 473 *) 474 (* 475 End TRANSF_FUNDEF. 476 477 Section TRANSF_PARTIAL_FUNDEF. 478 479 Variable A B: Type. 480 Variable transf_partial: A -> res B. 481 482 Definition transf_partial_fundef (fd: fundef A): res (fundef B) := 483 match fd with 484 | Internal f => do f' <- transf_partial f; OK (Internal f') 485 | External ef => OK (External ef) 486 end. 487 488 End TRANSF_PARTIAL_FUNDEF. 489 *) 490 491 492 493 (* Partially merged stuff derived from the prototype cerco compiler. *) 9 494 10 495 definition bool_to_Prop ≝ … … 20 505 ]. 21 506 507 (* TODO: merge in comparison definitions from Integers.ma. *) 22 508 inductive Compare: Type[0] ≝ 23 509 Compare_Equal: Compare … … 27 513 | Compare_GreaterEqual: Compare. 28 514 515 (* XXX unused definitions 29 516 inductive Cast: Type[0] ≝ 30 517 Cast_Int: Byte → Cast … … 32 519 | Cast_StackOffset: Immediate → Cast. 33 520 34 (*35 inductive Op1: Type[0] ≝36 Op1_Cast8U: Op137 | Op1_Cast8S: Op138 | Op1_Cast16U: Op139 | Op1_Cast16S: Op140 | Op1_NegInt: Op141 | Op1_NotBool: Op142 | Op1_NotInt: Op143 (*44 | Op1_NegFloat: Op145 | Op1_AbsFloat: Op146 | Op1_SingleOfFloat: Op147 | Op1_IntOfFloat: Op148 | Op1_IntUOfFloat: Op149 | Op1_FloatOfInt: Op150 | Op1_FloatOfIntU: Op151 *)52 | Op1_Id: Op153 | Op1_PtrOfInt: Op154 | Op1_IntOfPtr: Op1.55 56 inductive Op2: Type[0] ≝57 Op2_Add: Op258 | Op2_Sub: Op259 | Op2_Mul: Op260 | Op2_Div: Op261 | Op2_DivU: Op262 | Op2_Mod: Op263 | Op2_ModU: Op264 | Op2_And: Op265 | Op2_Or: Op266 | Op2_XOr: Op267 | Op2_ShL: Op268 | Op2_ShR: Op269 | Op2_ShRU: Op270 | Op2_AddF: Op271 | Op2_SubF: Op272 | Op2_MulF: Op273 | Op2_DivF: Op274 | Op2_Cmp: Compare → Op275 | Op2_CmpU: Compare → Op276 (*77 | Op2_CmpF: Compare → Op278 *)79 | Op2_AddP: Op280 | Op2_SubP: Op281 | Op2_CmpP: Compare → Op2.82 *)83 84 521 inductive Data: Type[0] ≝ 85 522 Data_Reserve: nat → Data … … 91 528 | DataSize_HalfWord: DataSize 92 529 | DataSize_Word: DataSize. 93 94 inductive SigType: Type[0] ≝ 95 SigType_Int: SigType 96 (* 97 | SigType_Float: SigType 98 *) 99 | SigType_Ptr: SigType. 100 101 inductive TypeReturn: Type[0] ≝ 102 TypeReturn_Ret: SigType → TypeReturn 103 | TypeReturn_Void: TypeReturn. 104 105 record Signature: Type[0] ≝ 106 { 107 signature_args: list SigType; 108 signature_return: TypeReturn 109 }. 110 111 record ExternalFunction: Type[0] ≝ 112 { 113 external_function_tag: Identifier; 114 external_function_sig: Signature 115 }. 530 *) 116 531 117 532 definition Trace ≝ list Identifier. -
src/common/CostLabel.ma
r738 r747 1 include " Clight/AST.ma".1 include "common/AST.ma". 2 2 3 3 axiom CostTag : String. -
src/common/Globalenvs.ma
r744 r747 35 35 36 36 include "common/Errors.ma". 37 include " Clight/AST.ma".37 include "common/AST.ma". 38 38 (*include "Values.ma".*) 39 39 include "common/Mem.ma". -
src/common/Maps.ma
r700 r747 35 35 include "utilities/Coqlib.ma". 36 36 (* XXX: For ident type; should maybe follow original and use positives *) 37 include " Clight/AST.ma".37 include "common/AST.ma". 38 38 39 39 (* -
src/common/Values.ma
r744 r747 18 18 19 19 include "utilities/Coqlib.ma". 20 include " Clight/AST.ma".20 include "common/AST.ma". 21 21 include "common/Integers.ma". 22 22 include "common/Floats.ma". … … 28 28 29 29 include "utilities/binary/Z.ma". 30 include "utilities/extralib.ma". 30 31 31 32 (* To define pointers we need a few details about the memory model. -
src/utilities/Coqlib.ma
r744 r747 18 18 library. *) 19 19 20 include "utilities/binary/Z.ma".21 20 include "basics/types.ma". 22 21 include "basics/list.ma". 23 22 24 include "utilities/extralib.ma".25 23 include "ASM/Util.ma". 26 24 … … 350 348 *) 351 349 (* * Properties of powers of two. *) 352 350 (* 353 351 lemma two_power_nat_O : two_power_nat O = one. 354 352 // qed. … … 362 360 [ // 363 361 | normalize #p elim p // #p' #H >(nat_succ_pos …) // 364 ] qed. 362 ] qed.*) 365 363 (* 366 364 Lemma two_p_monotone:
Note: See TracChangeset
for help on using the changeset viewer.