Set Implicit Arguments.
Require Import Coq.Init.Nat.
Require Import Coq.Arith.Even.
Require Import Coq.Arith.Div2.
Require Import BasicDefs.
Require Import Seqs.
Require Import FinType.
Require Import Ramsey.
Require Import NFAs.
Require Import RegularLanguages.
Require Import Buechi.
Require Import Complement.
Require Import ASStructures.
Require Import AbstractMSO.
Require Import Coq.Init.Nat.
Require Import Coq.Arith.Even.
Require Import Coq.Arith.Div2.
Require Import BasicDefs.
Require Import Seqs.
Require Import FinType.
Require Import Ramsey.
Require Import NFAs.
Require Import RegularLanguages.
Require Import Buechi.
Require Import Complement.
Require Import ASStructures.
Require Import AbstractMSO.
Section SpecialSeqOperations.
Context {CC: SequenceStructure}.
Context {A:finType}{X:eqType}.
Definition narrowASeq {l_1 l_2 : list X} (P: l_2 <<= l_1)(w: ASeq (A^^ l_1)) : (ASeq (A^^l_2)) := amap (narrowVector P) w.
Definition joinASeq (l: list X) x (w: ASeq (A^^ (rem l x))) (a: ASeq A): ASeq (A^^l) := amap (join (c:=x)) (azip w a).
Lemma joinASeq_correct_new (l: list X) x (P: x el l) (w:ASeq (A ^^(rem l x))) a: aseq_to_seq (bigpi (joinASeq w a) (toFinTypeFromList P)) === aseq_to_seq a.
Proof.
unfold joinASeq. intros n. rewrite bigpi_correct, amap_correct. unfold seq_map.
rewrite azip_correct. unfold seq_zip. apply join_fst.
Qed.
Lemma joinASeq_correct_old (l: list X) x (w: ASeq (A^^(rem l x))) (a: ASeq A):
forall (y:X) (Q: y el l)(Q': y el (rem l x)), aseq_to_seq (bigpi (joinASeq w a) (toFinTypeFromList Q)) === aseq_to_seq (bigpi w (toFinTypeFromList Q')).
Proof.
intros y Q Q'. unfold joinASeq. intros n. rewrite 2bigpi_correct, amap_correct. unfold seq_map.
rewrite azip_correct. unfold seq_zip. apply join_snd.
Qed.
End SpecialSeqOperations.
Section ListProjection.
Context {AC: AdmissibleSequenceStructure}.
Context {B:finType}{C:eqType} {l:list C} (c:C) (aut: NFA (B^^l)).
Definition LAproj_list (L : Language (ASeq (B^^l))) : Language (ASeq (B^^(rem l c))) :=
fun w => match (decision (c el l)) with
| left _ => exists w', L (joinASeq w w')
| right M => L (amap (convRemInv M) w)
end.
Lemma LA_proj_list_equiv_image (L : Language (ASeq (B^^l))) : (forall w w', aseq_to_seq w === aseq_to_seq w' -> L w -> L w') -> LAproj_list L =$= LAmap (separate c) L.
Proof.
intros Ext. unfold LAproj_list, LAmap. intros w. destruct decision as [M|M]; split.
- intros [w' P]. exists (joinASeq w w'); split; auto.
intros n. rewrite amap_correct. unfold seq_map. unfold joinASeq. rewrite amap_correct. unfold seq_map.
rewrite azip_correct. unfold seq_zip. now rewrite inv_separate_join.
- intros [w' [E P]]. exists (amap (rest M) w'). apply (Ext w' ); auto.
unfold joinASeq. intros n. rewrite !amap_correct. unfold seq_map. rewrite azip_correct. unfold seq_zip. rewrite <-E, !amap_correct. unfold seq_map. now rewrite inv_join_separate.
- intros P. exists (amap (convRemInv M) w). split; auto. intros n.
rewrite amap_correct. unfold seq_map. rewrite amap_correct. unfold seq_map. now rewrite separate_unchanged.
- intros [w' [E P]]. apply (Ext w'); auto.
intros n. rewrite amap_correct. unfold seq_map. rewrite <-E. rewrite amap_correct. unfold seq_map. now rewrite convRemInv_correct'.
Qed.
Definition list_proj_aut := image_aut (separate c) aut.
Lemma projection_list_aclosed : L_A list_proj_aut =$= LAproj_list (L_A aut).
Proof.
unfold list_proj_aut. rewrite LA_proj_list_equiv_image, map_aut_acorrect. reflexivity.
intros w w' E. unfold L_A. now rewrite E.
Qed.
End ListProjection.
Instance NatSetFromSeq (CC : SequenceStructure) : NatSetClass := {|
NatSet := ASeq finType_bool;
memSet := fun n M => (aseq_to_seq M) n = true;
singletonSet := fun n => exact_at true false n
|}.
- intros n. now apply exact_at_correct.
- now intros n m E % exact_at_correct.
Defined.
Section MSOtoBuechi.
Context {AC: AdmissibleSequenceStructure}.
Context {CC: SequenceStructure}.
Context {A:finType}{X:eqType}.
Definition narrowASeq {l_1 l_2 : list X} (P: l_2 <<= l_1)(w: ASeq (A^^ l_1)) : (ASeq (A^^l_2)) := amap (narrowVector P) w.
Definition joinASeq (l: list X) x (w: ASeq (A^^ (rem l x))) (a: ASeq A): ASeq (A^^l) := amap (join (c:=x)) (azip w a).
Lemma joinASeq_correct_new (l: list X) x (P: x el l) (w:ASeq (A ^^(rem l x))) a: aseq_to_seq (bigpi (joinASeq w a) (toFinTypeFromList P)) === aseq_to_seq a.
Proof.
unfold joinASeq. intros n. rewrite bigpi_correct, amap_correct. unfold seq_map.
rewrite azip_correct. unfold seq_zip. apply join_fst.
Qed.
Lemma joinASeq_correct_old (l: list X) x (w: ASeq (A^^(rem l x))) (a: ASeq A):
forall (y:X) (Q: y el l)(Q': y el (rem l x)), aseq_to_seq (bigpi (joinASeq w a) (toFinTypeFromList Q)) === aseq_to_seq (bigpi w (toFinTypeFromList Q')).
Proof.
intros y Q Q'. unfold joinASeq. intros n. rewrite 2bigpi_correct, amap_correct. unfold seq_map.
rewrite azip_correct. unfold seq_zip. apply join_snd.
Qed.
End SpecialSeqOperations.
Section ListProjection.
Context {AC: AdmissibleSequenceStructure}.
Context {B:finType}{C:eqType} {l:list C} (c:C) (aut: NFA (B^^l)).
Definition LAproj_list (L : Language (ASeq (B^^l))) : Language (ASeq (B^^(rem l c))) :=
fun w => match (decision (c el l)) with
| left _ => exists w', L (joinASeq w w')
| right M => L (amap (convRemInv M) w)
end.
Lemma LA_proj_list_equiv_image (L : Language (ASeq (B^^l))) : (forall w w', aseq_to_seq w === aseq_to_seq w' -> L w -> L w') -> LAproj_list L =$= LAmap (separate c) L.
Proof.
intros Ext. unfold LAproj_list, LAmap. intros w. destruct decision as [M|M]; split.
- intros [w' P]. exists (joinASeq w w'); split; auto.
intros n. rewrite amap_correct. unfold seq_map. unfold joinASeq. rewrite amap_correct. unfold seq_map.
rewrite azip_correct. unfold seq_zip. now rewrite inv_separate_join.
- intros [w' [E P]]. exists (amap (rest M) w'). apply (Ext w' ); auto.
unfold joinASeq. intros n. rewrite !amap_correct. unfold seq_map. rewrite azip_correct. unfold seq_zip. rewrite <-E, !amap_correct. unfold seq_map. now rewrite inv_join_separate.
- intros P. exists (amap (convRemInv M) w). split; auto. intros n.
rewrite amap_correct. unfold seq_map. rewrite amap_correct. unfold seq_map. now rewrite separate_unchanged.
- intros [w' [E P]]. apply (Ext w'); auto.
intros n. rewrite amap_correct. unfold seq_map. rewrite <-E. rewrite amap_correct. unfold seq_map. now rewrite convRemInv_correct'.
Qed.
Definition list_proj_aut := image_aut (separate c) aut.
Lemma projection_list_aclosed : L_A list_proj_aut =$= LAproj_list (L_A aut).
Proof.
unfold list_proj_aut. rewrite LA_proj_list_equiv_image, map_aut_acorrect. reflexivity.
intros w w' E. unfold L_A. now rewrite E.
Qed.
End ListProjection.
Instance NatSetFromSeq (CC : SequenceStructure) : NatSetClass := {|
NatSet := ASeq finType_bool;
memSet := fun n M => (aseq_to_seq M) n = true;
singletonSet := fun n => exact_at true false n
|}.
- intros n. now apply exact_at_correct.
- now intros n m E % exact_at_correct.
Defined.
Section MSOtoBuechi.
Context {AC: AdmissibleSequenceStructure}.
Definition interToSeq (L: list SVar) (I: SInter) : ASeq (finType_bool ^^ L) :=
bigzip (fun l => (I (fromFinTypeFromList (C:=EqType SVar) l))).
Definition seqToInter (L: list SVar) (w : ASeq (finType_bool ^^ L)) : SInter:=
fun X => match (decision (X el L)) with
|left D => (bigpi w (toFinTypeFromList D))
|right _ => singletonSet 0 end.
Lemma set_equivalent_iff_seq_extensional (M N : NatSet) : aseq_to_seq M === aseq_to_seq N <-> M =~= N.
Proof.
split.
- intros E n. unfold memSet. simpl. now rewrite E.
- intros E n. specialize (E n). unfold memSet in *. simpl in *. destruct (aseq_to_seq M n) eqn:H.
+ symmetry. now apply E.
+ destruct (aseq_to_seq N n) eqn:H'; tauto.
Qed.
Lemma inter_to_seq_to_inter_correct (L: list SVar) (I : SInter): forall X, X el L -> I X =~= (seqToInter (interToSeq L I)) X.
Proof.
intros X E. unfold seqToInter, interToSeq. decide (X el L).
- simpl. apply set_equivalent_iff_seq_extensional. intros n. now rewrite bigpi_correct, bigzip_correct.
- now exfalso.
Qed.
Definition formula_language : forall (s:FormMin) , Language (ASeq (finType_bool ^^ (free_vars s))) :=
fun (s:FormMin) v => (seqToInter v) |= s.
Arguments formula_language s v : clear implicits.
Notation "'L_M' " := formula_language .
Lemma formula_language_complete s I : I |= s -> L_M s (interToSeq (free_vars s) I).
Proof.
unfold formula_language. apply coincidence.
intros X F. now apply inter_to_seq_to_inter_correct.
Qed.
Lemma narrow_to_free_vars (L: list SVar) (s:FormMin)(P: free_vars s <<= L) (w: ASeq (finType_bool ^ (finType_fromList L))) :
forall X, X el (free_vars s) -> seqToInter(narrowASeq P w) X =~= seqToInter w X.
Proof.
intros X E. unfold seqToInter. repeat (destruct decision); try (exfalso; now auto).
intros n. unfold memSet. simpl. rewrite !bigpi_correct. split; intros F; rewrite <-F; unfold toFinTypeFromList, narrowASeq;
rewrite amap_correct; unfold narrowVector, seq_map, toFinTypeFromList; rewrite apply_vectorise_inverse; f_equal; f_equal; apply pure_eq.
Qed.
Lemma zip_existential s (X: SVar) (w: ASeq (finType_bool ^^ (free_vars (ex0 X, s)))) M: forall Y, Y el free_vars s -> seqToInter (joinASeq w M) Y =~= (seqToInter w) [X:=M] Y.
Proof.
intros Y El. apply set_equivalent_iff_seq_extensional. destruct decision.
- subst Y. unfold seqToInter. destruct decision; (try (exfalso; now auto)). now rewrite joinASeq_correct_new.
- unfold seqToInter. destruct decision; (try (exfalso; now auto)). cbn. destruct decision as [D|D].
+ now rewrite joinASeq_correct_old.
+ exfalso. apply D. apply in_rem_iff. auto.
Qed.
bigzip (fun l => (I (fromFinTypeFromList (C:=EqType SVar) l))).
Definition seqToInter (L: list SVar) (w : ASeq (finType_bool ^^ L)) : SInter:=
fun X => match (decision (X el L)) with
|left D => (bigpi w (toFinTypeFromList D))
|right _ => singletonSet 0 end.
Lemma set_equivalent_iff_seq_extensional (M N : NatSet) : aseq_to_seq M === aseq_to_seq N <-> M =~= N.
Proof.
split.
- intros E n. unfold memSet. simpl. now rewrite E.
- intros E n. specialize (E n). unfold memSet in *. simpl in *. destruct (aseq_to_seq M n) eqn:H.
+ symmetry. now apply E.
+ destruct (aseq_to_seq N n) eqn:H'; tauto.
Qed.
Lemma inter_to_seq_to_inter_correct (L: list SVar) (I : SInter): forall X, X el L -> I X =~= (seqToInter (interToSeq L I)) X.
Proof.
intros X E. unfold seqToInter, interToSeq. decide (X el L).
- simpl. apply set_equivalent_iff_seq_extensional. intros n. now rewrite bigpi_correct, bigzip_correct.
- now exfalso.
Qed.
Definition formula_language : forall (s:FormMin) , Language (ASeq (finType_bool ^^ (free_vars s))) :=
fun (s:FormMin) v => (seqToInter v) |= s.
Arguments formula_language s v : clear implicits.
Notation "'L_M' " := formula_language .
Lemma formula_language_complete s I : I |= s -> L_M s (interToSeq (free_vars s) I).
Proof.
unfold formula_language. apply coincidence.
intros X F. now apply inter_to_seq_to_inter_correct.
Qed.
Lemma narrow_to_free_vars (L: list SVar) (s:FormMin)(P: free_vars s <<= L) (w: ASeq (finType_bool ^ (finType_fromList L))) :
forall X, X el (free_vars s) -> seqToInter(narrowASeq P w) X =~= seqToInter w X.
Proof.
intros X E. unfold seqToInter. repeat (destruct decision); try (exfalso; now auto).
intros n. unfold memSet. simpl. rewrite !bigpi_correct. split; intros F; rewrite <-F; unfold toFinTypeFromList, narrowASeq;
rewrite amap_correct; unfold narrowVector, seq_map, toFinTypeFromList; rewrite apply_vectorise_inverse; f_equal; f_equal; apply pure_eq.
Qed.
Lemma zip_existential s (X: SVar) (w: ASeq (finType_bool ^^ (free_vars (ex0 X, s)))) M: forall Y, Y el free_vars s -> seqToInter (joinASeq w M) Y =~= (seqToInter w) [X:=M] Y.
Proof.
intros Y El. apply set_equivalent_iff_seq_extensional. destruct decision.
- subst Y. unfold seqToInter. destruct decision; (try (exfalso; now auto)). now rewrite joinASeq_correct_new.
- unfold seqToInter. destruct decision; (try (exfalso; now auto)). cbn. destruct decision as [D|D].
+ now rewrite joinASeq_correct_old.
+ exfalso. apply D. apply in_rem_iff. auto.
Qed.
Section BaseNFAs.
Variables (X Y : SVar).
Notation "'A'" := (finType_bool ^^ [X;Y]).
Close Scope list_scope.
Open Scope string_scope.
Lemma XinA : X el free_vars (X <0 Y). Proof. simpl. auto. Qed.
Lemma YinA : Y el free_vars (X <0 Y). Proof. simpl. auto. Qed.
Definition getX (a:A) := applyVect a (toFinTypeFromList XinA).
Definition getY (a:A) := applyVect a (toFinTypeFromList YinA).
Lemma seqToInterGetX (v:ASeq A) n : n elS (seqToInter v X) <-> getX (aseq_to_seq v n) = true.
Proof.
unfold memSet, seqToInter, getX. destruct decision as [D|D].
- rewrite <-bigpi_correct. now rewrite (toFinTypeFromListEq XinA D).
- exfalso. apply D. simpl. auto.
Qed.
Lemma seqToInterGetY (v:ASeq A) n : n elS (seqToInter v Y) <-> getY (aseq_to_seq v n) = true.
Proof.
unfold memSet, seqToInter, getY. destruct decision as [D|D].
- rewrite <-bigpi_correct. now rewrite (toFinTypeFromListEq YinA D).
- exfalso. apply D. simpl. auto.
Qed.
Definition constSeq (X:Type) x : Seq X:= fun _ => x.
Definition constStr (X:Type) x k : String X := mkstring (constSeq x) k.
Variables (X Y : SVar).
Notation "'A'" := (finType_bool ^^ [X;Y]).
Close Scope list_scope.
Open Scope string_scope.
Lemma XinA : X el free_vars (X <0 Y). Proof. simpl. auto. Qed.
Lemma YinA : Y el free_vars (X <0 Y). Proof. simpl. auto. Qed.
Definition getX (a:A) := applyVect a (toFinTypeFromList XinA).
Definition getY (a:A) := applyVect a (toFinTypeFromList YinA).
Lemma seqToInterGetX (v:ASeq A) n : n elS (seqToInter v X) <-> getX (aseq_to_seq v n) = true.
Proof.
unfold memSet, seqToInter, getX. destruct decision as [D|D].
- rewrite <-bigpi_correct. now rewrite (toFinTypeFromListEq XinA D).
- exfalso. apply D. simpl. auto.
Qed.
Lemma seqToInterGetY (v:ASeq A) n : n elS (seqToInter v Y) <-> getY (aseq_to_seq v n) = true.
Proof.
unfold memSet, seqToInter, getY. destruct decision as [D|D].
- rewrite <-bigpi_correct. now rewrite (toFinTypeFromListEq YinA D).
- exfalso. apply D. simpl. auto.
Qed.
Definition constSeq (X:Type) x : Seq X:= fun _ => x.
Definition constStr (X:Type) x k : String X := mkstring (constSeq x) k.
NFA for X <<=' Y
Section InclusionNFA.
Definition incl_state := finType_bool.
Notation "'InclS'" := true .
Notation "'NotInclS'" := false.
Definition incl_transition (s: incl_state) (a: A) (s' : incl_state) := match s with
| NotInclS => s' = NotInclS
| InclS => if (getX a)
then if (getY a) then s' = InclS else s' = NotInclS
else s' = InclS
end.
Instance dec_incl_transition s a s' : dec (incl_transition s a s').
Proof.
unfold incl_transition. destruct s , s' , (getX a), (getY a); auto.
Qed.
Definition incl_nfa : NFA (finType_bool ^^ (free_vars (X <<=0 Y))) := mknfa incl_transition (fun s => s = InclS) (fun s => s = InclS).
Lemma accepting_applies_incl: L_A incl_nfa <$= L_M (X <<=0 Y).
Proof.
intros v [r [V [I F]]].
assert (r === constSeq InclS) as H. {
intros n. induction n; auto. unfold constSeq in *. pose proof(V n) as V'. rewrite IHn in V'. cbn in V'.
destruct getX; auto. destruct getY; auto.
exfalso. destruct (F (S n)) as [m [G F']]. cbn in F'. enough (r m = NotInclS) by congruence.
clear F'. induction G; auto. specialize (V m). now rewrite IHG in V.
}
intros n IX % seqToInterGetX. specialize (V n). rewrite !H in V. cbn in V. rewrite IX in V.
apply seqToInterGetY. destruct getY; auto.
Qed.
Lemma incl_implies_accepting: L_M (X <<=0 Y) <$= L_A incl_nfa.
Proof.
intros v Inc. exists (constSeq InclS). repeat split.
- intros n. cbn. destruct getX eqn:HX; auto. destruct getY eqn : HY; auto.
exfalso. specialize(Inc n). apply seqToInterGetX in HX. specialize (Inc HX).
apply seqToInterGetY in Inc. congruence.
- intros n. exists n. split; oauto. reflexivity.
Qed.
Lemma incl_nfa_correct : L_A incl_nfa=$= L_M (X <<=0 Y).
Proof.
split; auto using incl_implies_accepting, accepting_applies_incl.
Qed.
End InclusionNFA.
Definition incl_state := finType_bool.
Notation "'InclS'" := true .
Notation "'NotInclS'" := false.
Definition incl_transition (s: incl_state) (a: A) (s' : incl_state) := match s with
| NotInclS => s' = NotInclS
| InclS => if (getX a)
then if (getY a) then s' = InclS else s' = NotInclS
else s' = InclS
end.
Instance dec_incl_transition s a s' : dec (incl_transition s a s').
Proof.
unfold incl_transition. destruct s , s' , (getX a), (getY a); auto.
Qed.
Definition incl_nfa : NFA (finType_bool ^^ (free_vars (X <<=0 Y))) := mknfa incl_transition (fun s => s = InclS) (fun s => s = InclS).
Lemma accepting_applies_incl: L_A incl_nfa <$= L_M (X <<=0 Y).
Proof.
intros v [r [V [I F]]].
assert (r === constSeq InclS) as H. {
intros n. induction n; auto. unfold constSeq in *. pose proof(V n) as V'. rewrite IHn in V'. cbn in V'.
destruct getX; auto. destruct getY; auto.
exfalso. destruct (F (S n)) as [m [G F']]. cbn in F'. enough (r m = NotInclS) by congruence.
clear F'. induction G; auto. specialize (V m). now rewrite IHG in V.
}
intros n IX % seqToInterGetX. specialize (V n). rewrite !H in V. cbn in V. rewrite IX in V.
apply seqToInterGetY. destruct getY; auto.
Qed.
Lemma incl_implies_accepting: L_M (X <<=0 Y) <$= L_A incl_nfa.
Proof.
intros v Inc. exists (constSeq InclS). repeat split.
- intros n. cbn. destruct getX eqn:HX; auto. destruct getY eqn : HY; auto.
exfalso. specialize(Inc n). apply seqToInterGetX in HX. specialize (Inc HX).
apply seqToInterGetY in Inc. congruence.
- intros n. exists n. split; oauto. reflexivity.
Qed.
Lemma incl_nfa_correct : L_A incl_nfa=$= L_M (X <<=0 Y).
Proof.
split; auto using incl_implies_accepting, accepting_applies_incl.
Qed.
End InclusionNFA.
NFA for X <' Y
Section LessNFA.
Definition less_state := ? (finType_bool).
Notation "'SearchX'" := None.
Notation "'SearchY'" := (Some false).
Notation "'Less'" := (Some true).
Definition less_transition (s: less_state) (a: A) (s': less_state) := match s with
| SearchX => (s' = SearchX) \/ (getX a = true /\ s' = SearchY) (*if (getX a) then s' = SearchY else s' = SearchX *)
| SearchY => (s' = SearchY) \/ (getY a = true /\ s' = Less) (*if (getY a) then s' = Less else s' = SearchY *)
| Less => s' = Less
end.
Instance dec_less_transition s a s': dec (less_transition s a s').
Proof.
destruct s as [[|]|]; destruct s' as [[|]|]; unfold less_transition; destruct (getY a), (getX a); auto.
Qed.
Definition less_nfa : NFA (finType_bool ^ (finType_fromList (free_vars (X <0 Y)))) := mknfa less_transition (fun s => s = SearchX) (fun s => s = Less).
Lemma accepting_run_search_Y r w n: initial r -> valid_run (aut:=less_nfa) r w -> r n = SearchY -> exists m, 0 < m <= n/\ r m = SearchY /\ forall k, k < m -> r k = SearchX.
Proof.
intros I V SY. assert (0 <= n) as H by omega. change ( (fun s => s = SearchY) (r n)) in SY.
exists (next_position H SY). repeat split.
- decide (0 < next_position H SY); auto.
exfalso. compute in I. enough (r 0 = SearchY) by congruence.
rewrite_eq (0 = next_position H SY). apply next_position_correct.
- pose proof (next_position_bounds H SY). omega.
- apply next_position_correct.
- intros k L. induction k.
+ apply I.
+ specialize (V k). rewrite (IHk) in V by omega. simpl in V. destruct V as [V|[V1 V2]]; auto.
exfalso. apply (next_position_all (j := S k) (L:=H) (F:=SY)); oauto.
Qed.
Lemma accepting_run_less r w n: initial r -> valid_run (aut:=less_nfa) r w -> r n = Less -> exists m_2 m_1 , 0 < m_1 /\ m_1 < m_2 <= n/\ r m_1 = SearchY /\ (forall k, k < m_1 -> r k = SearchX) /\ (forall k, m_1 <= k < m_2 -> r k = SearchY) /\ r m_2 = Less.
Proof.
intros I V L. assert (0 <= n) as H by omega. change ( (fun s => s = Less) (r n)) in L.
exists (next_position H L).
remember (next_position H L) as m_2.
assert (m_2 > 0). { decide (m_2 = 0)as [D|D]; oauto. exfalso. cbn in I. rewrite <-D in I.
enough (r m_2 = Less) by congruence. subst m_2. apply next_position_correct. }
assert (r (pred m_2) = SearchY) as H1. {
specialize (V (pred m_2)). rewrite_eq (S (pred (m_2)) = m_2) in V. cbn in V. subst m_2.
rewrite (next_position_correct H L) in V. destruct (r (pred (next_position H L))) as [[|]|] eqn:H'; cbn in V; auto.
- exfalso. apply (next_position_all (j := (pred (next_position H L))) (L:=H) (F:=L)); oauto.
- exfalso. destruct V as [V|[_ V]]; congruence. }
destruct (accepting_run_search_Y I V H1) as [m_1 [P_1 [Q_1 T_1]]].
exists m_1. repeat split; oauto; subst m_2.
- apply next_position_bounds.
- intros k [B1 B2]. induction B1; auto. specialize (V m). rewrite IHB1 in V by omega. cbn in V. destruct V as [V|[V1 V2]]; auto.
exfalso. apply (next_position_all (j := S m) (L:=H) (F:=L)); oauto.
- apply next_position_correct.
Qed.
Lemma accepting_implies_less: L_A less_nfa <$= L_M (X <0 Y).
Proof.
intros v [r [V [I F]]].
destruct (F 0) as [n [P Q]].
destruct (accepting_run_less I V Q) as [m_2 [m_1 [P_1 [P_2 [P_3 [P_4 [P_5 P_6]]]]]]].
exists (pred m_1), (pred m_2). repeat split; oauto.
- apply seqToInterGetX. specialize (V (pred m_1)). rewrite_eq (S (pred m_1) = m_1) in V.
rewrite P_3, P_4 in V by omega. cbn in V. now destruct V.
- apply seqToInterGetY. specialize (V (pred m_2)). rewrite_eq (S (pred m_2) = m_2) in V.
rewrite P_6, P_5 in V by omega. cbn in V. now destruct V.
Qed.
Lemma less_implies_accepting: L_M (X <0 Y) <$= L_A less_nfa.
Proof.
intros v [ n [m [EN [EM L]]]]. exists (fun k => if (decision (k <= n)) then SearchX else (if (decision (k <= m)) then SearchY else Less)). repeat split.
- intros k. destruct decision as [D|D].
+ destruct decision as [D'|D']; cbn; trivial_decision; auto.
right. split; auto. apply seqToInterGetX. now rewrite_eq (k = n).
+ destruct decision; cbn; trivial_decision; auto.
destruct decision; auto. right. split; auto. apply seqToInterGetY. now rewrite_eq (k = m).
- intros k. exists (m + S k). split; oauto. now trivial_decision.
Qed.
Lemma less_nfa_correct : L_A less_nfa =$= L_M (X <0 Y).
Proof.
split; auto using less_implies_accepting, accepting_implies_less.
Qed.
End LessNFA.
End BaseNFAs.
Definition less_state := ? (finType_bool).
Notation "'SearchX'" := None.
Notation "'SearchY'" := (Some false).
Notation "'Less'" := (Some true).
Definition less_transition (s: less_state) (a: A) (s': less_state) := match s with
| SearchX => (s' = SearchX) \/ (getX a = true /\ s' = SearchY) (*if (getX a) then s' = SearchY else s' = SearchX *)
| SearchY => (s' = SearchY) \/ (getY a = true /\ s' = Less) (*if (getY a) then s' = Less else s' = SearchY *)
| Less => s' = Less
end.
Instance dec_less_transition s a s': dec (less_transition s a s').
Proof.
destruct s as [[|]|]; destruct s' as [[|]|]; unfold less_transition; destruct (getY a), (getX a); auto.
Qed.
Definition less_nfa : NFA (finType_bool ^ (finType_fromList (free_vars (X <0 Y)))) := mknfa less_transition (fun s => s = SearchX) (fun s => s = Less).
Lemma accepting_run_search_Y r w n: initial r -> valid_run (aut:=less_nfa) r w -> r n = SearchY -> exists m, 0 < m <= n/\ r m = SearchY /\ forall k, k < m -> r k = SearchX.
Proof.
intros I V SY. assert (0 <= n) as H by omega. change ( (fun s => s = SearchY) (r n)) in SY.
exists (next_position H SY). repeat split.
- decide (0 < next_position H SY); auto.
exfalso. compute in I. enough (r 0 = SearchY) by congruence.
rewrite_eq (0 = next_position H SY). apply next_position_correct.
- pose proof (next_position_bounds H SY). omega.
- apply next_position_correct.
- intros k L. induction k.
+ apply I.
+ specialize (V k). rewrite (IHk) in V by omega. simpl in V. destruct V as [V|[V1 V2]]; auto.
exfalso. apply (next_position_all (j := S k) (L:=H) (F:=SY)); oauto.
Qed.
Lemma accepting_run_less r w n: initial r -> valid_run (aut:=less_nfa) r w -> r n = Less -> exists m_2 m_1 , 0 < m_1 /\ m_1 < m_2 <= n/\ r m_1 = SearchY /\ (forall k, k < m_1 -> r k = SearchX) /\ (forall k, m_1 <= k < m_2 -> r k = SearchY) /\ r m_2 = Less.
Proof.
intros I V L. assert (0 <= n) as H by omega. change ( (fun s => s = Less) (r n)) in L.
exists (next_position H L).
remember (next_position H L) as m_2.
assert (m_2 > 0). { decide (m_2 = 0)as [D|D]; oauto. exfalso. cbn in I. rewrite <-D in I.
enough (r m_2 = Less) by congruence. subst m_2. apply next_position_correct. }
assert (r (pred m_2) = SearchY) as H1. {
specialize (V (pred m_2)). rewrite_eq (S (pred (m_2)) = m_2) in V. cbn in V. subst m_2.
rewrite (next_position_correct H L) in V. destruct (r (pred (next_position H L))) as [[|]|] eqn:H'; cbn in V; auto.
- exfalso. apply (next_position_all (j := (pred (next_position H L))) (L:=H) (F:=L)); oauto.
- exfalso. destruct V as [V|[_ V]]; congruence. }
destruct (accepting_run_search_Y I V H1) as [m_1 [P_1 [Q_1 T_1]]].
exists m_1. repeat split; oauto; subst m_2.
- apply next_position_bounds.
- intros k [B1 B2]. induction B1; auto. specialize (V m). rewrite IHB1 in V by omega. cbn in V. destruct V as [V|[V1 V2]]; auto.
exfalso. apply (next_position_all (j := S m) (L:=H) (F:=L)); oauto.
- apply next_position_correct.
Qed.
Lemma accepting_implies_less: L_A less_nfa <$= L_M (X <0 Y).
Proof.
intros v [r [V [I F]]].
destruct (F 0) as [n [P Q]].
destruct (accepting_run_less I V Q) as [m_2 [m_1 [P_1 [P_2 [P_3 [P_4 [P_5 P_6]]]]]]].
exists (pred m_1), (pred m_2). repeat split; oauto.
- apply seqToInterGetX. specialize (V (pred m_1)). rewrite_eq (S (pred m_1) = m_1) in V.
rewrite P_3, P_4 in V by omega. cbn in V. now destruct V.
- apply seqToInterGetY. specialize (V (pred m_2)). rewrite_eq (S (pred m_2) = m_2) in V.
rewrite P_6, P_5 in V by omega. cbn in V. now destruct V.
Qed.
Lemma less_implies_accepting: L_M (X <0 Y) <$= L_A less_nfa.
Proof.
intros v [ n [m [EN [EM L]]]]. exists (fun k => if (decision (k <= n)) then SearchX else (if (decision (k <= m)) then SearchY else Less)). repeat split.
- intros k. destruct decision as [D|D].
+ destruct decision as [D'|D']; cbn; trivial_decision; auto.
right. split; auto. apply seqToInterGetX. now rewrite_eq (k = n).
+ destruct decision; cbn; trivial_decision; auto.
destruct decision; auto. right. split; auto. apply seqToInterGetY. now rewrite_eq (k = m).
- intros k. exists (m + S k). split; oauto. now trivial_decision.
Qed.
Lemma less_nfa_correct : L_A less_nfa =$= L_M (X <0 Y).
Proof.
split; auto using less_implies_accepting, accepting_implies_less.
Qed.
End LessNFA.
End BaseNFAs.
Recursive Translation of Formulas to NFAs
Fixpoint formulaNFA (s:FormMin) : NFA (finType_bool ^ (finType_fromList (free_vars s))) := match s with
| X <0 Y => less_nfa X Y
| X <<=0 Y => incl_nfa X Y
| s /\0 t => (intersect (preimage_aut (narrowVector (proj1 (free_vars_and_incl s t))) (formulaNFA s)) (preimage_aut (narrowVector (proj2 (free_vars_and_incl s t))) (formulaNFA t)))
| ~0 s => complement ((formulaNFA s) : NFA (finType_bool ^ (finType_fromList (free_vars (~0 s)))))
| ex0 X, s => list_proj_aut (l:=free_vars s) X (formulaNFA s)
end.
Lemma convRemInv_seqToInter s X w (D: ~ X el free_vars s) M: forall Y, Y el free_vars s ->
seqToInter (amap (convRemInv D) w) Y =~= (seqToInter w)[X:=M] Y.
Proof.
intros Y E. cbn. destruct decision as [<-|D']; [now exfalso|].
intros Z. unfold seqToInter. cbn. destruct decision.
++ destruct decision as [D''|D''].
** split; intros F; unfold memSet in *; rewrite <-F, !bigpi_correct, amap_correct; unfold seq_map.
apply convRemInv_correct. symmetry. apply convRemInv_correct.
** exfalso. apply D''. now apply in_rem_iff.
++ now exfalso.
Qed.
Lemma formulaNFA_correct : forall (s: FormMin), L_A (formulaNFA s) =$= L_M s.
Proof.
intros s. induction s as [X Y | X Y | s Hs t Ht| s Hs | X s Hs].
- cbn. apply less_nfa_correct.
- cbn. apply incl_nfa_correct.
- cbn. intros w. split.
+ intros [I_s I_t] % intersect_acorrect. unfold formula_language. simpl. split.
* apply coincidence with (I_1 := seqToInter(narrowASeq (proj1 (free_vars_and_incl s t)) w)).
-- apply narrow_to_free_vars.
-- apply Hs. apply preimage_aut_acorrect in I_s. apply I_s.
* apply coincidence with (I_1 := seqToInter(narrowASeq (proj2 (free_vars_and_incl s t)) w)).
-- apply narrow_to_free_vars.
-- apply Ht. apply preimage_aut_acorrect in I_t. apply I_t.
+ intros J. apply intersect_acorrect. split; apply preimage_aut_acorrect.
* apply Hs. apply coincidence with (I_1 := seqToInter w).
-- intros X F. symmetry. now apply narrow_to_free_vars.
-- apply J.
* apply Ht. apply coincidence with (I_1 := seqToInter w).
-- intros X F. symmetry. now apply narrow_to_free_vars.
-- apply J.
- intros w. split.
+ intros C. intros J. apply complement_correct in C. apply C. now apply Hs.
+ intros J. apply complement_correct. intros C. apply J. now apply Hs.
- cbn. intros w. split.
+ intros I. apply projection_list_aclosed in I.
unfold LAproj_list in I.
destruct decision as [D|D].
* destruct I as [M I]. exists M. unfold formula_language in Hs.
apply coincidence with (I_1:=seqToInter (joinASeq w M)).
-- apply zip_existential.
-- apply Hs. apply I.
* exists (singletonSet 0). apply coincidence with (I_1:=seqToInter (amap (convRemInv D) w)).
-- apply convRemInv_seqToInter.
-- apply Hs, I.
+ intros [M J]. apply projection_list_aclosed. unfold LAproj_list. destruct decision as[D|D].
* exists M. apply Hs. apply coincidence with (I_1 := (seqToInter w) [X := M] ).
-- intros Y F. symmetry. now apply zip_existential.
-- apply J.
* apply Hs. apply coincidence with (I_1 := (seqToInter w) [X := M] ).
-- intros Y E. symmetry. now apply convRemInv_seqToInter.
-- apply J.
Qed.
Theorem minmso_classic J phi : J |= phi \/ ~ J |= phi.
Proof.
destruct (xm_word_problem (formulaNFA phi) (interToSeq (free_vars phi) J)) as [H|H].
- left. apply coincidence with (I_1:= seqToInter ( (interToSeq (free_vars phi) J))).
+ intros X F. symmetry. now apply inter_to_seq_to_inter_correct.
+ apply formulaNFA_correct in H. apply H.
- right. intros Sat. apply H. apply formulaNFA_correct. now apply formula_language_complete.
Qed.
Lemma mso_classic I J phi : I # J |== phi \/ ~ I # J |== phi.
Proof.
apply mso_xm_satisfies, minmso_classic.
Qed.
Lemma minsat_iff_buechi_non_empty s : minsat s <-> exists w, L_A (formulaNFA s) w.
Proof.
split.
- intros [I Sat]. exists (interToSeq (free_vars s) I). now apply formulaNFA_correct, formula_language_complete.
- intros [w L]. exists (seqToInter w). now apply formulaNFA_correct.
Qed.
Lemma sat_iff_buechi_non_empty s: sat s <-> exists w, L_A (formulaNFA (toMinMSO s )) w.
Proof.
rewrite sat_iff_minsat by apply xm_satisfies.
now rewrite minsat_iff_buechi_non_empty.
Qed.
Theorem dec_sat s : dec (sat s).
Proof.
apply dec_trans with (P:= exists w, L_A (formulaNFA (toMinMSO s )) w) .
- destruct (dec_alanguage_empty_informative (formulaNFA (toMinMSO s ))) as [D|D].
+ now left.
+ right. intros [w L]. now apply (D w).
- now rewrite sat_iff_buechi_non_empty.
Qed.
End MSOtoBuechi.
Definition ARC :Prop := forall (C:FiniteSemigroup), AdditiveRamsey C.
Notation up_sat := (@sat (NatSetFromSeq (@CC UPStructure))).
Notation omega_sat ARC := (@sat (NatSetFromSeq (@CC (OmegaStructure ARC)))).
Corollary dec_up_sat s : dec (up_sat s).
Proof. apply dec_sat. Qed.
Corollary dec_general_sat s ARC: dec (omega_sat ARC s).
Proof. apply dec_sat. Qed.
Instance up_classic I J phi : logic_dec (@satisfies (NatSetFromSeq (@CC UPStructure)) I J phi).
Proof. apply mso_classic. Qed.
Instance omega_classic ARC I J phi : logic_dec (@satisfies (NatSetFromSeq (@CC (OmegaStructure ARC))) I J phi).
Proof. apply mso_classic. Qed.
Lemma up_buechi_nonempty_iff_buechi_nonempty (A:finType) (aut: NFA A): (exists w, L_B aut w) <-> (exists w, L_B aut (unfold w)).
Proof.
Open Scope string_scope.
split.
- intros [w L]. destruct (dec_language_empty_informative_periodic aut) as [[v [w' L']]|D].
+ exists (mkUPSeq v w'). apply L'.
+ exfalso. now apply (D w).
- intros [[v w] L]. exists (v +++ w to_omega). apply L.
Qed.
Theorem up_sat_iff_omega_sat ARC s : (omega_sat ARC s) <-> (up_sat s).
Proof.
rewrite 2sat_iff_buechi_non_empty. simpl. unfold L_A. cbn.
apply up_buechi_nonempty_iff_buechi_nonempty.
Qed.
Theorem up_equiv_iff_omega_equiv ARC phi psi:
(@mso_equiv (NatSetFromSeq (@CC UPStructure)) phi psi) <->
(@mso_equiv (NatSetFromSeq (@CC (OmegaStructure ARC))) phi psi).
Proof.
rewrite !equiv_unsat. split;
intros NSat Sat; apply NSat; eapply up_sat_iff_omega_sat; apply Sat.
Qed.
Lemma dec_up_in_lang' (X: finType) (vw : UPSeq X) (A : NFA X) : dec (L_A (CC:=UPSequenceStructure) A vw).
Proof.
destruct vw as [v w]. unfold L_A. simpl. unfold unfold. simpl.
apply dec_up_in_lang.
Qed.
Theorem dec_satisfaction_up I J phi : dec (@satisfies (NatSetFromSeq (@CC UPStructure)) I J phi).
Proof.
apply dec_trans with (P:= ItoM0 I J |= toMinMSO phi).
- destruct (dec_up_in_lang' (interToSeq (free_vars (toMinMSO phi)) (ItoM0 I J)) (formulaNFA (toMinMSO phi))) as [D|D].
+ left. pose proof (formulaNFA_correct (AC:=UPStructure)) as H. specialize (H (toMinMSO phi)).
apply H in D. unfold formula_language in D.
apply coincidence with (I_1 := seqToInter (interToSeq (free_vars (toMinMSO phi)) (ItoM0 I J))).
* intros X F. symmetry. now apply inter_to_seq_to_inter_correct.
* assumption.
+ right. intros Sat. apply D. apply (formulaNFA_correct (interToSeq (free_vars (toMinMSO phi)) (ItoM0 I J)) ).
now apply formula_language_complete.
- symmetry. apply to_min_mso_correct.
Qed.
Close Scope string_scope.
Notation up_sat := (@sat (NatSetFromSeq (@CC UPStructure))).
Notation omega_sat ARC := (@sat (NatSetFromSeq (@CC (OmegaStructure ARC)))).
Corollary dec_up_sat s : dec (up_sat s).
Proof. apply dec_sat. Qed.
Corollary dec_general_sat s ARC: dec (omega_sat ARC s).
Proof. apply dec_sat. Qed.
Instance up_classic I J phi : logic_dec (@satisfies (NatSetFromSeq (@CC UPStructure)) I J phi).
Proof. apply mso_classic. Qed.
Instance omega_classic ARC I J phi : logic_dec (@satisfies (NatSetFromSeq (@CC (OmegaStructure ARC))) I J phi).
Proof. apply mso_classic. Qed.
Lemma up_buechi_nonempty_iff_buechi_nonempty (A:finType) (aut: NFA A): (exists w, L_B aut w) <-> (exists w, L_B aut (unfold w)).
Proof.
Open Scope string_scope.
split.
- intros [w L]. destruct (dec_language_empty_informative_periodic aut) as [[v [w' L']]|D].
+ exists (mkUPSeq v w'). apply L'.
+ exfalso. now apply (D w).
- intros [[v w] L]. exists (v +++ w to_omega). apply L.
Qed.
Theorem up_sat_iff_omega_sat ARC s : (omega_sat ARC s) <-> (up_sat s).
Proof.
rewrite 2sat_iff_buechi_non_empty. simpl. unfold L_A. cbn.
apply up_buechi_nonempty_iff_buechi_nonempty.
Qed.
Theorem up_equiv_iff_omega_equiv ARC phi psi:
(@mso_equiv (NatSetFromSeq (@CC UPStructure)) phi psi) <->
(@mso_equiv (NatSetFromSeq (@CC (OmegaStructure ARC))) phi psi).
Proof.
rewrite !equiv_unsat. split;
intros NSat Sat; apply NSat; eapply up_sat_iff_omega_sat; apply Sat.
Qed.
Lemma dec_up_in_lang' (X: finType) (vw : UPSeq X) (A : NFA X) : dec (L_A (CC:=UPSequenceStructure) A vw).
Proof.
destruct vw as [v w]. unfold L_A. simpl. unfold unfold. simpl.
apply dec_up_in_lang.
Qed.
Theorem dec_satisfaction_up I J phi : dec (@satisfies (NatSetFromSeq (@CC UPStructure)) I J phi).
Proof.
apply dec_trans with (P:= ItoM0 I J |= toMinMSO phi).
- destruct (dec_up_in_lang' (interToSeq (free_vars (toMinMSO phi)) (ItoM0 I J)) (formulaNFA (toMinMSO phi))) as [D|D].
+ left. pose proof (formulaNFA_correct (AC:=UPStructure)) as H. specialize (H (toMinMSO phi)).
apply H in D. unfold formula_language in D.
apply coincidence with (I_1 := seqToInter (interToSeq (free_vars (toMinMSO phi)) (ItoM0 I J))).
* intros X F. symmetry. now apply inter_to_seq_to_inter_correct.
* assumption.
+ right. intros Sat. apply D. apply (formulaNFA_correct (interToSeq (free_vars (toMinMSO phi)) (ItoM0 I J)) ).
now apply formula_language_complete.
- symmetry. apply to_min_mso_correct.
Qed.
Close Scope string_scope.
Section Partition.
Context {CC: SequenceStructure}.
Context{MSO_classic : forall I J phi, logic_dec (I # J |== phi)}.
Conversion of Sequences to Sets and vice versa
Definition seqToSet (X: finType) (w:ASeq X) : (X -> NatSet) := fun x => amap (fun y => if (decision (x = y)) then true else false) w.
Lemma seqToSetCorrect (X:finType) (w: ASeq X) (x:X): forall n, n elS (seqToSet w x) <-> (aseq_to_seq w) n = x.
Proof.
intros n. split; unfold seqToSet; unfold memSet; simpl.
- intros E. rewrite amap_correct in E. unfold seq_map in *. destruct decision; congruence.
- intros E. rewrite amap_correct. unfold seq_map. now rewrite decision_true by auto.
Qed.
Definition NatCover (X : finType) (w : X -> NatSet) := forall n, exists x, n elS (w x).
Definition NatUnique(X : finType) (w : X -> NatSet) := forall x n, n elS (w x) -> forall y, n elS (w y) -> x = y.
Definition NatPartition (X: finType) (w: X -> NatSet) := NatCover w /\ NatUnique w.
Lemma nat_partition_extensional (X:finType) (w w' :X -> NatSet): NatPartition w -> (forall x, aseq_to_seq (w x) === aseq_to_seq (w' x)) -> NatPartition w'.
Proof.
intros [C U] E. split; unfold memSet in *; simpl in *.
- intros n. destruct (C n) as [x P]. exists x. unfold memSet. simpl. now rewrite <-E.
- intros x n Ex y Ey. unfold memSet in *. simpl in *. rewrite <-E in Ex,Ey. apply (U x n Ex y Ey).
Qed.
Lemma seqToSetCover (X: finType) (w: ASeq X) : NatCover (seqToSet w).
Proof.
intros n. exists (aseq_to_seq w n). now apply seqToSetCorrect.
Qed.
Lemma seqToSetUnique (X: finType) (w: ASeq X) : NatUnique (seqToSet w).
Proof.
intros x n Ex y Ey. rewrite seqToSetCorrect in Ex, Ey. now rewrite <-Ex, <-Ey.
Qed.
Lemma seqToSetPartition (X: finType) (w: ASeq X): NatPartition (seqToSet w).
Proof.
split. apply seqToSetCover. apply seqToSetUnique.
Qed.
Definition selectX (X:finType) (x:X) (v: finType_bool^X) : X.
Proof.
destruct (decision (exists x, applyVect v x = true)) as [D|D].
- apply finType_cc in D. + destruct D as [y _]. exact y. + auto.
- exact x.
Defined.
Definition memX (X: finType) (w: X -> NatSet) (C: NatCover w) : X.
Proof.
destruct (elem X) as [|x l] eqn:H.
- exfalso. destruct (C 0) as [x _]. pose (elementIn x) as H'. rewrite H in H'. auto.
- exact x.
Qed.
Definition setToSeq (X: finType) (w: X -> NatSet) (C: NatCover w) : ASeq X.
Proof.
exact (amap (selectX (memX C)) (bigzip w)).
Defined.
Lemma setToSeqCorrect (X: finType) (w: X -> NatSet) (C:NatCover w) : forall n, n elS (w (aseq_to_seq (setToSeq C) n)).
Proof.
intros n. unfold setToSeq. rewrite amap_correct. unfold seq_map, selectX.
destruct decision as [D|D].
- destruct finType_cc as [x P]. now rewrite bigzip_correct in P.
- exfalso. apply D. destruct (C n) as [x P]. exists x. now rewrite bigzip_correct.
Qed.
(* The following lemma show an equivalence, but sometimes rewriting is easier with two lemmata *)
Lemma setToSeqParitionCorrect (X: finType) (w: X -> NatSet) (x : X) (P: NatPartition w): forall n, n elS (w x) -> (aseq_to_seq (setToSeq (proj1 P)) n) = x.
Proof.
intros n Ex. unfold setToSeq. rewrite amap_correct. unfold seq_map.
unfold selectX. destruct decision as [D|D].
- destruct finType_cc as [y Ey]. rewrite bigzip_correct in Ey. destruct P as [_ U]. now specialize (U x n Ex y Ey).
- exfalso. apply D. destruct ((proj1 P) n) as [y Q]. exists y. now rewrite bigzip_correct.
Qed.
Lemma setToSeqParitionCorrectInv (X: finType) (w: X -> NatSet) (x : X) (P: NatPartition w): forall n, aseq_to_seq (setToSeq (proj1 P)) n = x -> n elS (w x) .
Proof.
intros n Eq. unfold setToSeq in Eq. rewrite amap_correct in Eq. unfold seq_map, selectX in Eq.
destruct decision as [D|D].
- destruct finType_cc as [y Ey]. subst y. now rewrite bigzip_correct in Ey.
- exfalso. apply D. destruct ((proj1 P) n) as [y Q]. exists y. now rewrite bigzip_correct.
Qed.
Lemma setToSeqExtensional (X:finType) (w_1 w_2: X -> NatSet) (P_1 : NatPartition w_1) (P_2: NatPartition w_2): (forall x, aseq_to_seq (w_1 x) === aseq_to_seq (w_2 x)) -> aseq_to_seq (setToSeq (proj1 P_1)) === aseq_to_seq (setToSeq (proj1 P_2)).
Proof.
intros E n.
destruct ((proj1 P_1) n) as [x_1 Q_1]. destruct ((proj1 P_2) n) as [x_2 Q_2].
rewrite (setToSeqParitionCorrect P_1 Q_1). rewrite (setToSeqParitionCorrect P_2 Q_2).
unfold memSet in *. simpl in *. rewrite E in Q_1. apply (proj2 P_2 x_1 n Q_1 x_2 Q_2).
Qed.
Lemma setToSeqExtensional2 (X:finType) w_1 ( w_2: X -> NatSet) (P_2: NatPartition w_2): (forall x, aseq_to_seq (seqToSet w_1 x) === aseq_to_seq (w_2 x)) -> aseq_to_seq w_1 === aseq_to_seq (setToSeq(proj1 P_2)).
Proof.
intros E n.
destruct ((proj1 P_2) n) as [x_2 Q_2].
rewrite (setToSeqParitionCorrect P_2 Q_2).
unfold memSet in Q_2.
apply seqToSetCorrect. simpl in *.
now rewrite <-E in Q_2.
Qed.
Definition I2chain (F: finType) (w: F -> SVar) J : (F -> NatSet) := fun f => (J (w f)).
Definition Cover (F: finType) (w : F -> SVar) : Form := (all1 0, OR { f | True } 0 el2 (w f)).
Lemma cover_correct I J (F:finType) (w: F -> SVar) : I # J |== Cover w <-> NatCover (I2chain w J).
Proof.
split; unfold Cover.
- intros C n. rewrite all1_correct in C. specialize (C n). fold satisfies in C. apply finBigOrCorrect in C. destruct C as [f C]. exists f. simpl in C. now trivial_decision.
- intros C. apply all1_correct. intros n. specialize (C n). apply finBigOrCorrect. destruct C as [f C]. exists f. simpl. now trivial_decision.
Qed.
Instance dec_pair_eq (F: finType) : forall (z: F *F), dec(match z with (f1, f2) => f1 <> f2 end ).
Proof. intros [f1 f2]. auto. Qed.
Definition Unique (F: finType) (w : F -> SVar) : Form := all1 0, AND { (f1,f2) | f1 <> f2 } ~2 (0 el2 (w f1) /\2 0 el2 (w f2)).
Lemma unique_correct I J (F:finType) (w: F -> SVar) : I # J |== Unique w <-> NatUnique (I2chain w J).
Proof.
split; unfold Unique.
- intros U f1 n E1 f2 E2. rewrite all1_correct in U. decide (f1 = f2) as [D|D].
+ assumption.
+ exfalso. specialize (U n). fold satisfies in U. rewrite finBigAndCorrect in U.
apply (U (f1,f2)); auto. now trivial_decision.
- intros U. apply all1_correct. intros n. apply finBigAndCorrect. intros [f1 f2] N [E1 E2]. simpl in *. trivial_decision. now specialize (U f1 n E1 f2 E2).
Qed.
Definition Partition (F: finType) (w : F -> SVar) : Form := Cover w /\2 Unique w.
Lemma partition_correct I J (F:finType) (w: F -> SVar) : I # J |== Partition w <-> NatPartition (I2chain w J).
Proof.
unfold Partition. unfold NatPartition. now rewrite <-(cover_correct I), <-(unique_correct I).
Qed.
End Partition.
Lemma seqToSetCorrect (X:finType) (w: ASeq X) (x:X): forall n, n elS (seqToSet w x) <-> (aseq_to_seq w) n = x.
Proof.
intros n. split; unfold seqToSet; unfold memSet; simpl.
- intros E. rewrite amap_correct in E. unfold seq_map in *. destruct decision; congruence.
- intros E. rewrite amap_correct. unfold seq_map. now rewrite decision_true by auto.
Qed.
Definition NatCover (X : finType) (w : X -> NatSet) := forall n, exists x, n elS (w x).
Definition NatUnique(X : finType) (w : X -> NatSet) := forall x n, n elS (w x) -> forall y, n elS (w y) -> x = y.
Definition NatPartition (X: finType) (w: X -> NatSet) := NatCover w /\ NatUnique w.
Lemma nat_partition_extensional (X:finType) (w w' :X -> NatSet): NatPartition w -> (forall x, aseq_to_seq (w x) === aseq_to_seq (w' x)) -> NatPartition w'.
Proof.
intros [C U] E. split; unfold memSet in *; simpl in *.
- intros n. destruct (C n) as [x P]. exists x. unfold memSet. simpl. now rewrite <-E.
- intros x n Ex y Ey. unfold memSet in *. simpl in *. rewrite <-E in Ex,Ey. apply (U x n Ex y Ey).
Qed.
Lemma seqToSetCover (X: finType) (w: ASeq X) : NatCover (seqToSet w).
Proof.
intros n. exists (aseq_to_seq w n). now apply seqToSetCorrect.
Qed.
Lemma seqToSetUnique (X: finType) (w: ASeq X) : NatUnique (seqToSet w).
Proof.
intros x n Ex y Ey. rewrite seqToSetCorrect in Ex, Ey. now rewrite <-Ex, <-Ey.
Qed.
Lemma seqToSetPartition (X: finType) (w: ASeq X): NatPartition (seqToSet w).
Proof.
split. apply seqToSetCover. apply seqToSetUnique.
Qed.
Definition selectX (X:finType) (x:X) (v: finType_bool^X) : X.
Proof.
destruct (decision (exists x, applyVect v x = true)) as [D|D].
- apply finType_cc in D. + destruct D as [y _]. exact y. + auto.
- exact x.
Defined.
Definition memX (X: finType) (w: X -> NatSet) (C: NatCover w) : X.
Proof.
destruct (elem X) as [|x l] eqn:H.
- exfalso. destruct (C 0) as [x _]. pose (elementIn x) as H'. rewrite H in H'. auto.
- exact x.
Qed.
Definition setToSeq (X: finType) (w: X -> NatSet) (C: NatCover w) : ASeq X.
Proof.
exact (amap (selectX (memX C)) (bigzip w)).
Defined.
Lemma setToSeqCorrect (X: finType) (w: X -> NatSet) (C:NatCover w) : forall n, n elS (w (aseq_to_seq (setToSeq C) n)).
Proof.
intros n. unfold setToSeq. rewrite amap_correct. unfold seq_map, selectX.
destruct decision as [D|D].
- destruct finType_cc as [x P]. now rewrite bigzip_correct in P.
- exfalso. apply D. destruct (C n) as [x P]. exists x. now rewrite bigzip_correct.
Qed.
(* The following lemma show an equivalence, but sometimes rewriting is easier with two lemmata *)
Lemma setToSeqParitionCorrect (X: finType) (w: X -> NatSet) (x : X) (P: NatPartition w): forall n, n elS (w x) -> (aseq_to_seq (setToSeq (proj1 P)) n) = x.
Proof.
intros n Ex. unfold setToSeq. rewrite amap_correct. unfold seq_map.
unfold selectX. destruct decision as [D|D].
- destruct finType_cc as [y Ey]. rewrite bigzip_correct in Ey. destruct P as [_ U]. now specialize (U x n Ex y Ey).
- exfalso. apply D. destruct ((proj1 P) n) as [y Q]. exists y. now rewrite bigzip_correct.
Qed.
Lemma setToSeqParitionCorrectInv (X: finType) (w: X -> NatSet) (x : X) (P: NatPartition w): forall n, aseq_to_seq (setToSeq (proj1 P)) n = x -> n elS (w x) .
Proof.
intros n Eq. unfold setToSeq in Eq. rewrite amap_correct in Eq. unfold seq_map, selectX in Eq.
destruct decision as [D|D].
- destruct finType_cc as [y Ey]. subst y. now rewrite bigzip_correct in Ey.
- exfalso. apply D. destruct ((proj1 P) n) as [y Q]. exists y. now rewrite bigzip_correct.
Qed.
Lemma setToSeqExtensional (X:finType) (w_1 w_2: X -> NatSet) (P_1 : NatPartition w_1) (P_2: NatPartition w_2): (forall x, aseq_to_seq (w_1 x) === aseq_to_seq (w_2 x)) -> aseq_to_seq (setToSeq (proj1 P_1)) === aseq_to_seq (setToSeq (proj1 P_2)).
Proof.
intros E n.
destruct ((proj1 P_1) n) as [x_1 Q_1]. destruct ((proj1 P_2) n) as [x_2 Q_2].
rewrite (setToSeqParitionCorrect P_1 Q_1). rewrite (setToSeqParitionCorrect P_2 Q_2).
unfold memSet in *. simpl in *. rewrite E in Q_1. apply (proj2 P_2 x_1 n Q_1 x_2 Q_2).
Qed.
Lemma setToSeqExtensional2 (X:finType) w_1 ( w_2: X -> NatSet) (P_2: NatPartition w_2): (forall x, aseq_to_seq (seqToSet w_1 x) === aseq_to_seq (w_2 x)) -> aseq_to_seq w_1 === aseq_to_seq (setToSeq(proj1 P_2)).
Proof.
intros E n.
destruct ((proj1 P_2) n) as [x_2 Q_2].
rewrite (setToSeqParitionCorrect P_2 Q_2).
unfold memSet in Q_2.
apply seqToSetCorrect. simpl in *.
now rewrite <-E in Q_2.
Qed.
Definition I2chain (F: finType) (w: F -> SVar) J : (F -> NatSet) := fun f => (J (w f)).
Definition Cover (F: finType) (w : F -> SVar) : Form := (all1 0, OR { f | True } 0 el2 (w f)).
Lemma cover_correct I J (F:finType) (w: F -> SVar) : I # J |== Cover w <-> NatCover (I2chain w J).
Proof.
split; unfold Cover.
- intros C n. rewrite all1_correct in C. specialize (C n). fold satisfies in C. apply finBigOrCorrect in C. destruct C as [f C]. exists f. simpl in C. now trivial_decision.
- intros C. apply all1_correct. intros n. specialize (C n). apply finBigOrCorrect. destruct C as [f C]. exists f. simpl. now trivial_decision.
Qed.
Instance dec_pair_eq (F: finType) : forall (z: F *F), dec(match z with (f1, f2) => f1 <> f2 end ).
Proof. intros [f1 f2]. auto. Qed.
Definition Unique (F: finType) (w : F -> SVar) : Form := all1 0, AND { (f1,f2) | f1 <> f2 } ~2 (0 el2 (w f1) /\2 0 el2 (w f2)).
Lemma unique_correct I J (F:finType) (w: F -> SVar) : I # J |== Unique w <-> NatUnique (I2chain w J).
Proof.
split; unfold Unique.
- intros U f1 n E1 f2 E2. rewrite all1_correct in U. decide (f1 = f2) as [D|D].
+ assumption.
+ exfalso. specialize (U n). fold satisfies in U. rewrite finBigAndCorrect in U.
apply (U (f1,f2)); auto. now trivial_decision.
- intros U. apply all1_correct. intros n. apply finBigAndCorrect. intros [f1 f2] N [E1 E2]. simpl in *. trivial_decision. now specialize (U f1 n E1 f2 E2).
Qed.
Definition Partition (F: finType) (w : F -> SVar) : Form := Cover w /\2 Unique w.
Lemma partition_correct I J (F:finType) (w: F -> SVar) : I # J |== Partition w <-> NatPartition (I2chain w J).
Proof.
unfold Partition. unfold NatPartition. now rewrite <-(cover_correct I), <-(unique_correct I).
Qed.
End Partition.