Require Import ILL.Definitions.

(** ** PCP reduces to BPCP *)

(* natural numbers n to bitstrings of the form 1^n *)

Definition to_bitstring (n : nat) : string bool := Nat.iter n (cons true) [].

Lemma bitstring_false a : ~ false el to_bitstring a.
Proof.
(* Goal: not (@In bool false (to_bitstring a)) *)
  induction a; cbn; firstorder.
Qed.

(* strings of natural numbers to bitstrings, [ n1, ... n2 ] |-> 1^n1 0 ... 1^n2 0 *)
Fixpoint f_s (x : string nat) : string bool :=
  match x with
  | nil => nil
  | a :: x => to_bitstring a ++ [false] ++ f_s x
  end.

Lemma f_s_app x y : f_s (x ++ y) = f_s x ++ f_s y.
Proof.
(* Goal: @eq (string bool) (f_s (@app nat x y)) (@app bool (f_s x) (f_s y)) *)
  induction x; cbn. 
  - reflexivity.
  - rewrite IHx. now simpl_list.
Qed.

(* extension to cards and stacks *)
Definition f_c '(x,y) := (f_s x, f_s y).
Definition f (P : SRS) : BSRS :=
  map f_c P.

Lemma tau1_f A : tau1 (f A) = f_s (tau1 A).
Proof.
(* Goal: forall _ : @incl (card bool) A (f B), @eq (string nat) (@tau2 nat (g A)) (g_s (@tau2 bool A)) *)
  induction A as [ | (x,y) ]; cbn.
  - reflexivity.
  - unfold f in IHA. now rewrite IHA, f_s_app.
Qed.

Lemma tau2_f A : tau2 (f A) = f_s (tau2 A).
Proof.
(* Goal: forall _ : @incl (card bool) A (f B), @eq (string nat) (@tau2 nat (g A)) (g_s (@tau2 bool A)) *)
  induction A as [ | (x,y) ]; cbn.
  - reflexivity.
  - unfold f in IHA. now rewrite IHA, f_s_app.
Qed.

(* interpretation of a bitstring as list of natural numbers *)
Fixpoint g_s' (x : string bool) (n : nat) : string nat :=
  match x with
  | nil => nil
  | true :: x' => g_s' x' (S n)
  | false :: x' => n :: g_s' x' 0
  end.

Lemma g_s'_app n x y :
  g_s' (f_s x ++ y) n = match x with nil => g_s' y n | m :: x => n + m :: x ++ g_s' y 0 end.
Proof.
(* Goal: @eq (string nat) (g_s' (@app bool (f_s x) y) n) match x with | nil => g_s' y n | cons m x => @cons nat (Init.Nat.add n m) (@app nat x (g_s' y O)) end *)
  revert n y. induction x as [ | m]; intros; cbn in *.
  - reflexivity.
  - revert n; induction m; intros; cbn in *.
    + destruct x.
      * do 2 f_equal. omega.
(* Goal: @eq (string nat) (@cons nat n (g_s' (@app bool (f_s (@cons nat n0 x)) y) O)) (@cons nat (Init.Nat.add n O) (@app nat (@cons nat n0 x) (g_s' y O))) *)
      * rewrite IHx. f_equal. omega.
    + rewrite IHm. f_equal. omega.
Qed.

Definition g_s x := g_s' x 0.

Lemma f_g_s'_inv x : g_s (f_s x) = x.
Proof.
  unfold g_s. setoid_rewrite <- app_nil_r at 2. rewrite g_s'_app.
(* Goal: @eq (string bool) (@app bool (to_bitstring a) (@cons bool false (@app bool (f_s x) (f_s y)))) (@app bool (@app bool (to_bitstring a) (@cons bool false (f_s x))) (f_s y)) *)
  destruct x; now simpl_list. 
Qed.

(* extension to cards and stacks *)
Definition g_c '(x,y) := (g_s x, g_s y).
Definition g (P : BSRS) : SRS :=
  map g_c P.

(* Invariants *)

Lemma tau1_g A B : A <<= f B -> tau1 (g A) = g_s (tau1 A).
Proof.
(* Goal: forall _ : @incl (card bool) A (f B), @eq (string nat) (@tau2 nat (g A)) (g_s (@tau2 bool A)) *)
  induction A as [ | (x,y)]; cbn.
  - reflexivity.
  - unfold g in IHA. intros. rewrite !IHA. 
(* Goal: @eq (string nat) (@app nat (g_s y) (g_s (@tau2 bool A))) (g_s' (@app bool y (@tau2 bool A)) O) *)
(* Goal: @incl (card bool) A (f B) *)
    assert ( x /y el map f_c B) as ((x',y') & ? & ?) % in_map_iff by firstorder; inv H0.
(* Goal: @eq (string nat) (@app nat (g_s (f_s y')) (g_s (@tau2 bool A))) (g_s' (@app bool (f_s y') (@tau2 bool A)) O) *)
(* Goal: @incl (card bool) A (f B) *)
    rewrite g_s'_app. destruct x'.
(* Goal: @eq (string nat) (@cons nat n (@app nat y' (g_s (@tau2 bool A)))) (@cons nat n (@app nat y' (g_s' (@tau2 bool A) O))) *)
    + cbn. reflexivity.
(* Goal: @eq (string nat) (@cons nat n (@app nat y' (g_s (@tau2 bool A)))) (@cons nat n (@app nat y' (g_s' (@tau2 bool A) O))) *)
    + rewrite f_g_s'_inv. cbn. reflexivity.
    + firstorder.
Qed.

Lemma tau2_g A B : A <<= f B -> tau2 (g A) = g_s (tau2 A).
Proof.
(* Goal: forall _ : @incl (card bool) A (f B), @eq (string nat) (@tau2 nat (g A)) (g_s (@tau2 bool A)) *)
  induction A as [ | (x,y)]; cbn.
  - reflexivity.
  - unfold g in IHA. intros. rewrite !IHA. 
(* Goal: @eq (string nat) (@app nat (g_s y) (g_s (@tau2 bool A))) (g_s' (@app bool y (@tau2 bool A)) O) *)
(* Goal: @incl (card bool) A (f B) *)
    assert ( x /y el map f_c B) as ((x',y') & ? & ?) % in_map_iff by firstorder; inv H0.
(* Goal: @eq (string nat) (@app nat (g_s (f_s y')) (g_s (@tau2 bool A))) (g_s' (@app bool (f_s y') (@tau2 bool A)) O) *)
(* Goal: @incl (card bool) A (f B) *)
    rewrite g_s'_app. destruct y'.
(* Goal: @eq (string nat) (@cons nat n (@app nat y' (g_s (@tau2 bool A)))) (@cons nat n (@app nat y' (g_s' (@tau2 bool A) O))) *)
    + cbn. reflexivity.
(* Goal: @eq (string nat) (@cons nat n (@app nat y' (g_s (@tau2 bool A)))) (@cons nat n (@app nat y' (g_s' (@tau2 bool A) O))) *)
    + rewrite f_g_s'_inv. cbn. reflexivity.
    + firstorder.
Qed.

Lemma f_subset B A : A <<= B -> f A <<= f B.
Proof.
  induction A in B |- *; intros H; cbn.
  * firstorder.
  * intros ? [| H0]; subst.
    -- unfold f. eapply in_map_iff. eauto.
    -- eapply IHA in H0; eauto.
Qed.

Lemma f_g_subset B A : A <<= f B -> g A <<= B.
Proof.
(* Goal: @In (card nat) (g_c (f_c (@pair (string nat) (string nat) x y))) B *)
(* Goal: @In (card nat) a B *)
  revert B; induction A; intros B H; cbn.
  * firstorder.
  * assert (a el f B) by firstorder.
(* Goal: @incl (card nat) (@cons (prod (string nat) (string nat)) (g_c a) (@map (prod (string bool) (string bool)) (prod (string nat) (string nat)) g_c A)) B *)
    unfold f in H0. eapply in_map_iff in H0 as ((x,y) & ? & ?). inv H0.
(* Goal: @In (card nat) (g_c (f_c (@pair (string nat) (string nat) x y))) B *)
(* Goal: @In (card nat) a B *)
    intros ? [|]; subst. cbn. now rewrite !f_g_s'_inv. firstorder.
Qed.

Lemma PCP_BPCP : PCP ⪯  BPCP.
Proof.
(* Goal: @reduces (list (card nat)) (list (card bool)) PCP BPCP *)
  exists f. intros B. split.
  - intros (A & HP & He & H). exists (f A). repeat split.
    + now eapply f_subset.
    + destruct A; cbn; congruence.
    + unfold f, f_c, f_s. setoid_rewrite tau1_f. setoid_rewrite tau2_f. now rewrite H.
  - intros (A & HP & He & H). exists (g A). repeat split.
    + eapply f_g_subset; eauto.
    + destruct A; cbn; congruence.
    + erewrite tau1_g, tau2_g, H; eauto.
Qed.

     

          
          

          
        
    
