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

Require Import List Arith Omega.

Require Import ILL.Definitions.

Require Import utils pos vec. 
Require Import subcode sss. 
Require Import tiles_solvable bsm_defs bsm_pcp.

Fact tile_concat_itau ln lt : tile_concat ln lt = (itau1 lt (rev ln), itau2 lt (rev ln)).
Proof.
(* Goal: @eq (prod (list bool) (list bool)) (tile_concat ln lt) (@pair (string bool) (string bool) (itau1 lt (@rev nat ln)) (itau2 lt (@rev nat ln))) *)
  induction ln as [ | i ln IH ]; simpl; auto.
(* Goal: @eq (prod (list bool) (list bool)) (let (th, tl) := @nth (prod (list bool) (list bool)) i lt (@pair (list bool) (list bool) (@nil bool) (@nil bool)) in let (hh, ll) := tile_concat ln lt in @pair (list bool) (list bool) (@app bool hh th) (@app bool ll tl)) (@pair (string bool) (string bool) (itau1 lt (@app nat (@rev nat ln) (@cons nat i (@nil nat)))) (itau2 lt (@app nat (@rev nat ln) (@cons nat i (@nil nat))))) *)
  rewrite itau1_app, itau2_app; simpl.
(* Goal: @eq (prod (list bool) (list bool)) (let (th, tl) := @nth (prod (list bool) (list bool)) i lt (@pair (list bool) (list bool) (@nil bool) (@nil bool)) in let (hh, ll) := tile_concat ln lt in @pair (list bool) (list bool) (@app bool hh th) (@app bool ll tl)) (@pair (string bool) (string bool) (@app bool (itau1 lt (@rev nat ln)) (@app bool (@fst (string bool) (string bool) (@nth (card bool) i lt (@pair (list bool) (list bool) (@nil bool) (@nil bool)))) (@nil bool))) (@app bool (itau2 lt (@rev nat ln)) (@app bool (@snd (string bool) (string bool) (@nth (card bool) i lt (@pair (list bool) (list bool) (@nil bool) (@nil bool)))) (@nil bool)))) *)
  unfold card, string; generalize (nth i lt ([] / [])); intros (a,b); rewrite IH.
(* Goal: @eq (prod (list bool) (list bool)) (@pair (list bool) (list bool) (@app bool (itau1 lt (@rev nat ln)) a) (@app bool (itau2 lt (@rev nat ln)) b)) (@pair (list bool) (list bool) (@app bool (itau1 lt (@rev nat ln)) (@app bool (@fst (list bool) (list bool) (@pair (list bool) (list bool) a b)) (@nil bool))) (@app bool (itau2 lt (@rev nat ln)) (@app bool (@snd (list bool) (list bool) (@pair (list bool) (list bool) a b)) (@nil bool)))) *)
  repeat rewrite <- app_nil_end; auto.
Qed.

(* tiles_solvable & iBPCP is the same predicate except that the existentially
   quantified list is reversed *)

Theorem tiles_solvable_iBPCP lt : tiles_solvable lt <-> iBPCP lt.
Proof.
(* Goal: iff (tiles_solvable lt) (iBPCP lt) *)
  split.
  + intros (ln & H1 & H2 & H3).
(* Goal: iBPCP lt *)
    rewrite tile_concat_itau in H3.
(* Goal: tiles_solvable lt *)
    exists (rev ln). 
(* Goal: and (forall (a : nat) (_ : @In nat a (@rev nat ln)), Peano.lt a (@length (card bool) lt)) (and (not (@eq (list nat) (@rev nat ln) (@nil nat))) (@eq (string bool) (itau1 lt (@rev nat ln)) (itau2 lt (@rev nat ln)))) *)
    rewrite <- Forall_forall.
(* Goal: and (not (@eq (list nat) (@rev nat ln) (@nil nat))) (and (@Forall nat (fun x : nat => Peano.lt x (@length (prod (list bool) (list bool)) lt)) (@rev nat ln)) (@eq (list bool) (itau1 lt ln) (itau2 lt ln))) *)
    repeat split; auto.
    * apply Forall_rev; auto.
    * contradict H1; rewrite <- (rev_involutive ln), H1; auto.
  + intros (ln & H1 & H2 & H3).
(* Goal: tiles_solvable lt *)
    exists (rev ln).
(* Goal: and (not (@eq (list nat) (@rev nat ln) (@nil nat))) (and (@Forall nat (fun x : nat => Peano.lt x (@length (prod (list bool) (list bool)) lt)) (@rev nat ln)) (let (hh, ll) := tile_concat (@rev nat ln) lt in @eq (list bool) hh ll)) *)
    rewrite tile_concat_itau, rev_involutive.
(* Goal: and (not (@eq (list nat) (@rev nat ln) (@nil nat))) (and (@Forall nat (fun x : nat => Peano.lt x (@length (prod (list bool) (list bool)) lt)) (@rev nat ln)) (@eq (list bool) (itau1 lt ln) (itau2 lt ln))) *)
    repeat split; auto.
    * contradict H2; rewrite <- (rev_involutive ln), H2; auto.
    * apply Forall_rev, Forall_forall; auto.
Qed.

Local Notation "P // s ->> t" := (sss_compute (@bsm_sss _) P s t).
Local Notation "P // s ~~> t" := (sss_output (@bsm_sss _) P s t).
Local Notation "P // s ↓" := (sss_terminates (@bsm_sss _) P s). 

Section iBPCP_BSM_HALTING.

  Let f (lt : list (card bool)) : BSM_PROBLEM.
  Proof.
(* Goal: BSM_PROBLEM *)
    exists 4, 1, (pcp_bsm lt).
(* Goal: vec (list bool) (S (S (S (S O)))) *)
    exact (vec_set_pos (fun _ => nil)).
  Defined.

  Goal forall x, | pcp_bsm x| >= 80.
(* Goal: forall x : list (prod (list bool) (list bool)), ge (@length (bsm_instr (S (S (S (S O))))) (pcp_bsm x)) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) *)
    intros; rewrite pcp_bsm_size; omega.
  Qed.
  
  Theorem iBPCP_BSM_HALTING : iBPCP ⪯ BSM_HALTING.
  Proof.
(* Goal: @reduces BSRS BSM_PROBLEM iBPCP BSM_HALTING *)
    exists f.
(* Goal: forall x : BSRS, iff (iBPCP x) (BSM_HALTING (f x)) *)
    intros lt.
(* Goal: iff (iBPCP lt) (BSM_HALTING (f lt)) *)
    rewrite <- tiles_solvable_iBPCP.
(* Goal: iff (tiles_solvable lt) (iBPCP lt) *)
    unfold BSM_HALTING; split.
    * intros H.
(* Goal: let (n, s) := f lt in let (i, s0) := s in let (P, v) := s0 in @sss_terminates (bsm_instr n) (vec (list bool) n) (@bsm_sss n) (@pair nat (list (bsm_instr n)) i P) (@pair nat (vec (list bool) n) i v) *)
      apply pcp_bsm_sound with (v := vec_set_pos (fun _ => nil)) in H.
      match type of H with  _ // _ ->> (?q,?w) => exists (q, w) end.
(* Goal: @sss_output (bsm_instr (S (S (S (S O))))) (vec (list bool) (S (S (S (S O))))) (@bsm_sss (S (S (S (S O))))) (@pair nat (list (bsm_instr (S (S (S (S O)))))) (S O) (pcp_bsm lt)) (@pair nat (vec (list bool) (S (S (S (S O))))) (S O) (@vec_set_pos (list bool) (S (S (S (S O)))) (fun _ : pos (S (S (S (S O)))) => @nil bool))) (@pair nat (vec (list bool) (S (S (S (S O))))) O (@vec_change (list bool) (S (S (S (S O)))) (@vec_change (list bool) (S (S (S (S O)))) (@vec_change (list bool) (S (S (S (S O)))) (@vec_change (list bool) (S (S (S (S O)))) (@vec_set_pos (list bool) (S (S (S (S O)))) (fun _ : pos (S (S (S (S O)))) => @nil bool)) (@pos_fst (S (S (S O)))) (@nil bool)) (@pos_nxt (S (S (S O))) (@pos_nxt (S (S O)) (@pos_nxt (S O) (@pos_fst O)))) (@nil bool)) (@pos_nxt (S (S (S O))) (@pos_fst (S (S O)))) (@nil bool)) (@pos_nxt (S (S (S O))) (@pos_nxt (S (S O)) (@pos_fst (S O)))) (@nil bool))) *)
      split; auto.
(* Goal: @out_code (bsm_instr (S (S (S (S O))))) (@fst nat (vec (list bool) (S (S (S (S O))))) (@pair nat (vec (list bool) (S (S (S (S O))))) O (@vec_change (list bool) (S (S (S (S O)))) (@vec_change (list bool) (S (S (S (S O)))) (@vec_change (list bool) (S (S (S (S O)))) (@vec_change (list bool) (S (S (S (S O)))) (@vec_set_pos (list bool) (S (S (S (S O)))) (fun _ : pos (S (S (S (S O)))) => @nil bool)) (@pos_fst (S (S (S O)))) (@nil bool)) (@pos_nxt (S (S (S O))) (@pos_nxt (S (S O)) (@pos_nxt (S O) (@pos_fst O)))) (@nil bool)) (@pos_nxt (S (S (S O))) (@pos_fst (S (S O)))) (@nil bool)) (@pos_nxt (S (S (S O))) (@pos_nxt (S (S O)) (@pos_fst (S O)))) (@nil bool)))) (@pair nat (list (bsm_instr (S (S (S (S O)))))) (S O) (pcp_bsm lt)) *)
      simpl; omega.
    * intros ((q & w) & H).
(* Goal: tiles_solvable lt *)
      apply pcp_bsm_complete in H; tauto.
  Qed.

End iBPCP_BSM_HALTING.

