Require Import Vectors.Fin.
Require Import NtlEqui.
Require Export NuTree.
Definition Q' : nat -> Set :=
Vectors.Fin.t.
Definition Delta1 : nat -> Type :=
fun n => list ((Q' n) * Name * list (Q' n)).
Definition Delta2 : nat -> Type :=
fun n => list ((Q' n) * (Q' n) * Name * list (Q' n)).
Definition Delta3 : nat -> Type :=
fun n => list ((Q' n) * Name * (Q' n)).
Definition Phi' : nat -> Type :=
fun n => Name -> (option (Q' n)).
Structure NTA :=
{
s' : nat;
D1' : Delta1 s';
D2' : Delta2 s';
D3' : Delta3 s';
}.
Parameter A : NTA.
Definition s := (s' A).
Definition D1 := (D1' A).
Definition D2 := (D2' A).
Definition D3 := (D3' A).
Definition Q := (Q' s).
Definition Phi := (Phi' s).
Implicit Type phi : Phi.
Implicit Type q : Q.
Implicit Type nt : NuTree.
Instance state_eq_dec k :
eq_dec (Q' k).
Proof. apply Vectors.Fin.eq_dec. Qed.
Instance option_eq_dec X :
eq_dec X -> eq_dec (option X).
Proof. unfold dec. decide equality. Qed.
Instance state_eq_dec' N :
eq_dec (Q' (s' N)).
Proof. auto. Qed.
Definition update phi a (q : option Q) :=
fun a' => if Dec (a' = a) then q else phi a'.
(*
The language of the automaton
*)
Inductive NtaAccept q phi : NuTree -> Prop :=
| AD1 a nl ql: phi a = None ->
(q, a, ql) el D1 -> |ql| = rk a ->
(forall i, i < | nl | -> NtaAccept (nth i ql q) phi (nth i nl DNT))
-> NtaAccept q phi (Tr a nl)
| AD2 a nl q' ql : phi a = Some q' ->
(q, q', a, ql) el D2 -> |ql| = rk a ->
(forall i, i < | nl | -> NtaAccept (nth i ql q) phi (nth i nl DNT))
-> NtaAccept q phi (Tr a nl)
| AD3 a n q' : (q, a, q') el D3 ->
NtaAccept q' (update phi a (Some q)) n
-> NtaAccept q phi (Nu a n).
(*
The internal alphabet of the automaton
*)
Definition nta_names : list Name :=
let l1 := map (fun x => match x with (_,a,_) => a end) D1 in
let l2 := map (fun x => match x with (_,_,a,_) => a end) D2 in
let l3 := map (fun x => match x with (_,a,_) => a end) D3 in
l1 ++ l2 ++ l3.
(*
The next 3 functions find all applicable transitions for a given lhs of a transition.
They return the rhs.
*)
Definition candsd1 q a :=
let trans := filter (fun x =>
match x with
| (qx, ax, qlx) => Dec (ax = a /\ qx = q /\ |qlx| = rk a)
end
) (D1)
in map (fun x => match x with (_,_,ql) => ql end) trans.
Definition candsd2 q q' a :=
let trans := filter (fun x =>
match x with
| (q1x, q2x, ax, qlx) => Dec (ax = a /\ q1x = q /\ q2x = q' /\ |qlx| = rk a)
end
) (D2)
in map (fun x => match x with (_,_,_,ql) => ql end) trans.
Definition candsd3 q a :=
let trans := filter (fun x =>
match x with
| (q1x, ax, q2x) => Dec (ax = a /\ q1x = q)
end
) (D3)
in map (fun x => match x with (_,_,q') => q' end) trans.
Definition tdec_all_true (f : NuTree -> Q -> bool) (ql : list Q) (l : list NuTree) : bool :=
all_true (map_pw (map f l) ql).
Definition tdec_some_true (f : NuTree -> Q -> bool) (qll : list (list Q)) (l : list NuTree) : bool :=
some_true (map (fun x => tdec_all_true f x l) qll).
Fixpoint tdec phi nt q : bool :=
match nt with
| Tr a l => match (phi a) with
| None => tdec_some_true (tdec phi) (candsd1 q a) l
(* | None => some_true (map (fun x => all_true (map_pw (map (tdec phi) l) x)) (candsd1 q a)) *)
| Some q' => tdec_some_true (tdec phi) (candsd2 q q' a) l
(* | Some q' => some_true (map (fun x => all_true (map_pw (map (tdec phi) l) x)) (candsd2 q q' a)) *)
end
| Nu a nt => some_true (map (tdec (update phi a (Some q)) nt) (candsd3 q a))
end.
Lemma in_candsd1 q ql a :
ql el candsd1 q a <-> (q, a, ql) el D1 /\ |ql| = rk a.
Proof.
unfold candsd1. split.
- intros [[[q' b] ql'] [H4 [H5 H6] % in_filter_iff]] % in_map_iff.
rewrite Dec_reflect in H6. destruct H6 as [H6 [H7 H8]]. now subst.
- intros [H1 H2]. apply in_map_iff. exists (q,a,ql). split; trivial.
apply in_filter_iff. split; auto.
Qed.
Lemma in_candsd2 q q' ql a :
ql el candsd2 q q' a <-> (q, q', a, ql) el D2 /\ |ql| = rk a.
Proof.
unfold candsd2. split.
- intros [[[[q2 q1] b] ql'] [H4 [H5 H6] % in_filter_iff]] % in_map_iff.
rewrite Dec_reflect in H6. destruct H6 as [H6 [H7 [H8 H9]]]. now subst.
- intros [H1 H2]. apply in_map_iff. exists (q,q',a,ql). split; trivial.
apply in_filter_iff. split; auto.
Qed.
Lemma in_candsd3 q q' a :
q' el candsd3 q a <-> (q, a, q') el D3.
Proof.
unfold candsd3. split.
- intros [[[q2 b] ql] [H4 [H5 H6] % in_filter_iff ]] % in_map_iff.
rewrite Dec_reflect in H6. destruct H6 as [H6 H7]. now subst.
- intros H1. apply in_map_iff. exists (q,a,q'). split; trivial.
apply in_filter_iff. split; auto.
Qed.
Fact tdec_correct_1 phi nt q :
Ntwr nt -> tdec phi nt q = true -> NtaAccept q phi nt.
Proof.
unfold Q, s in *. intros HW. revert q phi. induction HW as [a l H1 H2 H3| a nt H1 H2]; intros q phi; simpl.
- destruct (phi a) as [q'|] eqn:E1; unfold tdec_some_true, tdec_all_true; intros [ql [H4 H5]] % some_true_true % in_map_iff.
+ apply in_candsd2 in H5 as [H5 H6].
apply AD2 with (q':=q')(ql:=ql); try assumption.
intros k H8. apply H2; auto. rewrite all_true_map_pw_map with (x:=DNT)(y:=q) in H4; intuition.
+ apply in_candsd1 in H5 as [H5 H6].
apply AD1 with (ql:=ql); try assumption.
intros k H8. apply H2; auto. rewrite all_true_map_pw_map with (x:=DNT)(y:=q) in H4; intuition.
- intros [q' [H4 H5]] % some_true_true % in_map_iff.
apply in_candsd3 in H5.
apply AD3 with (q':=q'); try assumption.
apply H2, H4.
Qed.
Fact tdec_correct_2 phi nt q :
Ntwr nt -> NtaAccept q phi nt -> tdec phi nt q = true.
Proof.
intros HW HA. induction HA as [q phi a l ql H1 H2 H3 H4 H5| q phi a l q' ql H1 H2 H3 H4 H5| q phi a nt' q' H1 H2 H3]; unfold Q, s in *; inversion HW; subst.
- simpl. destruct (phi a) as [q'|] eqn:E; try inversion H1 as [HQ].
unfold tdec_some_true, tdec_all_true.
apply some_true_true, in_map_iff. exists ql. split.
+ rewrite all_true_map_pw_map with (x:=DNT)(y:=q); intuition.
+ now apply in_candsd1.
- simpl. destruct (phi a) as [q''|] eqn:E; try inversion H1 as [HQ].
unfold tdec_some_true, tdec_all_true. apply some_true_true, in_map_iff.
exists ql. split.
+ rewrite all_true_map_pw_map with (x:=DNT)(y:=q); intuition.
+ now apply in_candsd2.
- simpl. apply some_true_true, in_map_iff. exists q'. split.
+ now apply H3.
+ now apply in_candsd3.
Qed.
Fact tdec_correct phi nt q :
Ntwr nt -> tdec phi nt q = true <-> NtaAccept q phi nt.
Proof.
intros HW. split.
- eauto using tdec_correct_1.
- eauto using tdec_correct_2.
Qed.
Fact dec_accept nt q phi :
Ntwr nt -> dec (NtaAccept q phi nt).
Proof.
intros HW1. destruct (tdec phi nt q) eqn:E.
- left. apply tdec_correct in E; assumption.
- right. intros H % tdec_correct; try assumption. rewrite E in H. auto.
Qed.
(* Q is finite. We create a list that contains all elements and try them all. *)
Definition states : list Q :=
let st1 := map (fun x => match x with (q,_,_) => q end) (D1) in
let st2 := map (fun x => match x with (q,_,_,_) => q end) (D2) in
let st3 := map (fun x => match x with (q,_,_) => q end) (D3) in
st1 ++ st2 ++ st3.
(*
Any accepting state is in the states list
*)
Lemma accept_in_states phi nt q :
NtaAccept q phi nt -> q el states.
Proof.
unfold states. inversion 1; apply in_app_iff.
- left. apply in_map_iff. exists (q, a, ql). auto.
- right. apply in_app_iff. left. apply in_map_iff. exists (q,q',a,ql). auto.
- right. apply in_app_iff. right. apply in_map_iff. exists (q,a,q'). auto.
Qed.
(*
Using this definition is nicer, because I never have to restrict myself
to states that actually appear in the automaton.
I can just quantify over all Q.
*)
Definition qlist n :=
nat_rec (fun n : nat => list (t n)) [] (fun (n : nat) (IHn : list (t n)) => F1 :: map FS IHn) n.
Lemma qlist_correct n (q : Q' n) :
q el qlist n.
Proof.
induction q; cbn.
- now left.
- right. apply in_map_iff. exists q. firstorder.
Qed.
Hint Resolve qlist_correct.
Definition tdec_s nt phi : bool :=
some_true (map (tdec phi nt) (qlist s)).
Fact tdec_s_correct_1 phi nt :
Ntwr nt -> tdec_s nt phi = true -> exists q, NtaAccept q phi nt.
Proof.
unfold tdec_s. intros HW [q [HA _]] % some_true_true % in_map_iff.
exists q. apply tdec_correct; assumption.
Qed.
Fact tdec_s_correct_2 nt phi :
Ntwr nt -> (exists q, NtaAccept q phi nt) -> tdec_s nt phi = true.
Proof.
intros HW [q HA]. unfold tdec_s. unfold Q, s in *.
apply some_true_true, in_map_iff. exists q. split; auto.
apply tdec_correct; assumption.
Qed.
Fact tdec_s_correct nt phi :
Ntwr nt -> tdec_s nt phi = true <-> exists q, NtaAccept q phi nt.
Proof.
intros HW. split.
- eauto using tdec_s_correct_1.
- eauto using tdec_s_correct_2.
Qed.
Fact dec_accept_s nt phi :
Ntwr nt -> dec (exists q, NtaAccept q phi nt).
Proof.
intros HW. destruct (tdec_s nt phi) eqn:E.
- left. apply tdec_s_correct in E; assumption.
- right. intros H % tdec_s_correct; try assumption. rewrite E in H. auto.
Qed.
(*
Phi only matters for the names in the automaton
*)
Lemma nta_swap_phi phi phi' q :
(forall a, a el nta_names -> phi a = phi' a) -> forall nt, NtaAccept q phi nt -> NtaAccept q phi' nt.
Proof.
intros HPhi nt HA. revert HPhi. revert phi'. induction HA; intros phi' HP.
- apply AD1 with (ql:=ql); auto.
rewrite <-(HP a); trivial. apply in_app_iff. left.
apply in_map_iff. exists (q,a,ql). split; trivial.
- apply AD2 with (ql:=ql)(q':=q'); auto.
rewrite <-(HP a); trivial. apply in_app_iff. right. apply in_app_iff.
left. apply in_map_iff. exists (q,q',a,ql). split; trivial.
- apply AD3 with (q':=q'); trivial. apply IHHA.
intros b H5. unfold update. decide(b=a); auto.
Qed.
Definition nonphi : Phi := fun _ => None.
Notation "f == g 'on' l" := (forall a, a el l -> f a = g a)(at level 60).
(*
The type for lists that represent phi functions.
Functionality is not required.
*)
Definition lPhi := list (Name * (option Q)).
Implicit Type lp : lPhi.
Implicit Type lps : list lPhi.
(*
Interpret a list of pairs as a function realizing those mappings.
Duplicate values in the first component overwrite each other.
On values that do not appear in the first component of some pair in the list,
the function returns a constant value.
*)
Fixpoint to_fun lp : Phi :=
match lp with
| [] => nonphi
| (b,q) :: r => update (to_fun r) b q
end.
(*
For a given name 'a' generate a list of pairs
of all values that 'a' could be assigned to.
*)
Definition all_assns a : list (Name * (option Q)) :=
(a, None) :: (map (fun x => (a, Some x)) (qlist s)).
(*
Extend a given list phi by all assignments of one name.
This is the function where all the "copying" takes place.
*)
Definition all_conts a lp : list lPhi :=
map (fun x => x :: lp) (all_assns a).
(*
Extend a list of list phis by all assignments of one name
*)
Definition step_var a lps : list lPhi :=
concat (map (all_conts a) lps).
(*
Build up the list of all list phis by accumulating a list of list phis
and extending them by the names in l by folding over l.
*)
Fixpoint all_phis' (l : list Name) : (list lPhi) :=
match l with
| [] => [[]]
| a :: r => step_var a (all_phis' r)
end.
Definition all_phis : (list lPhi) :=
all_phis' (nta_names).
(*
lp is like a partial function.
Extending it by one name is in all_phis if that name is added.
*)
Lemma step_var_in_all a (q : option Q) l lp :
lp el all_phis' l -> (a, q) :: lp el all_phis' (a :: l).
Proof.
simpl. intros H1. unfold step_var.
apply concat_el. exists (all_conts a lp). split.
- simpl. destruct q as [q|]; auto.
right. apply in_map_iff. exists (a, Some q). split; try reflexivity.
apply in_map_iff. exists q. split; auto.
- apply in_map_iff. exists lp. split; auto.
Qed.
Lemma step_var_agree phi (q : option Q) lp a l :
phi == (to_fun lp) on l -> phi a = q -> phi == to_fun ((a, q) :: lp) on (a :: l).
Proof.
intros H1 H2 b [H3|H3]; simpl; unfold update; solve_dec. apply H1, H3.
Qed.
(*
This is the key lemma for decidability:
For ((all)) functions phi, there is a list of pairs in all_phis
that behaves the same as phi on nta_names.
So this is the lemma that reduces the infinite function space
to a finite list of mappings.
*)
Fact lphi_alt' phi :
{ lp | lp el all_phis /\ phi == (to_fun lp) on nta_names}.
Proof.
unfold all_phis. induction nta_names.
- simpl. exists []. split; auto.
- destruct IHl as [lp [H1 H2]]. exists ((a, phi a)::lp). split.
+ apply step_var_in_all; assumption.
+ apply step_var_agree; trivial.
Qed.
(*
Using the fact above, there is a list of mappings in all_phis
that preserves acceptance when interpreted as a function.
*)
Lemma lphi_alt phi nt q :
NtaAccept q phi nt -> exists l, l el all_phis /\ NtaAccept q (to_fun l) nt.
Proof.
intros H1.
destruct (lphi_alt' phi) as [lp [H2 H3]].
exists lp. split; try assumption. apply nta_swap_phi with (phi:=phi); assumption.
Qed.
Definition tdec_p nt : bool :=
some_true (map (tdec_s nt) (map (to_fun) (all_phis))).
Fact tdec_p_correct_1 nt :
Ntwr nt -> tdec_p nt = true -> (exists phi q, NtaAccept q phi nt).
Proof.
unfold tdec_p. rewrite some_true_true.
intros H1 [phi [[q [H2 H3]] % some_true_true % in_map_iff H4]] % in_map_iff.
exists phi. exists q. apply tdec_correct; assumption.
Qed.
Fact tdec_p_correct_2 nt :
Ntwr nt -> (exists phi q, NtaAccept q phi nt) -> tdec_p nt = true.
Proof.
intros HW [phi [q HA]].
assert(HP: exists lp, lp el (all_phis) /\ NtaAccept q (to_fun lp) nt). {
apply lphi_alt in HA as [l [H1 H2]]. exists l. split; assumption.
}
unfold tdec_p. apply some_true_true, in_map_iff.
destruct HP as [lp [H1 H2]]. exists (to_fun lp). split.
- apply some_true_true. unfold Q, s in *. apply in_map_iff. exists q. split; auto.
apply tdec_correct; assumption.
- apply in_map_iff. exists lp. split; auto.
Qed.
Fact tdec_p_correct nt :
Ntwr nt -> tdec_p nt = true <-> (exists phi q, NtaAccept q phi nt).
Proof.
intros HW. split.
- eauto using tdec_p_correct_1.
- eauto using tdec_p_correct_2.
Qed.
Fact dec_accept_p nt :
Ntwr nt -> dec (exists phi q, NtaAccept q phi nt).
Proof.
intros HW. destruct (tdec_p nt) eqn:E.
- left. apply tdec_p_correct in E; assumption.
- right. intros H % tdec_p_correct; try assumption. rewrite E in H. auto.
Qed.
Lemma nta_accept_has_name a nt q phi :
NtaAccept q phi (Nu a nt) -> a el nta_names.
Proof.
intros H1. unfold nta_names. inversion H1. subst. apply in_app_iff. right.
apply in_app_iff. right. apply in_map_iff.
exists (q, a, q'). split; trivial.
Qed.
(*
If the automaton accepts a nu-tree,
then there is an equivalent nu-tree
which is not accepted.
We construct an empty binding for which there is no transition.
*)
Fact nta_ntl_reject nt q phi A :
Ntwr nt -> NtaAccept q phi nt -> exists nt', NtlEq A nt nt' /\ ~NtaAccept q phi nt'.
Proof.
intros H1 H2.
pose(f := fresh' (nta_names ++ nt_names nt) 0).
assert(HF : ~ f el nta_names ++ nt_names nt) by apply freshness'.
exists (Nu f nt). split.
- intros t. split; apply ntl_nu_indep; auto; intros H3 % free_in_names; auto.
- intros H3 % nta_accept_has_name. apply HF, in_app_iff. now left.
Qed.
(*
For any NTA there is a nu-tree that is not accepted.
This is essentially because of the global infinite alphabet.
*)
Fact nta_ntl_reject' q phi :
exists nt, ~NtaAccept q phi nt.
Proof.
assert(H: Ntwr DNT). { unfold DNT. auto. }
destruct (dec_accept q phi H) as [E|E].
- destruct (nta_ntl_reject [] H E) as [nt [_ E2]]. now exists nt.
- now exists DNT.
Qed.