(** The language of Cobham *)

Require Import Bool Arith List.
Require Import BellantoniCook.Lib BellantoniCook.Bitstring BellantoniCook.MultiPoly.

(** * Syntax and induction principle

  - [Cobham_ind2] is a handmade induction principle because the one generated automatically by Coq
    ignores the type [list BC] in the constructor [Comp].
*)

Inductive Cobham : Type :=
| Zero : Cobham
| Proj : nat -> nat -> Cobham
| Succ : bool -> Cobham
| Smash : Cobham
| Rec  : Cobham -> Cobham -> Cobham -> Cobham -> Cobham
| Comp : nat -> Cobham -> list Cobham -> Cobham.

Definition Rec2 g h j := Rec g h h j.

Lemma Cobham_ind2' :
  forall P : Cobham -> Prop,
  forall Q : list Cobham -> Prop,
  Q nil ->
  (forall e l, P e -> Q l -> Q (e :: l)) ->
  P Zero ->
  (forall n i, P (Proj n i)) ->
  (forall b, P (Succ b)) ->
  P Smash ->
  (forall j g h0 h1, P j -> P g -> P h0 -> P h1 -> P (Rec j g h0 h1)) ->
  (forall n h l, P h -> Q l -> P (Comp n h l)) ->
  forall e, P e.
Proof.
(* Goal: forall (P : forall _ : Cobham, Prop) (Q : forall _ : list Cobham, Prop) (_ : Q (@nil Cobham)) (_ : forall (e : Cobham) (l : list Cobham) (_ : P e) (_ : Q l), Q (@cons Cobham e l)) (_ : P Zero) (_ : forall n i : nat, P (Proj n i)) (_ : forall b : bool, P (Succ b)) (_ : P Smash) (_ : forall (j g h0 h1 : Cobham) (_ : P j) (_ : P g) (_ : P h0) (_ : P h1), P (Rec j g h0 h1)) (_ : forall (n : nat) (h : Cobham) (l : list Cobham) (_ : P h) (_ : Q l), P (Comp n h l)) (e : Cobham), P e *)
 fix Cobham_ind2' 11; intros.
(* Goal: P e *)
 destruct e; auto.
(* Goal: P (Rec e1 e2 e3 e4) *)
(* Goal: P (Comp n e l) *)
 apply H5; eapply Cobham_ind2'; eauto.
(* Goal: P (Comp n e l) *)
 apply H6.
(* Goal: P c *)
(* Goal: Q l *)
 eapply Cobham_ind2'; eauto.
(* Goal: Q l *)
 revert l.
(* Goal: forall l : list Cobham, Q l *)
 fix Cobham_ind2'0 1.
(* Goal: forall l : list Cobham, Q l *)
 intro.
(* Goal: Q n l *)
 destruct l.
(* Goal: Q (@nil Cobham) *)
(* Goal: Q (@cons Cobham c l) *)
 apply H.
(* Goal: Q (@cons Cobham c l) *)
 apply H0.
(* Goal: P c *)
(* Goal: Q l *)
 eapply Cobham_ind2'; eauto.
(* Goal: Q l *)
 apply Cobham_ind2'0.
Qed.

Lemma Cobham_ind2 :
  forall P : Cobham -> Prop,
  P Zero ->
  (forall n i, P (Proj n i)) ->
  (forall b, P (Succ b)) ->
  P Smash ->
  (forall j g h0 h1, P j -> P g -> P h0 -> P h1 -> P (Rec j g h0 h1)) ->
  (forall n h l, P h -> (forall e, In e l -> P e) ->
    P (Comp n h l)) ->
  forall e, P e.
Proof.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
 intros.
 induction e using Cobham_ind2' 
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
   with (Q := fun l => forall e, In e l -> P e); auto.
(* Goal: forall (e : Cobham) (_ : @In Cobham e (@nil Cobham)), P e *)
(* Goal: forall (e0 : Cobham) (_ : @In Cobham e0 (@cons Cobham e l)), P e0 *)
 simpl;intros; tauto.
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 simpl.
(* Goal: forall (e0 : Cobham) (_ : or (@eq Cobham e e0) (@In Cobham e0 l)), P e0 *)
 intros e' [ | ]; intros; subst; auto.
Qed.

(** * Arity

  - [arity e] returns the arity (i.e., the number variables)
    of the expression [e] if it is well formed, or an error including the arity of the subterms.
*)

Inductive Arity : Set :=
| error_Rec : Arity -> Arity -> Arity -> Arity -> Arity
| error_Comp : Arity -> list Arity -> Arity
| error_Proj : nat -> nat -> Arity
| ok_arity : nat -> Arity.

Definition arity_eq (a1 a2 : Arity) :=
  match a1, a2 with
    | ok_arity n1, ok_arity n2 => beq_nat n1 n2
    | _, _ => false
  end.

Lemma arity_eq_true x1 x2 :
  arity_eq x1 x2 = true -> x1 = x2.
Proof.
(* Goal: forall _ : @eq bool (arity_eq x1 x2) true, @eq Arity x1 x2 *)
 intros; unfold arity_eq in H.
(* Goal: @eq Arity x1 x2 *)
 destruct x1; try discriminate.
(* Goal: @eq Arity (ok_arity n) x2 *)
 destruct x2; try discriminate.
(* Goal: @eq Arity (ok_arity n) (ok_arity n0) *)
 apply beq_nat_true in H; subst; trivial.
Qed.

Lemma arity_eq_refl : forall n, arity_eq (ok_arity n) (ok_arity n) = true.
Proof.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
  intros; case (ok_arity n); simpl; intros.
(* Goal: @eq bool (Nat.eqb n0 n0) true *)
  rewrite beq_nat_true_iff; trivial.
Qed.

Fixpoint arity (e : Cobham) : Arity :=
  match e with
    | Zero => ok_arity 0
    | Proj n j => if leb (S j) n 
      then ok_arity n else error_Proj n j 
    | Succ _ => ok_arity 1
    | Smash => ok_arity 2
    | Rec g h0 h1 j => 
      match arity g, arity h0, arity h1, arity j with
        | ok_arity gn, ok_arity h0n, ok_arity h1n, ok_arity jn =>
          if beq_nat (S (S gn)) h0n && 
             beq_nat h1n h0n &&
             beq_nat (S jn) h1n 
            then ok_arity jn 
            else error_Rec (ok_arity gn) (ok_arity h0n) 
              (ok_arity h1n) (ok_arity jn)
        | ag, ah0, ah1, aj => error_Rec ag ah0 ah1 aj 
      end
    | Comp n h l => 
      match arity h, map arity l with
        | ok_arity nh, al => 
          if beq_nat nh (length l) &&
            forallb (fun e => arity_eq e (ok_arity n)) al then
              ok_arity n else error_Comp (ok_arity nh) al
        | e , le => error_Comp e le 
      end
  end.

Lemma Cobham_ind_inf' :
  forall (P : nat -> Cobham -> Prop),
  forall Q : nat -> list Cobham -> Prop,
  (forall n, Q n nil) ->
  (forall e n l, P n e -> Q n l -> Q n (e :: l)) ->
  P 0 Zero ->
  (forall n i, i < n  ->  P n (Proj n i)) ->
  (forall b, P 1 (Succ b)) ->
  (P 2 Smash) ->
  (forall n g h0 h1 j, 
    arity g = ok_arity n ->
    arity h0 = ok_arity (S (S n)) ->
    arity h1 = ok_arity (S (S n)) ->
    arity j = ok_arity (S n) ->
    P n g -> 
    P (S (S n)) h0 -> 
    P (S (S n)) h1 -> 
    P (S n) j -> 
    P (S n) (Rec g h0 h1 j)) ->
  (forall n h rl, 
    arity h = ok_arity (length rl)  ->
    (forall e, In e rl -> arity e = ok_arity n) ->
    P (length rl)  h -> 
    Q n rl ->
    P n (Comp n h rl)) ->
  forall e n , arity e = ok_arity n -> P n e.
Proof.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
 fix Cobham_ind_inf' 11; intros.
(* Goal: P n e *)
 destruct e; simpl in *.

(* Goal: P n Smash *)
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 injection H7; intros; subst; auto.

(* Goal: P n (Proj n0 n1) *)
(* Goal: P n (Succ b) *)
(* Goal: P n Smash *)
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 destruct n0; try discriminate.
(* Goal: P n (Proj (S n0) n1) *)
(* Goal: P n (Succ b) *)
(* Goal: P n Smash *)
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 case_eq (leb n1 n0); intros; rewrite H8 in H7; try discriminate.
(* Goal: P n Smash *)
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 injection H7; intros; subst; auto.
(* Goal: P (S n0) (Proj (S n0) n1) *)
(* Goal: P n (Succ b) *)
(* Goal: P n Smash *)
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 apply H2.
(* Goal: lt n1 (S n0) *)
(* Goal: P n (Succ b) *)
(* Goal: P n Smash *)
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 apply leb_complete in H8; omega.

(* Goal: P n Smash *)
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 injection H7; intros; subst; auto.
(* Goal: P n Smash *)
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 injection H7; intros; subst; auto.

(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 case_eq (arity e1); intros; rewrite H8 in H7; try discriminate.
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 case_eq (arity e2); intros; rewrite H9 in H7; try discriminate.
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 case_eq (arity e3); intros; rewrite H10 in H7; try discriminate.
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 case_eq (arity e4); intros; rewrite H11 in H7; try discriminate.
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 destruct n1; simpl; intros; try discriminate; auto.
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 destruct n1; simpl; intros; try discriminate; auto.
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 case_eq (beq_nat n0 n1); intros; rewrite H12 in H7; try discriminate.
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 apply beq_nat_true in H12; subst.
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 case_eq (beq_nat n2 (S (S n1))); intros; rewrite H12 in H7; try discriminate.
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 apply beq_nat_true in H12; subst.
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 case_eq (beq_nat n3 (S n1)); intros; rewrite H12 in H7; try discriminate.
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 apply beq_nat_true in H12; subst.
(* Goal: P n (Comp n0 e l) *)
 simpl in H7.
(* Goal: P n (Comp n0 e l) *)
 injection H7; intros; subst.
(* Goal: P (S n1) (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 apply H5; auto.
(* Goal: P n c *)
(* Goal: Q n l *)
 eapply Cobham_ind_inf'; eauto.
(* Goal: P n c *)
(* Goal: Q n l *)
 eapply Cobham_ind_inf'; eauto.
(* Goal: P n c *)
(* Goal: Q n l *)
 eapply Cobham_ind_inf'; eauto.
(* Goal: P n c *)
(* Goal: Q n l *)
 eapply Cobham_ind_inf'; eauto.

(* Goal: P n (Comp n0 e l) *)
 case_eq (arity e); intros; rewrite H8 in H7; try discriminate.
(* Goal: P n (Comp n0 e l) *)
 case_eq (beq_nat n1 (length l)); intros; rewrite H9 in H7; try discriminate.
 case_eq (forallb (fun e : Arity => arity_eq e (ok_arity n0)) (map arity l)); 
 intros; rewrite H10 in H7;try discriminate.
(* Goal: P n (Comp n0 e l) *)
 simpl in H7.
(* Goal: P n (Comp n0 e l) *)
 injection H7; intros; subst.
(* Goal: P n (Comp n e l) *)
 rewrite forallb_forall in H10.
(* Goal: P n (Comp n e l) *)
 apply beq_nat_true in H9; subst.
(* Goal: P n (Comp n e l) *)
 apply H6; trivial.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
 intros.
(* Goal: @eq Arity (arity c) (ok_arity n) *)
(* Goal: Q n l *)
 apply arity_eq_true. 
(* Goal: @eq bool (arity_eq x (ok_arity n)) true *)
 apply H10.
(* Goal: @In Arity (arity e0) (@map Cobham Arity arity l) *)
(* Goal: P (@length Cobham l) e *)
(* Goal: Q n l *)
 apply in_map_iff.
(* Goal: @ex Cobham (fun x : Cobham => and (@eq Arity (arity x) (arity e0)) (@In Cobham x l)) *)
(* Goal: P (@length Cobham l) e *)
(* Goal: Q n l *)
 exists e0; split; trivial.
(* Goal: P n c *)
(* Goal: Q n l *)
 eapply Cobham_ind_inf'; eauto.
(* Goal: Q n l *)
 clear H8.
(* Goal: Q n l *)
 revert l H10.
(* Goal: forall (l : list Cobham) (_ : forall (x : Arity) (_ : @In Arity x (@map Cobham Arity arity l)), @eq bool (arity_eq x (ok_arity n)) true), Q n l *)
 fix Cobham_ind_inf'0 1.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
 intros.
(* Goal: Q n l *)
 destruct l.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 auto.
(* Goal: Q (@cons Cobham c l) *)
 eapply H0.
(* Goal: P n c *)
(* Goal: Q n l *)
 eapply Cobham_ind_inf'; eauto.
(* Goal: @eq Arity (arity c) (ok_arity n) *)
(* Goal: Q n l *)
 apply arity_eq_true.
(* Goal: @eq bool (arity_eq x (ok_arity n)) true *)
 apply H10.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 simpl; auto.
(* Goal: Q n l *)
 apply Cobham_ind_inf'0.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
 intros.
(* Goal: @eq bool (arity_eq x (ok_arity n)) true *)
 apply H10.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 simpl; auto.
Qed.

Lemma Cobham_ind_inf :
  forall (P : nat -> Cobham -> Prop),
  P 0 Zero ->
  (forall n i, i < n  ->  P n (Proj n i)) ->
  (forall b, P 1 (Succ b)) ->
  (P 2 Smash) ->
  (forall n g h0 h1 j, 
    arity g = ok_arity n ->
    arity h0 = ok_arity (S (S n)) ->
    arity h1 = ok_arity (S (S n)) ->
    arity j = ok_arity (S n) ->
    P n g -> 
    P (S (S n)) h0 -> 
    P (S (S n)) h1 -> 
    P (S n) j ->
    P (S n) (Rec g h0 h1 j)) ->
  (forall n h rl, 
    arity h = ok_arity (length rl)  ->
    (forall e, In e rl -> arity e = ok_arity n) ->
    P (length rl) h -> 
    (forall r, In r rl -> P n r) ->
    P n (Comp n h rl)) ->
  forall e n , arity e = ok_arity n -> P n e.
Proof.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
  intros.
  apply Cobham_ind_inf'
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
    with (Q := fun n l => forall e , In e l -> P n e); auto; simpl in *; intros.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
  tauto.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
  destruct H8; subst; auto.
Qed.

(** * Semantics

  - [Sem e vl] is the evaluation of the expression [e] where the [i]th variable is
    instantiated with the [i]th value of [vl].
    If a variable is not assigned a value, then it is assumed to be the empty bitstring [nil].
    Values in [vl] that do not correspond to a variable are ignored.

  - [Cobham_ind_inf] is an induction principle that makes easier dealing with arity in inductive proofs.
*)

Fixpoint sem_Rec (sem_g sem_h0 sem_h1 : list bs -> bs) (v : bs) (vl : list bs) : bs :=
  match v with
    | nil => sem_g vl
    | b::v' => if b then 
      sem_h1 (v' :: (sem_Rec sem_g sem_h0 sem_h1 v' vl) :: vl)
      else sem_h0 (v' :: (sem_Rec sem_g sem_h0 sem_h1 v' vl) :: vl)
  end.

Fixpoint smash' (x y : bs) :=
  match x with 
    | nil => y
    | _ :: x' => false :: smash' x' y
  end.

Lemma length_smash' x y :
  length (smash' x y) = length x + length y.
Proof.
(* Goal: @eq nat (@length bool (smash' x y)) (Init.Nat.add (@length bool x) (@length bool y)) *)
  induction x; simpl; trivial.
(* Goal: @eq nat (S (@length bool (smash' x y))) (S (Init.Nat.add (@length bool x) (@length bool y))) *)
  intros; rewrite IHx; trivial.
Qed.

Fixpoint smash_bs (x y : bs) : bs :=
  match x with
    | nil => true :: nil
    | _ :: x' => smash' y (smash_bs x' y)
  end.

Lemma length_smash x y :
  length (smash_bs x y) = 1 + length x * length y.
Proof.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
  induction x; simpl; trivial; intros.
(* Goal: @eq nat (@length bool (smash' y (smash_bs x y))) (S (Init.Nat.add (@length bool y) (Init.Nat.mul (@length bool x) (@length bool y)))) *)
  rewrite length_smash', IHx; omega.
Qed.

Fixpoint Sem (e: Cobham) (vl:list bs) : bs :=
  match e with
  | Zero => nil
  | Proj n j => nth j vl nil
  | Succ b => b :: hd nil vl
  | Smash => smash_bs (hd nil vl) (hd nil (tl vl))
  | Rec g h0 h1 j =>  
    sem_Rec (Sem g) (Sem h0) (Sem h1) (hd nil vl) (tail vl)
  | Comp _ h l => Sem h (List.map (fun e => Sem e vl) l)
  end.

Lemma simpl_Rec : forall g h0 h1 j l,
  Sem (Rec g h0 h1 j) l = sem_Rec (Sem g) (Sem h0) (Sem h1) (hd nil l) (tl l).
Proof.
(* Goal: forall (g h0 h1 j : Cobham) (l : list (list bool)), @eq (list bool) (Sem (Rec g h0 h1 j) l) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) *)
 intros; simpl; trivial.
Qed.

Lemma Sem_add_zero : forall e n,
  arity e = ok_arity n ->
  forall l,
  length l <= n ->
  Sem e l = Sem e (l ++ (map (fun e => nil) (seq 0 (n - length l)))).
Proof.
 refine (Cobham_ind_inf (fun n e =>  forall l : list bs,
   length l <= n ->
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
   Sem e l = Sem e (l ++ map (fun _ : nat => nil) (seq 0 (n - length l)))) _ _ _ _ _ _); simpl; auto; intros.

(* Goal: @eq (list bool) (@nth (list bool) i l (@nil bool)) (@nth (list bool) i (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l))))) (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (@hd (list bool) (@nil bool) l)) (@cons bool b (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S O | S l => O end))))) *)
(* Goal: @eq (list bool) (smash_bs (@hd (list bool) (@nil bool) l) (@hd (list bool) (@nil bool) (@tl (list bool) l))) (smash_bs (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))) (@hd (list bool) (@nil bool) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end)))) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 destruct (le_lt_dec (length l) i).
(* Goal: @eq (list bool) (@nth (list bool) i l (@nil bool)) (@nth (list bool) i (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l))))) (@nil bool)) *)
(* Goal: @eq (list bool) (@nth (list bool) i l (@nil bool)) (@nth (list bool) i (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l))))) (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (@hd (list bool) (@nil bool) l)) (@cons bool b (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S O | S l => O end))))) *)
(* Goal: @eq (list bool) (smash_bs (@hd (list bool) (@nil bool) l) (@hd (list bool) (@nil bool) (@tl (list bool) l))) (smash_bs (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))) (@hd (list bool) (@nil bool) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end)))) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 rewrite nth_overflow; trivial.
(* Goal: @eq (list bool) (@nil bool) (@nth (list bool) i (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l))))) (@nil bool)) *)
(* Goal: @eq (list bool) (@nth (list bool) i l (@nil bool)) (@nth (list bool) i (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l))))) (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (@hd (list bool) (@nil bool) l)) (@cons bool b (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S O | S l => O end))))) *)
(* Goal: @eq (list bool) (smash_bs (@hd (list bool) (@nil bool) l) (@hd (list bool) (@nil bool) (@tl (list bool) l))) (smash_bs (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))) (@hd (list bool) (@nil bool) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end)))) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 rewrite app_nth2; trivial.
(* Goal: @eq (list bool) (@nil bool) (@nth (list bool) (Init.Nat.sub i (@length (list bool) l)) (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))) (@nil bool)) *)
(* Goal: @eq (list bool) (@nth (list bool) i l (@nil bool)) (@nth (list bool) i (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l))))) (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (@hd (list bool) (@nil bool) l)) (@cons bool b (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S O | S l => O end))))) *)
(* Goal: @eq (list bool) (smash_bs (@hd (list bool) (@nil bool) l) (@hd (list bool) (@nil bool) (@tl (list bool) l))) (smash_bs (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))) (@hd (list bool) (@nil bool) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end)))) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 rewrite nth_map_cst; trivial. 
(* Goal: @eq (list bool) (@nth (list bool) i l (@nil bool)) (@nth (list bool) i (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l))))) (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (@hd (list bool) (@nil bool) l)) (@cons bool b (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S O | S l => O end))))) *)
(* Goal: @eq (list bool) (smash_bs (@hd (list bool) (@nil bool) l) (@hd (list bool) (@nil bool) (@tl (list bool) l))) (smash_bs (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))) (@hd (list bool) (@nil bool) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end)))) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 rewrite app_nth1; trivial.
(* Goal: @eq (list bool) (smash_bs (@hd (list bool) (@nil bool) l) (@hd (list bool) (@nil bool) (@tl (list bool) l))) (smash_bs (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))) (@hd (list bool) (@nil bool) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end)))) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 f_equal; destruct l; simpl; trivial.
(* Goal: @eq (list bool) (smash_bs (@hd (list bool) (@nil bool) l) (@hd (list bool) (@nil bool) (@tl (list bool) l))) (smash_bs (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))) (@hd (list bool) (@nil bool) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S (S O) | S (O as l) => S O | S (S l0 as l) => O end)))))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end)))) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 f_equal; destruct l; simpl; trivial.
(* Goal: @eq (list bool) (@hd (list bool) (@nil bool) l0) (@hd (list bool) (@nil bool) (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l0 with | O => S O | S l => O end)))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end)))) (@tl (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O match @length (list bool) l with | O => S n | S l => Init.Nat.sub n l end))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 destruct l0; simpl; trivial.
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l l')) (@tl (list bool) (@app (list bool) l l'))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 destruct l; simpl in *; try discriminate.
(* Goal: @eq (list bool) (Sem g (@nil (list bool))) (Sem g (@map nat (list bool) (fun _ : nat => @nil bool) (seq (S O) n))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 rewrite <- app_nil_l with (l := (map (fun _ : nat => nil) (seq 1 n))).
(* Goal: @eq (list bool) (Sem g (@nil (list bool))) (Sem g (@app (list bool) (@nil (list bool)) (@map nat (list bool) (fun _ : nat => @nil bool) (seq (S O) n)))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 rewrite <- seq_shift, map_map.
(* Goal: @eq (list bool) (Sem g (@nil (list bool))) (Sem g (@app (list bool) (@nil (list bool)) (@map nat (list bool) (fun _ : nat => @nil bool) (seq O n)))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 replace n with (n - length (@nil bs)).
(* Goal: @eq (list bool) (Sem g (@nil (list bool))) (Sem g (@app (list bool) (@nil (list bool)) (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) (@nil (list bool)))))))) *)
(* Goal: @eq nat (Init.Nat.sub n (@length (list bool) (@nil (list bool)))) n *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 apply H3; trivial.
(* Goal: @eq nat (Init.Nat.sub n (@length (list bool) (@nil (list bool)))) n *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 simpl; omega.
(* Goal: @eq nat (Init.Nat.sub n (@length (list bool) (@nil (list bool)))) n *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 simpl; omega.
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 induction l; simpl.
(* Goal: @eq (list bool) (Sem g l0) (Sem g (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (if a then Sem h1 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) else Sem h0 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0))) (if a then Sem h1 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0))))))) else Sem h0 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 apply H3; trivial; omega.
(* Goal: @eq (list bool) (if a then Sem h1 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) else Sem h0 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0))) (if a then Sem h1 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 l')) (@app (list bool) l0 l'))) else Sem h0 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 l')) (@app (list bool) l0 l')))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 rewrite <- IHl.
 replace (l :: sem_Rec (Sem g) (Sem h0) (Sem h1) l l0
   :: l0 ++ map (fun _ : nat => nil) (seq 0 (n - length l0))) with
 ((l :: sem_Rec (Sem g) (Sem h0) (Sem h1) l l0 :: l0) ++ 
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
   (map (fun _ : nat => nil) (seq 0 (n - length l0)))); trivial.
(* Goal: @eq (list bool) (if a then Sem h1 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) else Sem h0 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0))) (if a then Sem h1 (@app (list bool) (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) l') else Sem h0 (@app (list bool) (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) l')) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 case a.
(* Goal: @eq (list bool) (Sem h1 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0))) (Sem h1 (@app (list bool) (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (Sem h0 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0))) (Sem h0 (@app (list bool) (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 erewrite H5; eauto; simpl; trivial; omega.
(* Goal: @eq (list bool) (Sem h0 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0))) (Sem h0 (@app (list bool) (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 erewrite H4; eauto; simpl; trivial; omega. 
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 f_equal.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
 apply map_ext2; intros.
(* Goal: @eq (list bool) (Sem a l) (Sem a (@app (list bool) l l')) *)
 eapply H2; trivial.
Qed.

Lemma Sem_remove_zero : forall e n,
  arity e = ok_arity n ->
  forall l l',  n = length l ->
    Sem e l = Sem e (l ++ l').
Proof.
 refine (Cobham_ind_inf (fun n e => 
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
   forall l l',  n = length l -> Sem e l = Sem e (l ++ l')) _ _ _ _ _ _); simpl; auto; intros.
(* Goal: @eq (list bool) (@nth (list bool) i l (@nil bool)) (@nth (list bool) i (@app (list bool) l l') (@nil bool)) *)
(* Goal: @eq (list bool) (@cons bool b (@hd (list bool) (@nil bool) l)) (@cons bool b (@hd (list bool) (@nil bool) (@app (list bool) l l'))) *)
(* Goal: @eq (list bool) (smash_bs (@hd (list bool) (@nil bool) l) (@hd (list bool) (@nil bool) (@tl (list bool) l))) (smash_bs (@hd (list bool) (@nil bool) (@app (list bool) l l')) (@hd (list bool) (@nil bool) (@tl (list bool) (@app (list bool) l l')))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l l')) (@tl (list bool) (@app (list bool) l l'))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 rewrite app_nth1; trivial; omega.
(* Goal: @eq (list bool) (smash_bs (@hd (list bool) (@nil bool) l) (@hd (list bool) (@nil bool) (@tl (list bool) l))) (smash_bs (@hd (list bool) (@nil bool) (@app (list bool) l l')) (@hd (list bool) (@nil bool) (@tl (list bool) (@app (list bool) l l')))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l l')) (@tl (list bool) (@app (list bool) l l'))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 destruct l; simpl in *; try discriminate; trivial.
(* Goal: @eq (list bool) (smash_bs (@hd (list bool) (@nil bool) l) (@hd (list bool) (@nil bool) (@tl (list bool) l))) (smash_bs (@hd (list bool) (@nil bool) (@app (list bool) l l')) (@hd (list bool) (@nil bool) (@tl (list bool) (@app (list bool) l l')))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l l')) (@tl (list bool) (@app (list bool) l l'))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 destruct l; simpl in *; try discriminate; trivial.
(* Goal: @eq (list bool) (smash_bs l (@hd (list bool) (@nil bool) l0)) (smash_bs l (@hd (list bool) (@nil bool) (@app (list bool) l0 l'))) *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l l')) (@tl (list bool) (@app (list bool) l l'))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 destruct l0; simpl in *; try discriminate; trivial.
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l)) (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) (@app (list bool) l l')) (@tl (list bool) (@app (list bool) l l'))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 destruct l; simpl in *; try discriminate.
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 induction l; simpl.
(* Goal: @eq (list bool) (Sem g l0) (Sem g (@app (list bool) l0 l')) *)
(* Goal: @eq (list bool) (if a then Sem h1 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) else Sem h0 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0))) (if a then Sem h1 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 l')) (@app (list bool) l0 l'))) else Sem h0 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 l')) (@app (list bool) l0 l')))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 eapply H3; eauto; omega.
(* Goal: @eq (list bool) (if a then Sem h1 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) else Sem h0 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0))) (if a then Sem h1 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 l')) (@app (list bool) l0 l'))) else Sem h0 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 l')) (@app (list bool) l0 l')))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 rewrite <- IHl.
 replace (l :: sem_Rec (Sem g) (Sem h0) (Sem h1) l l0 :: l0 ++ l') with
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
   ((l :: sem_Rec (Sem g) (Sem h0) (Sem h1) l l0 :: l0) ++ l'); trivial.
(* Goal: @eq (list bool) (if a then Sem h1 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) else Sem h0 (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0))) (if a then Sem h1 (@app (list bool) (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) l') else Sem h0 (@app (list bool) (@cons (list bool) l (@cons (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) l0)) l')) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 case a.
(* Goal: @eq nat (Init.Nat.sub n (@length (list bool) (@nil (list bool)))) n *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 eapply H5; eauto; simpl; omega.
(* Goal: @eq nat (Init.Nat.sub n (@length (list bool) (@nil (list bool)))) n *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 eapply H4; eauto; simpl; omega.
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l l')) rl)) *)
 f_equal.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
 apply map_ext2; intros.
(* Goal: @eq (list bool) (Sem a l) (Sem a (@app (list bool) l l')) *)
 eapply H2; trivial.
Qed.

(** * Length-bounding condition that must hold for a Cobham expression to be valid *)

Fixpoint rec_bounded' (e : Cobham) : Prop :=
  match e with
    | Rec g h0 h1 j =>
      rec_bounded' j  /\ 
      rec_bounded' g /\ 
      rec_bounded' h0 /\ 
      rec_bounded' h1 /\
      (match (arity e) with
         | ok_arity n => forall l, length l = n ->
           length (Sem e l) <= length (Sem j l)
        | _ => True (* never happen *)
       end)
    | Comp n h l => rec_bounded' h /\
        andl rec_bounded' l
    | _ => True
  end.

Fixpoint rec_bounded (e : Cobham) : Prop :=
  match e with
    | Rec g h0 h1 j =>
      rec_bounded j  /\ 
      rec_bounded g /\ 
      rec_bounded h0 /\ 
      rec_bounded h1 /\
      (forall l, 
        length (Sem e l) <= length (Sem j l))
    | Comp n h l => rec_bounded h /\
        andl rec_bounded l
    | _ => True
  end.

Lemma rec_bounded_spec (e : Cobham) :
  rec_bounded e -> rec_bounded' e.
Proof.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
 induction e using Cobham_ind2; simpl; auto; intros.
 decompose [and] H; clear H.
(* Goal: and (rec_bounded j) (and (rec_bounded g) (and (rec_bounded h0) (and (rec_bounded h1) (forall l : list (list bool), le (@length bool (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem j l)))))) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 repeat (split; try tauto).
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 case_eq (arity e1); intros; try discriminate; auto.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 case_eq (arity e2); intros; try discriminate; auto.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 case_eq (arity e3); intros; try discriminate; auto.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 case_eq (arity e4); intros; try discriminate; auto.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 destruct n0; simpl; intros; try discriminate; auto.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 destruct n0; simpl; intros; try discriminate; auto.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 case_eq (beq_nat n n0); simpl; intros; try discriminate; auto.
 case_eq (beq_nat n1 (S (S n0))); simpl; intros; 
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
   try discriminate; auto.
(* Goal: P n (Rec e1 e2 e3 e4) *)
(* Goal: P n (Comp n0 e l) *)
 destruct n1; simpl; intros; try discriminate; auto.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 case_eq (beq_nat n2 n1); simpl; intros; try discriminate; auto.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 split; try tauto.
 revert e IHe H0.
 induction l; simpl; intros; trivial.
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 split.
(* Goal: Q (@nil Cobham) *)
(* Goal: Q (@cons Cobham c l) *)
 apply H.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
simpl; tauto.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
tauto.
eapply IHl.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
intros.
(* Goal: Q (@nil Cobham) *)
(* Goal: Q (@cons Cobham c l) *)
apply H.
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
simpl.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
tauto.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
trivial.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
auto.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
tauto.
Qed.

Lemma rec_bounded'_spec : forall (e : Cobham) n,
  arity e = ok_arity n ->
  rec_bounded' e -> 
  rec_bounded e.
Proof.
 refine (Cobham_ind_inf (fun n e => 
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
   rec_bounded' e -> rec_bounded e) _ _ _ _ _ _); simpl; auto; intros.
(* Goal: and (rec_bounded j) (and (rec_bounded g) (and (rec_bounded h0) (and (rec_bounded h1) (forall l : list (list bool), le (@length bool (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem j l)))))) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 decompose [and] H7; clear H7.
(* Goal: and (rec_bounded j) (and (rec_bounded g) (and (rec_bounded h0) (and (rec_bounded h1) (forall l : list (list bool), le (@length bool (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem j l)))))) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite H, H0, H1,H2 in H13.
(* Goal: and (rec_bounded j) (and (rec_bounded g) (and (rec_bounded h0) (and (rec_bounded h1) (forall l : list (list bool), le (@length bool (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem j l)))))) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 simpl in H13. 
(* Goal: and (rec_bounded j) (and (rec_bounded g) (and (rec_bounded h0) (and (rec_bounded h1) (forall l : list (list bool), le (@length bool (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem j l)))))) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite <- beq_nat_refl in H13.
(* Goal: and (rec_bounded j) (and (rec_bounded g) (and (rec_bounded h0) (and (rec_bounded h1) (forall l : list (list bool), le (@length bool (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem j l)))))) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 simpl in H13.
(* Goal: and (rec_bounded j) (and (rec_bounded g) (and (rec_bounded h0) (and (rec_bounded h1) (forall l : list (list bool), le (@length bool (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem j l)))))) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 repeat (split; try tauto).
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
 intros.
(* Goal: le (@length bool (sem_Rec (Sem g) (Sem h0) (Sem h1) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem j l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite <- simpl_Rec with (j := j).
(* Goal: le (@length bool (Sem (Rec g h0 h1 j) l)) (@length bool (Sem j l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 destruct (le_lt_dec (length l) (S n)).
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite Sem_add_zero with (n := S n); trivial.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite Sem_add_zero with (e := j) (n := S n); trivial.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 apply H13; trivial.
(* Goal: @eq nat (@length (list bool) (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub (S n) (@length (list bool) l)))))) (S n) *)
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: le (@length bool (Sem (Rec g h0 h1 j) l)) (@length bool (Sem j l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite app_length, map_length, seq_length.
(* Goal: @eq nat (Init.Nat.add (@length (list bool) l) (Init.Nat.sub (S n) (@length (list bool) l))) (S n) *)
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: le (@length bool (Sem (Rec g h0 h1 j) l)) (@length bool (Sem j l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 omega.
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 simpl.
(* Goal: @eq Arity match arity g with | error_Rec a a0 a1 a2 => error_Rec (error_Rec a a0 a1 a2) (arity h0) (arity h1) (arity j) | error_Comp a l => error_Rec (error_Comp a l) (arity h0) (arity h1) (arity j) | error_Proj n n0 => error_Rec (error_Proj n n0) (arity h0) (arity h1) (arity j) | ok_arity gn => match arity h0 with | error_Rec a a0 a1 a2 => error_Rec (ok_arity gn) (error_Rec a a0 a1 a2) (arity h1) (arity j) | error_Comp a l => error_Rec (ok_arity gn) (error_Comp a l) (arity h1) (arity j) | error_Proj n n0 => error_Rec (ok_arity gn) (error_Proj n n0) (arity h1) (arity j) | ok_arity h0n => match arity h1 with | error_Rec a a0 a1 a2 => error_Rec (ok_arity gn) (ok_arity h0n) (error_Rec a a0 a1 a2) (arity j) | error_Comp a l => error_Rec (ok_arity gn) (ok_arity h0n) (error_Comp a l) (arity j) | error_Proj n n0 => error_Rec (ok_arity gn) (ok_arity h0n) (error_Proj n n0) (arity j) | ok_arity h1n => match arity j with | error_Rec a a0 a1 a2 => error_Rec (ok_arity gn) (ok_arity h0n) (ok_arity h1n) (error_Rec a a0 a1 a2) | error_Comp a l => error_Rec (ok_arity gn) (ok_arity h0n) (ok_arity h1n) (error_Comp a l) | error_Proj n n0 => error_Rec (ok_arity gn) (ok_arity h0n) (ok_arity h1n) (error_Proj n n0) | ok_arity jn => if andb (andb match h0n with | O => false | S (O as m') => false | S (S m'0 as m') => Nat.eqb gn m'0 end (Nat.eqb h1n h0n)) match h1n with | O => false | S m' => Nat.eqb jn m' end then ok_arity jn else error_Rec (ok_arity gn) (ok_arity h0n) (ok_arity h1n) (ok_arity jn) end end end end (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite H, H0, H1, H2.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 repeat rewrite <- beq_nat_refl; simpl; trivial.

(* Goal: le (@length bool (Sem (Rec g h0 h1 j) l)) (@length bool (Sem j l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite <- firstn_skipn with (n := S n) (l := l).
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite <- Sem_remove_zero with (n := S n); trivial.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite <- Sem_remove_zero with (n := S n); trivial.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 apply H13; trivial; trivial.
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite firstn_length.
(* Goal: @eq nat (Init.Nat.add (@length (list bool) l) (Init.Nat.sub (S n) (@length (list bool) l))) (S n) *)
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: le (@length bool (Sem (Rec g h0 h1 j) l)) (@length bool (Sem j l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite min_l; trivial; omega.
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite firstn_length.
(* Goal: @eq nat (Init.Nat.add (@length (list bool) l) (Init.Nat.sub (S n) (@length (list bool) l))) (S n) *)
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: le (@length bool (Sem (Rec g h0 h1 j) l)) (@length bool (Sem j l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite min_l; trivial; omega.
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 simpl.
(* Goal: @eq Arity match arity g with | error_Rec a a0 a1 a2 => error_Rec (error_Rec a a0 a1 a2) (arity h0) (arity h1) (arity j) | error_Comp a l => error_Rec (error_Comp a l) (arity h0) (arity h1) (arity j) | error_Proj n n0 => error_Rec (error_Proj n n0) (arity h0) (arity h1) (arity j) | ok_arity gn => match arity h0 with | error_Rec a a0 a1 a2 => error_Rec (ok_arity gn) (error_Rec a a0 a1 a2) (arity h1) (arity j) | error_Comp a l => error_Rec (ok_arity gn) (error_Comp a l) (arity h1) (arity j) | error_Proj n n0 => error_Rec (ok_arity gn) (error_Proj n n0) (arity h1) (arity j) | ok_arity h0n => match arity h1 with | error_Rec a a0 a1 a2 => error_Rec (ok_arity gn) (ok_arity h0n) (error_Rec a a0 a1 a2) (arity j) | error_Comp a l => error_Rec (ok_arity gn) (ok_arity h0n) (error_Comp a l) (arity j) | error_Proj n n0 => error_Rec (ok_arity gn) (ok_arity h0n) (error_Proj n n0) (arity j) | ok_arity h1n => match arity j with | error_Rec a a0 a1 a2 => error_Rec (ok_arity gn) (ok_arity h0n) (ok_arity h1n) (error_Rec a a0 a1 a2) | error_Comp a l => error_Rec (ok_arity gn) (ok_arity h0n) (ok_arity h1n) (error_Comp a l) | error_Proj n n0 => error_Rec (ok_arity gn) (ok_arity h0n) (ok_arity h1n) (error_Proj n n0) | ok_arity jn => if andb (andb match h0n with | O => false | S (O as m') => false | S (S m'0 as m') => Nat.eqb gn m'0 end (Nat.eqb h1n h0n)) match h1n with | O => false | S m' => Nat.eqb jn m' end then ok_arity jn else error_Rec (ok_arity gn) (ok_arity h0n) (ok_arity h1n) (ok_arity jn) end end end end (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite H, H0, H1, H2.
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 repeat rewrite <- beq_nat_refl; simpl.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 trivial.
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite firstn_length.
(* Goal: @eq nat (Init.Nat.add (@length (list bool) l) (Init.Nat.sub (S n) (@length (list bool) l))) (S n) *)
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: le (@length bool (Sem (Rec g h0 h1 j) l)) (@length bool (Sem j l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite min_l; trivial; omega.

(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 split.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 tauto.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
 apply forall_andl; intros.
(* Goal: rec_bounded x *)
 destruct H3.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 rewrite <- forall_andl in H5; auto.
Qed.

(** * Length-bounding polynomial for Cobham expressions

  - The lemma [poly_Cobham_correct] states that the output of an expression [e]
    is bounded by the polynomial [poly_Cobham e].
*)

Fixpoint poly_Cobham (e : Cobham) :=
  match e with
    | Zero => pcst 0 0
    | Proj n i => pproj n i
    | Succ b => pplus (pcst 0 1) (pproj 1 0)
    | Smash => pplus (pcst 0 1) (pmult (pproj 2 0) (pproj 2 1))
    | Rec g h0 h1 j => poly_Cobham j
    | Comp n h l => 
      pplus (pcst n 0) 
      (pcomp (poly_Cobham h) (map poly_Cobham l))
  end.

Lemma parity_poly_Cobham : forall (e : Cobham) n,
  arity e = ok_arity n ->
  parity (poly_Cobham e) = n.
Proof.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
  apply Cobham_ind_inf; simpl; auto; intros.
(* Goal: @eq nat (Init.Nat.max n (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) (@map Cobham pol poly_Cobham rl)))) n *)
  apply max_l.
(* Goal: le (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) (@map Cobham pol poly_Cobham rl))) n *)
  apply maxl_map.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
  intros.
(* Goal: pWF x *)
  apply in_map_iff in H3.
(* Goal: pWF x *)
  destruct H3 as (? & ? & ?); subst.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
  apply H2; trivial.
Qed.

Lemma pWF_poly_Cobham : forall (e : Cobham) n,
  arity e = ok_arity n ->
  pWF (poly_Cobham e).
Proof.
(* Goal: forall (e : Cobham) (n : nat) (_ : @eq Arity (arity e) (ok_arity n)), pWF (poly_Cobham e) *)
  apply Cobham_ind_inf; simpl; auto; intros; try pWF.
(* Goal: pWF x *)
  apply in_map_iff in H3.
(* Goal: pWF x *)
  destruct H3 as (? & ? & ?); subst.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
  apply H2; trivial.
Qed.

Lemma poly_Cobham_correct : forall (e : Cobham) xl,
  rec_bounded e ->  
  length (Sem e xl) <= 
  peval (poly_Cobham e) (map (@length _) xl).
Proof.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 induction e using Cobham_ind2; intros; simpl in *; trivial.

(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite <- (@map_nth _ _ (@length _) xl); simpl; trivial.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite pproj_correct; trivial.

 rewrite pplus_correct, pproj_correct.
(* Goal: @eq nat (Init.Nat.sub n (@length (list bool) (@nil (list bool)))) n *)
(* Goal: @eq (list bool) (sem_Rec (Sem g) (Sem h0) (Sem h1) l l0) (sem_Rec (Sem g) (Sem h0) (Sem h1) l (@app (list bool) l0 (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l0)))))) *)
(* Goal: @eq (list bool) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e l) rl)) (Sem h (@map Cobham (list bool) (fun e : Cobham => Sem e (@app (list bool) l (@map nat (list bool) (fun _ : nat => @nil bool) (seq O (Init.Nat.sub n (@length (list bool) l)))))) rl)) *)
 rewrite <- hd_nth_0, (map_hd _ _ (@length _)); simpl; omega.

 rewrite length_smash, pplus_correct, pmult_correct, pcst_correct, 
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
   pproj_correct, pproj_correct, <- hd_nth_0, hd_nth_1, (map_hd _ _ (@length _)); simpl.
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite <- (@map_nth _ _ (@length _) xl); simpl.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 trivial.
 
 decompose [and] H; clear H.
 apply le_trans with (1 := H5 xl).
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 apply IHe4; trivial.
 rewrite pplus_correct.
 rewrite pcst_correct.
 rewrite pcomp_correct.
 eapply le_trans.
 apply IHe.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 tauto.
 repeat rewrite map_map.
 apply peval_monotonic.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
 intros.
 rewrite map_nth2 with (d := Zero);[ | simpl; trivial].
 rewrite map_nth2 with (d := Zero);[ | simpl; trivial].
 clear IHe.
 assert (rec_bounded (nth i l Zero)).
 clear H.
 revert i.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 induction l; simpl in *; intros; case i; simpl; trivial.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 tauto.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map Cobham pol poly_Cobham rl)), @eq nat (@fst nat (list mon) x) n *)
 intros.
 apply IHl.
(* Goal: Q n (@nil Cobham) *)
(* Goal: Q n (@cons Cobham c l) *)
 tauto.
 destruct (lt_dec i (length l)).
(* Goal: Q (@nil Cobham) *)
(* Goal: Q (@cons Cobham c l) *)
 apply H.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 apply nth_In; trivial.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 trivial.
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 rewrite nth_overflow; simpl.
(* Goal: @eq Arity (ok_arity (S n)) (ok_arity (S n)) *)
(* Goal: @eq nat (S n) (@length (list bool) (@firstn (list bool) (S n) l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 trivial.
(* Goal: @eq nat (Init.Nat.add (@length (list bool) l) (Init.Nat.sub (S n) (@length (list bool) l))) (S n) *)
(* Goal: @eq Arity (arity (Rec g h0 h1 j)) (ok_arity (S n)) *)
(* Goal: le (@length bool (Sem (Rec g h0 h1 j) l)) (@length bool (Sem j l)) *)
(* Goal: and (rec_bounded h) (@andl Cobham rec_bounded rl) *)
 omega.
Qed.
