Machblock: some cleaning

4 files changed, 146 insertions, 203 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 86bfa248..3fe1ea2e 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -90,13 +90,6 @@ Ltac exploit x :=
  || refine (modusponens _ _ (x _ _) _)
  || refine (modusponens _ _ (x _) _).
 
-Ltac totologize H :=
-  match type of H with
-  | ( ?id = _ ) =>
-    let Hassert := fresh "Htoto" in (
-    assert (id = id) as Hassert; auto; rewrite H in Hassert at 2; simpl in Hassert; rewrite H in Hassert)
-  end.
-
 (** * Definitions and theorems over the type [positive] *)
 
 Definition peq: forall (x y: positive), {x = y} + {x <> y} := Pos.eq_dec.
diff --git a/mppa_k1c/Machblock.v b/mppa_k1c/Machblock.v
index 9b36fc43..6d28844b 100644
--- a/mppa_k1c/Machblock.v
+++ b/mppa_k1c/Machblock.v
@@ -55,7 +55,7 @@ Proof.
 Qed.
 
 Definition length_opt {A} (o: option A) : nat :=
-  match o with 
+  match o with
   | Some o => 1
   | None => 0
   end.
@@ -110,10 +110,11 @@ Qed.
 
 Local Open Scope nat_scope.
 
+(* FIXME - avoir une définition un peu plus simple, au prix de la preuve Mach -> Machblock ? *)
 Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
   match c with
   | nil => None
-  | bb1 :: bbl => if is_label lbl bb1 
+  | bb1 :: bbl => if is_label lbl bb1
       then let bb' := {| header := None ; body := body bb1 ; exit := exit bb1 |} in (
         Some (match size bb' with
         | O => bbl
@@ -191,7 +192,7 @@ Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (m:
   | exec_MBsetstack:
       forall src ofs ty m' rs',
       store_stack m sp ty ofs (rs src) = Some m' ->
-      rs' = undef_regs (destroyed_by_setstack ty) rs -> 
+      rs' = undef_regs (destroyed_by_setstack ty) rs ->
       basic_step s fb sp rs m (MBsetstack src ofs ty) rs' m'
   | exec_MBgetparam:
       forall ofs ty dst v rs' f,
@@ -225,8 +226,8 @@ Inductive body_step (s: list stackframe) (f: block) (sp: val): bblock_body -> re
        forall rs m,
        body_step s f sp nil rs m rs m
    | exec_cons_body:
-       forall rs m bi p rs' m' rs'' m'', 
-       basic_step s f sp rs m bi rs' m' -> 
+       forall rs m bi p rs' m' rs'' m'',
+       basic_step s f sp rs m bi rs' m' ->
        body_step s f sp p rs' m' rs'' m'' ->
        body_step s f sp (bi::p) rs m rs'' m''
    .
diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v
index 93284b0b..039e6c6e 100644
--- a/mppa_k1c/Machblockgen.v
+++ b/mppa_k1c/Machblockgen.v
@@ -26,14 +26,13 @@ Definition to_basic_inst(i: Mach.instruction): option basic_inst :=
   | _ => None
   end.
 
-(* version pas récursive terminale, mais plus facile pour la preuve *)
 Fixpoint to_bblock_body(c: Mach.code): bblock_body * Mach.code :=
   match c with
   | nil => (nil,nil)
-  | i::c' => 
+  | i::c' =>
     match to_basic_inst i with
-    | Some bi => 
-       let (p,c'') := to_bblock_body c' in 
+    | Some bi =>
+       let (p,c'') := to_bblock_body c' in
        (bi::p, c'')
     | None => (nil, c)
     end
@@ -61,7 +60,7 @@ Definition to_cfi (i: Mach.instruction): option control_flow_inst :=
 Definition to_bblock_exit (c: Mach.code): option control_flow_inst * Mach.code :=
   match c with
   | nil => (None,nil)
-  | i::c' => 
+  | i::c' =>
     match to_cfi i with
     | Some bi as o => (o, c')
     | None => (None, c)
@@ -80,195 +79,162 @@ Definition get_code_nature (c: Mach.code): code_nature :=
          end
   end.
 
-Ltac Discriminate :=
-  match goal with
-  | [ H: ?a <> ?a |- _ ] => contradict H; auto
-  | _ => discriminate
-  end.
-
-
 Lemma cn_eqdec (cn1 cn2: code_nature): { cn1=cn2 } + {cn1 <> cn2}.
 Proof.
   decide equality.
-Qed.  
+Qed.
 
 Lemma get_code_nature_nil c: c<>nil -> get_code_nature c <> IsEmpty.
 Proof.
-  intro. unfold get_code_nature. destruct c; try Discriminate.
+  intros H. unfold get_code_nature.
+  destruct c; try (contradict H; auto; fail).
   destruct i; discriminate.
 Qed.
 
 Lemma get_code_nature_nil_contra c: get_code_nature c = IsEmpty -> c = nil.
 Proof.
-  intro. destruct c; auto. exploit (get_code_nature_nil (i::c)); discriminate || auto.
-  intro. contradict H0.
+  intros H. destruct c; auto. exploit (get_code_nature_nil (i::c)); discriminate || auto.
+  intro F. contradict F.
 Qed.
 
-Lemma get_code_nature_basic_inst:
-  forall c a c0,
+Lemma get_code_nature_basic_inst c a c0:
   c = a :: c0 ->
   get_code_nature c = IsBasicInst ->
   to_basic_inst a <> None.
 Proof.
-  intros. destruct a; discriminate || contradict H0; subst; simpl; discriminate.
+  intros H1 H2. destruct a; discriminate || contradict H2; subst; simpl; discriminate.
 Qed.
 
-Lemma to_bblock_header_not_IsLabel:
-  forall c b c0,
+Lemma to_bblock_header_not_IsLabel c b c0:
   get_code_nature c <> IsLabel ->
   to_bblock_header c = (b, c0) ->
   c = c0 /\ b=None.
 Proof.
-  intros. destruct c.
-  - simpl in H0; inversion H0; auto.
-  - destruct i; unfold to_bblock_header in H0; inversion H0; auto.
-    simpl in H; contradict H; auto.
+  intros H1 H2. destruct c.
+  - simpl in H2; inversion H2; auto.
+  - destruct i; unfold to_bblock_header in H2; inversion H2; auto.
+    simpl in H1; contradict H1; auto.
 Qed.
 
-
-Lemma to_bblock_header_eq:
-  forall c b c0,
+Lemma to_bblock_header_eq c b c0:
   get_code_nature c <> IsLabel ->
   to_bblock_header c = (b, c0) ->
   c = c0.
 Proof.
-  intros; exploit to_bblock_header_not_IsLabel; intuition eauto.
+  intros H1 H2; exploit to_bblock_header_not_IsLabel; intuition eauto.
 Qed.
 
-Lemma to_bblock_header_IsLabel: 
-  forall c c0 b, 
-  get_code_nature c = IsLabel -> 
+Lemma to_bblock_header_IsLabel c c0 b:
+  get_code_nature c = IsLabel ->
   to_bblock_header c = (b, c0) ->
   exists l, c = (Mlabel l)::c0.
 Proof.
-  intros. destruct c; try discriminate.
+  intros H1 H2. destruct c; try discriminate.
   destruct i; try discriminate.
-  unfold to_bblock_header in H0; inversion H0; eauto.
+  unfold to_bblock_header in H2; inversion H2; eauto.
 Qed.
 
-Lemma to_bblock_header_wf: 
-  forall c b c0, 
-  get_code_nature c = IsLabel -> 
+Lemma to_bblock_header_wf c b c0:
+  get_code_nature c = IsLabel ->
   to_bblock_header c = (b, c0) ->
   (length c > length c0)%nat.
 Proof.
-  intros; exploit to_bblock_header_IsLabel; eauto.
-  intros [l H1]; subst; simpl; auto.
+  intros H1 H2; exploit to_bblock_header_IsLabel; eauto.
+  intros [l X]; subst; simpl; auto.
 Qed.
 
-Ltac ExploitHeaderEq := 
-  match goal with
-  | [ H: to_bblock_header (?i0 :: ?c) = (?b, ?c0) |- _ ] =>
-      exploit (to_bblock_header_eq (i0::c) b c0); [subst; simpl; discriminate | auto | intro; subst; auto]
-  | _ => idtac
-  end.
-
-Lemma to_bblock_header_wfe:
-  forall c b c0,
+Lemma to_bblock_header_wfe c b c0:
   to_bblock_header c = (b, c0) ->
   (length c >= length c0)%nat.
 Proof.
-  intros c b c0; destruct (cn_eqdec (get_code_nature c) IsLabel).
+  destruct (cn_eqdec (get_code_nature c) IsLabel).
   - intros; exploit to_bblock_header_wf; eauto; omega.
   - intros; exploit to_bblock_header_eq; eauto. intros; subst; auto.
 Qed.
 
-Lemma to_bblock_body_eq:
-  forall c b c0,
+Lemma to_bblock_body_eq c b c0:
   get_code_nature c <> IsBasicInst ->
   to_bblock_body c = (b, c0) ->
   c = c0.
 Proof.
-  intros. destruct c.
-  - simpl in H0. inversion H0. auto.
-  - destruct i; simpl in *; try Discriminate || inversion H0; subst; auto.
+  intros H1 H2. destruct c.
+  - simpl in H2. inversion H2. auto.
+  - destruct i; try ( simpl in *; destruct H1; auto; fail ).
+    all: simpl in *; inversion H2; subst; clear H2; auto.
 Qed.
 
-Lemma to_bblock_body_wfe:
-  forall c b c0,
+Lemma to_bblock_body_wfe c b c0:
   to_bblock_body c = (b, c0) ->
   (length c >= length c0)%nat.
 Proof.
-  induction c.
-  - intros. simpl in H. inversion H. subst. auto.
-  - intros. simpl in H. destruct (to_basic_inst a).
-    + remember (to_bblock_body c) as tbbc. destruct tbbc as [p c''].
-      exploit (IHc p c''); auto. inversion H. subst. simpl. omega.
+  generalize b c0; clear b c0.
+  induction c as [|i c].
+  - intros b c0 H. simpl in H. inversion H; subst; auto.
+  - intros b c0 H. simpl in H. destruct (to_basic_inst i).
+    + remember (to_bblock_body c) as tbbc; destruct tbbc as [p c''].
+      exploit (IHc p c''); auto. inversion H; subst; simpl; omega.
     + inversion H; subst; auto.
 Qed.
 
-
 Inductive cons_to_bblock_body c0: Mach.code -> bblock_body -> Prop :=
-  Cons_to_bbloc_body i bi c' b': 
+  Cons_to_bbloc_body i bi c' b':
     to_basic_inst i = Some bi
     -> to_bblock_body c' = (b', c0)
     -> cons_to_bblock_body c0 (i::c') (bi::b').
 
-Lemma to_bblock_body_IsBasicInst: 
-  forall c b c0, 
+Lemma to_bblock_body_IsBasicInst c b c0:
   get_code_nature c = IsBasicInst ->
-  to_bblock_body c = (b, c0) -> 
+  to_bblock_body c = (b, c0) ->
   cons_to_bblock_body c0 c b.
 Proof.
-  intros. destruct c; [ contradict H; simpl; discriminate | ].
+  intros H1 H2. destruct c; [ contradict H1; simpl; discriminate | ].
   remember (to_basic_inst i) as tbii. destruct tbii.
-  - simpl in H0. rewrite <- Heqtbii in H0.
+  - simpl in H2. rewrite <- Heqtbii in H2.
     remember (to_bblock_body c) as tbbc. destruct tbbc as [p1 c1].
-    inversion H0. subst. eapply Cons_to_bbloc_body; eauto.
+    inversion H2. subst. eapply Cons_to_bbloc_body; eauto.
   - destruct i; try discriminate.
 Qed.
 
-Lemma to_bblock_body_wf: 
-  forall c b c0, 
+Lemma to_bblock_body_wf c b c0:
   get_code_nature c = IsBasicInst ->
-  to_bblock_body c = (b, c0) -> 
+  to_bblock_body c = (b, c0) ->
   (length c > length c0)%nat.
 Proof.
-  intros; exploit to_bblock_body_IsBasicInst; eauto.
-  intros H1; destruct H1.
+  intros H1 H2; exploit to_bblock_body_IsBasicInst; eauto.
+  intros X; destruct X.
   exploit to_bblock_body_wfe; eauto.
   simpl; omega.
 Qed.
 
-Lemma to_bblock_exit_eq:
-  forall c b c0,
+Lemma to_bblock_exit_eq c b c0:
   get_code_nature c <> IsCFI ->
   to_bblock_exit c = (b, c0) ->
   c = c0.
 Proof.
-  intros. destruct c.
-  - simpl in H0; inversion H0; auto.
-  - destruct i; unfold to_bblock_header in H0; inversion H0; auto;
-    simpl in H; contradict H; auto.
+  intros H1 H2. destruct c as [|i c].
+  - simpl in H2; inversion H2; auto.
+  - destruct i; unfold to_bblock_header in H2; inversion H2; auto;
+    simpl in H1; contradict H1; auto.
 Qed.
 
-Lemma to_bblock_exit_wf:
-  forall c b c0,
+Lemma to_bblock_exit_wf c b c0:
   get_code_nature c = IsCFI ->
   to_bblock_exit c = (b, c0) ->
   (length c > length c0)%nat.
 Proof.
-  intros. destruct c; try discriminate.
+  intros H1 H2. destruct c as [|i c]; try discriminate.
   destruct i; try discriminate;
-  unfold to_bblock_header in H0; inversion H0; auto.
+  unfold to_bblock_header in H2; inversion H2; auto.
 Qed.
 
-Ltac ExploitExitEq := 
-  match goal with
-  | [ H: to_bblock_exit (?i0 :: ?c) = (?b, ?c0) |- _ ] =>
-      exploit (to_bblock_exit_eq (i0::c) b c0); [subst; simpl; discriminate | auto | intro; subst; auto]
-  | _ => idtac
-  end.
-
-Lemma to_bblock_exit_wfe:
-  forall c b c0,
+Lemma to_bblock_exit_wfe c b c0:
   to_bblock_exit c = (b, c0) ->
   (length c >= length c0)%nat.
 Proof.
-  intros. destruct c. unfold to_bblock_exit in H; inversion H; auto.
-  remember i as i0.
-  destruct i; try ExploitExitEq.
-  all: exploit (to_bblock_exit_wf (i0::c) b c0); [subst; simpl; auto | auto | try omega].
+  intros H. destruct c as [|i c].
+  - simpl in H. inversion H; subst; clear H; auto.
+  - destruct i; try ( simpl in H; inversion H; subst; clear H; auto ).
+    all: simpl; auto.
 Qed.
 
 Definition to_bblock(c: Mach.code): bblock * Mach.code :=
@@ -278,45 +244,41 @@ Definition to_bblock(c: Mach.code): bblock * Mach.code :=
   ({| header := h; body := bdy; exit := ext |}, c2)
   .
 
-Lemma to_bblock_double_label:
-  forall c l,
+Lemma to_bblock_double_label c l:
   get_code_nature c = IsLabel ->
   to_bblock (Mlabel l :: c) = ({| header := Some l; body := nil; exit := None |}, c).
 Proof.
-  intros.
-  destruct c; try (contradict H; simpl; discriminate).
+  intros H.
+  destruct c as [|i c]; try (contradict H; simpl; discriminate).
   destruct i; try (contradict H; simpl; discriminate).
-  simpl. auto.
+  auto.
 Qed.
 
-Lemma to_bblock_basic_inst_then_label:
-  forall i c bi,
+Lemma to_bblock_basic_inst_then_label i c bi:
   get_code_nature (i::c) = IsBasicInst ->
   get_code_nature c = IsLabel ->
   to_basic_inst i = Some bi ->
   fst (to_bblock (i::c)) = {| header := None; body := bi::nil; exit := None |}.
 Proof.
-  intros.
-  destruct c; try (contradict H; simpl; discriminate).
-  destruct i0; try (contradict H; simpl; discriminate).
-  destruct i; simpl in *; inversion H1; subst; auto.
+  intros H1 H2 H3.
+  destruct c as [|i' c]; try (contradict H1; simpl; discriminate).
+  destruct i'; try (contradict H1; simpl; discriminate).
+  destruct i; simpl in *; inversion H3; subst; auto.
 Qed.
 
-Lemma to_bblock_cf_inst_then_label:
-  forall i c cfi,
+Lemma to_bblock_cf_inst_then_label i c cfi:
   get_code_nature (i::c) = IsCFI ->
   get_code_nature c = IsLabel ->
   to_cfi i = Some cfi ->
   fst (to_bblock (i::c)) = {| header := None; body := nil; exit := Some cfi |}.
 Proof.
-  intros.
-  destruct c; try (contradict H; simpl; discriminate).
-  destruct i0; try (contradict H; simpl; discriminate).
-  destruct i; simpl in *; inversion H1; subst; auto.
+  intros H1 H2 H3.
+  destruct c as [|i' c]; try (contradict H1; simpl; discriminate).
+  destruct i'; try (contradict H1; simpl; discriminate).
+  destruct i; simpl in *; inversion H3; subst; auto.
 Qed.
 
-Lemma to_bblock_single_label:
-  forall c l,
+Lemma to_bblock_single_label c l:
   get_code_nature c <> IsLabel ->
   fst (to_bblock (Mlabel l :: c)) = {|
     header := Some l;
@@ -324,8 +286,8 @@ Lemma to_bblock_single_label:
     exit := exit (fst (to_bblock c))
   |}.
 Proof.
-  intros.
-  destruct c; simpl; auto.
+  intros H.
+  destruct c as [|i c]; simpl; auto.
   apply bblock_eq; simpl.
 (* header *)
   + destruct i; try (
@@ -361,8 +323,7 @@ Proof.
       ). contradict H; simpl; auto.
 Qed.
 
-Lemma to_bblock_no_label:
-  forall c,
+Lemma to_bblock_no_label c:
   get_code_nature c <> IsLabel ->
   fst (to_bblock c) = {|
     header := None;
@@ -370,8 +331,8 @@ Lemma to_bblock_no_label:
     exit := exit (fst (to_bblock c))
   |}.
 Proof.
-  intros.
-  destruct c; simpl; auto.
+  intros H.
+  destruct c as [|i c]; simpl; auto.
   apply bblock_eq; simpl;
   destruct i; (
       try (
@@ -391,7 +352,7 @@ Lemma to_bblock_body_nil c c':
   c = c'.
 Proof.
   intros H.
-  destruct c; [ simpl in *; inversion H; auto |].
+  destruct c as [|i c]; [ simpl in *; inversion H; auto |].
   destruct i; try ( simpl in *; remember (to_bblock_body c) as tbc; destruct tbc as [p c'']; inversion H ).
   all: auto.
 Qed.
@@ -401,7 +362,7 @@ Lemma to_bblock_exit_nil c c':
   c = c'.
 Proof.
   intros H.
-  destruct c; [ simpl in *; inversion H; auto |].
+  destruct c as [|i c]; [ simpl in *; inversion H; auto |].
   destruct i; try ( simpl in *; remember (to_bblock_exit c) as tbe; destruct tbe as [p c'']; inversion H ).
   all: auto.
 Qed.
@@ -411,8 +372,7 @@ Lemma to_bblock_label b l c c':
   exists bdy c1, to_bblock_body c = (bdy, c1) /\
   header b = Some l /\ body b = bdy /\ exit b = fst (to_bblock_exit c1).
 Proof.
-  intros H. 
-  (* destruct b as [bhd bbd bex]. simpl. *)
+  intros H.
   unfold to_bblock in H; simpl in H.
   remember (to_bblock_body c) as tbbc; destruct tbbc as [bdy' c1'].
   remember (to_bblock_exit c1') as tbbe; destruct tbbe as [ext c2].
@@ -438,8 +398,7 @@ Proof.
   exploit to_bblock_exit_nil; eauto.
 Qed.
 
-Lemma to_bblock_basic_inst:
-  forall c i bi,
+Lemma to_bblock_basic_inst c i bi:
   get_code_nature (i::c) = IsBasicInst ->
   to_basic_inst i = Some bi ->
   get_code_nature c <> IsLabel ->
@@ -490,8 +449,7 @@ Proof.
       contradict H1; simpl; auto ).
 Qed.
 
-Lemma to_bblock_size_single_label:
-  forall c i,
+Lemma to_bblock_size_single_label c i:
   get_code_nature (i::c) = IsLabel ->
   get_code_nature c <> IsLabel ->
   size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))).
@@ -506,12 +464,11 @@ Proof.
   Unshelve. all: auto.
 Qed.
 
-Lemma to_bblock_size_label_neqz:
-  forall c,
+Lemma to_bblock_size_label_neqz c:
   get_code_nature c = IsLabel ->
   size (fst (to_bblock c)) <> 0%nat.
 Proof.
-  intros. destruct c; try (contradict H; auto; simpl; discriminate).
+  intros H. destruct c as [|i c]; try (contradict H; auto; simpl; discriminate).
   destruct i; try (contradict H; simpl; discriminate).
   destruct (get_code_nature c) eqn:gcnc.
   (* Case gcnc is not IsLabel *)
@@ -520,12 +477,11 @@ Proof.
   rewrite to_bblock_double_label; auto; unfold size; simpl; auto.
 Qed.
 
-Lemma to_bblock_size_basicinst_neqz:
-  forall c,
+Lemma to_bblock_size_basicinst_neqz c:
   get_code_nature c = IsBasicInst ->
   size (fst (to_bblock c)) <> 0%nat.
 Proof.
-  intros. destruct c; try (contradict H; auto; simpl; discriminate).
+  intros H. destruct c as [|i c]; try (contradict H; auto; simpl; discriminate).
   destruct i; try (contradict H; simpl; discriminate);
   (
     destruct (get_code_nature c) eqn:gcnc;
@@ -542,17 +498,15 @@ Proof.
   ).
 Qed.
 
-Lemma to_bblock_size_cfi_neqz:
-  forall c,
+Lemma to_bblock_size_cfi_neqz c:
   get_code_nature c = IsCFI ->
   size (fst (to_bblock c)) <> 0%nat.
 Proof.
-  intros. destruct c; try (contradict H; auto; simpl; discriminate).
+  intros H. destruct c as [|i c]; try (contradict H; auto; simpl; discriminate).
   destruct i; discriminate.
 Qed.
 
-Lemma to_bblock_size_single_basicinst:
-  forall c i,
+Lemma to_bblock_size_single_basicinst c i:
   get_code_nature (i::c) = IsBasicInst ->
   get_code_nature c <> IsLabel ->
   size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))).
@@ -569,7 +523,7 @@ Proof.
 Qed.
 
 Lemma to_bblock_wf c b c0:
-  c <> nil -> 
+  c <> nil ->
   to_bblock c = (b, c0) ->
   (length c > length c0)%nat.
 Proof.
@@ -579,7 +533,7 @@ Proof.
   remember (to_bblock_header c) as p1; eauto.
   destruct p1 as [h c1].
   intro H0.
-  destruct gcn. 
+  destruct gcn.
   - contradict H'; auto.
   - exploit to_bblock_header_wf; eauto.
     remember (to_bblock_body c1) as p2; eauto.
@@ -610,23 +564,21 @@ Proof.
     inversion H0. omega.
 Qed.
 
-Lemma to_bblock_nonil:
-  forall c i c0,
-  c = i :: c0 -> 
+Lemma to_bblock_nonil c i c0:
+  c = i :: c0 ->
   size (fst (to_bblock c)) <> 0%nat.
 Proof.
-  intros. remember (get_code_nature c) as gcnc. destruct gcnc.
+  intros H. remember (get_code_nature c) as gcnc. destruct gcnc.
   - contradict Heqgcnc. subst. simpl. destruct i; discriminate.
   - eapply to_bblock_size_label_neqz; auto.
   - eapply to_bblock_size_basicinst_neqz; auto.
   - eapply to_bblock_size_cfi_neqz; auto.
 Qed.
 
-Lemma to_bblock_islabel:
-  forall c l,
+Lemma to_bblock_islabel c l:
   is_label l (fst (to_bblock (Mlabel l :: c))) = true.
 Proof.
-  intros. unfold to_bblock.
+  unfold to_bblock.
   remember (to_bblock_header _) as tbh; destruct tbh as [h c0].
   remember (to_bblock_body _) as tbc; destruct tbc as [bdy c1].
   remember (to_bblock_exit _) as tbe; destruct tbe as [ext c2].
@@ -634,11 +586,10 @@ Proof.
   apply peq_true.
 Qed.
 
-Lemma body_fst_to_bblock_label:
-  forall l c,
+Lemma body_fst_to_bblock_label l c:
   body (fst (to_bblock (Mlabel l :: c))) = fst (to_bblock_body c).
 Proof.
-  intros. destruct c as [|i c']; simpl; auto.
+  destruct c as [|i c']; simpl; auto.
   destruct i; simpl; auto.
   all: (
     remember (to_bblock_body c') as tbbc; destruct tbbc as [tc c'']; simpl;
@@ -652,12 +603,11 @@ Proof.
   ).
 Qed.
 
-Lemma exit_fst_to_bblock_label:
-  forall c c' l,
+Lemma exit_fst_to_bblock_label c c' l:
   snd (to_bblock_body c) = c' ->
   exit (fst (to_bblock (Mlabel l :: c))) = fst (to_bblock_exit c').
 Proof.
-  intros. destruct c as [|i c]; [simpl in *; subst; auto |].
+  intros H. destruct c as [|i c]; [simpl in *; subst; auto |].
   unfold to_bblock.
   remember (to_bblock_header _) as tbh; destruct tbh as [h c0].
   remember (to_bblock_body c0) as tbc; destruct tbc as [bdy c1].
@@ -675,7 +625,7 @@ Qed.
 Function trans_code (c: Mach.code) { measure length c }: code :=
   match c with
   | nil => nil
-  | _ => 
+  | _ =>
      let (b, c0) := to_bblock c in
      b::(trans_code c0)
   end.
@@ -683,22 +633,16 @@ Proof.
   intros; eapply to_bblock_wf; eauto. discriminate.
 Qed.
 
-(*
-Functional Scheme trans_code_ind := Induction for trans_code Sort Prop.
-*)
-
 Definition hd_code (bc: code) := (hd {| header := None; body := nil; exit := None |} bc).
 
-Lemma trans_code_nonil:
-  forall c,
+Lemma trans_code_nonil c:
   c <> nil -> trans_code c <> nil.
 Proof.
-  intros.
+  intros H.
   induction c, (trans_code c) using trans_code_ind; simpl; auto. discriminate.
 Qed.
 
-Lemma trans_code_step:
-  forall c b lb0 hb c1 bb c2 eb c3,
+Lemma trans_code_step c b lb0 hb c1 bb c2 eb c3:
   trans_code c = b :: lb0 ->
   to_bblock_header c = (hb, c1) ->
   to_bblock_body c1 = (bb, c2) ->
@@ -719,8 +663,7 @@ Proof.
   auto.
 Qed.
 
-Lemma trans_code_cfi:
-  forall i c cfi,
+Lemma trans_code_cfi i c cfi:
   to_cfi i = Some cfi ->
   trans_code (i :: c) = {| header := None ; body := nil ; exit := Some cfi |} :: trans_code c.
 Proof.
@@ -735,7 +678,7 @@ Qed.
 
 (* à finir pour passer des Mach.function au function, etc. *)
 Definition trans_function (f: Mach.function) : function :=
-  {| fn_sig:=Mach.fn_sig f; 
+  {| fn_sig:=Mach.fn_sig f;
      fn_code:=trans_code (Mach.fn_code f);
      fn_stacksize := Mach.fn_stacksize f;
      fn_link_ofs := Mach.fn_link_ofs f;
diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v
index 838f7977..b53af131 100644
--- a/mppa_k1c/Machblockgenproof.v
+++ b/mppa_k1c/Machblockgenproof.v
@@ -17,12 +17,11 @@ Require Import Machblock.
 Require Import Machblockgen.
 Require Import ForwardSimulationBlock.
 
-(* FIXME: put this section somewhere else. 
-   In "Smallstep" ? 
-
-TODO: also move "starN_last_step" in the same section ?
-
-*)
+(** FIXME: put this section somewhere else.
+ * In "Smallstep" ?
+ *
+ * also move "starN_last_step" in the same section ?
+ *)
 
 Section starN_lemma.
 (* Auxiliary Lemma on starN *)
@@ -35,16 +34,16 @@ Variable L: semantics.
 
 Local Hint Resolve starN_refl starN_step Eapp_assoc.
 
-Lemma starN_split n s t s': 
+Lemma starN_split n s t s':
   starN (step L) (globalenv L) n s t s' ->
-  forall m k, n=m+k -> 
+  forall m k, n=m+k ->
   exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2.
 Proof.
   induction 1; simpl.
   + intros m k H; assert (X: m=0); try omega.
     assert (X0: k=0); try omega.
     subst; repeat (eapply ex_intro); intuition eauto.
-  + intros m; destruct m as [| m']; simpl. 
+  + intros m; destruct m as [| m']; simpl.
     - intros k H2; subst; repeat (eapply ex_intro); intuition eauto.
     - intros k H2. inversion H2.
       exploit (IHstarN m' k); eauto. intro.
@@ -104,7 +103,7 @@ Proof (Genv.senv_match TRANSF).
 
 Lemma init_mem_preserved:
   forall m,
-  Genv.init_mem prog = Some m -> 
+  Genv.init_mem prog = Some m ->
   Genv.init_mem tprog = Some m.
 Proof (Genv.init_mem_transf TRANSF).
 
@@ -174,7 +173,7 @@ Proof.
 Qed.
 
 Lemma Mach_find_label_split l i c c':
-  Mach.find_label l (i :: c) = Some c' -> 
+  Mach.find_label l (i :: c) = Some c' ->
    (i=Mlabel l /\ c' = c) \/ (i <> Mlabel l /\ Mach.find_label l c = Some c').
 Proof.
   intros H.
@@ -270,7 +269,7 @@ Proof.
     symmetry. destruct i; try (simpl; auto).
     assert (l0 <> l); [ intro; subst; contradict H1; auto |].
     rewrite peq_false; auto.
-Qed. 
+Qed.
 
 Lemma to_bblock_body_find_label c2 bdy l c1:
   (bdy, c2) = to_bblock_body c1 ->
@@ -376,6 +375,13 @@ Ltac ExploitDistEndBlockCode :=
   | _ => idtac
   end.
 
+Ltac totologize H :=
+  match type of H with
+  | ( ?id = _ ) =>
+    let Hassert := fresh "Htoto" in (
+    assert (id = id) as Hassert; auto; rewrite H in Hassert at 2; simpl in Hassert; rewrite H in Hassert)
+  end.
+
 (* FIXME - refactoriser avec get_code_nature pour que ce soit plus joli *)
 Lemma dist_end_block_code_simu_mid_block i c:
   dist_end_block_code (i::c) <> 0%nat ->
@@ -420,7 +426,7 @@ Lemma step_simu_basic_step (i: Mach.instruction) (bi: basic_inst) (c: Mach.code)
   Mach.step (inv_trans_rao rao) ge (Mach.State s f sp (i::c) rs m) t s' ->
   exists rs' m', s'=Mach.State s f sp c rs' m' /\ t=E0 /\ basic_step tge (trans_stack s) f sp rs m bi rs' m'.
 Proof.
-  destruct i; simpl in * |-; 
+  destruct i; simpl in * |-;
    (discriminate
     || (intro H; inversion_clear H; intro X; inversion_clear X; eapply ex_intro; eapply ex_intro; intuition eauto)).
   - eapply exec_MBgetparam; eauto. exploit (functions_translated); eauto. intro.
@@ -435,14 +441,14 @@ Proof.
 Qed.
 
 
-Lemma star_step_simu_body_step s f sp c: 
+Lemma star_step_simu_body_step s f sp c:
  forall (p:bblock_body) c' rs m t s',
   to_bblock_body c = (p, c') ->
-  starN (Mach.step (inv_trans_rao rao)) ge (length p) (Mach.State s f sp c rs m) t s' -> 
+  starN (Mach.step (inv_trans_rao rao)) ge (length p) (Mach.State s f sp c rs m) t s' ->
   exists rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp p rs m rs' m'.
 Proof.
-  induction c as [ | i0 c0 Hc0]; simpl; intros p c' rs m t s' H. 
-  * (* nil *) 
+  induction c as [ | i0 c0 Hc0]; simpl; intros p c' rs m t s' H.
+  * (* nil *)
     inversion_clear H; simpl; intros X; inversion_clear X.
     eapply ex_intro; eapply ex_intro; intuition eauto.
   * (* cons *)
@@ -510,10 +516,10 @@ Lemma simu_end_block:
   step rao tge (trans_state s1) t (trans_state s1').
 Proof.
   destruct s1; simpl.
-  + (* State *) 
+  + (* State *)
     (* c cannot be nil *)
-    destruct c as [|i c]; simpl; try ( (* nil => absurd *) 
-      unfold dist_end_block_code; simpl; 
+    destruct c as [|i c]; simpl; try ( (* nil => absurd *)
+      unfold dist_end_block_code; simpl;
       intros t s1' H; inversion_clear H;
       inversion_clear H0; fail
     ).
@@ -526,7 +532,7 @@ Proof.
     ( exploit (trans_code_nonil c0); subst; auto; try discriminate; intro H0; contradict H0 ).
 
     assert (X: Datatypes.S (dist_end_block_code c0) = (size (fst (to_bblock c0)))).
-    { 
+    {
       unfold dist_end_block_code. remember (size _) as siz.
       assert (siz <> 0%nat). rewrite Heqsiz; apply to_bblock_nonil with (c0 := c) (i := i) (c := c0); auto.
       omega.
@@ -587,7 +593,7 @@ Proof.
     - simpl in H3. inversion H3; subst. simpl.
       destruct c2 as [|ei c2']; inversion Heqexb; subst; try eapply exec_None_exit.
       clear H3. destruct (to_cfi ei) as [cfi|] eqn:TOCFI; inversion H0.
-      subst. eapply exec_None_exit. 
+      subst. eapply exec_None_exit.
 
   + (* Callstate *)
     intros t s1' H; inversion_clear H.