Require Import Arith List.
Require Import BellantoniCook.Lib BellantoniCook.MultiPoly BellantoniCook.Cobham BellantoniCook.CobhamLib.

Lemma Zero_correct n l: 
  length (Sem (Zero_e n) l) = 0.
Proof.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  trivial.
Qed.

Lemma One_correct n l: 
  length (Sem (One_e n) l) = 1.
Proof.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  trivial.
Qed.

Definition Succ_e : Cobham :=
  Comp 1 (Succ true) [Proj 1 0].

Lemma arity_Succ : arity Succ_e = ok_arity 1.
Proof.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  trivial.
Qed.

Lemma rec_bounded_Succ :
  rec_bounded Succ_e.
Proof.
(* Goal: rec_bounded Succ_e *)
  simpl; tauto.
Qed.

Lemma Succ_correct l : 
  length (Sem Succ_e l) = S (length (Sem (Proj 1 0) l)).
Proof.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  trivial.
Qed.

Opaque Succ_e.

Fixpoint Nat_e (n:nat) : Cobham :=
  match n with
    | 0 => Zero
    | S n' => Comp 0 Succ_e [Nat_e n']
  end.

Lemma arity_Nat n : arity (Nat_e n) = ok_arity 0.
Proof.
(* Goal: @eq Arity (arity (Nat_e n)) (ok_arity O) *)
  induction n; trivial; simpl.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  rewrite arity_Succ, IHn; simpl; trivial.
Qed.

Lemma rec_bounded_Nat n :
  rec_bounded (Nat_e n).
Proof.
(* Goal: rec_bounded (Nat_e n) *)
  induction n; simpl; trivial; split; auto.
(* Goal: rec_bounded Succ_e *)
  apply rec_bounded_Succ.
Qed.

Lemma Nat_correct : forall n l,
  length (Sem (Nat_e n) l) = n.
Proof.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  induction n; simpl; intros; trivial.
(* Goal: @eq nat (@length bool (Sem Succ_e (@cons (list bool) (Sem (Nat_e n) l) (@nil (list bool))))) (S n) *)
  rewrite Succ_correct; simpl; auto.
Qed.

Notation Plus_e := App_e.

Notation arity_Plus := arity_App.

Notation rec_bounded_Plus := rec_bounded_App.

Lemma Plus_correct : forall l,
  length (Sem Plus_e l) = length (hd nil l) + length (hd nil (tl l)).
Proof.
(* Goal: forall l : list (list bool), @eq nat (@length bool (Sem App_e l)) (Init.Nat.add (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
  intro l; rewrite App_correct.
(* Goal: @eq nat (@length bool (@app bool (@hd (list bool) (@nil bool) l) (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (Init.Nat.add (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
  apply app_length.
Qed.

Opaque Plus_e.

Fixpoint Plusl_e (ar:nat)(el:list Cobham) : Cobham :=
  match el with
    | nil => Zero_e ar
    | e' :: el' => Comp ar Plus_e [e'; Plusl_e ar el']
  end. 

Lemma arity_Plusl ar el : 
  andl (fun e => arity e = ok_arity ar) el ->
  arity (Plusl_e ar el) = ok_arity ar.
Proof.
(* Goal: forall _ : @andl Cobham (fun e : Cobham => @eq Arity (arity e) (ok_arity ar)) el, @eq Arity (arity (Plusl_e ar el)) (ok_arity ar) *)
  induction el as [ | e' el' IH]; simpl; trivial; intros (H1, H2).
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  rewrite arity_Plus, IH, H1; simpl; trivial.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  rewrite <- beq_nat_refl; simpl; trivial.
Qed.

Lemma rec_bounded_Plusl ar el :
  andl rec_bounded el -> rec_bounded (Plusl_e ar el).
Proof.
(* Goal: forall _ : @andl Cobham rec_bounded el, rec_bounded (Plusl_e ar el) *)
  induction el as [ | e' el' IH]; simpl; auto.
(* Goal: forall _ : and (rec_bounded e') (@andl Cobham rec_bounded el'), and (rec_bounded App_e) (and (rec_bounded e') (and (rec_bounded (Plusl_e ar el')) True)) *)
  intros [H1 H2]; split.
(* Goal: rec_bounded App_e *)
(* Goal: and (rec_bounded e') (and (rec_bounded (Plusl_e ar el')) True) *)
  apply rec_bounded_Plus.
(* Goal: and (rec_bounded e') (and (rec_bounded (Multl_e ar el')) True) *)
  tauto.
Qed.

Lemma Plusl_correct : forall ar el l,
  length (Sem (Plusl_e ar el) l) = plusl (map (fun e => length (Sem e l)) el).
Proof.
(* Goal: forall (ar : nat) (el : list Cobham) (l : list (list bool)), @eq nat (@length bool (Sem (Multl_e ar el) l)) (multl (@map Cobham nat (fun e : Cobham => @length bool (Sem e l)) el)) *)
  induction el as [ | e' el' IH]; simpl; trivial; intros.
(* Goal: @eq nat (@length bool (Sem App_e (@cons (list bool) (Sem e' l) (@cons (list bool) (Sem (Plusl_e ar el') l) (@nil (list bool)))))) (Init.Nat.add (@length bool (Sem e' l)) (plusl (@map Cobham nat (fun e : Cobham => @length bool (Sem e l)) el'))) *)
  rewrite Plus_correct; simpl; f_equal; apply IH.
Qed.

Opaque Plusl_e.

Definition Mult_e : Cobham :=
  Rec2
  (Zero_e 1)
  (Comp 3 Plus_e [Proj 3 1; Proj 3 2])
  (Comp 2 Smash [
    One_e 2;
    Comp 2 Smash [Comp 2 (Succ true) [Proj 2 0]; Comp 2 (Succ true) [Proj 2 1] ] ] ).

Lemma arity_Mult : arity Mult_e = ok_arity 2.
Proof.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  trivial.
Qed.

Lemma rec_bounded_Mult : rec_bounded Mult_e.
Proof.
  simpl.
  repeat (split; trivial); intros; simpl;
  destruct l; simpl; try omega; rewrite length_smash';
  induction l; simpl; try omega; case a; simpl; rewrite length_smash'; try omega;
  rewrite App_correct; simpl; simpl_list; eapply le_trans.
  apply plus_le_compat_r;  apply IHl; simpl; omega.
  simpl; omega.
  apply plus_le_compat_r;  apply IHl; simpl; omega.
  simpl; omega.
Qed.

Lemma Mult_correct : forall l,
  length (Sem Mult_e l) = length (hd nil l) * length (hd nil (tl l)).
Proof.
(* Goal: forall l : list (list bool), @eq nat (@length bool (Sem Mult_e l)) (Init.Nat.mul (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
  simpl; intros [ | v1 ]; simpl; trivial; intros.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  induction v1; simpl; trivial.
  case a; simpl; rewrite Plus_correct; simpl; rewrite IHv1;
    destruct l; simpl; omega.
Qed.

Opaque Mult_e.

Fixpoint Multl_e (ar:nat)(el:list Cobham) : Cobham :=
  match el with
    | nil => One_e ar
    | e' :: el' => Comp ar Mult_e [e'; Multl_e ar el']
  end. 

Lemma arity_Multl ar el : 
  andl (fun e => arity e = ok_arity ar) el ->
  arity (Multl_e ar el) = ok_arity ar.
Proof.
(* Goal: forall _ : @andl Cobham (fun e : Cobham => @eq Arity (arity e) (ok_arity ar)) el, @eq Arity (arity (Multl_e ar el)) (ok_arity ar) *)
  induction el as [ | e' el' IH]; simpl; trivial; intros [H1 H2].
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  rewrite arity_Mult, IH, H1; simpl; trivial; rewrite <- beq_nat_refl; simpl; trivial.
Qed.

Lemma rec_bounded_Multl ar el :
  andl rec_bounded el -> rec_bounded (Multl_e ar el).
Proof.
(* Goal: forall _ : and (rec_bounded e') (@andl Cobham rec_bounded el'), and (rec_bounded App_e) (and (rec_bounded e') (and (rec_bounded (Plusl_e ar el')) True)) *)
  induction el as [ | e' el' IH]; simpl; auto; intros [H1 H2]; split.
(* Goal: rec_bounded Mult_e *)
(* Goal: and (and (rec_bounded (Nat_e a)) True) (and (rec_bounded (Multl_e ar (@map pow Cobham (Poly_pow ar) xl))) True) *)
  apply rec_bounded_Mult.
(* Goal: and (rec_bounded e') (and (rec_bounded (Multl_e ar el')) True) *)
  tauto.
Qed.

Lemma Multl_correct : forall ar el l,
  length (Sem (Multl_e ar el) l) = 
  multl (map (fun e => length (Sem e l)) el).
Proof.
(* Goal: forall (ar : nat) (el : list Cobham) (l : list (list bool)), @eq nat (@length bool (Sem (Multl_e ar el) l)) (multl (@map Cobham nat (fun e : Cobham => @length bool (Sem e l)) el)) *)
  induction el as [ | e' el' IH]; simpl; trivial; intros.
(* Goal: @eq nat (@length bool (Sem Mult_e (@cons (list bool) (Sem e' l) (@cons (list bool) (Sem (Multl_e ar el') l) (@nil (list bool)))))) (Init.Nat.mul (@length bool (Sem e' l)) (multl (@map Cobham nat (fun e : Cobham => @length bool (Sem e l)) el'))) *)
  rewrite Mult_correct; simpl; auto.
Qed.

Fixpoint Power_e (n:nat) : Cobham :=
  match n with
    | 0 => One_e 1
    | S n' => Comp 1 Mult_e [Proj 1 0; Power_e n']
  end.

Lemma arity_Power n : arity (Power_e n) = ok_arity 1.
Proof.
  induction n as [ | n' IH]; trivial; simpl.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  rewrite arity_Mult, <- beq_nat_refl, IH; simpl; trivial.
Qed.

Lemma rec_bounded_Power n : rec_bounded (Power_e n).
Proof.
(* Goal: rec_bounded (Power_e n) *)
  induction n as [ | n' IH]; simpl; intuition.
(* Goal: rec_bounded Mult_e *)
(* Goal: and (and (rec_bounded (Nat_e a)) True) (and (rec_bounded (Multl_e ar (@map pow Cobham (Poly_pow ar) xl))) True) *)
  apply rec_bounded_Mult.
Qed.

Lemma Power_correct : forall n l,
  length (Sem (Power_e n) l) = power (length (hd nil l)) n.
Proof.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  induction n as [ | n' IH]; simpl; intros; trivial.
  rewrite Mult_correct; simpl.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  rewrite IH, hd_nth_0; trivial.
Qed.

Definition Poly_pow (ar:nat) (xn:pow) : Cobham :=
  Comp ar (Power_e (snd xn)) [Proj ar (fst xn)].

Lemma arity_Poly_pow : forall ar xn,
  pWF_pow ar xn -> arity (Poly_pow ar xn) = ok_arity ar.
Proof.
  unfold pWF_pow; intros ar [x n] H;  simpl in *.
  rewrite arity_Power, <- beq_nat_refl; simpl.
(* Goal: @eq Arity (if andb (arity_eq (if match ar with | O => false | S m' => Nat.leb x m' end then ok_arity ar else error_Proj ar x) (ok_arity ar)) true then ok_arity ar else error_Comp (ok_arity (S O)) (@cons Arity (if match ar with | O => false | S m' => Nat.leb x m' end then ok_arity ar else error_Proj ar x) (@nil Arity))) (ok_arity ar) *)
  destruct ar; simpl in *.
(* Goal: @eq Arity (error_Comp (ok_arity (S O)) (@cons Arity (error_Proj O x) (@nil Arity))) (ok_arity O) *)
(* Goal: @eq Arity (if andb (arity_eq (if Nat.leb x ar then ok_arity (S ar) else error_Proj (S ar) x) (ok_arity (S ar))) true then ok_arity (S ar) else error_Comp (ok_arity (S O)) (@cons Arity (if Nat.leb x ar then ok_arity (S ar) else error_Proj (S ar) x) (@nil Arity))) (ok_arity (S ar)) *)
  contradict H; omega.
(* Goal: @eq Arity (if andb (arity_eq (if Nat.leb x ar then ok_arity (S ar) else error_Proj (S ar) x) (ok_arity (S ar))) true then ok_arity (S ar) else error_Comp (ok_arity (S O)) (@cons Arity (if Nat.leb x ar then ok_arity (S ar) else error_Proj (S ar) x) (@nil Arity))) (ok_arity (S ar)) *)
  case_eq (leb x ar); simpl; intro H0.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  rewrite <- beq_nat_refl; simpl; trivial.
(* Goal: @eq Arity (error_Comp (ok_arity (S O)) (@cons Arity (error_Proj (S ar) x) (@nil Arity))) (ok_arity (S ar)) *)
  apply leb_complete_conv in H0.
(* Goal: @eq Arity (error_Comp (ok_arity (S O)) (@cons Arity (error_Proj (S ar) x) (@nil Arity))) (ok_arity (S ar)) *)
  contradict H0; omega.
Qed.

Lemma rec_bounded_Poly_pow : forall ar xn,
  rec_bounded (Poly_pow ar xn).
Proof.
(* Goal: forall (ar : nat) (xn : pow), rec_bounded (Poly_pow ar xn) *)
  simpl; intros _ xn; split; auto.
(* Goal: rec_bounded (Power_e (@snd nat nat xn)) *)
  apply rec_bounded_Power.
Qed.

Lemma Poly_pow_correct : forall ar xn l,
  length (Sem (Poly_pow ar xn) l) = peval_pow xn (map (@length _) l).
Proof.
  intros ar [x n] l;  simpl.
  rewrite Power_correct; unfold peval_pow; simpl.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  rewrite (@map_nth _ _ (@length _) l nil); trivial.
Qed.

Opaque Poly_pow.

Definition Poly_mon (ar:nat)(m:mon) : Cobham :=
  Comp ar Mult_e [Comp ar (Nat_e (fst m)) nil; Multl_e ar (map (Poly_pow ar) (snd m))].

Lemma arity_Poly_mon : forall ar m,
  pWF_mon ar m ->
  arity (Poly_mon ar m) = ok_arity ar.
Proof.
  unfold pWF_mon; intros ar [a xl] H; simpl.
  rewrite arity_Mult, arity_Nat, arity_Multl; simpl.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  rewrite <- beq_nat_refl; simpl; trivial.
(* Goal: and (rec_bounded e') (and (rec_bounded (Multl_e ar el')) True) *)
  induction xl; simpl in *; trivial; split; try tauto.
(* Goal: and (rec_bounded e') (and (rec_bounded (Multl_e ar el')) True) *)
  apply arity_Poly_pow; tauto.
Qed.

Lemma rec_bounded_Poly_mon : forall ar m,
  rec_bounded (Poly_mon ar m).
Proof.
(* Goal: forall (ar : nat) (m : mon), rec_bounded (Poly_mon ar m) *)
  intros ar [a xl]; simpl; split.
(* Goal: rec_bounded Mult_e *)
(* Goal: and (and (rec_bounded (Nat_e a)) True) (and (rec_bounded (Multl_e ar (@map pow Cobham (Poly_pow ar) xl))) True) *)
  apply rec_bounded_Mult.
(* Goal: and (and (rec_bounded (Nat_e a)) True) (and (rec_bounded (Multl_e ar (@map pow Cobham (Poly_pow ar) xl))) True) *)
  split.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  split; trivial.
(* Goal: rec_bounded (Nat_e a) *)
(* Goal: and (rec_bounded (Multl_e ar (@map pow Cobham (Poly_pow ar) xl))) True *)
  apply rec_bounded_Nat.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  split; trivial.
(* Goal: rec_bounded (Multl_e ar (@map pow Cobham (Poly_pow ar) xl)) *)
  apply rec_bounded_Multl.
(* Goal: @andl Cobham rec_bounded (@map pow Cobham (Poly_pow ar) xl) *)
  rewrite <- forall_andl; intros.
(* Goal: rec_bounded x *)
  rewrite in_map_iff in H.
(* Goal: rec_bounded x *)
  destruct H as [xn [H _] ]; subst.
(* Goal: rec_bounded (Poly_pow ar xn) *)
  apply rec_bounded_Poly_pow.
Qed.

Lemma Poly_mon_correct : forall ar m l,
  length (Sem (Poly_mon ar m) l) = peval_mon m (map (@length _) l).
Proof.
  intros ar [a xl] l; simpl.
  rewrite Mult_correct; simpl.
  rewrite Nat_correct, Multl_correct; unfold peval_mon; simpl.
(* Goal: @eq nat (plusl (@map Cobham nat (fun e : Cobham => @length bool (Sem e l)) (@map mon Cobham (Poly_mon ar) ml))) (plusl (@map mon nat (fun m : mon => peval_mon m (@map (list bool) nat (@length bool) l)) ml)) *)
  rewrite map_map.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  induction xl; simpl; trivial.
(* Goal: @eq nat (Init.Nat.mul a (Init.Nat.mul (@length bool (Sem (Poly_pow ar a0) l)) (multl (@map pow nat (fun x : pow => @length bool (Sem (Poly_pow ar x) l)) xl)))) (Init.Nat.mul a (Init.Nat.mul (peval_pow a0 (@map (list bool) nat (@length bool) l)) (multl (@map pow nat (fun x : pow => peval_pow x (@map (list bool) nat (@length bool) l)) xl)))) *)
  rewrite Poly_pow_correct.
(* Goal: @eq nat (Init.Nat.mul a (Init.Nat.mul (peval_pow a0 (@map (list bool) nat (@length bool) l)) (multl (@map pow nat (fun x : pow => @length bool (Sem (Poly_pow ar x) l)) xl)))) (Init.Nat.mul a (Init.Nat.mul (peval_pow a0 (@map (list bool) nat (@length bool) l)) (multl (@map pow nat (fun x : pow => peval_pow x (@map (list bool) nat (@length bool) l)) xl)))) *)
  unfold peval_pow in *.
(* Goal: @eq nat (Init.Nat.mul a (Init.Nat.mul (power (@nth nat (@fst nat nat a0) (@map (list bool) nat (@length bool) l) O) (@snd nat nat a0)) (multl (@map pow nat (fun x : pow => @length bool (Sem (Poly_pow ar x) l)) xl)))) (Init.Nat.mul a (Init.Nat.mul (power (@nth nat (@fst nat nat a0) (@map (list bool) nat (@length bool) l) O) (@snd nat nat a0)) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@map (list bool) nat (@length bool) l) O) (@snd nat nat x)) xl)))) *)
  rewrite (@map_nth _ _ (@length _) l nil).
(* Goal: @eq nat (Init.Nat.mul a (Init.Nat.mul (power (@length bool (@nth (list bool) (@fst nat nat a0) l (@nil bool))) (@snd nat nat a0)) (multl (@map pow nat (fun x : pow => @length bool (Sem (Poly_pow ar x) l)) xl)))) (Init.Nat.mul a (Init.Nat.mul (power (@length bool (@nth (list bool) (@fst nat nat a0) l (@nil bool))) (@snd nat nat a0)) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@map (list bool) nat (@length bool) l) O) (@snd nat nat x)) xl)))) *)
  ring [IHxl].
Qed.

Opaque Poly_mon.

Definition Poly (p : pol) : Cobham :=
  Plusl_e (fst p) (map (Poly_mon (fst p)) (snd p)).

Lemma arity_Poly : forall p,
  pWF p ->
  arity (Poly p) = ok_arity (parity p).
Proof.
(* Goal: forall (p : pol) (_ : pWF p), @eq Arity (arity (Poly p)) (ok_arity (@fst nat (list mon) p)) *)
  unfold pWF, pWF', pWF_mon, pWF_pow; intros [ar ml] H.
(* Goal: @eq Arity (arity (Poly (@pair nat (list mon) ar ml))) (ok_arity (@fst nat (list mon) (@pair nat (list mon) ar ml))) *)
  unfold Poly.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  rewrite arity_Plusl; trivial.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  induction ml; simpl in *; trivial.
(* Goal: and (rec_bounded e') (and (rec_bounded (Multl_e ar el')) True) *)
  split; try tauto.
(* Goal: and (rec_bounded e') (and (rec_bounded (Multl_e ar el')) True) *)
  apply arity_Poly_mon; tauto.
Qed.

Lemma rec_bounded_Poly : forall p,
  rec_bounded (Poly p).
Proof.
intros [ar ml]; unfold Poly; simpl.
(* Goal: rec_bounded (Plusl_e ar (@map mon Cobham (Poly_mon ar) ml)) *)
apply rec_bounded_Plusl.
(* Goal: @andl Cobham rec_bounded (@map mon Cobham (Poly_mon ar) ml) *)
rewrite <- forall_andl; intros e He.
(* Goal: rec_bounded e *)
rewrite in_map_iff in He.
(* Goal: rec_bounded e *)
destruct He as [m [He _] ]; subst.
(* Goal: rec_bounded (Poly_mon ar m) *)
apply rec_bounded_Poly_mon.
Qed.

Lemma Poly_correct : forall p l,
  length (Sem (Poly p) l) = peval p (map (@length _) l).
Proof.
  unfold Poly; intros [ar ml] l; simpl.
  rewrite Plusl_correct; unfold peval; simpl.
(* Goal: @eq nat (plusl (@map Cobham nat (fun e : Cobham => @length bool (Sem e l)) (@map mon Cobham (Poly_mon ar) ml))) (plusl (@map mon nat (fun m : mon => peval_mon m (@map (list bool) nat (@length bool) l)) ml)) *)
  rewrite map_map.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  induction ml; simpl; trivial.
(* Goal: @eq nat (Init.Nat.add (@length bool (Sem (Poly_mon ar a) l)) (plusl (@map mon nat (fun x : mon => @length bool (Sem (Poly_mon ar x) l)) ml))) (Init.Nat.add (peval_mon a (@map (list bool) nat (@length bool) l)) (plusl (@map mon nat (fun m : mon => peval_mon m (@map (list bool) nat (@length bool) l)) ml))) *)
  rewrite Poly_mon_correct.
(* Goal: @eq nat (Init.Nat.add (peval_mon a (@map (list bool) nat (@length bool) l)) (plusl (@map mon nat (fun x : mon => @length bool (Sem (Poly_mon ar x) l)) ml))) (Init.Nat.add (peval_mon a (@map (list bool) nat (@length bool) l)) (plusl (@map mon nat (fun m : mon => peval_mon m (@map (list bool) nat (@length bool) l)) ml))) *)
  unfold peval_mon in *.
(* Goal: @eq Arity (arity Mult_e) (ok_arity (S (S O))) *)
  rewrite IHml; trivial.
Qed.

Opaque Poly.
