Require Export NtlEqui.

(*
  Inductive predicate for two trees of similar structure (one nu-tree and one pure tree)
 *)
Inductive Sim : NuTree -> Tree -> Prop :=
| SimA a b l l' :
    rk a = rk b -> |l| = |l'|
  -> (forall k, k < |l| -> Sim (nth k l DNT) (nth k l' DTR))
  -> Sim (Tr a l) (TrA b l')
| SimB a n t : Sim n t -> Sim (Nu a n) t.

Lemma sim_perm n t :
  Sim n t -> forall p, Perm p -> Sim (p *' n) t.
Proof.
  intros H1. induction H1; intros p HP.
  - simpl. constructor; try now rewrite map_length.
    + destruct HP as [HP _ ]. now rewrite <-(HP a).
    + intros k H3. rewrite map_length in H3.
      rewrite map_nth_indep; trivial. apply H2; assumption.
  - simpl. constructor. apply IHSim, HP.
Qed.

Lemma sim_perm' n t :
  Ntwr n -> forall p, Perm p -> Sim (p *' n) t -> Sim n t.
Proof.
  intros HW p HP H1. assert(Perm p) by assumption. destruct HP as [HP1 [p' HP2]].
  apply sim_perm with (p := p') in H1.
  - rewrite <-nt_perm_apply_inv in H1; auto.
  - apply perm_inv_perm with (p := p); assumption.
Qed.

Fixpoint similar n t : bool :=
  match n, t with
  | Tr a l, TrA b l' => if Dec (rk a = rk b) then all_true (map_pw (map (similar) l) l') else false
  | Nu a n', _ => similar n' t
  end.

(*
  similar is a decider for Sim
 *)
Fact similar_correct n t :
  Ntwr n -> Twr t -> similar n t = true <-> Sim n t.
Proof.
  intros H1 H2. split.
  - revert H2. revert t. induction H1 as [a l H1 H2 H3|a' n H1 H2]; intros t H4; induction H4 as [b l' H4 H5 H6]; intros H7.
    + simpl in H7. decide (rk a = rk b) as [E|E]; auto.
      constructor; try assumption; try congruence. intros k H8. apply H2; auto; try solve_wr_sub.
      rewrite all_true_map_pw_map with (x:=DNT)(y:=DTR) in H7; try congruence. now apply H7.
    + constructor. simpl in *. apply H2; try assumption. constructor; assumption.
  - intros H3. induction H3 as [a b l l' H3 H4 H5 H6|a n t H3 H4]; simpl.
    + decide (rk a = rk b) as [_|E]; auto.
      rewrite all_true_map_pw_map with (x:=DNT)(y:=DTR); try assumption. intros k H7.
      apply H6; try assumption; solve_wr_sub.
    + eauto.
Qed.

(*
  I don't really show equivariance, because I don't need any permutation on
  the pure tree t.
 *)
Lemma similar_equiv n :
  Ntwr n -> forall t, Twr t -> forall p, Perm p -> similar n t = true -> similar (p *' n) t = true.
Proof.
  intros H1 t H2 p H3 H4 % similar_correct; auto.
  apply similar_correct, sim_perm; auto.
Qed.

Lemma similar_swap_perm n :
  Ntwr n -> forall t, Twr t -> forall p p', Perm p -> Perm p' -> similar (p *' n) t = true -> similar (p' *' n) t = true.
Proof.
  intros H1 t H2 p p' HP1 HP2 H3.
  assert(HT: Perm p) by assumption. destruct HP1 as [HP11 [p'' HP12]].
  apply similar_equiv; auto. apply similar_equiv with (p:=p'') in H3; auto.
  rewrite <-nt_perm_apply_inv in H3; auto. apply (perm_inv_perm HT HP12).
Qed.

Inductive PSim : NuTree -> Tree -> Prop :=
| PSimA a b l l' :
    rk a = rk b -> |l| = |l'|
-> (forall p k, Perm p -> k < |l| -> PSim (p *' (nth k l DNT)) (nth k l' DTR))
-> PSim (Tr a l) (TrA b l')
| PSimB a n t : (forall p, Perm p -> PSim (p *' n) t) -> PSim (Nu a n) t.

Lemma psim_perm n t :
  Ntwr n -> PSim n t -> forall p, Perm p -> PSim (p *' n) t.
Proof.
  intros HW1 H1. induction H1.
  - intros p HP. simpl. constructor.
    + destruct HP as [HP _]. now rewrite <-(HP a).
    + now rewrite map_length.
    + rewrite map_length. intros p2 k HP2 H3.
      rewrite map_nth_indep; trivial.
      apply H2; auto. apply nt_perm_wr; try assumption. solve_wr_sub.
  - intros q HP. simpl. constructor. inversion HW1. apply H0; auto.
Qed.

Lemma psim_perm' n t :
  Ntwr n -> forall p, Perm p -> PSim (p *' n) t -> PSim n t.
Proof.
  intros HW1 p HP H1. assert(HP3: Perm p ) by assumption.
  destruct HP as [HP1 [p' HP2]].
  rewrite (nt_perm_apply_inv HW1 (inv_comm HP2)). apply psim_perm; auto.
  apply (perm_inv_perm HP3 HP2).
Qed.

(*
  similar is also a decider for the PSim predicate.
 *)
Lemma similar_correct' n t :
  Ntwr n -> Twr t -> similar n t = true <-> PSim n t.
Proof.
  intros H1 H2. split.
  - revert H2. revert t. induction H1 as [a l H1 H2 H3|a' n H1 H2]; intros t H4; induction H4 as [b l' H4 H5 H6]; intros H7.
    + simpl in H7. decide (rk a = rk b) as [E|E]; auto.
      constructor; try assumption; try congruence.
      intros p k H8 H9. apply psim_perm; auto. apply H2; auto; try solve_wr_sub.
      rewrite all_true_map_pw_map with (x:=DNT)(y:=DTR) in H7; try congruence. now apply H7.
    + constructor. simpl in *. intros p HP. apply psim_perm; auto.
  - intros H3. induction H3 as [a b l l' H3 H4 H5 H6|a n t H3 H4]; simpl.
    + decide (rk a = rk b); auto.
      rewrite all_true_map_pw_map with (x:=DNT)(y:=DTR); try congruence.
      intros k H9. rewrite <-nt_id with (n:=nth k l DNT); try solve_wr_sub.
      apply H6; auto; try rewrite (nt_id); solve_wr_sub.
    + inversion H1. rewrite <-(nt_id H0). eauto.
Qed.

(*
    Sim is equivalent to PSim.
    Therefore PSim predicate isn't actually stronger.
    This makes sense intuitively, since permutations don't change structure anyway.
    But PSim gives us a better inductive hypothesis.
 *)
Lemma sim_psim n t :
  Ntwr n -> Twr t -> Sim n t <-> PSim n t.
Proof.
  intros H1 H2. split; intros H3.
  - apply similar_correct', similar_correct; assumption.
  - apply similar_correct, similar_correct'; assumption.
Qed.

(*
  candidate names are all those names in the pure tree, that aren't used already
  and aren't free in the nu-tree.
  These are used when the nu has to be instantiated, i.e. when the nu actually
  binds a name somewhere. This is subtle, but crucial.
*)
Definition candidates n A t r :=
  filter (fun x => Dec ((r = rk x) /\ ~(x el A) /\ ~(x el (FN n)))) (names t).

(*
  dmap_nu is a helper function that
  instantiates the name a in n with each element of l and applies f
  while adding the current instantiation to the accumulator.
  l will be the list of candidates, f will be the ntl_dec function.
*)
Fixpoint dmap_nu (f : list Name -> NuTree -> Tree -> bool) A a n t l : list bool :=
  match l with
  | [] => []
  | b :: xs => (f (b::A) (a$b *' n) t) :: (dmap_nu f A a n t xs)
  end.

(*
  To summarize the function:
  For ntl_dec to return true:
  - In the tree case all children t_i have to be in the language of n_i
  - In the nu case there has to be one candidate name that fits.
 *)
Fixpoint ntl_dec (k: nat) (A : list Name) (n: NuTree) (t : Tree) : bool :=
  match k with
  | 0 => true
  | S k' =>
    match n, t with
    | Tr a l, TrA b l' => if Dec(a=b)
                           then all_true (map2 (ntl_dec k' (a::A)) l l' )
                           else false
    | Nu a n', _ => if Dec(a el FN n')
                    then some_true (dmap_nu (ntl_dec k') A a n' t (candidates n A t (rk a)))
                    else ntl_dec k' A n' t
    end
  end.

Lemma candidates_valid n A t r a :
  a el candidates n A t r <-> a el names t /\ r = rk a /\ ~a el A /\ ~a el FN n .
Proof. unfold candidates. now rewrite in_filter_iff, Dec_reflect. Qed.

Lemma in_dmap_nu_iff (f : list Name -> NuTree -> Tree -> bool) (z : bool) A a n t l :
  z el (dmap_nu f A a n t l) <-> (exists b, b el l /\ (f (b::A) (a$b *' n) t = z)).
Proof.
  split.
  - induction l; simpl; auto. intros [H1|H1]; eauto.
    specialize (IHl H1) as [b [IH1 IH2]]. eauto.
  - revert A n a. induction l; simpl; intros A n a0 [b [H1 H2]]; auto.
    destruct H1 as [->|H1]; eauto.
Qed.

(*
  This establishes that the left hand side works like
  a big boolean 'or' on the function applications.
*)
Lemma dmap_nu_some_true (f : list Name -> NuTree -> Tree -> bool) A a n t l :
  some_true (dmap_nu f A a n t l) = true <-> (exists b, b el l /\ (f (b::A) (a$b *' n) t = true)).
Proof.
  rewrite some_true_true. split.
  - intros [b [H1 H2]] % in_dmap_nu_iff. eauto.
  - intros [b [H1 H2]]. apply in_dmap_nu_iff. eauto.
Qed.

(*
  The name at the top has to match if ntl_dec returns true.
  Analogous to the ntl_name lemma.
*)
Lemma ntl_dec_true_name k A a a' l l' :
  ntl_dec k A (Tr a l) (TrA a' l') = true -> k >= (nt_depth (Tr a l)) -> a = a'.
Proof.
  intros H1. destruct k; simpl; intros; simpl in *; try omega. decide (a=a'); auto.
Qed.

Lemma ntl_dec_true_name' A d p a b l l' :
  (forall x, x el l -> Ntwr x) -> d >= (nt_depth (Tr a l)) ->
  ntl_dec d A (p *' Tr a l) (TrA b l') = true -> p a = b.
Proof.
  simpl. intros H1 H2 H3.
  apply ntl_dec_true_name with (k:=d)(A:=A)(l:=(map (nt_apply_perm p) l))(l':=l'); simpl; try congruence.
  rewrite map_map. rewrite map_ext_in with (g := nt_depth); try assumption.
  intros x H10. symmetry. auto using nt_depth_perm.
Qed.

(*
  If ntl_dec is true, then similar is true.
*)
Lemma ntl_dec_similar n :
  Ntwr n -> forall t, Twr t -> forall A d p,
  d >= nt_depth n -> Perm p -> ntl_dec d A (p *' n) t = true -> similar (p *' n) t = true.
Proof.
  intros H1. induction H1 as [a l H1 H2 H3|a n H1 H2];
               intros t H4; induction H4 as [b l' H4 H5 H6];
                 intros A d p H7 H8 H9; simpl in *.
  - destruct d; try omega. assert(H10: p a = b) by apply (ntl_dec_true_name' H1 H7 H9).
    rewrite H10 in *.
    assert(H12: rk (p a) = rk a) by now destruct H8.
    decide (rk b = rk b) as [_|]; try contradiction.
    rewrite all_true_map_pw_map with (x:=p*'DNT)(y:=DTR); try (rewrite map_length; congruence).
    intros k H11. rewrite map_nth. rewrite map_length in H11.
    apply H2 with (d:=d)(A:=b::A); auto; try solve_wr_sub.
    + apply gt_depth_sub with (d:=d); try assumption. omega.
    + simpl in H9. solve_dec.
      rewrite map2_all_true with (x:=p*'DNT)(y:=DTR), map_length in H9; try (rewrite map_length; congruence).
      specialize (H9 k H11). now rewrite map_nth in H9.
  - destruct d; try omega. simpl in H9. decide (p a el FN(p*'n)) as [E1|E1].
    + rewrite dmap_nu_some_true in H9. destruct H9 as [c [H9 H10]].
      assert(Perm ( (p a) $ c ** p)). {
        apply perm_compose_perm; try assumption. apply transp_perm.
        apply candidates_valid in H9. apply H9.
      }
      apply similar_swap_perm with (p := (p a) $ c ** p); auto.
      apply H2 with (A:=c::A)(d:=d); auto using Twr; try omega.
      now rewrite nt_assoc.
    + assert(d >= nt_depth n) by omega. apply H2 with (A:=A)(d:=d); auto.
Qed.

(*
  A tree t in n has to be similar to it.
*)
Lemma ntl_sim n t :
  Ntwr n -> forall A, t El [n] A -> Sim n t.
Proof.
  intros HW A H3.
  induction H3 as [A' l l' a H3 H4 H5| A' n' t a b H3 H4 H5 H6 H7]; constructor; auto.
  - intros k H6. apply H5; auto. solve_wr_sub.
  - inversion HW. apply sim_perm' with (p := a$b); auto.
Qed.

(*
  If ntl_dec returns true for some d whose value is at least the depth of the nu-tree,
  then it returns true for all d.
*)
Lemma ntl_dec_depth A n t d :
  Ntwr n -> Twr t -> ntl_dec d A n t = true -> d >= nt_depth n -> forall d', ntl_dec d' A n t = true.
Proof.
  intros HW1 HW2 H1 HD d'.
  assert(HS: PSim n t). {
    apply similar_correct'; auto. rewrite <-(nt_id HW1).
    apply ntl_dec_similar with (A:=A)(d:=d); auto. now rewrite (nt_id HW1).
  }
  revert d'. revert H1. revert A. revert HD. revert d.
  induction HS as [a b l l' H1 H2 H3 H4 | a n t H1 H2]; intros d HD A HA d'.
  - destruct d.
    { contradict HD. assert(nt_depth (Tr a l) > 0) by apply ntd_S'. omega. }
    assert(a=b).
    { apply ntl_dec_true_name with (k:=S d)(A:=A)(l:=l)(l':=l'); auto. }
    subst b. destruct d'; simpl; auto. decide (a=a) as [_|]; auto.
    rewrite map2_all_true with (x:=DNT)(y:=DTR); try assumption. intros k H6.
    specialize(H4 id k perm_id H6). rewrite (nt_id) in H4; try solve_wr_sub.
    apply H4 with (d:= d); auto; try omega; try solve_wr_sub.
    + simpl in HD. apply gt_depth_sub; try assumption. omega.
    + simpl in HA. decide (a=a) as [_|]; auto.
      rewrite map2_all_true with (x:=DNT)(y:=DTR) in HA; try assumption. apply HA, H6.
  - destruct d.
    { contradict HD. assert(nt_depth (Nu a n) > 0) by apply ntd_S'. omega. }
    destruct d'; auto. simpl in *. decide (a el FN n) as [HF|HF].
    + rewrite dmap_nu_some_true. rewrite dmap_nu_some_true in HA.
      destruct HA as [ b [HA1 HA2]].
      assert(HP: Perm (a$b)).
      { apply candidates_valid in HA1. apply transp_perm, HA1. }
      inversion HW1. exists b. split; try assumption.
      apply H2 with (d:=d); auto; try omega.
      rewrite <-nt_depth_perm; try assumption. omega.
    + inversion HW1. rewrite <-(nt_id H0).
      apply H2 with (d:=d); auto; try omega; rewrite (nt_id H0); try assumption; omega.
Qed.

Section Correct.

  Variable n : NuTree.
  Variable t : Tree.
  Variable A : list Name.
  Hypothesis HW1 : Ntwr n.
  Hypothesis HW2 : Twr t.

  (*
  Finally we can prove the ntl_dec function correct in the next lemmas.
  The proofs make use of the PSim predicate to get a nice inductive hypothesis.
  In the Tr case we use the list lemma for map2.
  In the Nu case we show that we either found the instantiation in the candidates list
  or we can ignore the nu.
  In both cases we additionally use ntl_dec_depth to treat the depth parameter.
   *)
  Lemma ntl_dec_correct_1 :
    t El [n] A -> ntl_dec (nt_depth n) A n t = true.
  Proof.
    intros HD.
    assert(HT: PSim n t).
    { apply sim_psim; try assumption. apply ntl_sim with (A:=A); assumption. }
    revert HD. revert A. induction HT as [a b l l' H1 H2 H3 H4| a n t H1 H2]; intros A HD; simpl in *.
    - assert(a = b).
      { apply ntl_name with (A:=A)(l:=l)(l':=l'); assumption. }
      subst b. decide(a = a) as [_|E1]; try contradiction.
      rewrite map2_all_true with (x:=DNT)(y:=DTR); try assumption. intros k HL.
      assert(HW3: Ntwr (nth k l DNT)) by solve_wr_sub.
      assert(HW4: Twr (nth k l' DTR)) by solve_wr_sub.
      rewrite <-(nt_id HW3).
      apply ntl_dec_depth with(d:= nt_depth(id *' nth k l DNT)); auto.
      apply H4; auto. rewrite (nt_id HW3). inversion HD. subst. auto.
    - inversion HW1. subst. decide (a el FN n) as [E1|E1].
      + inversion HD. subst.
        assert(b el names t). {
          apply ntl_name_in with (n:=a$b *' n)(A:=b::A); auto.
          rewrite FN_equiv_shift with (p':= a$b); auto. solve_dec.
        }
        rewrite dmap_nu_some_true. exists b. split.
        * apply candidates_valid. now repeat split.
        * rewrite ntl_dec_depth with (d:=nt_depth (a$b *' n)); auto.
      + apply ntl_nu_indep in HD; try assumption.
        rewrite <-(nt_id H0). apply H2; auto. now rewrite (nt_id H0).
  Qed.

  Lemma ntl_dec_correct_2 :
    ntl_dec (nt_depth n) A n t = true -> t El [n]A.
  Proof.
    intros H3.
    assert(HT: PSim n t). {
      apply similar_correct'; try assumption.
      rewrite <-nt_id with (n:=n); try assumption.
      apply ntl_dec_similar with (A:=A)(d:=(nt_depth n)); auto.
      rewrite nt_id with (n:=n); try assumption.
    }
    revert H3. revert A. induction HT as [a b l l' H1 H2 H3 H4| a n t H1 H2]; intros A H5.
    - simpl in H5.
      assert(a = b).
      { apply ntl_dec_true_name with (k:=nt_depth (Tr a l))(A:=A)(l:=l)(l':=l'); auto. }
      subst b. constructor; try assumption; fold nt_apply_perm. intros k H7.
      assert(HW3: Ntwr (nth k l DNT)) by solve_wr_sub.
      assert(HW4: Twr (nth k l' DTR)) by solve_wr_sub.
      decide (a = a) as [_|]; try contradiction.
      rewrite map2_all_true with (x:= DNT)(y:=DTR) in H5; try assumption.
      rewrite <-(nt_id HW3). apply H4; try assumption; auto; try now rewrite nt_id.
      rewrite (nt_id HW3), ntl_dec_depth with (d:= list_max(map nt_depth l)); auto.
      apply list_max_max, in_map_iff. eauto.
    - simpl in H5. inversion HW1. subst. decide (a el FN n) as [E1|E1].
      + rewrite dmap_nu_some_true in H5. destruct H5 as [b [H5 % candidates_valid H7]].
        apply DNNu with (b:=b); intuition; fold nt_apply_perm.
        apply H2; auto. rewrite ntl_dec_depth with (d := nt_depth n); auto. rewrite <-nt_depth_perm; auto.
      + apply ntl_nu_indep; auto. rewrite <-(nt_id H0). apply H2; auto. now rewrite (nt_id H0).
  Qed.

  Theorem ntl_dec_correct :
    t El [n] A <-> ntl_dec (nt_depth n) A n t = true.
  Proof.
    split.
    - apply ntl_dec_correct_1; assumption.
    - apply ntl_dec_correct_2; assumption.
  Qed.

  Theorem dec_ntl :
    dec(t El [n] A).
  Proof.
    destruct (ntl_dec (nt_depth n) A n t) eqn:E.
    - left. rewrite ntl_dec_correct; assumption.
    - right. intros H3. rewrite ntl_dec_correct in H3; congruence.
  Qed.

End Correct.