Require Import Bool Arith Euclid List.
Require Import BellantoniCook.Lib BellantoniCook.Bitstring BellantoniCook.BC BellantoniCook.BCLib.

Fixpoint unary_preserv (e : BC) : bool :=
  match e with
    | zero => true
    | proj n s j => true
    | succ b => b
    | pred => true
    | cond => true
    | rec g h0 h1 => unary_preserv g  &&
                     unary_preserv h0 && 
                     unary_preserv h1 
    | comp _ _ h nl sl => unary_preserv h && 
                          forallb unary_preserv nl &&
                          forallb unary_preserv sl
  end.

 Lemma preservation : forall (e : BC) (vnl vsl : list bs),
  unary_preserv e = true ->
  forallb unary vnl = true ->
  forallb unary vsl = true ->
  unary (sem e vnl vsl) = true.
Proof.
(* Goal: forall (e : BC) (vnl vsl : list (list bool)) (_ : @eq bool (unary_preserv e) true) (_ : @eq bool (@forallb (list bool) unary vnl) true) (_ : @eq bool (@forallb (list bool) unary vsl) true), @eq bool (unary (sem e vnl vsl)) true *)
 induction e using BC_ind2; simpl; intros; trivial.

(* Goal: @eq bool (unary (if match n with | O => false | S m' => Nat.leb i m' end then @nth (list bool) i vnl (@nil bool) else @nth (list bool) (Init.Nat.sub i n) vsl (@nil bool))) true *)
(* Goal: @eq bool (andb (@id bool b) (unary (@hd (list bool) (@nil bool) vsl))) true *)
(* Goal: @eq bool (unary (@tl bool (@hd (list bool) (@nil bool) vsl))) true *)
(* Goal: @eq bool (unary match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 case n; simpl.
(* Goal: @eq bool (unary (@nth (list bool) (Init.Nat.sub i O) vsl (@nil bool))) true *)
(* Goal: forall n : nat, @eq bool (unary (if Nat.leb i n then @nth (list bool) i vnl (@nil bool) else @nth (list bool) (Init.Nat.sub i (S n)) vsl (@nil bool))) true *)
(* Goal: @eq bool (andb (@id bool b) (unary (@hd (list bool) (@nil bool) vsl))) true *)
(* Goal: @eq bool (unary (@tl bool (@hd (list bool) (@nil bool) vsl))) true *)
(* Goal: @eq bool (unary match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 apply forallb_nth; simpl; trivial.
(* Goal: @eq bool (unary (@nth (list bool) (Init.Nat.sub i O) vsl (@nil bool))) true *)
(* Goal: forall n : nat, @eq bool (unary (if Nat.leb i n then @nth (list bool) i vnl (@nil bool) else @nth (list bool) (Init.Nat.sub i (S n)) vsl (@nil bool))) true *)
(* Goal: @eq bool (andb (@id bool b) (unary (@hd (list bool) (@nil bool) vsl))) true *)
(* Goal: @eq bool (unary (@tl bool (@hd (list bool) (@nil bool) vsl))) true *)
(* Goal: @eq bool (unary match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 intros; case (leb i n0); apply forallb_nth; simpl; trivial.

(* Goal: @eq bool (andb (@id bool b) (unary (@hd (list bool) (@nil bool) vsl))) true *)
(* Goal: @eq bool (unary (@tl bool (@hd (list bool) (@nil bool) vsl))) true *)
(* Goal: @eq bool (unary match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 subst; simpl; apply forallb_hd; simpl; trivial.

(* Goal: @eq bool (@forallb (list bool) unary (@tl (list bool) vnl)) true *)
(* Goal: @eq bool (andb (unary (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl)) (@forallb (list bool) unary vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 apply forallb_tl; trivial.
(* Goal: @eq bool (@forallb bool (@id bool) (@hd (list bool) (@nil bool) vsl)) true *)
(* Goal: @eq bool (unary match vsl with | nil => @nil bool | cons a (nil as l) => @nil bool | cons a (cons b (nil as l0) as l) => match a with | nil => b | cons b0 l1 => @nil bool end | cons a (cons b (cons c (nil as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l2 => c | cons (false as b0) l2 => @nil bool end | cons a (cons b (cons c (cons d l2 as l1) as l0) as l) => match a with | nil => b | cons (true as b0) l3 => c | cons (false as b0) l3 => d end end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 apply forallb_hd; simpl; trivial.

(* Goal: @eq bool (unary match vsl with | nil => match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => @nil bool end | cons d l2 => match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => d end end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 destruct vsl; simpl; trivial.
(* Goal: @eq bool (unary match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => @nil bool end) true *)
(* Goal: @eq bool (unary match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => l2 end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 simpl in H1;rewrite andb_true_iff in H1.
(* Goal: @eq bool (unary match vsl with | nil => match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => @nil bool end | cons d l2 => match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => d end end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 destruct vsl; simpl; trivial.
(* Goal: @eq bool (unary match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => @nil bool end) true *)
(* Goal: @eq bool (unary match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => l2 end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 simpl in H1;rewrite andb_true_iff in H1.
(* Goal: @eq bool (unary match vsl with | nil => match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => @nil bool end | cons d l2 => match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => d end end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 destruct vsl; simpl; trivial.
(* Goal: @eq bool (unary match l with | nil => l0 | cons b l => @nil bool end) true *)
(* Goal: @eq bool (unary match vsl with | nil => match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => @nil bool end | cons d l2 => match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => d end end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 case l; trivial; tauto.
(* Goal: @eq bool (unary match vsl with | nil => match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => @nil bool end | cons d l2 => match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => d end end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 destruct vsl; simpl; trivial.
(* Goal: @eq bool (unary match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => @nil bool end) true *)
(* Goal: @eq bool (unary match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => l2 end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 simpl in H1;rewrite andb_true_iff in H1.
(* Goal: @eq bool (unary match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => @nil bool end) true *)
(* Goal: @eq bool (unary match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => l2 end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 case l; trivial; intros.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 tauto.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 case b; tauto.
(* Goal: @eq bool (unary match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => l2 end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 simpl in H1;rewrite andb_true_iff,andb_true_iff in H1.
(* Goal: @eq bool (unary match l with | nil => l0 | cons (true as b) l => l1 | cons (false as b) l => l2 end) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 case l; trivial; try tauto; intros.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 case b; tauto.

(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 repeat rewrite andb_true_iff in H.  
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 assert (unary (hd nil vnl) = true).
(* Goal: @eq bool (unary (@hd (list bool) (@nil bool) vnl)) true *)
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 apply forallb_hd; trivial.
(* Goal: @eq bool (unary (sem_rec (sem e1) (sem e2) (sem e3) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 induction (hd nil vnl); simpl in *; intros.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 apply IHe1; [ tauto | apply forallb_tl | ];  trivial.
(* Goal: @eq bool (unary (if a then sem e3 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl) vsl) else sem e2 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl) vsl))) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 case a.
(* Goal: @eq bool (unary (sem e2 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl) vsl))) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 rewrite andb_true_iff in H2.
(* Goal: @eq bool (unary (sem e3 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl) vsl))) true *)
(* Goal: @eq bool (unary (sem e2 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl) vsl))) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 apply IHe3; [ tauto | | ]; simpl.
(* Goal: @eq bool (andb (unary l) (@forallb (list bool) unary (@tl (list bool) vnl))) true *)
(* Goal: @eq bool (andb (unary (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl)) (@forallb (list bool) unary vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 rewrite andb_true_iff; split; [tauto | ].
(* Goal: @eq bool (@forallb (list bool) unary (@tl (list bool) vnl)) true *)
(* Goal: @eq bool (andb (unary (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl)) (@forallb (list bool) unary vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 apply forallb_tl; trivial.
(* Goal: @eq bool (andb (unary (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl)) (@forallb (list bool) unary vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 rewrite andb_true_iff; split.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 apply IHl; tauto.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 trivial.
(* Goal: @eq bool (unary (sem e2 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl) vsl))) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 rewrite andb_true_iff in H2.
(* Goal: @eq bool (unary (sem e2 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl) vsl))) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 apply IHe2; [ tauto | | ]; simpl.
(* Goal: @eq bool (andb (unary l) (@forallb (list bool) unary (@tl (list bool) vnl))) true *)
(* Goal: @eq bool (andb (unary (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl)) (@forallb (list bool) unary vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 rewrite andb_true_iff; split; [tauto | ].
(* Goal: @eq bool (@forallb (list bool) unary (@tl (list bool) vnl)) true *)
(* Goal: @eq bool (andb (unary (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl)) (@forallb (list bool) unary vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 apply forallb_tl; trivial.
(* Goal: @eq bool (andb (unary (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl)) (@forallb (list bool) unary vsl)) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 rewrite andb_true_iff; split.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 apply IHl; tauto.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 trivial.

(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 repeat rewrite andb_true_iff in H1.
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
 apply IHe; [ tauto | | ].
(* Goal: @eq bool (@forallb (list bool) unary (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl)) true *)
 apply forallb_map; auto; intros.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 apply H; trivial.
(* Goal: @eq bool (unary_preserv x) true *)
(* Goal: @eq bool (@forallb (list bool) unary (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl)) true *)
 rewrite forallb_forall in H1.
(* Goal: @eq bool (unary_preserv x) true *)
 decompose [and] H1.
(* Goal: @eq bool (unary_preserv x) true *)
 auto.
(* Goal: @eq bool (@forallb (list bool) unary (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl)) true *)
 apply forallb_map; auto; intros.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 apply H0; trivial.
(* Goal: @eq bool (unary_preserv x) true *)
 decompose [and] H1.
(* Goal: @eq bool (unary_preserv x) true *)
 rewrite forallb_forall in H6.
(* Goal: @eq bool (unary_preserv x) true *)
 auto.
Qed.

(** * Zero

  - with any arities (n, s)
*)

Lemma zero_correct n s l1 l2: 
 length (sem (zero_e n s) l1 l2) = 0.
Proof.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 intros; simpl; trivial.
Qed.

(** * One

  - with any arities (n, s)
*)

Definition one_e (n s:nat) : BC :=
  comp n s (comp 0 0 (succ true) nil (zero :: nil)) nil nil.

Lemma one_correct n s l1 l2: 
 length (sem (one_e n s) l1 l2) = 1.
Proof.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 intros; simpl; trivial.
Qed.

(** * Successor

  - arities: (1, 0)
*)

Definition succ_e : BC := succ true.

Lemma succ_correct :
  forall n, length (sem succ_e nil [n]) = S (length n).
Proof.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 intros; simpl; trivial.
Qed.

(** * Conversion from [nat] to [BC]

  - with any arities (n, s)
*)

Fixpoint nat2BC (n s x:nat) : BC :=
  match x with
    | 0 => zero_e n s
    | S x' => comp n s succ_e nil [nat2BC n s x']
  end.

Lemma nat2BC_arities : forall n s x, arities (nat2BC n s x) = ok_arities n s.
Proof.
(* Goal: forall (n s x : nat) (nl sl : list (list bool)), @eq nat (@length bool (sem (nat2BC n s x) nl sl)) x *)
induction x as [ | x IH].
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
(* Goal: @eq nat (@length bool (sem (nat2BC n s (S x)) nl sl)) (S x) *)
simpl nat2BC.
(* Goal: @eq Arities (arities (comp n O plus_e (@cons BC e' (@nil BC)) (@cons BC (plusl_e n el') (@nil BC)))) (ok_arities n O) *)
rewrite comp_arities.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
simpl; trivial.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
simpl; tauto.
Qed.

Lemma nat2BC_correct :
  forall n s x nl sl, length (sem (nat2BC n s x) nl sl) = x.
Proof.
(* Goal: forall (n s x : nat) (nl sl : list (list bool)), @eq nat (@length bool (sem (nat2BC n s x) nl sl)) x *)
induction x as [ | x IH].
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
(* Goal: forall nl sl : list (list bool), @eq nat (@length bool (sem (nat2BC n s (S x)) nl sl)) (S x) *)
intros nl sl.
(* Goal: @eq nat (@length bool (sem (nat2BC n s (S x)) nl sl)) (S x) *)
simpl nat2BC.
(* Goal: @eq nat (@length bool (sem (comp n s succ_e (@nil BC) (@cons BC (nat2BC n s x) (@nil BC))) nl sl)) (S x) *)
rewrite sem_comp.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
simpl.
(* Goal: @eq nat (S (@length bool (sem (nat2BC n s x) nl sl))) (S x) *)
rewrite IH.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
Qed.

Opaque succ_e.

(** * Addition

  - arities: (1,1)
*)

Definition plus_e : BC :=
  rec (proj 0 1 0)
      (comp 1 2 succ_e nil ((proj 1 2 1) :: nil))
      (comp 1 2 succ_e nil ((proj 1 2 1) :: nil)).

Lemma plus_correct :
  forall m n, length (sem plus_e [m] [n]) = length m + length n.
Proof.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  induction m; simpl in *; intros; trivial.
(* Goal: @eq bool (unary_preserv x) true *)
  case a; simpl; rewrite succ_correct; auto.
Qed.

Opaque plus_e.

Fixpoint plusl_e (n:nat)(el:list BC) : BC :=
  match el with
    | nil => zero_e n 0
    | e' :: el' => comp n 0 plus_e [e'] [plusl_e n el']
  end.

Lemma plusl_arities n el : 
  andl (fun e => arities e = ok_arities n 0) el ->
  arities (plusl_e n el) = ok_arities n 0.
Proof.
(* Goal: forall _ : @andl BC (fun e : BC => @eq Arities (arities e) (ok_arities n O)) el, @eq Arities (arities (plusl_e n el)) (ok_arities n O) *)
induction el as [ | e' el' IH].
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
(* Goal: forall _ : @andl BC (fun e : BC => @eq Arities (arities e) (ok_arities n O)) (@cons BC e' el'), @eq Arities (arities (plusl_e n (@cons BC e' el'))) (ok_arities n O) *)
intro H.
(* Goal: @eq bool (unary l) true *)
simpl in H.
(* Goal: @eq Arities (arities (plusl_e n (@cons BC e' el'))) (ok_arities n O) *)
simpl plusl_e.
(* Goal: @eq Arities (arities (comp n O plus_e (@cons BC e' (@nil BC)) (@cons BC (plusl_e n el') (@nil BC)))) (ok_arities n O) *)
rewrite comp_arities.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
simpl; tauto.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
simpl; tauto.
Qed.

Lemma plusl_correct :
  forall n nl el,
  length (sem (plusl_e n el) nl nil) = plusl (map (fun e => length (sem e nl nil)) el).
Proof.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
induction el as [ | e el IH]; simpl.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
(* Goal: @eq nat (@length bool (sem plus_e (@cons (list bool) (sem e nl (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (sem (scalar_e a n e) nl (@nil (list bool))) (@nil (list bool))))) (Init.Nat.add (@length bool (sem e nl (@nil (list bool)))) (Init.Nat.mul a (@length bool (sem e nl (@nil (list bool)))))) *)
rewrite plus_correct, IH.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
Qed.

(** * Logical or

  - arities: (1,1)
*)

Notation or_e := plus_e (only parsing).

Lemma or_correct :
  forall b1 b2, bs2bool (sem or_e [bool2bs b1] [bool2bs b2]) = b1 || b2.
Proof.
(* Goal: forall b1 b2 : bool, @eq bool (bs2bool (sem mult_e (@cons (list bool) (bool2bs b1) (@cons (list bool) (bool2bs b2) (@nil (list bool)))) (@nil (list bool)))) (andb b1 b2) *)
intros [ | ] [ | ]; reflexivity.
Qed.

(** * Multiplication

  - arities: (2,0)
*)

Definition mult_e : BC :=
  rec (zero_e 1 0)
      (comp 2 1 plus_e ((proj 2 0 1) :: nil) ((proj 2 1 2) :: nil))
      (comp 2 1 plus_e ((proj 2 0 1) :: nil) ((proj 2 1 2) :: nil)).

Lemma mult_correct :
  forall m n, length (sem mult_e [m; n] nil) = (length m) * (length n).
Proof.
(* Goal: forall m n : list bool, @eq nat (@length bool (sem mult_e (@cons (list bool) m (@cons (list bool) n (@nil (list bool)))) (@nil (list bool)))) (Init.Nat.mul (@length bool m) (@length bool n)) *)
induction m; intro n; trivial; simpl in *.
(* Goal: @eq bool (unary_preserv x) true *)
case a; rewrite plus_correct; auto.
Qed.

Opaque mult_e.

(** Logical and

  - arities: (2,0)
*)

Notation and_e := mult_e (only parsing).

Lemma and_correct :
  forall b1 b2, bs2bool 
    (sem and_e [bool2bs b1; bool2bs b2] nil) = b1 && b2.
Proof.
(* Goal: forall b1 b2 : bool, @eq bool (bs2bool (sem mult_e (@cons (list bool) (bool2bs b1) (@cons (list bool) (bool2bs b2) (@nil (list bool)))) (@nil (list bool)))) (andb b1 b2) *)
intros [ | ] [ | ]; reflexivity.
Qed.

(** * Minus (with reversed arguments)

  - arities: (1,1)
*)

Definition minus_rev_e : BC :=
  rec (proj 0 1 0)
      (comp 1 2 pred nil ((proj 1 2 1) :: nil))
      (comp 1 2 pred nil ((proj 1 2 1) :: nil)).

Lemma minus_rev_correct :
  forall m n, length (sem minus_rev_e [n] [m]) = (length m) - (length n).
Proof.
(* Goal: forall m n : list bool, @eq nat (@length bool (sem minus_rev_e (@cons (list bool) n (@nil (list bool))) (@cons (list bool) m (@nil (list bool))))) (Init.Nat.sub (@length bool m) (@length bool n)) *)
 induction n; simpl in *; [ omega | ].
(* Goal: @eq nat (@length bool (if a then @tl bool (sem_rec (fun _ vsl : list (list bool) => @nth (list bool) O vsl (@nil bool)) (fun _ vsl : list (list bool) => @tl bool (@nth (list bool) O vsl (@nil bool))) (fun _ vsl : list (list bool) => @tl bool (@nth (list bool) O vsl (@nil bool))) n (@nil (list bool)) (@cons (list bool) m (@nil (list bool)))) else @tl bool (sem_rec (fun _ vsl : list (list bool) => @nth (list bool) O vsl (@nil bool)) (fun _ vsl : list (list bool) => @tl bool (@nth (list bool) O vsl (@nil bool))) (fun _ vsl : list (list bool) => @tl bool (@nth (list bool) O vsl (@nil bool))) n (@nil (list bool)) (@cons (list bool) m (@nil (list bool)))))) (Init.Nat.sub (@length bool m) (S (@length bool n))) *)
 case a; rewrite length_tail, IHn; omega.
Qed.  

Opaque minus_rev_e.

(** * Less than predicate

  - arities: (1,1)
*)

Notation lt_e := minus_rev_e.

Lemma lt_correct v1 v2:
  bs2bool (sem lt_e [v1] [v2]) = true ->
  length v1 < length v2.
Proof.
(* Goal: forall _ : @eq bool (bs2bool (sem minus_rev_e (@cons (list bool) v1 (@nil (list bool))) (@cons (list bool) v2 (@nil (list bool))))) true, lt (@length bool v1) (@length bool v2) *)
  intros; simpl in *.
(* Goal: lt (@length bool v1) (@length bool v2) *)
  apply bs_nat2bool_true in H.
(* Goal: lt (@length bool v1) (@length bool v2) *)
  rewrite minus_rev_correct in H; omega.
Qed.

Lemma unary_tl l :
  unary l = true ->
  unary (tl l) = true.
Proof.
(* Goal: forall _ : @eq bool (unary l) true, @eq bool (unary (@tl bool l)) true *)
 intros.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 destruct l; simpl; trivial.
(* Goal: @eq bool (unary l) true *)
 simpl in H.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 rewrite andb_true_iff in H; tauto.
Qed.

Lemma lt_correct_conv_bool v1 v2:
  unary v2 = true ->
  length v1 < length v2 ->
  bs2bool (sem lt_e [v1] [v2]) = true.
Proof.
(* Goal: forall _ : @eq bool (bs2bool (sem minus_rev_e (@cons (list bool) v1 (@nil (list bool))) (@cons (list bool) v2 (@nil (list bool))))) true, lt (@length bool v1) (@length bool v2) *)
  intros; simpl in *.
  apply bs_nat2bool_true_conv.
  Transparent lt_e.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
  simpl.
  Opaque lt_e.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  induction v1; simpl; trivial.
(* Goal: @eq bool (unary (if a then sem e3 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl) vsl) else sem e2 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem e1) (sem e2) (sem e3) l (@tl (list bool) vnl) vsl) vsl))) true *)
(* Goal: @eq bool (unary (sem e (@map BC (list bool) (fun ne : BC => sem ne vnl (@nil (list bool))) rl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl))) true *)
  case a.
  apply unary_tl.
  apply IHv1.
  simpl in *; omega.
  apply unary_tl.
  apply IHv1.
  simpl in *; omega.
  rewrite minus_rev_correct.
(* Goal: lt O y *)
  omega.
Qed.

Lemma lt_correct_conv v1 v2 :
  unary v1 = true ->
  unary v2 = true ->
  bs2bool (sem lt_e [v1] [v2]) = false ->
  length v2 <= length v1.
Proof.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  intros; trivial.
(* Goal: le (@length bool v2) (@length bool v1) *)
  apply bs_nat2bool_false in H1.
(* Goal: le (@length bool v2) (@length bool v1) *)
(* Goal: @eq bool (unary (sem minus_rev_e (@cons (list bool) v1 (@nil (list bool))) (@cons (list bool) v2 (@nil (list bool))))) true *)
  rewrite minus_rev_correct in H1.
(* Goal: lt O y *)
  omega.
  apply preservation; simpl; try reflexivity;
(* Goal: @eq bool (unary_preserv x) true *)
  rewrite andb_true_iff; auto.
Qed.

Lemma lt_correct_conv_nil v1 v2 :
  unary v1 = true ->
  unary v2 = true ->
  sem lt_e [v1] [v2] = nil ->
  length v2 <= length v1.
Proof.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  intros; trivial.
(* Goal: le (@length bool v2) (@length bool v1) *)
  assert (bs2bool (sem lt_e [v1] [v2]) = false).
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  rewrite H1; simpl; trivial.
(* Goal: le (@length bool v2) (@length bool v1) *)
  apply bs_nat2bool_false in H2.
(* Goal: le (@length bool v2) (@length bool v1) *)
(* Goal: @eq bool (unary (sem minus_rev_e (@cons (list bool) v1 (@nil (list bool))) (@cons (list bool) v2 (@nil (list bool))))) true *)
  rewrite minus_rev_correct in H2.
(* Goal: lt O y *)
  omega.
  apply preservation; simpl; try reflexivity;
(* Goal: @eq bool (unary_preserv x) true *)
  rewrite andb_true_iff; auto.
Qed.

(** * Less than or equal to predicate

  - arities: (1,1)
*)

Definition le_e : BC :=
  comp 1 1 lt_e (proj 1 0 0 :: nil) (comp 1 1 succ_e nil (proj 1 1 1 :: nil) :: nil).

Lemma le_correct : forall v1 v2,
  bs2bool (sem le_e [v1] [v2]) = true ->
  length v1 <= length v2.
Proof.
(* Goal: @eq bool (unary l) true *)
  intros v1 v2 H; simpl in H.
(* Goal: le (@length bool v1) (@length bool v2) *)
  apply lt_correct in H.
(* Goal: le (@length bool v1) (@length bool v2) *)
  rewrite succ_correct in H.
(* Goal: lt O y *)
  omega.
Qed.

Lemma le_correct_conv v1 v2 :
  unary v1 = true ->
  unary v2 = true ->
  bs2bool (sem le_e [v1] [v2]) = false ->
  length v2 < length v1.
Proof.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  intros; trivial.
(* Goal: le (S (@length bool v2)) (@length bool v1) *)
  simpl in H1.
(* Goal: lt (@length bool v2) (@length bool v1) *)
  apply lt_correct_conv in H1.
(* Goal: le (S (@length bool v2)) (@length bool v1) *)
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq bool (unary (sem succ_e (@nil (list bool)) (@cons (list bool) v2 (@nil (list bool))))) true *)
  rewrite succ_correct in H1.
(* Goal: lt O y *)
  omega.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  trivial.
  apply preservation; simpl; try reflexivity;
(* Goal: @eq bool (unary_preserv x) true *)
    rewrite andb_true_iff; auto.
Qed.

Lemma le_correct_conv_nil v1 v2 :
  unary v1 = true ->
  unary v2 = true ->
  sem le_e [v1] [v2] = nil ->
  S (length v2) <= length v1.
Proof.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  intros; trivial.
(* Goal: le (S (@length bool v2)) (@length bool v1) *)
  simpl in H1.
(* Goal: le (S (@length bool v2)) (@length bool v1) *)
  apply lt_correct_conv_nil in H1.
(* Goal: le (S (@length bool v2)) (@length bool v1) *)
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq bool (unary (sem succ_e (@nil (list bool)) (@cons (list bool) v2 (@nil (list bool))))) true *)
  rewrite succ_correct in H1.
(* Goal: lt O y *)
  omega.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  trivial.
  apply preservation; simpl; try reflexivity;
(* Goal: @eq bool (unary_preserv x) true *)
  rewrite andb_true_iff; auto.
Qed.
 
Opaque le_e.

(** * Minus

  - arities: (2,0)
*)

Notation minus_e := (inv_e (from_11_to_20 minus_rev_e)) (only parsing).

Lemma minus_correct :
  forall m n, length (sem minus_e [n; m] nil) = (length n) - (length m).
Proof.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 intros; simpl; rewrite minus_rev_correct; trivial.
Qed.

(** * Maximum

  - arities: (2,0)
*)

Definition max_e : BC :=
  comp 2 0 (rec (proj 2 0 0) (proj 3 1 2) (proj 3 1 2) )
  [ P'_e; proj 2 0 0; proj 2 0 1] nil.

Lemma max_correct_l v1 v2 : length v2 <= length v1 ->
  sem max_e [v1; v2] nil = v1.
Proof.
(* Goal: forall _ : @eq bool (unary l) true, @eq bool (unary (@tl bool l)) true *)
  simpl; intros.
(* Goal: @eq (list bool) (sem_rec (fun vnl _ : list (list bool) => @nth (list bool) O vnl (@nil bool)) (fun vnl _ : list (list bool) => @nth (list bool) (S (S O)) vnl (@nil bool)) (fun vnl _ : list (list bool) => @nth (list bool) (S (S O)) vnl (@nil bool)) (sem P_e (@cons (list bool) v1 (@nil (list bool))) (@cons (list bool) v2 (@nil (list bool)))) (@cons (list bool) v1 (@cons (list bool) v2 (@nil (list bool)))) (@nil (list bool))) v2 *)
  rewrite P_correct; unfold P.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  rewrite skipn_nil; simpl; trivial.
Qed.

Lemma max_correct_r v1 v2 : length v1 < length v2 ->
  sem max_e [v1; v2] nil = v2.
Proof.
(* Goal: forall _ : @eq bool (unary l) true, @eq bool (unary (@tl bool l)) true *)
  simpl; intros.
(* Goal: @eq (list bool) (sem_rec (fun vnl _ : list (list bool) => @nth (list bool) O vnl (@nil bool)) (fun vnl _ : list (list bool) => @nth (list bool) (S (S O)) vnl (@nil bool)) (fun vnl _ : list (list bool) => @nth (list bool) (S (S O)) vnl (@nil bool)) (sem P_e (@cons (list bool) v1 (@nil (list bool))) (@cons (list bool) v2 (@nil (list bool)))) (@cons (list bool) v1 (@cons (list bool) v2 (@nil (list bool)))) (@nil (list bool))) v2 *)
  rewrite P_correct; unfold P.
(* Goal: forall _ : @eq bool (unary l) true, @eq bool (unary (@tl bool l)) true *)
  case_eq (  (skipn (length v1) v2) ); simpl; intros.
(* Goal: @eq nat (div' q' y (Init.Nat.add (Init.Nat.mul (S q') y) r)) q' *)
(* Goal: @eq nat (div' q' y (Init.Nat.add (Init.Nat.mul qu y) r)) q' *)
  contradict H.
(* Goal: not (lt (S q') qu) *)
  apply le_not_lt.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  apply skipn_nil_length; trivial.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  case b; trivial.
Qed.

(** * Euclidean division

  - arities: (2,0)
*)

Fixpoint div' (q y:nat)(x:nat) : nat :=
  match q with
  | 0 => 0
  | S q' => if leb (q' * y) x then q' else div' q' y x
  end.

Lemma div'_coq_correct : forall (q x y : nat) (Hy:y>0),
  (q > proj1_sig (quotient y Hy x) -> 
    div' q y x = proj1_sig (quotient y Hy x)) /\
  (q <= proj1_sig (quotient y Hy x) -> 
    div' q y x = Peano.pred q).
Proof.
(* Goal: forall (q x y : nat) (Hy : gt y O), and (forall _ : gt q (@proj1_sig nat (fun q0 : nat => @ex nat (fun r : nat => and (@eq nat x (Init.Nat.add (Init.Nat.mul q0 y) r)) (gt y r))) (quotient y Hy x)), @eq nat (div' q y x) (@proj1_sig nat (fun q0 : nat => @ex nat (fun r : nat => and (@eq nat x (Init.Nat.add (Init.Nat.mul q0 y) r)) (gt y r))) (quotient y Hy x))) (forall _ : le q (@proj1_sig nat (fun q0 : nat => @ex nat (fun r : nat => and (@eq nat x (Init.Nat.add (Init.Nat.mul q0 y) r)) (gt y r))) (quotient y Hy x)), @eq nat (div' q y x) (Init.Nat.pred q)) *)
intros q x y Hy.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
destruct (quotient y Hy x) as (qu & r & H1 & H2); simpl.
(* Goal: and (forall _ : gt q qu, @eq nat (div' q y x) qu) (forall _ : le q qu, @eq nat (div' q y x) (Init.Nat.pred q)) *)
induction q as [ | q' IH]; simpl; [ omega | ].
(* Goal: forall _ : @andl BC (fun e : BC => @eq Arities (arities e) (ok_arities n O)) (@cons BC e' el'), @eq Arities (arities (plusl_e n (@cons BC e' el'))) (ok_arities n O) *)
case_eq (leb (q' * y) x); intro H.
(* Goal: and (forall _ : gt (S q') qu, @eq nat q' qu) (forall _ : le (S q') qu, @eq nat q' q') *)
(* Goal: and (forall _ : gt (S q') qu, @eq nat (div' q' y x) qu) (forall _ : le (S q') qu, @eq nat (div' q' y x) q') *)
clear IH.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
apply leb_complete in H; split; subst x; intros; trivial.
(* Goal: @eq nat q' qu *)
(* Goal: and (forall _ : gt (S q') qu, @eq nat (div' q' y x) qu) (forall _ : le (S q') qu, @eq nat (div' q' y x) q') *)
assert (qu <= q') as H1 by omega; clear H0.
(* Goal: @eq nat q' qu *)
(* Goal: and (forall _ : gt (S q') qu, @eq nat (div' q' y x) qu) (forall _ : le (S q') qu, @eq nat (div' q' y x) q') *)
apply le_lt_or_eq in H1.
(* Goal: @eq bool (unary_preserv x) true *)
destruct H1; auto.
(* Goal: @eq nat (div' q' y (Init.Nat.add (Init.Nat.mul (S q') y) r)) q' *)
(* Goal: @eq nat (div' q' y (Init.Nat.add (Init.Nat.mul qu y) r)) q' *)
contradict H.
(* Goal: not (le (Init.Nat.mul q' y) (Init.Nat.add (Init.Nat.mul qu y) r)) *)
(* Goal: and (forall _ : gt (S q') qu, @eq nat (div' q' y x) qu) (forall _ : le (S q') qu, @eq nat (div' q' y x) q') *)
apply lt_not_le.
(* Goal: lt (Init.Nat.add (Init.Nat.mul qu y) r) (Init.Nat.mul q' y) *)
(* Goal: and (forall _ : gt (S q') qu, @eq nat (div' q' y x) qu) (forall _ : le (S q') qu, @eq nat (div' q' y x) q') *)
apply lt_le_trans with (qu * y + y); [ omega | ].
(* Goal: le (Init.Nat.add (Init.Nat.mul qu y) y) (Init.Nat.mul q' y) *)
(* Goal: and (forall _ : gt (S q') qu, @eq nat (div' q' y x) qu) (forall _ : le (S q') qu, @eq nat (div' q' y x) q') *)
rewrite <- mult_succ_l.
(* Goal: lt O y *)
apply mult_le_compat_r; omega.
(* Goal: and (forall _ : gt (S q') qu, @eq nat (div' q' y x) qu) (forall _ : le (S q') qu, @eq nat (div' q' y x) q') *)
apply leb_complete_conv in H; split; intros; subst.
(* Goal: lt O y *)
assert (q'=qu \/ q'>qu) as [H3 | H3]; subst; omega.
(* Goal: @eq nat (div' q' y (Init.Nat.add (Init.Nat.mul qu y) r)) q' *)
assert (S q' = qu \/ S q' < qu) as [H4 | H4] by omega; subst.
(* Goal: @eq nat (div' q' y (Init.Nat.add (Init.Nat.mul (S q') y) r)) q' *)
(* Goal: @eq nat (div' q' y (Init.Nat.add (Init.Nat.mul qu y) r)) q' *)
contradict H.
(* Goal: lt O y *)
apply le_not_lt; simpl; omega.
(* Goal: @eq nat (div' q' y (Init.Nat.add (Init.Nat.mul qu y) r)) q' *)
contradict H4.
(* Goal: not (lt (S q') qu) *)
apply le_not_lt.
(* Goal: le qu (S q') *)
apply mult_S_le_reg_l with (Peano.pred y).
(* Goal: le (Init.Nat.mul (S (Init.Nat.pred y)) qu) (Init.Nat.mul (S (Init.Nat.pred y)) (S q')) *)
rewrite <- S_pred with (m:=0), mult_comm, (mult_comm y (S q')).
(* Goal: lt O y *)
simpl; omega.
(* Goal: lt O y *)
omega.
Qed.

Definition div (x y:nat) : nat := div' (S x) y x.

Lemma div_coq_correct : forall (x y:nat) (Hy:y>0),
  div x y = proj1_sig (quotient y Hy x).
Proof.
(* Goal: forall (x y : nat) (Hy : gt y O), @eq nat (div x y) (@proj1_sig nat (fun q : nat => @ex nat (fun r : nat => and (@eq nat x (Init.Nat.add (Init.Nat.mul q y) r)) (gt y r))) (quotient y Hy x)) *)
unfold div; intros x y Hy.
(* Goal: @eq nat (div' (S x) y x) (@proj1_sig nat (fun q : nat => @ex nat (fun r : nat => and (@eq nat x (Init.Nat.add (Init.Nat.mul q y) r)) (gt y r))) (quotient y Hy x)) *)
generalize (div'_coq_correct (S x) x y Hy).
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
destruct (quotient y Hy x) as (q & r & H1 & H2); simpl.
(* Goal: forall _ : and (forall _ : gt (S x) q, @eq nat (if Nat.leb (Init.Nat.mul x y) x then x else div' x y x) q) (forall _ : le (S x) q, @eq nat (if Nat.leb (Init.Nat.mul x y) x then x else div' x y x) x), @eq nat (if Nat.leb (Init.Nat.mul x y) x then x else div' x y x) q *)
intros [H3 _].
(* Goal: @eq nat (if Nat.leb (Init.Nat.mul x y) x then x else div' x y x) q *)
apply H3; subst x.
(* Goal: gt (S (Init.Nat.add (Init.Nat.mul q y) r)) q *)
apply le_gt_S.
(* Goal: le q (Init.Nat.add (Init.Nat.mul q y) r) *)
apply le_trans with (q*y); [ | omega ].
(* Goal: le q (Init.Nat.mul q y) *)
rewrite <- (mult_1_r q) at 1.
(* Goal: lt O y *)
apply mult_le_compat_l; omega.
Qed.

Definition div'_e : BC :=
  rec (zero_e 1 1)
  (comp 2 2 cond nil
    [comp 2 2 le_e [comp 2 0 mult_e [proj 2 0 0; proj 2 0 1] nil]
      [proj 2 2 3]; proj 2 2 2; proj 2 2 0; proj 2 2 2])
  (comp 2 2 cond nil
    [comp 2 2 le_e [comp 2 0 mult_e [proj 2 0 0; proj 2 0 1] nil]
      [proj 2 2 3]; proj 2 2 2; proj 2 2 0; proj 2 2 2]).

Lemma hd_cons l a l' :
  l = a :: l' ->
  bs2bool l = a.
Proof.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  intros; subst; trivial.
Qed.

Ltac elim_if :=  match goal with 
   | |- context [if ?c then ?c1 else ?c2]  => case_eq c
 end.

Lemma div'_correct v1 v2 v3 :
  unary v1 = true -> unary v2 = true -> unary v3 = true ->
  length (sem div'_e [v1;v2] [v3]) = 
  div' (length v1) (length v2) (length v3).
Proof.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 intros; induction v1; simpl in *; intros; trivial.
(* Goal: @eq nat (@length bool (if a then match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) v1 (@cons (list bool) v2 (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))) with | nil => sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))) | cons (true as b) l => v1 | cons (false as b) l => sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b0) l0 => @nth (list bool) O vnl (@nil bool) | cons (false as b0) l0 => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b0) l0 => @nth (list bool) O vnl (@nil bool) | cons (false as b0) l0 => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))) end else match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) v1 (@cons (list bool) v2 (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))) with | nil => sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))) | cons (true as b) l => v1 | cons (false as b) l => sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b0) l0 => @nth (list bool) O vnl (@nil bool) | cons (false as b0) l0 => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b0) l0 => @nth (list bool) O vnl (@nil bool) | cons (false as b0) l0 => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))) end)) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 rewrite andb_true_iff in H.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
 case a; simpl.
(* Goal: forall _ : @eq bool (unary l) true, @eq bool (unary (@tl bool l)) true *)
 case_eq ( sem le_e [sem mult_e [v1; v2] nil] [v3] ); intros.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 rewrite IHv1; trivial.
(* Goal: @eq nat (div' (@length bool v1) (@length bool v2) (@length bool v3)) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 apply le_correct_conv_nil in H2.
(* Goal: @eq nat (@length bool v1) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
(* Goal: @eq nat (@length bool (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 rewrite mult_correct in H2.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 rewrite leb_correct_conv; trivial.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
 apply preservation; trivial; simpl.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 repeat rewrite andb_true_iff; tauto.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 trivial.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 tauto. 
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 apply hd_cons in H2.
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 destruct b.
(* Goal: @eq nat (@length bool v1) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
(* Goal: @eq nat (@length bool (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 apply le_correct in H2.
(* Goal: @eq nat (@length bool v1) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
(* Goal: @eq nat (@length bool (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 rewrite mult_correct in H2.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 rewrite leb_correct; trivial.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 apply le_correct_conv in H2; trivial.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 simpl in IHv1; rewrite IHv1; clear IHv1; try tauto.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 rewrite leb_correct_conv; trivial.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 rewrite mult_correct in H2; trivial.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
 apply preservation; trivial; simpl.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 do 2 rewrite andb_true_iff; tauto.
(* Goal: forall _ : @eq bool (unary l) true, @eq bool (unary (@tl bool l)) true *)
 case_eq ( sem le_e [sem mult_e [v1; v2] nil] [v3] ); intros.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 rewrite IHv1; trivial.
(* Goal: @eq nat (div' (@length bool v1) (@length bool v2) (@length bool v3)) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 apply le_correct_conv_nil in H2.
(* Goal: @eq nat (@length bool v1) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
(* Goal: @eq nat (@length bool (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 rewrite mult_correct in H2.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 rewrite leb_correct_conv; trivial.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
 apply preservation; trivial; simpl.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 repeat rewrite andb_true_iff; tauto.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 trivial.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 tauto. 
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 apply hd_cons in H2.
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 destruct b.
(* Goal: @eq nat (@length bool v1) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
(* Goal: @eq nat (@length bool (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 apply le_correct in H2.
(* Goal: @eq nat (@length bool v1) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
(* Goal: @eq nat (@length bool (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 rewrite mult_correct in H2.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 rewrite leb_correct; trivial.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 apply le_correct_conv in H2; trivial.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 simpl in IHv1; rewrite IHv1; clear IHv1; try tauto.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 rewrite leb_correct_conv; trivial.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
 rewrite mult_correct in H2; trivial.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
 apply preservation; trivial; simpl.
(* Goal: @eq bool (unary v1) true *)
(* Goal: @eq nat (@length bool (if b then v1 else sem_rec (fun _ _ : list (list bool) => @nil bool) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) (fun vnl vsl : list (list bool) => match sem le_e (@cons (list bool) (sem mult_e (@cons (list bool) (@nth (list bool) O vnl (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) vnl (@nil bool)) (@nil (list bool)))) (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (@nth (list bool) (S O) vsl (@nil bool)) (@nil (list bool))) with | nil => @nth (list bool) O vsl (@nil bool) | cons (true as b) l => @nth (list bool) O vnl (@nil bool) | cons (false as b) l => @nth (list bool) O vsl (@nil bool) end) v1 (@cons (list bool) v2 (@nil (list bool))) (@cons (list bool) v3 (@nil (list bool))))) (if Nat.leb (Init.Nat.mul (@length bool v1) (@length bool v2)) (@length bool v3) then @length bool v1 else div' (@length bool v1) (@length bool v2) (@length bool v3)) *)
 do 2 rewrite andb_true_iff; tauto.
Qed.

Opaque div'_e.

Definition div_e : BC :=
  comp 2 0 div'_e [comp 2 0 succ_e nil [proj 2 0 0]; proj 2 0 1] [proj 2 0 0].

Lemma div_correct v1 v2 :
  unary v1 = true -> unary v2 = true -> 
  length (sem div_e [v1; v2] nil) = div (length v1) (length v2).
Proof.
(* Goal: forall (_ : @eq bool (unary v1) true) (_ : @eq bool (unary v2) true), @eq nat (@length bool (sem div_e (@cons (list bool) v1 (@cons (list bool) v2 (@nil (list bool)))) (@nil (list bool)))) (div (@length bool v1) (@length bool v2)) *)
  intros; simpl sem.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
  rewrite div'_correct; trivial.
Qed.

(** * Multiplication by a constant

  - with any arities: (n,0)
*)

Fixpoint scalar_e (a:nat)(n:nat)(e:BC) : BC :=
  match a with
  | 0 => zero_e n 0
  | S a' => comp n 0 plus_e [e] [scalar_e a' n e]
  end.

Lemma scalar_arities :
  forall a n e,
  arities e = ok_arities n 0 ->
  arities (scalar_e a n e) = ok_arities n 0.
Proof.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
induction a as [ | a IH]; simpl.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
(* Goal: forall (n : nat) (e : BC) (_ : @eq Arities (arities e) (ok_arities n O)), @eq Arities match arities plus_e with | error_rec a0 a1 a2 => error_comp (error_rec a0 a1 a2) (@cons Arities (arities e) (@nil Arities)) (@cons Arities (arities (scalar_e a n e)) (@nil Arities)) | error_comp a0 l l0 => error_comp (error_comp a0 l l0) (@cons Arities (arities e) (@nil Arities)) (@cons Arities (arities (scalar_e a n e)) (@nil Arities)) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (arities e) (@nil Arities)) (@cons Arities (arities (scalar_e a n e)) (@nil Arities)) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S O)) (Nat.eqb hs (S O))) (andb (aeq (arities e) (ok_arities n O)) true)) (andb (aeq (arities (scalar_e a n e)) (ok_arities n O)) true) then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (arities e) (@nil Arities)) (@cons Arities (arities (scalar_e a n e)) (@nil Arities)) end (ok_arities n O) *)
intros n e H.
(* Goal: @eq Arities match arities plus_e with | error_rec a0 a1 a2 => error_comp (error_rec a0 a1 a2) (@cons Arities (arities e) (@nil Arities)) (@cons Arities (arities (scalar_e a n e)) (@nil Arities)) | error_comp a0 l l0 => error_comp (error_comp a0 l l0) (@cons Arities (arities e) (@nil Arities)) (@cons Arities (arities (scalar_e a n e)) (@nil Arities)) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (arities e) (@nil Arities)) (@cons Arities (arities (scalar_e a n e)) (@nil Arities)) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S O)) (Nat.eqb hs (S O))) (andb (aeq (arities e) (ok_arities n O)) true)) (andb (aeq (arities (scalar_e a n e)) (ok_arities n O)) true) then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (arities e) (@nil Arities)) (@cons Arities (arities (scalar_e a n e)) (@nil Arities)) end (ok_arities n O) *)
rewrite H, (IH _ _ H).
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
simpl.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (andb (Nat.eqb n n) true) (andb (andb (Nat.eqb n n) true) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
rewrite <- beq_nat_refl.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
Qed.

Opaque plus_e.

Lemma scalar_correct :
  forall a n nl e,
  length (sem (scalar_e a n e) nl nil) = a * length (sem e nl nil).
Proof.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
induction a as [ | a IH]; simpl.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
(* Goal: forall (n : nat) (nl : list (list bool)) (e : BC), @eq nat (@length bool (sem plus_e (@cons (list bool) (sem e nl (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (sem (scalar_e a n e) nl (@nil (list bool))) (@nil (list bool))))) (Init.Nat.add (@length bool (sem e nl (@nil (list bool)))) (Init.Nat.mul a (@length bool (sem e nl (@nil (list bool)))))) *)
intros n nl e.
(* Goal: @eq nat (@length bool (sem plus_e (@cons (list bool) (sem e nl (@nil (list bool))) (@nil (list bool))) (@cons (list bool) (sem (scalar_e a n e) nl (@nil (list bool))) (@nil (list bool))))) (Init.Nat.add (@length bool (sem e nl (@nil (list bool)))) (Init.Nat.mul a (@length bool (sem e nl (@nil (list bool)))))) *)
rewrite plus_correct, IH.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
Qed.

(** * Multiplication of a list of expressions

  - with any arities: (n,0)
*)

Fixpoint multl_e (n:nat)(el:list BC) : BC :=
  match el with
    | nil => one_e n 0
    | e' :: el' => comp n 0 mult_e [e'; multl_e n el'] nil
  end.

Lemma multl_arities :
  forall el n,
  andl (fun e => arities e = ok_arities n 0) el ->
  arities (multl_e n el) = ok_arities n 0.
Proof.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
induction el as [ | e el IH]; simpl.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
(* Goal: forall (n : nat) (_ : and (@eq Arities (arities e) (ok_arities n O)) (@andl BC (fun e : BC => @eq Arities (arities e) (ok_arities n O)) el)), @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (arities e) (@cons Arities (arities (multl_e n el)) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (arities e) (@cons Arities (arities (multl_e n el)) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (arities e) (@cons Arities (arities (multl_e n el)) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (arities e) (ok_arities n O)) (andb (aeq (arities (multl_e n el)) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (arities e) (@cons Arities (arities (multl_e n el)) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
intros n [H1 H2].
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (arities e) (@cons Arities (arities (multl_e n el)) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (arities e) (@cons Arities (arities (multl_e n el)) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (arities e) (@cons Arities (arities (multl_e n el)) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (arities e) (ok_arities n O)) (andb (aeq (arities (multl_e n el)) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (arities e) (@cons Arities (arities (multl_e n el)) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
rewrite H1, (IH _ H2).
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
simpl.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (andb (Nat.eqb n n) true) (andb (andb (Nat.eqb n n) true) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
rewrite <- beq_nat_refl.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
Qed.

Opaque mult_e.

Lemma multl_correct :
  forall n nl el,
  length (sem (multl_e n el) nl nil) = multl (map (fun e => length (sem e nl nil)) el).
Proof.
(* Goal: @eq Arities match arities mult_e with | error_rec a a0 a1 => error_comp (error_rec a a0 a1) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_comp a l l0 => error_comp (error_comp a l l0) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | error_proj n0 n1 n2 => error_comp (error_proj n0 n1 n2) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) | ok_arities hn hs => if andb (andb (andb (Nat.eqb hn (S (S O))) (Nat.eqb hs O)) (andb (aeq (ok_arities n O) (ok_arities n O)) (andb (aeq (ok_arities n O) (ok_arities n O)) true))) true then ok_arities n O else error_comp (ok_arities hn hs) (@cons Arities (ok_arities n O) (@cons Arities (ok_arities n O) (@nil Arities))) (@nil Arities) end (ok_arities n O) *)
induction el as [ | e el IH]; simpl.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
(* Goal: @eq nat (@length bool (sem mult_e (@cons (list bool) (sem e nl (@nil (list bool))) (@cons (list bool) (sem (multl_e n el) nl (@nil (list bool))) (@nil (list bool)))) (@nil (list bool)))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
rewrite mult_correct, IH.
(* Goal: @eq nat (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) (Init.Nat.mul (@length bool (sem e nl (@nil (list bool)))) (multl (@map BC nat (fun e : BC => @length bool (sem e nl (@nil (list bool)))) el))) *)
trivial.
Qed.
