(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Omega.

Require Import utils subcode.

Set Implicit Arguments.

(** * A certified low-level compiler *)

Tactic Notation "dest" "eq" "nat" "dec" "as" intropattern(H) :=
    match goal with 
      |- context[eq_nat_dec ?x ?y] => destruct (eq_nat_dec x y) as H
    end; auto.

Tactic Notation "solve" "eq" "nat" "dec" := 
    match goal with 
      |- context[eq_nat_dec ?x ?x] => destruct (eq_nat_dec x x) as [ | [] ]; [ | reflexivity ]
    end; auto.
    
Section linker.
 
  Variable (X Y : Type)
           (c : (nat -> nat) -> nat -> X -> list Y) (* instruction compiler w.r.t. a given linker & a position *)
           (lc : X -> nat)                          (* compiled code length does not depend on linker or position *)
           (Hc : forall f n x, length (c f n x) = lc x).

  Fixpoint length_compiler lx :=
    match lx with
      | nil   => 0
      | x::lx => lc x+length_compiler lx
    end.
    
  Fact length_compiler_app ll mm : length_compiler (ll++mm) = length_compiler ll + length_compiler mm.
  Proof.
(* Goal: @eq nat (length_compiler (@app X ll mm)) (Init.Nat.add (length_compiler ll) (length_compiler mm)) *)
    induction ll as [ | x ll IH ]; simpl; auto.
(* Goal: @eq nat (Init.Nat.add (lc x) (length_compiler (@app X ll mm))) (Init.Nat.add (Init.Nat.add (lc x) (length_compiler ll)) (length_compiler mm)) *)
    rewrite IH; omega.
  Qed.
    
  Notation lsum := length_compiler.

  Fixpoint link i ll j : list (nat*nat) :=
    match ll with
      | nil   => nil
      | x::ll => (i,j)::link (S i) ll (lc x+j)
    end.
    
  Fact link_app i ll mm j : link i (ll++mm) j = link i ll j ++ link (length ll+i) mm (lsum ll+j).
  Proof.
(* Goal: @eq (list (prod nat nat)) (link i (@app X ll mm) j) (@app (prod nat nat) (link i ll j) (link (Init.Nat.add (@length X ll) i) mm (Init.Nat.add (length_compiler ll) j))) *)
    revert i j; induction ll as [ | x ll IH ]; simpl; intros i j; f_equal.
(* Goal: @eq (list (prod nat nat)) (link (S i) (@app X ll mm) (Init.Nat.add (lc x) j)) (@app (prod nat nat) (link (S i) ll (Init.Nat.add (lc x) j)) (link (S (Init.Nat.add (@length X ll) i)) mm (Init.Nat.add (Init.Nat.add (lc x) (length_compiler ll)) j))) *)
    rewrite IH; do 2 f_equal; omega.
  Qed.
  
  Fact link_fst i ll j : map fst (link i ll j) = list_an i (length ll).
  Proof.
(* Goal: @eq (list nat) (@map (prod nat nat) nat (@fst nat nat) (link i ll j)) (list_an i (@length X ll)) *)
    revert i j; induction ll; simpl; intros; f_equal; auto.
  Qed.
  
  Section comp.
  
    Variable lnk : nat -> nat.

    Fixpoint comp i ll j :=
      match ll with
        | nil   => nil
        | x::ll => c lnk i x ++ comp (S i) ll (lc x+j)
      end.
    
    Fact comp_app i ll mm j : comp i (ll++mm) j = comp i ll j ++ comp (length ll+i) mm (lsum ll+j).
    Proof.
(* Goal: @eq nat (@length Y (comp i ll j)) (length_compiler ll) *)
      revert i j; induction ll as [ | x ll IH ]; simpl; intros i j; auto.
(* Goal: @eq (list Y) (@app Y (c lnk i x) (comp (S i) (@app X ll mm) (Init.Nat.add (lc x) j))) (@app Y (@app Y (c lnk i x) (comp (S i) ll (Init.Nat.add (lc x) j))) (comp (S (Init.Nat.add (@length X ll) i)) mm (Init.Nat.add (Init.Nat.add (lc x) (length_compiler ll)) j))) *)
      rewrite IH; solve list eq; do 3 f_equal; omega.
    Qed.
    
    Fact comp_length i ll j : length (comp i ll j) = lsum ll.
    Proof.
(* Goal: @eq nat (@length Y (comp i ll j)) (length_compiler ll) *)
      revert i j; induction ll as [ | x ll IH ]; simpl; intros i j; auto.
(* Goal: @eq nat (@length Y (@app Y (c lnk i x) (comp (S i) ll (Init.Nat.add (lc x) j)))) (Init.Nat.add (lc x) (length_compiler ll)) *)
      rew length; rewrite IH, Hc; trivial.
    Qed.
  
  End comp.

  Variable (P : nat * list X) (i : nat) (err : nat).

  Definition linker :=
    let ll := (length (snd P) + fst P,lsum (snd P)+i)::link (fst P) (snd P) i
    in fun j => match list_assoc eq_nat_dec j ll with
        | None   => err
        | Some p => p
    end.
    
  (* These two lemmas specify the linker *)
    
  Fact linker_app ll mm : snd P = ll++mm -> linker (length ll+fst P) = lsum ll + i.
  Proof.
(* Goal: forall _ : @eq (list X) (@snd nat (list X) P) (@app X ll mm), @eq nat (linker (Init.Nat.add (@length X ll) (@fst nat (list X) P))) (Init.Nat.add (length_compiler ll) i) *)
    intros H; unfold linker.
(* Goal: @eq nat match @list_assoc nat nat Nat.eq_dec (Init.Nat.add (@length X ll) (@fst nat (list X) P)) (@cons (prod nat nat) (@pair nat nat (Init.Nat.add (@length X (@snd nat (list X) P)) (@fst nat (list X) P)) (Init.Nat.add (length_compiler (@snd nat (list X) P)) i)) (link (@fst nat (list X) P) (@snd nat (list X) P) i)) with | Some p => p | None => err end (Init.Nat.add (length_compiler ll) i) *)
    destruct P as (iP,lP).
(* Goal: @eq nat match @list_assoc nat nat Nat.eq_dec (Init.Nat.add (@length X ll) (@fst nat (list X) (@pair nat (list X) iP lP))) (@cons (prod nat nat) (@pair nat nat (Init.Nat.add (@length X (@snd nat (list X) (@pair nat (list X) iP lP))) (@fst nat (list X) (@pair nat (list X) iP lP))) (Init.Nat.add (length_compiler (@snd nat (list X) (@pair nat (list X) iP lP))) i)) (link (@fst nat (list X) (@pair nat (list X) iP lP)) (@snd nat (list X) (@pair nat (list X) iP lP)) i)) with | Some p => p | None => err end (Init.Nat.add (length_compiler ll) i) *)
    rewrite H; simpl in H |- *.
(* Goal: @eq nat match (if Nat.eq_dec (Init.Nat.add (@length X ll) iP) (Init.Nat.add (@length X (@app X ll mm)) iP) then @Some nat (Init.Nat.add (length_compiler (@app X ll mm)) i) else @list_assoc nat nat Nat.eq_dec (Init.Nat.add (@length X ll) iP) (link iP (@app X ll mm) i)) with | Some p => p | None => err end (Init.Nat.add (length_compiler ll) i) *)
    destruct mm as [ | x mm ].
    * rewrite <- app_nil_end.
(* Goal: @eq nat match (if Nat.eq_dec (Init.Nat.add (@length X ll) iP) (Init.Nat.add (@length X ll) iP) then @Some nat (Init.Nat.add (length_compiler ll) i) else @list_assoc nat nat Nat.eq_dec (Init.Nat.add (@length X ll) iP) (link iP ll i)) with | Some p => p | None => err end (Init.Nat.add (length_compiler ll) i) *)
      solve eq nat dec.
    * rew length.
(* Goal: @eq nat match (if Nat.eq_dec (Init.Nat.add (@length X ll) iP) (Init.Nat.add (Init.Nat.add (@length X ll) (S (@length X mm))) iP) then @Some nat (Init.Nat.add (length_compiler (@app X ll (@cons X x mm))) i) else @list_assoc nat nat Nat.eq_dec (Init.Nat.add (@length X ll) iP) (link iP (@app X ll (@cons X x mm)) i)) with | Some p => p | None => err end (Init.Nat.add (length_compiler ll) i) *)
      dest eq nat dec as [ H1 | H1 ]; [ omega | clear H1 ].
(* Goal: @eq nat match @list_assoc nat nat Nat.eq_dec (Init.Nat.add (@length X ll) iP) (link iP (@app X ll (@cons X x mm)) i) with | Some p => p | None => err end (Init.Nat.add (length_compiler ll) i) *)
      rewrite link_app, list_assoc_app.
(* Goal: @eq nat match match @list_assoc nat nat Nat.eq_dec (Init.Nat.add (@length X ll) iP) (link iP ll i) with | Some y => @Some nat y | None => @list_assoc nat nat Nat.eq_dec (Init.Nat.add (@length X ll) iP) (link (Init.Nat.add (@length X ll) iP) (@cons X x mm) (Init.Nat.add (length_compiler ll) i)) end with | Some p => p | None => err end (Init.Nat.add (length_compiler ll) i) *)
      generalize (list_assoc_In eq_nat_dec (length ll + iP) (link iP ll i)).
(* Goal: forall _ : match @list_assoc nat nat Nat.eq_dec (Init.Nat.add (@length X ll) iP) (link iP ll i) with | Some y => @In (prod nat nat) (@pair nat nat (Init.Nat.add (@length X ll) iP) y) (link iP ll i) | None => not (@In nat (Init.Nat.add (@length X ll) iP) (@map (prod nat nat) nat (@fst nat nat) (link iP ll i))) end, @eq nat match match @list_assoc nat nat Nat.eq_dec (Init.Nat.add (@length X ll) iP) (link iP ll i) with | Some y => @Some nat y | None => @list_assoc nat nat Nat.eq_dec (Init.Nat.add (@length X ll) iP) (link (Init.Nat.add (@length X ll) iP) (@cons X x mm) (Init.Nat.add (length_compiler ll) i)) end with | Some p => p | None => err end (Init.Nat.add (length_compiler ll) i) *)
      destruct (list_assoc eq_nat_dec (length ll + iP) (link iP ll i)) as [ j | ].
      - intros H1.
(* Goal: @eq nat n err *)
        apply in_map with (f := @fst _ _) in H1.
(* Goal: @eq nat n err *)
        rewrite link_fst, list_an_spec in H1; simpl in H1; omega.
(* Goal: @eq nat match (if Nat.eq_dec (Init.Nat.add (@length X ll) iP) (Init.Nat.add (@length X ll) iP) then @Some nat (Init.Nat.add (length_compiler ll) i) else @list_assoc nat nat Nat.eq_dec (Init.Nat.add (@length X ll) iP) (link iP ll i)) with | Some p => p | None => err end (Init.Nat.add (length_compiler ll) i) *)
      - intros; simpl; solve eq nat dec.
  Qed.
  
  Fact linker_err_code j : j < fst P \/ length (snd P) + fst P < j -> linker j = err.
  Proof.
(* Goal: forall _ : or (lt j (@fst nat (list X) P)) (lt (Init.Nat.add (@length X (@snd nat (list X) P)) (@fst nat (list X) P)) j), @eq nat (linker j) err *)
    unfold linker.
(* Goal: forall _ : or (lt j (@fst nat (list X) P)) (lt (Init.Nat.add (@length X (@snd nat (list X) P)) (@fst nat (list X) P)) j), @eq nat match @list_assoc nat nat Nat.eq_dec j (@cons (prod nat nat) (@pair nat nat (Init.Nat.add (@length X (@snd nat (list X) P)) (@fst nat (list X) P)) (Init.Nat.add (length_compiler (@snd nat (list X) P)) i)) (link (@fst nat (list X) P) (@snd nat (list X) P) i)) with | Some p => p | None => err end err *)
    destruct P as (iP,lP); simpl; intros H.
(* Goal: @eq nat match (if Nat.eq_dec j (Init.Nat.add (@length X lP) iP) then @Some nat (Init.Nat.add (length_compiler lP) i) else @list_assoc nat nat Nat.eq_dec j (link iP lP i)) with | Some p => p | None => err end err *)
    dest eq nat dec as [ H1 | _ ]; [ omega | ].
(* Goal: @eq nat match @list_assoc nat nat Nat.eq_dec j (link iP lP i) with | Some p => p | None => err end err *)
    generalize (list_assoc_In eq_nat_dec j (link iP lP i)).
(* Goal: forall _ : match @list_assoc nat nat Nat.eq_dec j (link iP lP i) with | Some y => @In (prod nat nat) (@pair nat nat j y) (link iP lP i) | None => not (@In nat j (@map (prod nat nat) nat (@fst nat nat) (link iP lP i))) end, @eq nat match @list_assoc nat nat Nat.eq_dec j (link iP lP i) with | Some p => p | None => err end err *)
    destruct (list_assoc eq_nat_dec j (link iP lP i)); auto.
(* Goal: forall _ : @In (prod nat nat) (@pair nat nat j n) (link iP lP i), @eq nat n err *)
    intros H1.
(* Goal: @eq nat n err *)
    apply in_map with (f := @fst _ _) in H1.
(* Goal: @eq nat n err *)
    rewrite link_fst, list_an_spec in H1; simpl in H1; omega.
  Qed.

  Definition compiler := comp linker (fst P) (snd P) i.
  
  Fact compiler_length : length compiler = length_compiler (snd P).
  Proof. apply comp_length. Qed.

  Section linker_in_code.

    Hypothesis (Hlc : forall x, 1 <= lc x).

    Fact linker_in_code j : in_code j P -> in_code (linker j) (i,compiler).
    Proof.
(* Goal: forall _ : @in_code X j P, @in_code Y (linker j) (@pair nat (list Y) i compiler) *)
      intros H; red in H; simpl in H.
      destruct (@list_split_length _ (snd P) (j - fst P)) as (ll & mm & H1 & H2);
        try omega.
(* Goal: @in_code Y (linker j) (@pair nat (list Y) i compiler) *)
      replace j with (length ll+fst P) by omega.
(* Goal: @in_code Y (linker (Init.Nat.add (@length X ll) (@fst nat (list X) P))) (@pair nat (list Y) i compiler) *)
      rewrite (linker_app _ _ H1).
(* Goal: @in_code Y (Init.Nat.add (length_compiler ll) i) (@pair nat (list Y) i compiler) *)
      red; simpl; rewrite compiler_length, H1, length_compiler_app.
(* Goal: and (le i (Init.Nat.add (length_compiler ll) i)) (lt (Init.Nat.add (length_compiler ll) i) (Init.Nat.add i (Init.Nat.add (length_compiler ll) (length_compiler mm)))) *)
      rewrite H1, app_length in H.
(* Goal: and (le i (Init.Nat.add (length_compiler ll) i)) (lt (Init.Nat.add (length_compiler ll) i) (Init.Nat.add i (Init.Nat.add (length_compiler ll) (length_compiler mm)))) *)
      destruct mm. 
(* Goal: and (le i (Init.Nat.add (length_compiler ll) i)) (lt (Init.Nat.add (length_compiler ll) i) (Init.Nat.add i (Init.Nat.add (length_compiler ll) (length_compiler (@nil X))))) *)
(* Goal: and (le i (Init.Nat.add (length_compiler ll) i)) (lt (Init.Nat.add (length_compiler ll) i) (Init.Nat.add i (Init.Nat.add (length_compiler ll) (length_compiler (@cons X x mm))))) *)
      simpl in H; omega.
(* Goal: and (le i (Init.Nat.add (length_compiler ll) i)) (lt (Init.Nat.add (length_compiler ll) i) (Init.Nat.add i (Init.Nat.add (length_compiler ll) (length_compiler (@cons X x mm))))) *)
      simpl.
(* Goal: and (le i (Init.Nat.add (length_compiler ll) i)) (lt (Init.Nat.add (length_compiler ll) i) (Init.Nat.add i (Init.Nat.add (length_compiler ll) (Init.Nat.add (lc x) (length_compiler mm))))) *)
      generalize (Hlc x); omega.
    Qed.

  End linker_in_code.
  
  Fact compiler_subcode j x : 
          (j,x::nil) <sc P 
       -> (linker j, c linker j x) <sc (i,compiler)
       /\  linker (1+j) = lc x + linker j.
  Proof.
(* Goal: forall _ : @subcode X (@pair nat (list X) j (@cons X x (@nil X))) P, and (@subcode Y (@pair nat (list Y) (linker j) (c linker j x)) (@pair nat (list Y) i compiler)) (@eq nat (linker (Init.Nat.add (S O) j)) (Init.Nat.add (lc x) (linker j))) *)
    case_eq P; intros iP lP HP (l & r & H1 & H2); simpl in H1.
(* Goal: and (@subcode Y (@pair nat (list Y) (linker j) (c linker j x)) (@pair nat (list Y) i compiler)) (@eq nat (linker (Init.Nat.add (S O) j)) (Init.Nat.add (lc x) (linker j))) *)
    assert (linker j = lsum l + i) as Hj.
(* Goal: @eq nat (linker (Init.Nat.add (S O) j)) (Init.Nat.add (lc x) (linker j)) *)
(* Goal: and (@subcode Y (@pair nat (list Y) (linker j) (c linker j x)) (@pair nat (list Y) i compiler)) (@eq nat (linker (Init.Nat.add (S O) j)) (Init.Nat.add (lc x) (linker j))) *)
    { generalize (linker_app l (x::r)).
(* Goal: forall _ : forall _ : @eq (list X) (@snd nat (list X) P) (@app X l (@cons X x r)), @eq nat (linker (Init.Nat.add (@length X l) (@fst nat (list X) P))) (Init.Nat.add (length_compiler l) i), @eq nat (linker j) (Init.Nat.add (length_compiler l) i) *)
      rewrite HP; simpl; intros E.
      rewrite <- E; auto; f_equal; omega. }
(* Goal: and (@subcode Y (@pair nat (list Y) (linker j) (c linker j x)) (@pair nat (list Y) i compiler)) (@eq nat (linker (Init.Nat.add (S O) j)) (Init.Nat.add (lc x) (linker j))) *)
    assert (linker (1+j) = lc x + linker j) as HSj.
(* Goal: @eq nat (linker (Init.Nat.add (S O) j)) (Init.Nat.add (lc x) (linker j)) *)
(* Goal: and (@subcode Y (@pair nat (list Y) (linker j) (c linker j x)) (@pair nat (list Y) i compiler)) (@eq nat (linker (Init.Nat.add (S O) j)) (Init.Nat.add (lc x) (linker j))) *)
    {  generalize (linker_app (l++x::nil) r).
(* Goal: forall _ : forall _ : @eq (list X) (@snd nat (list X) P) (@app X (@app X l (@cons X x (@nil X))) r), @eq nat (linker (Init.Nat.add (@length X (@app X l (@cons X x (@nil X)))) (@fst nat (list X) P))) (Init.Nat.add (length_compiler (@app X l (@cons X x (@nil X)))) i), @eq nat (linker (Init.Nat.add (S O) j)) (Init.Nat.add (lc x) (linker j)) *)
      rewrite HP, app_ass; simpl; intros H3.
(* Goal: @eq nat (linker (S j)) (Init.Nat.add (lc x) (linker j)) *)
      specialize (H3 H1).
(* Goal: @eq nat (linker (S j)) (Init.Nat.add (lc x) (linker j)) *)
      eq goal H3; f_equal.
(* Goal: @eq nat (linker (Init.Nat.add (@length X (@app X l (@cons X x (@nil X)))) iP)) (linker (S j)) *)
(* Goal: @eq nat (Init.Nat.add (length_compiler (@app X l (@cons X x (@nil X)))) i) (Init.Nat.add (lc x) (linker j)) *)
      f_equal.
(* Goal: @eq nat (Init.Nat.add (@length X (@app X l (@cons X x (@nil X)))) iP) (S j) *)
(* Goal: @eq nat (Init.Nat.add (length_compiler (@app X l (@cons X x (@nil X)))) i) (Init.Nat.add (lc x) (linker j)) *)
      rew length; omega.
      rewrite length_compiler_app; simpl; omega. }
(* Goal: and (@subcode Y (@pair nat (list Y) (linker j) (c linker j x)) (@pair nat (list Y) i compiler)) (@eq nat (linker (Init.Nat.add (S O) j)) (Init.Nat.add (lc x) (linker j))) *)
    split; auto.
(* Goal: and (le i (Init.Nat.add (length_compiler ll) i)) (lt (Init.Nat.add (length_compiler ll) i) (Init.Nat.add i (Init.Nat.add (length_compiler ll) (length_compiler (@cons X x mm))))) *)
    unfold compiler; rewrite HP, H1; simpl.
(* Goal: @ex (list Y) (fun l0 : list Y => @ex (list Y) (fun r0 : list Y => and (@eq (list Y) (comp linker iP (@app X l (@cons X x r)) i) (@app Y l0 (@app Y (c linker j x) r0))) (@eq nat (linker j) (Init.Nat.add i (@length Y l0))))) *)
    exists (comp linker iP l i), (comp linker (1+length l+iP) r (lc x+lsum l+i)); split.
(* Goal: @eq (list Y) (comp linker iP (@app X l (@cons X x r)) i) (@app Y (comp linker iP l i) (@app Y (c linker j x) (comp linker (Init.Nat.add (Init.Nat.add (S O) (@length X l)) iP) r (Init.Nat.add (Init.Nat.add (lc x) (length_compiler l)) i)))) *)
(* Goal: @eq nat (linker j) (Init.Nat.add i (@length Y (comp linker iP l i))) *)
    rewrite comp_app; simpl; do 3 f_equal; omega.
(* Goal: @eq nat (linker j) (Init.Nat.add i (@length Y (comp linker iP l i))) *)
    rewrite comp_length; omega.
  Qed.
  
  Fact linker_code_start : linker (code_start P) = i.
  Proof. apply (linker_app nil (snd P)); auto. Qed.
  
  Fact linker_middle ll x mm : snd P = ll++x::mm -> linker (length ll+fst P) = lsum ll+i.
  Proof. apply linker_app. Qed.
  
  Fact linker_code_end : linker (code_end P) = lsum (snd P)+i.
  Proof.
(* Goal: @eq nat (linker (@code_end X P)) (Init.Nat.add (length_compiler (@snd nat (list X) P)) i) *)
    unfold code_end; rewrite plus_comm.
(* Goal: @eq nat (linker (Nat.add (@length X (@snd nat (list X) P)) (@fst nat (list X) P))) (Init.Nat.add (length_compiler (@snd nat (list X) P)) i) *)
    apply (linker_app _ nil), app_nil_end.
  Qed.
  
   Fact linker_out_code j : err < i \/ length_compiler (snd P) + i <= err 
                        -> out_code j P -> out_code (linker j) (i,compiler).
  Proof.
(* Goal: forall (_ : @eq nat err (Init.Nat.add (length_compiler (@snd nat (list X) P)) i)) (_ : @out_code X j P), @eq nat (linker j) err *)
    intros H1 H2.
(* Goal: @out_code Y (linker j) (@pair nat (list Y) i compiler) *)
    red in H2.
(* Goal: @eq nat (linker j) err *)
    destruct (eq_nat_dec j (code_end P)) as [ H | H ].
(* Goal: and (le i (Init.Nat.add (length_compiler ll) i)) (lt (Init.Nat.add (length_compiler ll) i) (Init.Nat.add i (Init.Nat.add (length_compiler ll) (length_compiler (@cons X x mm))))) *)
    rewrite H, linker_code_end; simpl.
(* Goal: or (lt (Init.Nat.add (length_compiler (@snd nat (list X) P)) i) i) (le (Init.Nat.add i (@length Y compiler)) (Init.Nat.add (length_compiler (@snd nat (list X) P)) i)) *)
(* Goal: @out_code Y (linker j) (@pair nat (list Y) i compiler) *)
    rewrite compiler_length; omega.
(* Goal: @out_code Y (linker j) (@pair nat (list Y) i compiler) *)
    rewrite linker_err_code.
(* Goal: or (lt (Init.Nat.add (length_compiler (@snd nat (list X) P)) i) i) (le (Init.Nat.add i (@length Y compiler)) (Init.Nat.add (length_compiler (@snd nat (list X) P)) i)) *)
(* Goal: @out_code Y (linker j) (@pair nat (list Y) i compiler) *)
    simpl; rewrite compiler_length; omega.
(* Goal: or (lt j (@fst nat (list X) P)) (lt (Init.Nat.add (@length X (@snd nat (list X) P)) (@fst nat (list X) P)) j) *)
    simpl in H2, H; omega.
  Qed.

  Fact linker_out_err j : err = lsum (snd P) + i -> out_code j P -> linker j = err.
  Proof.
(* Goal: forall (_ : @eq nat err (Init.Nat.add (length_compiler (@snd nat (list X) P)) i)) (_ : @out_code X j P), @eq nat (linker j) err *)
    intros H1 H2.
(* Goal: @eq nat (linker j) err *)
    destruct (eq_nat_dec j (code_end P)) as [ H | H ].
    + rewrite H1, H; unfold code_end.
(* Goal: @eq nat (linker (Init.Nat.add (@fst nat (list X) P) (@length X (@snd nat (list X) P)))) (Init.Nat.add (length_compiler (@snd nat (list X) P)) i) *)
      rewrite plus_comm, linker_app with (mm := nil); auto.
      rewrite <- app_nil_end; auto.
    + apply linker_err_code; red in H2; unfold code_end, code_start in *; omega.
  Qed.

End linker.
