Changeset 747 for src

Timestamp:

Apr 8, 2011, 2:06:46 PM (9 years ago)

Author:

campbell

Message:

Merge the two AST files together (although some definitions still need to be
harmonised).

Location:

src

Files:

• Clight/AST.ma (deleted)
• Clight/Csyntax.ma (modified) (1 diff)
• RTLabs/RTLabs-syntax.ma (modified) (1 diff)
• common/AST.ma (modified) (5 diffs)
• common/CostLabel.ma (modified) (1 diff)
• common/Globalenvs.ma (modified) (1 diff)
• common/Maps.ma (modified) (1 diff)
• common/Values.ma (modified) (2 diffs)
• utilities/Coqlib.ma (modified) (3 diffs)

src/Clight/Csyntax.ma

@@ -17 +17 @@
 
 (*include "Integers.ma".*)
-include "Clight/AST.ma".
+include "common/AST.ma".
 include "utilities/Coqlib.ma".
 include "common/Errors.ma".

src/RTLabs/RTLabs-syntax.ma

@@ -2 +2 @@
 include "basics/logic.ma".
 
-include "Clight/AST.ma".
+include "common/AST.ma".
 include "common/CostLabel.ma".
 include "common/FrontEndOps.ma".

src/common/AST.ma

@@ -1 @@
-include "arithmetics/nat.ma".
-
-include "ASM/String.ma".
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* * This file defines a number of data types and operations used in
+  the abstract syntax trees of many of the intermediate languages. *)
+
+include "basics/types.ma".
+include "common/Integers.ma".
+include "common/Floats.ma".
 include "ASM/BitVector.ma".
-include "utilities/Compare.ma".
-
+include "common/Identifiers.ma".
+
+
+(* * * Syntactic elements *)
+
+(* Global variables and functions are represented by identifiers with the
+   tag for symbols.  Note that Clight also uses them for locals due to
+   the ambiguous syntax. *)
+
+axiom SymbolTag : String.
+
+definition ident ≝ identifier SymbolTag.
+
+definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?.
+
+definition ident_of_nat : nat → ident ≝ identifier_of_nat ?.
+
+(* XXX backend is currently using untagged words as identifiers. *)
 definition Identifier ≝ Word.
-definition Immediate ≝ nat.
+
+definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
+
+(* Memory spaces *)
+
+inductive region : Type[0] ≝
+  | Any : region
+  | Data : region
+  | IData : region
+  | PData : region
+  | XData : region
+  | Code : region.
+
+definition eq_region : region → region → bool ≝
+λr1,r2.
+  match r1 with
+  [ Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
+  | Data ⇒  match r2 with [ Data ⇒ true | _ ⇒ false ]
+  | IData ⇒ match r2 with [ IData ⇒ true | _ ⇒ false ]
+  | PData ⇒ match r2 with [ PData ⇒ true | _ ⇒ false ]
+  | XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
+  | Code ⇒  match r2 with [ Code ⇒ true | _ ⇒ false ]
+  ].
+
+lemma eq_region_elim : ∀P:bool → Type[0]. ∀r1,r2.
+  (r1 = r2 → P true) → (r1 ≠ r2 → P false) →
+  P (eq_region r1 r2).
+#P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse
+try ( @Ptrue // )
+@Pfalse % #E destruct;
+qed.
+
+definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
+#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
+
+definition size_pointer : region → nat ≝
+λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
+
+(* * The intermediate languages are weakly typed, using only three types:
+  [ASTint] for integers, [ASTptr] for pointers, and [ASTfloat] for floating-point
+  numbers. *)
+
+inductive typ : Type[0] ≝
+  | ASTint : typ
+  | ASTptr : region → typ
+  | ASTfloat : typ.
+
+(* XXX aliases *)
+definition SigType ≝ typ.
+definition SigType_Int ≝ ASTint.
+(*
+| SigType_Float: SigType
+*)
+definition SigType_Ptr ≝ ASTptr Any.
+
+
+(* FIXME: ASTint size is not 1 for Clight32 *)
+definition typesize : typ → nat ≝ λty.
+  match ty with [ ASTint ⇒ 1 | ASTptr r ⇒ size_pointer r | ASTfloat ⇒ 8 ].
+
+lemma typesize_pos: ∀ty. typesize ty > 0.
+#ty cases ty [ 2: * ] /2/ qed.
+
+lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
+#t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct; qed.
+
+lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
+#t1 #t2 cases t1 cases t2
+[ %1 @refl
+| 2,3: #ty %2 % #H destruct
+| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/
+]
+qed.
+
+(* * Additionally, function definitions and function calls are annotated
+  by function signatures indicating the number and types of arguments,
+  as well as the type of the returned value if any.  These signatures
+  are used in particular to determine appropriate calling conventions
+  for the function. *)
+
+record signature : Type[0] ≝ {
+  sig_args: list typ;
+  sig_res: option typ
+}.
+
+(* XXX aliases *)
+definition Signature ≝ signature.
+definition signature_args ≝ sig_args.
+definition signature_return ≝ sig_res.
+
+definition proj_sig_res : signature → typ ≝ λs.
+  match sig_res s with
+  [ None ⇒ ASTint
+  | Some t ⇒ t
+  ].
+
+(* * Memory accesses (load and store instructions) are annotated by
+  a ``memory chunk'' indicating the type, size and signedness of the
+  chunk of memory being accessed. *)
+
+inductive memory_chunk : Type[0] ≝
+  | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
+  | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
+  | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
+  | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
+  | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
+  | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
+  | Mfloat64 : memory_chunk        (*r 64-bit double-precision float *)
+  | Mpointer : region → memory_chunk. (* pointer addressing given region *)
+
+(* * Initialization data for global variables. *)
+
+inductive init_data: Type[0] ≝ 
+  | Init_int8: int → init_data
+  | Init_int16: int → init_data
+  | Init_int32: int → init_data
+  | Init_float32: float → init_data
+  | Init_float64: float → init_data
+  | Init_space: nat → init_data 
+  | Init_null: region → init_data
+  | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
+
+(* * Whole programs consist of:
+- a collection of function definitions (name and description);
+- the name of the ``main'' function that serves as entry point in the program;
+- a collection of global variable declarations, consisting of
+  a name, initialization data, and additional information.
+
+The type of function descriptions and that of additional information
+for variables vary among the various intermediate languages and are
+taken as parameters to the [program] type.  The other parts of whole
+programs are common to all languages. *)
+
+record program (F,V: Type[0]) : Type[0] := {
+  prog_funct: list (ident × F);
+  prog_main: ident;
+  prog_vars: list (ident × (list init_data) × region × V)
+}.
+
+definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
+  map ?? (fst ident F) (prog_funct ?? p).
+
+definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
+  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
+(*
+(** * Generic transformations over programs *)
+
+(** We now define a general iterator over programs that applies a given
+  code transformation function to all function descriptions and leaves
+  the other parts of the program unchanged. *)
+
+Section TRANSF_PROGRAM.
+
+Variable A B V: Type.
+Variable transf: A -> B.
+*)
+
+definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
+λA,B,transf,l.
+  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
+
+definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
+λA,B,V,transf,p.
+  mk_program B V
+    (transf_program ?? transf (prog_funct A V p))
+    (prog_main A V p)
+    (prog_vars A V p).
+(*
+lemma transform_program_function:
+  ∀A,B,V,transf,p,i,tf.
+  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
+  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
+normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
+#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
+qed.
+*)
+(*
+End TRANSF_PROGRAM.
+
+(** The following is a variant of [transform_program] where the
+  code transformation function can fail and therefore returns an
+  option type. *)
+
+Open Local Scope error_monad_scope.
+Open Local Scope string_scope.
+
+Section MAP_PARTIAL.
+
+Variable A B C: Type.
+Variable prefix_errmsg: A -> errmsg.
+Variable f: B -> res C.
+
+Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
+  match l with
+  | nil => OK nil
+  | (a, b) :: rem =>
+      match f b with
+      | Error msg => Error (prefix_errmsg a ++ msg)%list
+      | OK c =>
+          do rem' <- map_partial rem; 
+          OK ((a, c) :: rem')
+      end
+  end.
+
+Remark In_map_partial:
+  forall l l' a c,
+  map_partial l = OK l' ->
+  In (a, c) l' ->
+  exists b, In (a, b) l /\ f b = OK c.
+Proof.
+  induction l; simpl.
+  intros. inv H. elim H0.
+  intros until c. destruct a as [a1 b1].
+  caseEq (f b1); try congruence.
+  intro c1; intros. monadInv H0. 
+  elim H1; intro. inv H0. exists b1; auto. 
+  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
+Qed.
+
+Remark map_partial_forall2:
+  forall l l',
+  map_partial l = OK l' ->
+  list_forall2
+    (fun (a_b: A * B) (a_c: A * C) =>
+       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
+    l l'.
+Proof.
+  induction l; simpl.
+  intros. inv H. constructor.
+  intro l'. destruct a as [a b].
+  caseEq (f b). 2: congruence. intro c; intros. monadInv H0.  
+  constructor. simpl. auto. auto. 
+Qed.
+
+End MAP_PARTIAL.
+
+Remark map_partial_total:
+  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
+  map_partial prefix (fun b => OK (f b)) l =
+  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
+Proof.
+  induction l; simpl.
+  auto.
+  destruct a as [a1 b1]. rewrite IHl. reflexivity.
+Qed.
+
+Remark map_partial_identity:
+  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
+  map_partial prefix (fun b => OK b) l = OK l.
+Proof.
+  induction l; simpl.
+  auto.
+  destruct a as [a1 b1]. rewrite IHl. reflexivity.
+Qed.
+
+Section TRANSF_PARTIAL_PROGRAM.
+
+Variable A B V: Type.
+Variable transf_partial: A -> res B.
+
+Definition prefix_funct_name (id: ident) : errmsg :=
+  MSG "In function " :: CTX id :: MSG ": " :: nil.
+
+Definition transform_partial_program (p: program A V) : res (program B V) :=
+  do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct);
+  OK (mkprogram fl p.(prog_main) p.(prog_vars)).
+
+Lemma transform_partial_program_function:
+  forall p tp i tf,
+  transform_partial_program p = OK tp ->
+  In (i, tf) tp.(prog_funct) ->
+  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
+Proof.
+  intros. monadInv H. simpl in H0.  
+  eapply In_map_partial; eauto.
+Qed.
+
+Lemma transform_partial_program_main:
+  forall p tp,
+  transform_partial_program p = OK tp ->
+  tp.(prog_main) = p.(prog_main).
+Proof.
+  intros. monadInv H. reflexivity.
+Qed.
+
+Lemma transform_partial_program_vars:
+  forall p tp,
+  transform_partial_program p = OK tp ->
+  tp.(prog_vars) = p.(prog_vars).
+Proof.
+  intros. monadInv H. reflexivity.
+Qed.
+
+End TRANSF_PARTIAL_PROGRAM.
+
+(** The following is a variant of [transform_program_partial] where
+  both the program functions and the additional variable information
+  are transformed by functions that can fail. *)
+
+Section TRANSF_PARTIAL_PROGRAM2.
+
+Variable A B V W: Type.
+Variable transf_partial_function: A -> res B.
+Variable transf_partial_variable: V -> res W.
+
+Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
+  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
+
+Definition transform_partial_program2 (p: program A V) : res (program B W) :=
+  do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct);
+  do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars);
+  OK (mkprogram fl p.(prog_main) vl).
+
+Lemma transform_partial_program2_function:
+  forall p tp i tf,
+  transform_partial_program2 p = OK tp ->
+  In (i, tf) tp.(prog_funct) ->
+  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
+Proof.
+  intros. monadInv H.  
+  eapply In_map_partial; eauto. 
+Qed.
+
+Lemma transform_partial_program2_variable:
+  forall p tp i tv,
+  transform_partial_program2 p = OK tp ->
+  In (i, tv) tp.(prog_vars) ->
+  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
+Proof.
+  intros. monadInv H. 
+  eapply In_map_partial; eauto. 
+Qed.
+
+Lemma transform_partial_program2_main:
+  forall p tp,
+  transform_partial_program2 p = OK tp ->
+  tp.(prog_main) = p.(prog_main).
+Proof.
+  intros. monadInv H. reflexivity.
+Qed.
+
+End TRANSF_PARTIAL_PROGRAM2.
+
+(** The following is a relational presentation of 
+  [transform_program_partial2].  Given relations between function
+  definitions and between variable information, it defines a relation
+  between programs stating that the two programs have the same shape
+  (same global names, etc) and that identically-named function definitions 
+  are variable information are related. *)
+
+Section MATCH_PROGRAM.
+
+Variable A B V W: Type.
+Variable match_fundef: A -> B -> Prop.
+Variable match_varinfo: V -> W -> Prop.
+
+Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
+  match x1, x2 with
+  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
+  end.
+
+Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
+  match x1, x2 with
+  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
+  end.
+
+Definition match_program (p1: program A V) (p2: program B W) : Prop :=
+  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
+  /\ p1.(prog_main) = p2.(prog_main)
+  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
+
+End MATCH_PROGRAM.
+
+Remark transform_partial_program2_match:
+  forall (A B V W: Type)
+         (transf_partial_function: A -> res B)
+         (transf_partial_variable: V -> res W)
+         (p: program A V) (tp: program B W),
+  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
+  match_program 
+    (fun fd tfd => transf_partial_function fd = OK tfd)
+    (fun info tinfo => transf_partial_variable info = OK tinfo)
+    p tp.
+Proof.
+  intros. monadInv H. split.
+  apply list_forall2_imply with
+    (fun (ab: ident * A) (ac: ident * B) =>
+       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
+  eapply map_partial_forall2. eauto. 
+  intros. destruct v1; destruct v2; simpl in *. auto.
+  split. auto.
+  apply list_forall2_imply with
+    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
+       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
+  eapply map_partial_forall2. eauto. 
+  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
+Qed.
+*)
+(* * * External functions *)
+
+(* * For most languages, the functions composing the program are either
+  internal functions, defined within the language, or external functions
+  (a.k.a. system calls) that emit an event when applied.  We define
+  a type for such functions and some generic transformation functions. *)
+
+record external_function : Type[0] ≝ {
+  ef_id: ident;
+  ef_sig: signature
+}.
+
+definition ExternalFunction ≝ external_function.
+definition external_function_tag ≝ ef_id.
+definition external_function_sig ≝ ef_sig.
+
+inductive fundef (F: Type[0]): Type[0] ≝
+  | Internal: F → fundef F
+  | External: external_function → fundef F.
+(*
+(* Implicit Arguments External [F]. *)
+(*
+Section TRANSF_FUNDEF.
+
+Variable A B: Type.
+Variable transf: A -> B.
+*)
+definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
+λA,B,transf,fd.
+  match fd with
+  [ Internal f ⇒ Internal ? (transf f)
+  | External ef ⇒ External ? ef
+  ].
+*)
+(*
+End TRANSF_FUNDEF.
+
+Section TRANSF_PARTIAL_FUNDEF.
+
+Variable A B: Type.
+Variable transf_partial: A -> res B.
+
+Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
+  match fd with
+  | Internal f => do f' <- transf_partial f; OK (Internal f')
+  | External ef => OK (External ef)
+  end.
+
+End TRANSF_PARTIAL_FUNDEF.
+*)
+
+
+
+(* Partially merged stuff derived from the prototype cerco compiler. *)
 
 definition bool_to_Prop ≝
@@ -20 +505 @@
   ].
 
+(* TODO: merge in comparison definitions from Integers.ma. *)
 inductive Compare: Type[0] ≝
   Compare_Equal: Compare
@@ -27 +513 @@
 | Compare_GreaterEqual: Compare.
 
+(* XXX unused definitions
 inductive Cast: Type[0] ≝
   Cast_Int: Byte → Cast
@@ -32 +519 @@
 | Cast_StackOffset: Immediate → Cast.
 
-(*
-inductive Op1: Type[0] ≝
-  Op1_Cast8U: Op1
-| Op1_Cast8S: Op1
-| Op1_Cast16U: Op1
-| Op1_Cast16S: Op1
-| Op1_NegInt: Op1
-| Op1_NotBool: Op1
-| Op1_NotInt: Op1
-(*
-| Op1_NegFloat: Op1
-| Op1_AbsFloat: Op1
-| Op1_SingleOfFloat: Op1
-| Op1_IntOfFloat: Op1
-| Op1_IntUOfFloat: Op1
-| Op1_FloatOfInt: Op1
-| Op1_FloatOfIntU: Op1
-*)
-| Op1_Id: Op1
-| Op1_PtrOfInt: Op1
-| Op1_IntOfPtr: Op1.
-
-inductive Op2: Type[0] ≝
-  Op2_Add: Op2
-| Op2_Sub: Op2
-| Op2_Mul: Op2
-| Op2_Div: Op2
-| Op2_DivU: Op2
-| Op2_Mod: Op2
-| Op2_ModU: Op2
-| Op2_And: Op2
-| Op2_Or: Op2
-| Op2_XOr: Op2
-| Op2_ShL: Op2
-| Op2_ShR: Op2
-| Op2_ShRU: Op2
-| Op2_AddF: Op2
-| Op2_SubF: Op2
-| Op2_MulF: Op2
-| Op2_DivF: Op2
-| Op2_Cmp: Compare → Op2
-| Op2_CmpU: Compare → Op2
-(*
-| Op2_CmpF: Compare → Op2
-*)
-| Op2_AddP: Op2
-| Op2_SubP: Op2
-| Op2_CmpP: Compare → Op2.
-*)
-
 inductive Data: Type[0] ≝
   Data_Reserve: nat → Data
@@ -91 +528 @@
 | DataSize_HalfWord: DataSize
 | DataSize_Word: DataSize.
-
-inductive SigType: Type[0] ≝
-  SigType_Int: SigType
-(*
-| SigType_Float: SigType
-*)
-| SigType_Ptr: SigType.
-
-inductive TypeReturn: Type[0] ≝
-  TypeReturn_Ret: SigType → TypeReturn
-| TypeReturn_Void: TypeReturn.
-
-record Signature: Type[0] ≝
-{
-  signature_args: list SigType;
-  signature_return: TypeReturn
-}.
-
-record ExternalFunction: Type[0] ≝
-{
-  external_function_tag: Identifier;
-  external_function_sig: Signature
-}.
+*)
 
 definition Trace ≝ list Identifier.

src/common/CostLabel.ma

@@ -1 @@
-include "Clight/AST.ma".
+include "common/AST.ma".
 
 axiom CostTag : String.

src/common/Globalenvs.ma

@@ -35 +35 @@
 
 include "common/Errors.ma".
-include "Clight/AST.ma".
+include "common/AST.ma".
 (*include "Values.ma".*)
 include "common/Mem.ma".

src/common/Maps.ma

@@ -35 +35 @@
 include "utilities/Coqlib.ma".
 (* XXX: For ident type; should maybe follow original and use positives *)
-include "Clight/AST.ma".
+include "common/AST.ma".
 
 (*

src/common/Values.ma

@@ -18 +18 @@
 
 include "utilities/Coqlib.ma".
-include "Clight/AST.ma".
+include "common/AST.ma".
 include "common/Integers.ma".
 include "common/Floats.ma".
@@ -28 +28 @@
 
 include "utilities/binary/Z.ma".
+include "utilities/extralib.ma".
 
 (* To define pointers we need a few details about the memory model.

src/utilities/Coqlib.ma

@@ -18 +18 @@
     library. *)
 
-include "utilities/binary/Z.ma".
 include "basics/types.ma".
 include "basics/list.ma".
 
-include "utilities/extralib.ma".
 include "ASM/Util.ma".
 
@@ -350 +348 @@
 *)
 (* * Properties of powers of two. *)
-
+(*
 lemma two_power_nat_O : two_power_nat O = one.
 // qed.
@@ -362 +360 @@
 [ //
 | normalize #p elim p // #p' #H >(nat_succ_pos …) //
-] qed.
+] qed.*)
 (*
 Lemma two_p_monotone: