Require Import Arith List.
Require Import BellantoniCook.Lib BellantoniCook.BC BellantoniCook.BCI BellantoniCook.BCI_to_BC.

Fixpoint convI (e : BC) : BCI :=
  match e with
    | zero => zeroI
    | proj n s i =>
      if leb (S i) n then projIn i else projIs (i - n)
    | succ b => succI b
    | pred => predI
    | cond => condI
    | rec g h0 h1 => recI (convI g) (convI h0) (convI h1)
    | comp n s g ln ls =>
      compI (convI g) (map convI ln) (map convI ls)
  end.

Opaque maxl.

Lemma convI_inf_correct : forall (e : BC) n s,
  arities e = ok_arities n s ->
  exists n', exists s', 
    n' <= n /\ s' <= s /\ inf (convI e) = I n' s'.
Proof.
  apply BC_ind_inf; simpl; intros.
  exists 0; exists 0; auto.

  destruct n; simpl.
  exists 0; exists (S (i - 0)).
  repeat (split; try omega).
  case_eq (leb i n); intros; simpl.
  apply leb_complete in H0.
  exists (S i); exists 0.
  repeat (split; try omega).
  apply leb_complete_conv in H0.
  exists 0; exists (S (i - S n)).
  repeat (split; try omega).

  exists 0; exists 1; auto.
  exists 0; exists 1; auto.
  exists 0; exists 4; auto.

  destruct H2 as (ne1 & se1 & He1).
  destruct H3 as (ne2 & se2 & He2).
  destruct H4 as (ne3 & se3 & He3).
  decompose [and] He1; decompose [and] He2; decompose [and] He3.
  clear He1 He2 He3.    
  rewrite H5, H8, H11.
  eexists; eexists.
  split; try split.
  3: eauto.
  apply maxl_bound; omega.
  apply maxl_bound; omega.

  destruct H2 as (ne & se & He).
  decompose [and] He; clear He.
  rewrite H7.
  repeat rewrite leb_correct.
  simpl.
  case_eq ( inf_list (map inf (map convI rl)) ) ; intros.  
  case_eq ( inf_list (map inf (map convI tl)) ) ; intros.
  case_eq (beq_nat n1 0); intros.
  eexists; eexists; split; try split.
  3: eauto.
  apply Nat.max_lub.
  apply inf_list_maxl_l in H5.
  rewrite H5.
(* Goal: @eq (list (list bool)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl) *)
  rewrite map_map.
(* Goal: @eq (list (list bool)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl) *)
  rewrite map_map.  
  apply maxl_bound_in.
  intros.
  apply in_map_iff in H10.
  destruct H10 as [? [? ?]].
  destruct (H3 x H11) as (? & ? & ?).
  decompose [and] H12.
  subst.
  rewrite H16; simpl; trivial.
  apply inf_list_maxl_l in H8.
  rewrite H8.
(* Goal: @eq (list (list bool)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl) *)
  rewrite map_map.
(* Goal: @eq (list (list bool)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl) *)
  rewrite map_map.  
  apply maxl_bound_in.
  intros.
  apply in_map_iff in H10.
  destruct H10 as [? [? ?]].
  destruct (H4 x H11) as (? & ? & ?).
  decompose [and] H12.
  subst.
  rewrite H16; simpl; trivial.
  apply inf_list_maxl_r in H8.
  rewrite H8.
(* Goal: @eq (list (list bool)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl) *)
  rewrite map_map.
(* Goal: @eq (list (list bool)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl) *)
  rewrite map_map.  
  apply maxl_bound_in.
  intros.
  apply in_map_iff in H10.
  destruct H10 as [? [? ?]].
  destruct (H4 x H11) as (? & ? & ?).
  decompose [and] H12.
  subst.
  rewrite H16; simpl; trivial.
  apply beq_nat_false in H9.
  elim H9.
  apply inf_list_maxl_r in H5.
  rewrite H5, map_map, map_map.
  apply maxl_map_0.
  intros.
  destruct (H3 x H10) as (? & ? & ?).
  decompose [and] H11.
  subst.
  rewrite H15; simpl; trivial.
  omega.

  elimtype False.
  apply in_inf_list_err_conv in H8.
  destruct H8.
  rewrite map_map in H8.
  apply in_map_iff in H8.
  destruct H8 as [? [? ?]].
  destruct (H4 x0 H9) as (? & ? & ?).
  decompose [and] H10.
  rewrite H8 in H14; discriminate.

  elimtype False.
  apply in_inf_list_err_conv in H5.
  destruct H5.
  rewrite map_map in H5.
  apply in_map_iff in H5.
  destruct H5 as [? [? ?]].
  destruct (H3 x0 H8) as (? & ? & ?).
  decompose [and] H9.
  rewrite H5 in H13; discriminate.

  rewrite map_length; omega.
  rewrite map_length; omega.
Qed.

Lemma convI_correct : forall e n s,
  arities e = ok_arities n s ->
  forall vnl vsl,
  semI (convI e) vnl vsl = sem e vnl vsl.
Proof.
(* Goal: forall (e : BC) (n s : nat) (_ : @eq Arities (arities e) (ok_arities n s)) (vnl vsl : list (list bool)), @eq (list bool) (semI (convI e) vnl vsl) (sem e vnl vsl) *)
  refine (BC_ind_inf _ _ _ _ _ _ _ _); simpl; intros; trivial.
(* Goal: @eq (list bool) (semI (if match n with | Datatypes.O => false | S m' => Nat.leb i m' end then projIn i else projIs (Init.Nat.sub i n)) vnl vsl) (if match n with | Datatypes.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)) *)
(* Goal: @eq (list bool) (sem_rec (semI (convI g)) (semI (convI h0)) (semI (convI h1)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (semI (convI h) (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) (@map BC BCI convI rl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl))) (sem h (@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)) *)
  destruct n; simpl; trivial.
(* Goal: @eq (list bool) (semI (if Nat.leb i n then projIn i else projIs (Init.Nat.sub i (S n))) vnl vsl) (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)) *)
(* Goal: @eq (list bool) (sem_rec (semI (convI g)) (semI (convI h0)) (semI (convI h1)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (semI (convI h) (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) (@map BC BCI convI rl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl))) (sem h (@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)) *)
  case_eq (leb i n); intros; simpl; trivial.
(* Goal: @eq (list bool) (sem_rec (semI (convI g)) (semI (convI h0)) (semI (convI h1)) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) (sem_rec (sem g) (sem h0) (sem h1) (@hd (list bool) (@nil bool) vnl) (@tl (list bool) vnl) vsl) *)
(* Goal: @eq (list bool) (semI (convI h) (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) (@map BC BCI convI rl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl))) (sem h (@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)) *)
  induction (hd nil vnl); simpl; intros; auto.
(* Goal: @eq (list bool) (if a then semI (convI h1) (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (semI (convI g)) (semI (convI h0)) (semI (convI h1)) l (@tl (list bool) vnl) vsl) vsl) else semI (convI h0) (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (semI (convI g)) (semI (convI h0)) (semI (convI h1)) l (@tl (list bool) vnl) vsl) vsl)) (if a then sem h1 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l (@tl (list bool) vnl) vsl) vsl) else sem h0 (@cons (list bool) l (@tl (list bool) vnl)) (@cons (list bool) (sem_rec (sem g) (sem h0) (sem h1) l (@tl (list bool) vnl) vsl) vsl)) *)
(* Goal: @eq (list bool) (semI (convI h) (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) (@map BC BCI convI rl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl))) (sem h (@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)) *)
  rewrite IHl; case a; auto.
(* Goal: @eq (list bool) (semI (convI h) (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) (@map BC BCI convI rl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl))) (sem h (@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)) *)
  rewrite H2.
(* Goal: @eq (list bool) (sem h (@map BCI (list bool) (fun ne : BCI => semI ne vnl (@nil (list bool))) (@map BC BCI convI rl)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl))) (sem h (@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)) *)
  f_equal.
(* Goal: @eq (list (list bool)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl) *)
  rewrite map_map.
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun x : BC => semI (convI x) vnl vsl) tl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl) *)
  apply map_ext2; auto.
(* Goal: @eq (list (list bool)) (@map BCI (list bool) (fun se : BCI => semI se vnl vsl) (@map BC BCI convI tl)) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl) *)
  rewrite map_map.
(* Goal: @eq (list (list bool)) (@map BC (list bool) (fun x : BC => semI (convI x) vnl vsl) tl) (@map BC (list bool) (fun se : BC => sem se vnl vsl) tl) *)
  apply map_ext2; auto.
Qed.