From c3f6fc2d5bf60ae521e2cbf845569ef5b4f600f9 Mon Sep 17 00:00:00 2001 From: HeyLey Date: Sat, 22 Apr 2017 21:15:53 +0300 Subject: [PATCH 01/23] initial commit --- DFA.v | 183 +++++++ cf/Base.v | 1319 ++++++++++++++++++++++++++++++++++++++++++++++ cf/Binarize.v | 138 +++++ cf/Chomsky.v | 116 ++++ cf/Dec_Empty.v | 114 ++++ cf/Dec_Word.v | 221 ++++++++ cf/Definitions.v | 84 +++ cf/Derivation.v | 219 ++++++++ cf/ElimE.v | 288 ++++++++++ cf/ElimU.v | 186 +++++++ cf/Inlining.v | 233 ++++++++ cf/Lists.v | 363 +++++++++++++ cf/Separate.v | 239 +++++++++ cf/Symbols.v | 194 +++++++ 14 files changed, 3897 insertions(+) create mode 100644 DFA.v create mode 100644 cf/Base.v create mode 100644 cf/Binarize.v create mode 100644 cf/Chomsky.v create mode 100644 cf/Dec_Empty.v create mode 100644 cf/Dec_Word.v create mode 100644 cf/Definitions.v create mode 100644 cf/Derivation.v create mode 100644 cf/ElimE.v create mode 100644 cf/ElimU.v create mode 100644 cf/Inlining.v create mode 100644 cf/Lists.v create mode 100644 cf/Separate.v create mode 100644 cf/Symbols.v diff --git a/DFA.v b/DFA.v new file mode 100644 index 0000000..b36bf88 --- /dev/null +++ b/DFA.v @@ -0,0 +1,183 @@ +Require Import List Ensembles. + +Require Import Fin. + + +Inductive ter : Type := +| T : nat -> ter. + + +(** The type of deterministic finite automata. ***) +Record dfa : Type := mkDfa { + states_n: nat; + start: t states_n; + final: Ensemble (t states_n); + next: (t states_n) -> ter -> (t states_n); +}. + + +Definition word := list ter. + +Definition language := word -> Prop. + + +Fixpoint accepts (d : dfa) (s: t (states_n d)) (w: word) : Prop := + match w with + | nil => In (t (states_n d)) (final d) s + | h :: t => accepts d (next d s h) t + end. + +Definition dfa_language (d : dfa) := (accepts d (start d)). + +Definition language_union (l1 l2 : language) := fun w => (l1 w) \/ (l2 w). + +Definition language_intersection (l1 l2 : language) := fun w => (l1 w) /\ (l2 w). + +Definition language_eq (l1 l2 : language) := forall w : word, l1 w <-> l2 w. + + +Theorem th1 : forall l1 l2 l3 : language, language_eq (language_intersection l1 (language_union l2 l3)) (language_union (language_intersection l1 l2) (language_intersection l1 l3)). +Proof. + intros. + unfold language_eq. + intros. + split. + intro. + unfold language_intersection in H. + destruct H. + unfold language_union in H0. + unfold language_union. + destruct H0. + left. + unfold language_intersection. + intuition. + right. + unfold language_intersection. + intuition. + + intros. + unfold language_union in H. + destruct H. + unfold language_intersection in H. + destruct H. + unfold language_intersection. + split. + exact H. + unfold language_union. + left. + exact H0. + unfold language_intersection in H. + unfold language_intersection. + destruct H. + split. + + exact H. + unfold language_union. + right. + exact H0. +Qed. + + +Fixpoint language_list_union (l : list language) := fun w => + match l with + | nil => False + | h :: t => (h w) \/ language_list_union t w + end. + + +Lemma distr : forall (a b c : Prop), (a /\ c) -> a /\ (b \/ c). +Proof. + intros. + destruct H. + split. + exact H. + right. + exact H0. +Qed. + +Theorem th2 : forall (l2 : language) (ls : list language), + language_eq (language_intersection l2 (language_list_union ls)) + (language_list_union (map (language_intersection l2) ls)). +Proof. + intros l2 ls. + unfold language_eq. + intros w. + split. + elim ls. + intros H0. + unfold language_intersection in H0. + destruct H0. + simpl in H0. + elim H0. + intros a tail. + intro HR. + intro LI. + + simpl. + + unfold language_intersection in LI. + simpl language_list_union in LI. + + destruct LI as [l2_w H1]. + + elim H1. + + intro. + + left. + + unfold language_intersection. + + apply (conj l2_w H). + + intro. + + right. + + apply HR. + + unfold language_intersection. + + apply (conj l2_w H). + + elim ls. + + simpl. + + intros F; case F. + + clear ls. + + intros LA ls H0 LU. + + simpl language_list_union in LU. + + case LU. + + intro H1. + + unfold language_intersection. + + unfold language_intersection in H1. + + destruct H1. + + split. + + exact H. + + simpl language_list_union. + + left; exact H1. + + intro. + + apply H0 in H. + + unfold language_intersection. + simpl language_list_union. + + apply distr. + unfold language_intersection in H. + exact H. +Qed. \ No newline at end of file diff --git a/cf/Base.v b/cf/Base.v new file mode 100644 index 0000000..ce22951 --- /dev/null +++ b/cf/Base.v @@ -0,0 +1,1319 @@ +(** * Base Library for ICL + + - Version: 25 June 2014 + - Author: Gert Smolka, Saarland University + - Acknowlegments: Sigurd Schneider, Dominik Karst + *) + +(* Switch Coq into implicit argument mode *) + +Global Set Implicit Arguments. +Global Unset Strict Implicit. + +(* Load basic Coq libraries *) + +Require Export Omega List Morphisms. + +(* Inversion tactic *) + +Ltac inv H := inversion H; subst; try clear H. + +(** * Size recursion *) + +Lemma size_recursion (X : Type) (sigma : X -> nat) (p : X -> Type) : + (forall x, (forall y, sigma y < sigma x -> p y) -> p x) -> + forall x, p x. +Proof. + intros D x. apply D. + cut (forall n y, sigma y < n -> p y). + now eauto. + clear x. intros n. + induction n; intros y E. + - exfalso; omega. + - apply D. intros x F. apply IHn. omega. +Qed. + +Arguments size_recursion {X} sigma {p} _ _. + +(** * Iteration *) + +Section Iteration. + Variable X : Type. + Variable f : X -> X. + + Fixpoint it (n : nat) (x : X) : X := + match n with + | 0 => x + | S n' => f (it n' x) + end. + + Lemma it_ind (p : X -> Prop) x n : + p x -> (forall z, p z -> p (f z)) -> p (it n x). + Proof. + intros A B. induction n; simpl; auto. + Qed. + + Definition FP (x : X) : Prop := f x = x. + + Lemma it_fp (sigma : X -> nat) x : + (forall n, FP (it n x) \/ sigma (it n x) > sigma (it (S n) x)) -> + FP (it (sigma x) x). + Proof. + intros A. + assert (B: forall n, FP (it n x) \/ sigma x >= n + sigma (it n x)). + { intros n; induction n; simpl. + - auto. + - destruct IHn as [B|B]. + + left. now rewrite B. + + destruct (A n) as [C|C]. + * left. now rewrite C. + * right. simpl in C. omega. } + destruct (A (sigma x)), (B (sigma x)); auto; exfalso; omega. + Qed. +End Iteration. + +(** * Decidability *) + +Definition dec (X : Prop) : Type := {X} + {~ X}. + +Notation "'eq_dec' X" := (forall x y : X, dec (x=y)) (at level 70). + +(* Register dec as a type class *) + +Existing Class dec. + +Definition decision (X : Prop) (D : dec X) : dec X := D. +Arguments decision X {D}. + +Tactic Notation "decide" constr(p) := + destruct (decision p). +Tactic Notation "decide" constr(p) "as" simple_intropattern(i) := + destruct (decision p) as i. + +(* Hints for auto concerning dec *) + +Hint Extern 4 => +match goal with + | [ |- dec ?p ] => exact (decision p) +end. + +(* Improves type class inference *) + +Hint Extern 4 => +match goal with + | [ |- dec ((fun _ => _) _) ] => simpl +end : typeclass_instances. + +(* Register instance rules for dec *) + +Instance True_dec : dec True := + left I. + +Instance False_dec : dec False := + right (fun A => A). + +Instance impl_dec (X Y : Prop) : + dec X -> dec Y -> dec (X -> Y). +Proof. + unfold dec; tauto. +Defined. + +Instance and_dec (X Y : Prop) : + dec X -> dec Y -> dec (X /\ Y). +Proof. + unfold dec; tauto. +Defined. + +Instance or_dec (X Y : Prop) : + dec X -> dec Y -> dec (X \/ Y). +Proof. + unfold dec; tauto. +Defined. + +(* Coq standard modules make "not" and "iff" opaque for type class inference, can be seen with Print HintDb typeclass_instances. *) + +Instance not_dec (X : Prop) : + dec X -> dec (~ X). +Proof. + unfold not. auto. +Defined. + +Instance iff_dec (X Y : Prop) : + dec X -> dec Y -> dec (X <-> Y). +Proof. + unfold iff. auto. +Qed. + +Lemma dec_DN X : + dec X -> ~~ X -> X. +Proof. + unfold dec; tauto. +Qed. + +Lemma dec_DM_and X Y : + dec X -> dec Y -> ~ (X /\ Y) -> ~ X \/ ~ Y. +Proof. + unfold dec; tauto. +Qed. + +Lemma dec_DM_impl X Y : + dec X -> dec Y -> ~ (X -> Y) -> X /\ ~ Y. +Proof. + unfold dec; tauto. +Qed. + +Lemma dec_prop_iff (X Y : Prop) : + (X <-> Y) -> dec X -> dec Y. +Proof. + unfold dec; tauto. +Defined. + +Instance bool_eq_dec : + eq_dec bool. +Proof. + intros x y. hnf. decide equality. +Defined. + +Instance nat_eq_dec : + eq_dec nat. +Proof. + intros x y. hnf. decide equality. +Defined. + +Instance nat_le_dec (x y : nat) : dec (x <= y) := + le_dec x y. + +(** * Lists *) + +(* Notations for lists *) + +Definition equi X (A B : list X) : Prop := + incl A B /\ incl B A. + +Hint Unfold equi. + +Export ListNotations. +Notation "| A |" := (length A) (at level 65). +Notation "x 'el' A" := (In x A) (at level 70). +Notation "A <<= B" := (incl A B) (at level 70). +Notation "A === B" := (equi A B) (at level 70). + +(* The following comments are for coqdoc *) +(** printing el #∊# *) +(** printing <<= #⊆# *) +(** printing === #≡# *) + +(** Register additional simplification rules with autorewrite / simpl_list *) + +Hint Rewrite <- app_assoc : list. +Hint Rewrite rev_app_distr map_app prod_length : list. +(* Print Rewrite HintDb list. *) + +(** A useful lemma *) + +Lemma list_cycle (X : Type) (A : list X) x : + x::A <> A. +Proof. + intros B. + assert (C: |x::A| <> |A|) by (simpl; omega). + apply C. now rewrite B. +Qed. + +(** Decidability laws for lists *) + +Instance list_eq_dec X : + eq_dec X -> eq_dec (list X). +Proof. + intros D. apply list_eq_dec. exact D. +Defined. + +Instance list_in_dec (X : Type) (x : X) (A : list X) : + eq_dec X -> dec (x el A). +Proof. + intros D. apply in_dec. exact D. +Defined. + +Lemma list_sigma_forall X A (p : X -> Prop) (p_dec : forall x, dec (p x)) : + {x | x el A /\ p x} + {forall x, x el A -> ~ p x}. +Proof. + induction A as [|x A]; simpl. + - tauto. + - destruct IHA as [[y [D E]]|D]. + + eauto. + + destruct (p_dec x) as [E|E]. + * eauto. + * right. intros y [[]|F]; auto. +Defined. + +Arguments list_sigma_forall {X} A p {p_dec}. + +Instance list_forall_dec X A (p : X -> Prop) : + (forall x, dec (p x)) -> dec (forall x, x el A -> p x). +Proof. + intros p_dec. + destruct (list_sigma_forall A (fun x => ~ p x)) as [[x [D E]]|D]. + - right. auto. + - left. intros x E. apply dec_DN; auto. +Defined. + +Instance list_exists_dec X A (p : X -> Prop) : + (forall x, dec (p x)) -> dec (exists x, x el A /\ p x). +Proof. + intros p_dec. + destruct (list_sigma_forall A p) as [[x [D E]]|D]. + - unfold dec. eauto. + - right. intros [x [E F]]. exact (D x E F). +Defined. + +Lemma list_exists_DM X A (p : X -> Prop) : + (forall x, dec (p x)) -> + ~ (forall x, x el A -> ~ p x) -> exists x, x el A /\ p x. +Proof. + intros D E. + destruct (list_sigma_forall A p) as [F|F]. + + destruct F as [x F]. eauto. + + contradiction (E F). +Qed. + +Lemma list_exists_not_incl X (A B : list X) : + eq_dec X -> + ~ A <<= B -> exists x, x el A /\ ~ x el B. +Proof. + intros D E. + apply list_exists_DM; auto. + intros F. apply E. intros x G. + apply dec_DN; auto. +Qed. + +Lemma list_cc X (p : X -> Prop) A : + (forall x, dec (p x)) -> + (exists x, x el A /\ p x) -> {x | x el A /\ p x}. +Proof. + intros D E. + destruct (list_sigma_forall A p) as [[x [F G]]|F]. + - eauto. + - exfalso. destruct E as [x [G H]]. apply (F x); auto. +Defined. + +(** Membership + +We use the following lemmas from Coq's standard library List. +- [in_eq : x el x::A] +- [in_nil : ~ x el nil] +- [in_cons : x el A -> x el y::A] +- [in_or_app : x el A \/ x el B -> x el A++B] +- [in_app_iff : x el A++B <-> x el A \/ x el B] +- [in_map_iff : y el map f A <-> exists x, f x = y /\ x el A] +*) + +Hint Resolve in_eq in_nil in_cons in_or_app. + +Section Membership. + Variable X : Type. + Implicit Types x y : X. + Implicit Types A B : list X. + + Lemma in_sing x y : + x el [y] -> x = y. + Proof. + simpl. intros [[]|[]]. reflexivity. + Qed. + + Lemma in_cons_neq x y A : + x el y::A -> x <> y -> x el A. + Proof. + simpl. intros [[]|D] E; congruence. + Qed. + + Lemma not_in_cons x y A : + ~ x el y :: A -> x <> y /\ ~ x el A. + Proof. + intuition; subst; auto. + Qed. + + Definition disjoint A B := + ~ exists x, x el A /\ x el B. + + Lemma disjoint_nil B : + disjoint nil B. + Proof. + firstorder. + Qed. + + Lemma disjoint_nil' A : + disjoint A nil. + Proof. + firstorder. + Qed. + + Lemma disjoint_symm A B : + disjoint A B -> disjoint B A. + Proof. + firstorder. + Qed. + + Lemma disjoint_incl A B B' : + B' <<= B -> disjoint A B -> disjoint A B'. + Proof. + firstorder. + Qed. + + Lemma disjoint_forall A B : + disjoint A B <-> forall x, x el A -> ~ x el B. + Proof. + split. + - intros D x E F. apply D. exists x. auto. + - intros D [x [E F]]. exact (D x E F). + Qed. + + Lemma disjoint_cons x A B : + disjoint (x::A) B <-> ~ x el B /\ disjoint A B. + Proof. + split. + - intros D. split. + + intros E. apply D. eauto. + + intros [y [E F]]. apply D. eauto. + - intros [D E] [y [[F|F] G]]. + + congruence. + + apply E. eauto. + Qed. +End Membership. + +Hint Resolve disjoint_nil disjoint_nil'. + +(** Inclusion + +We use the following lemmas from Coq's standard library List. +- [incl_refl : A <<= A] +- [incl_tl : A <<= B -> A <<= x::B] +- [incl_cons : x el B -> A <<= B -> x::A <<= B] +- [incl_appl : A <<= B -> A <<= B++C] +- [incl_appr : A <<= C -> A <<= B++C] +- [incl_app : A <<= C -> B <<= C -> A++B <<= C] +*) + +Hint Resolve incl_refl incl_tl incl_cons incl_appl incl_appr incl_app. + +Lemma incl_nil X (A : list X) : + nil <<= A. + +Proof. intros x []. Qed. + +Hint Resolve incl_nil. + +Lemma incl_map X Y A B (f : X -> Y) : + A <<= B -> map f A <<= map f B. + +Proof. + intros D y E. apply in_map_iff in E as [x [E E']]. + subst y. apply in_map_iff. eauto. +Qed. + +Section Inclusion. + Variable X : Type. + Implicit Types A B : list X. + + Lemma incl_nil_eq A : + A <<= nil -> A=nil. + + Proof. + intros D. destruct A as [|x A]. + - reflexivity. + - exfalso. apply (D x). auto. + Qed. + + Lemma incl_shift x A B : + A <<= B -> x::A <<= x::B. + + Proof. auto. Qed. + + Lemma incl_lcons x A B : + x::A <<= B <-> x el B /\ A <<= B. + Proof. + split. + - intros D. split; hnf; auto. + - intros [D E] z [F|F]; subst; auto. + Qed. + + Lemma incl_sing x A y : + x::A <<= [y] -> x = y /\ A <<= [y]. + Proof. + rewrite incl_lcons. intros [D E]. + apply in_sing in D. auto. + Qed. + + Lemma incl_rcons x A B : + A <<= x::B -> ~ x el A -> A <<= B. + + Proof. intros C D y E. destruct (C y E) as [F|F]; congruence. Qed. + + Lemma incl_lrcons x A B : + x::A <<= x::B -> ~ x el A -> A <<= B. + + Proof. + intros C D y E. + assert (F: y el x::B) by auto. + destruct F as [F|F]; congruence. + Qed. + + Lemma incl_app_left A B C : + A ++ B <<= C -> A <<= C /\ B <<= C. + Proof. + firstorder. + Qed. + +End Inclusion. + +Definition inclp (X : Type) (A : list X) (p : X -> Prop) : Prop := + forall x, x el A -> p x. + +(** Setoid rewriting with list inclusion and list equivalence *) + +Instance incl_preorder X : + PreOrder (@incl X). +Proof. + constructor; hnf; unfold incl; auto. +Qed. + +Instance equi_Equivalence X : + Equivalence (@equi X). +Proof. + constructor; hnf; firstorder. +Qed. + +Instance incl_equi_proper X : + Proper (@equi X ==> @equi X ==> iff) (@incl X). +Proof. + hnf. intros A B D. hnf. firstorder. +Qed. + +Instance cons_incl_proper X x : + Proper (@incl X ==> @incl X) (@cons X x). +Proof. + hnf. apply incl_shift. +Qed. + +Instance cons_equi_proper X x : + Proper (@equi X ==> @equi X) (@cons X x). +Proof. + hnf. firstorder. +Qed. + +Instance in_incl_proper X x : + Proper (@incl X ==> Basics.impl) (@In X x). +Proof. + intros A B D. hnf. auto. +Qed. + +Instance in_equi_proper X x : + Proper (@equi X ==> iff) (@In X x). +Proof. + intros A B D. firstorder. +Qed. + +Instance app_incl_proper X : + Proper (@incl X ==> @incl X ==> @incl X) (@app X). +Proof. + intros A B D A' B' E. auto. +Qed. + +Instance app_equi_proper X : + Proper (@equi X ==> @equi X ==> @equi X) (@app X). +Proof. + hnf. intros A B D. hnf. intros A' B' E. + destruct D, E; auto. +Qed. + +(** Equivalence *) + +Section Equi. + Variable X : Type. + Implicit Types A B : list X. + + Lemma equi_push x A : + x el A -> A === x::A. + + Proof. auto. Qed. + + Lemma equi_dup x A : + x::A === x::x::A. + + Proof. auto. Qed. + + Lemma equi_swap x y A: + x::y::A === y::x::A. + + Proof. split; intros z; simpl; tauto. Qed. + + Lemma equi_shift x A B : + x::A++B === A++x::B. + + Proof. + split; intros y. + - intros [D|D]. + + subst; auto. + + apply in_app_iff in D as [D|D]; auto. + - intros D. apply in_app_iff in D as [D|D]. + + auto. + + destruct D; subst; auto. + Qed. + + Lemma equi_rotate x A : + x::A === A++[x]. + + Proof. + split; intros y; simpl. + - intros [D|D]; subst; auto. + - intros D. apply in_app_iff in D as [D|D]. + + auto. + + apply in_sing in D. auto. + Qed. +End Equi. + +(** * Filter *) + +Definition filter (X : Type) (p : X -> Prop) (p_dec : forall x, dec (p x)) : list X -> list X := + fix f A := match A with + | nil => nil + | x::A' => if decision (p x) then x :: f A' else f A' + end. + +Arguments filter {X} p {p_dec} A. + +Section FilterLemmas. + Variable X : Type. + Variable p : X -> Prop. + Context {p_dec : forall x, dec (p x)}. + + Lemma in_filter_iff x A : + x el filter p A <-> x el A /\ p x. + + Proof. + induction A as [|y A]; simpl. + - tauto. + - decide (p y) as [B|B]; simpl; + rewrite IHA; intuition; subst; tauto. + Qed. + + Lemma filter_incl A : + filter p A <<= A. + + Proof. + intros x D. apply in_filter_iff in D. apply D. + Qed. + + Lemma filter_mono A B : + A <<= B -> filter p A <<= filter p B. + + Proof. + intros D x E. apply in_filter_iff in E as [E E']. + apply in_filter_iff. auto. + Qed. + + Lemma filter_id A : + (forall x, x el A -> p x) -> filter p A = A. + Proof. + intros D. + induction A as [|x A]; simpl. + - reflexivity. + - decide (p x) as [E|E]. + + f_equal; auto. + + exfalso. auto. + Qed. + + Lemma filter_app A B : + filter p (A ++ B) = filter p A ++ filter p B. + Proof. + induction A as [|y A]; simpl. + - reflexivity. + - rewrite IHA. decide (p y); reflexivity. + Qed. + + Lemma filter_fst x A : + p x -> filter p (x::A) = x::filter p A. + Proof. + simpl. decide (p x); tauto. + Qed. + + Lemma filter_fst' x A : + ~ p x -> filter p (x::A) = filter p A. + Proof. + simpl. decide (p x); tauto. + Qed. + +End FilterLemmas. + +Section FilterLemmas_pq. + Variable X : Type. + Variable p q : X -> Prop. + Context {p_dec : forall x, dec (p x)}. + Context {q_dec : forall x, dec (q x)}. + + Lemma filter_pq_mono A : + (forall x, x el A -> p x -> q x) -> filter p A <<= filter q A. + + Proof. + intros D x E. apply in_filter_iff in E as [E E']. + apply in_filter_iff. auto. + Qed. + + Lemma filter_pq_eq A : + (forall x, x el A -> (p x <-> q x)) -> filter p A = filter q A. + + Proof. + intros C; induction A as [|x A]; simpl. + - reflexivity. + - decide (p x) as [D|D]; decide (q x) as [E|E]. + + f_equal. auto. + + exfalso. apply E, (C x); auto. + + exfalso. apply D, (C x); auto. + + auto. + Qed. + + Lemma filter_and A : + filter p (filter q A) = filter (fun x => p x /\ q x) A. + Proof. + set (r x := p x /\ q x). + induction A as [|x A]; simpl. reflexivity. + decide (q x) as [E|E]; simpl; rewrite IHA. + - decide (p x); decide (r x); unfold r in *|-; auto; tauto. + - decide (r x); unfold r in *|-; auto; tauto. + Qed. + +End FilterLemmas_pq. + +Section FilterComm. + Variable X : Type. + Variable p q : X -> Prop. + Context {p_dec : forall x, dec (p x)}. + Context {q_dec : forall x, dec (q x)}. + + Lemma filter_comm A : + filter p (filter q A) = filter q (filter p A). + Proof. + rewrite !filter_and. apply filter_pq_eq. tauto. + Qed. +End FilterComm. + +(** * Element removal *) + +Section Removal. + Variable X : Type. + Context {eq_X_dec : eq_dec X}. + + Definition rem (A : list X) (x : X) : list X := + filter (fun z => z <> x) A. + + Lemma in_rem_iff x A y : + x el rem A y <-> x el A /\ x <> y. + Proof. + apply in_filter_iff. + Qed. + + Lemma rem_not_in x y A : + x = y \/ ~ x el A -> ~ x el rem A y. + Proof. + intros D E. apply in_rem_iff in E. tauto. + Qed. + + Lemma rem_incl A x : + rem A x <<= A. + Proof. + apply filter_incl. + Qed. + + Lemma rem_mono A B x : + A <<= B -> rem A x <<= rem B x. + Proof. + apply filter_mono. + Qed. + + Lemma rem_cons A B x : + A <<= B -> rem (x::A) x <<= B. + Proof. + intros E y F. apply E. apply in_rem_iff in F. + destruct F as [[|]]; congruence. + Qed. + + Lemma rem_cons' A B x y : + x el B -> rem A y <<= B -> rem (x::A) y <<= B. + Proof. + intros E F u G. + apply in_rem_iff in G as [[[]|G] H]. exact E. + apply F. apply in_rem_iff. auto. + Qed. + + Lemma rem_in x y A : + x el rem A y -> x el A. + Proof. + apply rem_incl. + Qed. + + Lemma rem_neq x y A : + x <> y -> x el A -> x el rem A y. + Proof. + intros E F. apply in_rem_iff. auto. + Qed. + + Lemma rem_app x A B : + x el A -> B <<= A ++ rem B x. + Proof. + intros E y F. decide (x=y) as [[]|]; auto using rem_neq. + Qed. + + Lemma rem_app' x A B C : + rem A x <<= C -> rem B x <<= C -> rem (A ++ B) x <<= C. + Proof. + unfold rem; rewrite filter_app; auto. + Qed. + + Lemma rem_equi x A : + x::A === x::rem A x. + Proof. + split; intros y; + intros [[]|E]; decide (x=y) as [[]|D]; + eauto using rem_in, rem_neq. + Qed. + + Lemma rem_comm A x y : + rem (rem A x) y = rem (rem A y) x. + Proof. + apply filter_comm. + Qed. + + Lemma rem_fst x A : + rem (x::A) x = rem A x. + Proof. + unfold rem. rewrite filter_fst'; auto. + Qed. + + Lemma rem_fst' x y A : + x <> y -> rem (x::A) y = x::rem A y. + Proof. + intros E. unfold rem. rewrite filter_fst; auto. + Qed. + + Lemma rem_id x A : + ~ x el A -> rem A x = A. + Proof. + intros D. apply filter_id. + intros y E F. subst. auto. + Qed. + + Lemma rem_reorder x A : + x el A -> A === x :: rem A x. + Proof. + intros D. rewrite <- rem_equi. apply equi_push, D. + Qed. + + Lemma rem_inclr A B x : + A <<= B -> ~ x el A -> A <<= rem B x. + Proof. + intros D E y F. apply in_rem_iff. + intuition; subst; auto. + Qed. + +End Removal. + +Hint Resolve rem_not_in rem_incl rem_mono rem_cons rem_cons' rem_app rem_app' rem_in rem_neq rem_inclr. + +(** * Cardinality *) + +Section Cardinality. + Variable X : Type. + Context { eq_X_dec : eq_dec X }. + Implicit Types A B : list X. + + Fixpoint card A := + match A with + | nil => 0 + | x::A => if decision (x el A) then card A else 1 + card A + end. + + Lemma card_in_rem x A : + x el A -> card A = 1 + card (rem A x). + Proof. + intros D. + induction A as [|y A]; simpl. + - contradiction D. + - decide (y <> x) as [E|E]; simpl. + + rewrite IHA. + * { decide (y el A) as [G|G]; + decide (y el rem A x) as [K|K]; + (reflexivity || exfalso). + - auto. + - eapply G, in_rem_iff, K. } + * destruct D; tauto. + + apply dec_DN in E; auto; subst y. + decide (x el A) as [F|F]. + * auto. + * rewrite rem_id; auto. + Qed. + + Lemma card_not_in_rem A x : + ~ x el A -> card A = card (rem A x). + Proof. + intros D; rewrite rem_id; auto. + Qed. + + Lemma card_le A B : + A <<= B -> card A <= card B. + Proof. + revert B. + induction A as [|x A]; intros B D; simpl. + - omega. + - apply incl_lcons in D as [D D1]. + decide (x el A) as [E|E]. + + auto. + + rewrite (card_in_rem D). + cut (card A <= card (rem B x)). omega. + apply IHA. auto. + Qed. + + Lemma card_eq A B : + A === B -> card A = card B. + Proof. + intros [E F]. apply card_le in E. apply card_le in F. omega. + Qed. + + Lemma card_cons_rem x A : + card (x::A) = 1 + card (rem A x). + Proof. + rewrite (card_eq (rem_equi x A)). simpl. + decide (x el rem A x) as [D|D]. + - exfalso. apply in_rem_iff in D; tauto. + - reflexivity. + Qed. + + Lemma card_0 A : + card A = 0 -> A = nil. + Proof. + destruct A as [|x A]; intros D. + - reflexivity. + - exfalso. rewrite card_cons_rem in D. omega. + Qed. + + Lemma card_ex A B : + card A < card B -> exists x, x el B /\ ~ x el A. + Proof. + intros D. + decide (B <<= A) as [E|E]. + - exfalso. apply card_le in E. omega. + - apply list_exists_not_incl; auto. + Qed. + + Lemma card_equi A B : + A <<= B -> card A = card B -> A === B. + Proof. + revert B. + induction A as [|x A]; simpl; intros B D E. + - symmetry in E. apply card_0 in E. now rewrite E. + - apply incl_lcons in D as [D D1]. + decide (x el A) as [F|F]. + + rewrite (IHA B); auto. + + rewrite (IHA (rem B x)). + * symmetry. apply rem_reorder, D. + * auto. + * apply card_in_rem in D. omega. + Qed. + + Lemma card_lt A B x : + A <<= B -> x el B -> ~ x el A -> card A < card B. + Proof. + intros D E F. + decide (card A = card B) as [G|G]. + + exfalso. apply F. apply (card_equi D); auto. + + apply card_le in D. omega. + Qed. + + Lemma card_or A B : + A <<= B -> A === B \/ card A < card B. + Proof. + intros D. + decide (card A = card B) as [F|F]. + - left. apply card_equi; auto. + - right. apply card_le in D. omega. + Qed. + +End Cardinality. + +Instance card_equi_proper X (D: eq_dec X) : + Proper (@equi X ==> eq) (@card X D). +Proof. + hnf. apply card_eq. +Qed. + +(** * Duplicate-free lists *) + +Inductive dupfree (X : Type) : list X -> Prop := +| dupfreeN : dupfree nil +| dupfreeC x A : ~ x el A -> dupfree A -> dupfree (x::A). + +Section Dupfree. + Variable X : Type. + Implicit Types A B : list X. + + Lemma dupfree_cons x A : + dupfree (x::A) <-> ~ x el A /\ dupfree A. + Proof. + split; intros D. + - inv D; auto. + - apply dupfreeC; tauto. + Qed. + + Lemma dupfree_app A B : + disjoint A B -> dupfree A -> dupfree B -> dupfree (A++B). + + Proof. + intros D E F. induction E as [|x A E' E]; simpl. + - exact F. + - apply disjoint_cons in D as [D D']. + constructor; [|exact (IHE D')]. + intros G. apply in_app_iff in G; tauto. + Qed. + + Lemma dupfree_map Y A (f : X -> Y) : + (forall x y, x el A -> y el A -> f x = f y -> x=y) -> + dupfree A -> dupfree (map f A). + + Proof. + intros D E. induction E as [|x A E' E]; simpl. + - constructor. + - constructor; [|now auto]. + intros F. apply in_map_iff in F as [y [F F']]. + rewrite (D y x) in F'; auto. + Qed. + + Lemma dupfree_filter p (p_dec : forall x, dec (p x)) A : + dupfree A -> dupfree (filter p A). + + Proof. + intros D. induction D as [|x A C D]; simpl. + - left. + - decide (p x) as [E|E]; [|exact IHD]. + right; [|exact IHD]. + intros F. apply C. apply filter_incl in F. exact F. + Qed. + + Lemma dupfree_dec A : + eq_dec X -> dec (dupfree A). + + Proof. + intros D. induction A as [|x A]. + - left. left. + - decide (x el A) as [E|E]. + + right. intros F. inv F; tauto. + + destruct (IHA) as [F|F]. + * unfold dec. auto using dupfree. + * right. intros G. inv G; tauto. + Qed. + + Lemma dupfree_card A (eq_X_dec : eq_dec X) : + dupfree A -> card A = |A|. + Proof. + intros D. + induction D as [|x A E F]; simpl. + - reflexivity. + - decide (x el A) as [G|]. + + contradiction (E G). + + omega. + Qed. + +End Dupfree. + +Section Undup. + Variable X : Type. + Context {eq_X_dec : eq_dec X}. + Implicit Types A B : list X. + + Fixpoint undup (A : list X) : list X := + match A with + | nil => nil + | x::A' => if decision (x el A') then undup A' else x :: undup A' + end. + + Lemma undup_id_equi A : + undup A === A. + Proof. + induction A as [|x A]; simpl. + - reflexivity. + - decide (x el A) as [E|E]; rewrite IHA; auto. + Qed. + + Lemma dupfree_undup A : + dupfree (undup A). + Proof. + induction A as [|x A]; simpl. + - left. + - decide (x el A) as [E|E]; auto. + right; auto. now rewrite undup_id_equi. + Qed. + + Lemma undup_incl A B : + A <<= B <-> undup A <<= undup B. + Proof. + now rewrite !undup_id_equi. + Qed. + + Lemma undup_equi A B : + A === B <-> undup A === undup B. + Proof. + now rewrite !undup_id_equi. + Qed. + + Lemma undup_id A : + dupfree A -> undup A = A. + Proof. + intros E. induction E as [|x A E F]; simpl. + - reflexivity. + - rewrite IHF. decide (x el A) as [G|G]; tauto. + Qed. + + Lemma undup_idempotent A : + undup (undup A) = undup A. + + Proof. apply undup_id, dupfree_undup. Qed. + +End Undup. + +(** * Power lists *) + +Section PowerRep. + Variable X : Type. + Context {eq_X_dec : eq_dec X}. + + Fixpoint power (U : list X ) : list (list X) := + match U with + | nil => [nil] + | x :: U' => power U' ++ map (cons x) (power U') + end. + + Lemma power_incl A U : + A el power U -> A <<= U. + + Proof. + revert A; induction U as [|x U]; simpl; intros A D. + - destruct D as [[]|[]]; auto. + - apply in_app_iff in D as [E|E]. now auto. + apply in_map_iff in E as [A' [E F]]. subst A. + auto. + Qed. + + Lemma power_nil U : + nil el power U. + + Proof. induction U; simpl; auto. Qed. + + Definition rep (A U : list X) : list X := + filter (fun x => x el A) U. + + Lemma rep_power A U : + rep A U el power U. + + Proof. + revert A; induction U as [|x U]; intros A. + - simpl; auto. + - simpl. decide (x el A) as [D|D]; auto using in_map. + Qed. + + Lemma rep_incl A U : + rep A U <<= A. + + Proof. + unfold rep. intros x D. apply in_filter_iff in D. apply D. + Qed. + + Lemma rep_in x A U : + A <<= U -> x el A -> x el rep A U. + Proof. + intros D E. apply in_filter_iff; auto. + Qed. + + Lemma rep_equi A U : + A <<= U -> rep A U === A. + + Proof. + intros D. split. now apply rep_incl. + intros x. apply rep_in, D. + Qed. + + Lemma rep_mono A B U : + A <<= B -> rep A U <<= rep B U. + + Proof. intros D. apply filter_pq_mono. auto. Qed. + + Lemma rep_eq' A B U : + (forall x, x el U -> (x el A <-> x el B)) -> rep A U = rep B U. + + Proof. intros D. apply filter_pq_eq. auto. Qed. + + Lemma rep_eq A B U : + A === B -> rep A U = rep B U. + + Proof. intros D. apply filter_pq_eq. firstorder. Qed. + + Lemma rep_injective A B U : + A <<= U -> B <<= U -> rep A U = rep B U -> A === B. + + Proof. + intros D E F. transitivity (rep A U). + - symmetry. apply rep_equi, D. + - rewrite F. apply rep_equi, E. + Qed. + + Lemma rep_idempotent A U : + rep (rep A U) U = rep A U. + + Proof. + unfold rep at 1 3. apply filter_pq_eq. + intros x D. split. + + apply rep_incl. + + intros E. apply in_filter_iff. auto. + Qed. + + Lemma dupfree_power U : + dupfree U -> dupfree (power U). + + Proof. + intros D. induction D as [|x U E D]; simpl. + - constructor. now auto. constructor. + - apply dupfree_app. + + intros [A [F G]]. apply in_map_iff in G as [A' [G G']]. + subst A. apply E. apply (power_incl F). auto. + + exact IHD. + + apply dupfree_map; congruence. + Qed. + + Lemma dupfree_in_power U A : + A el power U -> dupfree U -> dupfree A. + + Proof. + intros E D. revert A E. + induction D as [|x U D D']; simpl; intros A E. + - destruct E as [[]|[]]. constructor. + - apply in_app_iff in E as [E|E]. + + auto. + + apply in_map_iff in E as [A' [E E']]. subst A. + constructor. + * intros F; apply D. apply (power_incl E'), F. + * auto. + Qed. + + Lemma rep_dupfree A U : + dupfree U -> A el power U -> rep A U = A. + + Proof. + intros D; revert A. + induction D as [|x U E F]; intros A G. + - destruct G as [[]|[]]; reflexivity. + - simpl in G. apply in_app_iff in G as [G|G]. + + simpl. decide (x el A) as [H|H]. + * exfalso. apply E. apply (power_incl G), H. + * auto. + + apply in_map_iff in G as [A' [G H]]. subst A. + simpl. decide (x=x \/ x el A') as [G|G]. + * f_equal. rewrite <- (IHF A' H) at 2. + apply filter_pq_eq. apply power_incl in H. + intros z K. split; [|now auto]. + intros [L|L]; subst; tauto. + * exfalso; auto. + Qed. + + Lemma power_extensional A B U : + dupfree U -> A el power U -> B el power U -> A === B -> A = B. + + Proof. + intros D E F G. + rewrite <- (rep_dupfree D E). rewrite <- (rep_dupfree D F). + apply rep_eq, G. + Qed. + +End PowerRep. + +(** * Finite closure iteration *) + +Module FCI. +Section FCI. + Variable X : Type. + Context {eq_X_dec : eq_dec X}. + Variable step : list X -> X -> Prop. + Context {step_dec : forall A x, dec (step A x)}. + Variable V : list X. + + Lemma pick (A : list X) : + { x | x el V /\ step A x /\ ~ x el A } + { forall x, x el V -> step A x -> x el A }. + Proof. + destruct (list_sigma_forall V (fun x => step A x /\ ~ x el A)) as [E|E]. + - auto. + - right. intros x F G. + decide (x el A). assumption. exfalso. + eapply E; eauto. + Qed. + + Definition F (A : list X) : list X. + destruct (pick A) as [[x _]|_]. + - exact (x::A). + - exact A. + Defined. + + Definition C := it F (card V) nil. + + Lemma it_incl n : + it F n nil <<= V. + Proof. + apply it_ind. now auto. + intros A E. unfold F. + destruct (pick A) as [[x G]|G]; intuition. + Qed. + + Lemma incl : + C <<= V. + Proof. + apply it_incl. + Qed. + + Lemma ind p : + (forall A x, inclp A p -> x el V -> step A x -> p x) -> inclp C p. + Proof. + intros B. unfold C. apply it_ind. + + intros x []. + + intros D G x. unfold F. + destruct (pick D) as [[y E]|E]. + * intros [[]|]; intuition; eauto. + * intuition. + Qed. + + Lemma fp : + F C = C. + Proof. + pose (sigma (A : list X) := card V - card A). + replace C with (it F (sigma nil) nil). + - apply it_fp. intros n. simpl. + set (J:= it F n nil). unfold FP, F. + destruct (pick J) as [[x B]|B]. + + right. + assert (G: card J < card (x :: J)). + { apply card_lt with (x:=x); intuition. } + assert (H: card (x :: J) <= card V). + { apply card_le, incl_cons. apply B. apply it_incl. } + unfold sigma. omega. + + auto. + - unfold C, sigma. f_equal. change (card nil) with 0. omega. + Qed. + + Lemma closure x : + x el V -> step C x -> x el C. + Proof. + assert (A2:= fp). + unfold F in A2. + destruct (pick C) as [[y _]| B]. + + contradiction (list_cycle A2). + + apply B. + Qed. + +End FCI. +End FCI. + +(** * Deprecated names, defined for backward compatibilitly *) + +Definition dupfree_inv := dupfree_cons. diff --git a/cf/Binarize.v b/cf/Binarize.v new file mode 100644 index 0000000..b611ffb --- /dev/null +++ b/cf/Binarize.v @@ -0,0 +1,138 @@ +Require Export Separate. + +Fixpoint step G G' := + match G' with + [] => [] + | R A [] :: Gr => R A [] :: step G Gr + | R A [s0] :: Gr => R A [s0] :: step G Gr + | R A [s0 ; s1] :: Gr => R A [s0 ; s1] :: step G Gr + | R A (s0 :: ur) :: Gr => + let (B, H) := pickFresh G + in R A [s0 ; Vs B] :: R B ur :: Gr + end. + +Definition step' G := step G G. + +Fixpoint count_bin G := + match G with + [] => 0 + | R A u :: Gr => if decision ((|u|) <= 2) then count_bin Gr else |u| + count_bin Gr + end. + +Definition bin G := it step' (count_bin G) G. + +Definition binary G := forall A u, R A u el G -> (|u|) <= 2. + +(** * Binarization yields binary gramar *) + +Lemma count_decr G G' : + step G' G <> G -> count_bin G > count_bin (step G' G). +Proof. + intros H. + induction G as [| [A u] G IHG] ; simpl in * ; [tauto | ]. + destruct u as [| s0 [| s1 [| s2 u]]] ; try now (simpl ; apply IHG ; intros H0 ; apply H ; f_equal). + simpl. decide (S (S (| u |)) <= 2) as [D | D] ; omega. +Qed. + +Lemma fp_bin G : + FP step' (bin G). +Proof. + apply it_fp. intros n. + remember (it step' n G) as G'. + decide (step' G' = G') as [D | D]. + - left. auto. + - right. simpl. rewrite <- HeqG'. + apply count_decr in D. unfold step'. omega. +Qed. + +Lemma fp_binary G : + FP step' G -> binary G. +Proof. + intros Ss A u Ru. + unfold FP, step' in Ss. + remember G as G'. + do 2 rewrite HeqG' in Ss at 2. + rewrite HeqG' in Ru. clear HeqG'. + induction G as [| [B v] Gr IHGr] ; simpl in * ; [tauto |]. + destruct Ru as [Ru | Ru]. + - inv Ru. destruct u as [| s0 [| s1 [| s2 u]]] ; simpl ; auto. inv Ss. + - destruct v as [| s0 [| s1 [| s2 v]]] ; try now (simpl in Ss ; inversion Ss ; apply IHGr ; auto). +Qed. + + Lemma bin_binary G : + binary (bin G). + Proof. + apply fp_binary, fp_bin. + Qed. + +(** * Binarization preserves languages *) + +Lemma step_or G G' : + step G' G = G \/ exists A Gr B u s, G === R A (s :: u) :: Gr /\ step G' G === R A [s ; Vs B] :: R B u :: Gr /\ ~ Vs B el symbs G'. +Proof. + induction G as [| [A u] G IHG]. + - simpl. now left. + - destruct u as [| s0 [| s1 [| s2 u]]] ; unfold step. + + destruct IHG as [H | [A' [Gr [B' [u' [s [H0 [H1 H2]]]]]]]] ; try now (left ; f_equal). + right. exists A', (R A [] :: Gr), B', u', s. repeat split ; try rewrite H0 ; auto using Base.equi_swap ; rewrite H1 ; auto 7 using Base.equi_swap. + + simpl ; destruct IHG as [H | [A' [Gr [B' [u' [s [H0 [H1 H2]]]]]]]] ; try now (left ; f_equal). + right. exists A', (R A [s0] :: Gr), B', u', s. repeat split ; try rewrite H0 ; auto using Base.equi_swap ; rewrite H1 ; auto 7 using Base.equi_swap. + + simpl ; destruct IHG as [H | [A' [Gr [B' [u' [s [H0 [H1 H2]]]]]]]] ; try now (left ; f_equal). + right. exists A', (R A [s0 ; s1] :: Gr), B', u', s. repeat split ; try rewrite H0 ; auto using Base.equi_swap ; rewrite H1 ; auto 7 using Base.equi_swap. + + destruct (pickFresh G') as [B N]. + right. exists A, G, B, (s1 :: s2 :: u), s0. repeat split ; auto. + intros H. specialize (N (Vs B) H). unfold sless' in N. omega. +Qed. + +Lemma step_der_equiv G A u : + terminal u -> (Vs A) el dom G -> (der G A u <-> der (step G G) A u). +Proof. + intros T Do. + destruct (step_or G G) as [Ss | Ss]. + - rewrite <- Ss at 1. split ; auto. + - destruct Ss as [A' [Gr [B [v [s [H0 [H1 H2]]]]]]]. + assert (RL : substG (R A' [s; Vs B] :: Gr) (Vs B) v = R A' (s :: v) :: Gr). { + simpl. decide (s = Vs B). + + exfalso. rewrite e in H0. + apply H2. apply symbs_inv. exists A', (Vs B :: v). rewrite H0. split ; auto. + + decide (Vs B = Vs B) ; try tauto. rewrite app_nil_r. f_equal. + apply substG_skip. intros H. apply H2. + apply symbs_subset with (G := Gr) ; auto. rewrite H0. auto. } + rewrite der_equiv_G with (G1 := step G G) (G2 := R B v :: R A' [s; Vs B] :: Gr) by (rewrite Base.equi_swap ; auto). + rewrite der_equiv_G with (G2 := R A' (s :: v) :: Gr) ; auto. + rewrite <- RL. symmetry. apply der_substG_G_equiv. + + intros H. apply symbs_dom in Do. inv H. tauto. + + simpl. intros [H | H]. + { inv H. apply H2. apply symbs_inv. exists B, (s :: v). rewrite H0. split ; auto. } + { apply symbs_dom in H. apply H2. + apply symbs_subset with (G := Gr) ; auto. rewrite H0. auto. } + + intros H. apply H2. apply symbs_inv. exists A', (s :: v). rewrite H0. split ; auto. + + intros H. destruct (T (Vs B) H) as [t T']. inv T'. +Qed. + +Lemma step_dom G G' : + dom G <<= dom (step G' G). +Proof. + revert G'. + induction G as [| [A u] G IHG] ; intros G' ; try destruct u as [| s0 [| s1 [| s2 u]]] ; simpl ; auto. +Qed. + +Lemma bin_der_equiv G A u : + terminal u -> (Vs A) el dom G -> (der G A u <-> der (bin G) A u). +Proof. + unfold bin. remember (count_bin G) as n. clear Heqn. + intros T. revert G. + induction n as [| n IHn] ; intros G Do ; simpl. + - split ; auto. + - rewrite (IHn G Do). + apply step_der_equiv ; auto. + apply it_ind ; auto. + intros r H0. now apply step_dom. +Qed. + +Lemma bin_language G A u : + Vs A el dom G -> (language G A u <-> language (bin G) A u). +Proof. + intros D. + split ; intros [L0 L1] ; split ; auto ; [rewrite <- bin_der_equiv | rewrite bin_der_equiv] ; auto. +Qed. \ No newline at end of file diff --git a/cf/Chomsky.v b/cf/Chomsky.v new file mode 100644 index 0000000..7ab3626 --- /dev/null +++ b/cf/Chomsky.v @@ -0,0 +1,116 @@ +Require Export Basics Separate Binarize ElimE ElimU. +Local Open Scope program_scope. + +Definition chomsky G := efree G /\ uniform G /\ binary G /\ unitfree G. +Definition normalize := elimU ∘ elimE ∘ sep ∘ bin. + +(** * Normalization yields Chomsky normal form *) + +Lemma substG_preservesLength G s s' : + binary G -> binary (substG G s [s']). +Proof. + intros H. induction G as [| [A u] G IHG] ; simpl ; auto. + intros B v [E | E]. + - inv E. rewrite <- substL_length_unit ; eauto. + - eapply IHG ; eauto. + intros B' v' E'. eapply H ; eauto. +Qed. + +(** ** Preservation of binarity *) + +Lemma binary_sep G : binary G -> binary (sep G). +Proof. + intros H. + unfold sep. + apply it_ind ; auto. + intros G' Bi. + unfold Separate.step. + destruct (pickCharRule G') as [[a [B [v [H0 [H1 H2]]]]] | H0 ] ; auto. + destruct (pickFresh G') as [C N]. + cut (binary (substG G' (Ts a) [Vs C])) ; auto using substG_preservesLength. + intros Bin A u E. destruct E ; [inv H3 | ] ; eauto. +Qed. + +Lemma binary_elimE G : binary G -> binary (elimE G). +Proof. + intros H A u H0. + apply delE_rules, closure_slist in H0. + destruct H0 as [u' [H0 H1]]. + apply slist_length in H1. + specialize (H A u' H0). omega. +Qed. + +Lemma binary_unit G : binary G -> binary (elimU G). +Proof. + intros H A u H0. + apply rule_ranG, ran_elimU_G, ranG_rule in H0. + destruct H0 as [B H0]. + apply (H B u H0). +Qed. + +(** ** Preservation of uniformness *) + +Lemma excluded_free G : uniform G -> uniform (elimE G). +Proof. + intros H A u H0 a E. + apply delE_rules in H0. + apply closure_slist in H0. + destruct H0 as [u' [H1 H2]]. + assert (H4 : Ts a el u') by (apply slist_subsumes in H2 ; auto). + specialize (H A u' H1 a H4). + subst. inv H2. + - inv H6. destruct E. + - now inv H3. +Qed. + +Lemma excluded_unit G : uniform G -> uniform (elimU G). +Proof. + intros H A u Ru. + apply rule_ranG, ran_elimU_G, ranG_rule in Ru. + destruct Ru as [B H0]. + apply (H B u H0). +Qed. + +(** ** Preservation of epsilon-freeness *) + +Lemma efree_unit G : efree G -> efree (elimU G). +Proof. + intros H A u Ru. + apply rule_ranG, ran_elimU_G, ranG_rule in Ru. + destruct Ru as [B H0]. + apply (H B u H0). +Qed. + +Lemma chomsky_normalform G : + chomsky (normalize G). +Proof. + repeat split. + - apply efree_unit, efree_elimE. + - apply excluded_unit, excluded_free, sep_uniform. + - apply binary_unit, binary_elimE, binary_sep, bin_binary. + - apply unitfree_elimU. +Qed. + +(** * Normalization preserves languages *) + +Lemma bin_dom G : + dom G <<= dom (bin G). +Proof. + unfold bin. + apply it_ind ; auto. + intros G' H. + setoid_transitivity (dom G') ; auto. + apply Binarize.step_dom. +Qed. + +Lemma language_normalform G A u : + Vs A el dom G -> u <> [] -> (language G A u <-> language (normalize G) A u). +Proof. + intros Do U. + unfold normalize. + rewrite bin_language ; auto. + rewrite sep_language ; try now apply bin_dom. + rewrite elimE_language ; auto. + now rewrite unit_language. +Qed. + diff --git a/cf/Dec_Empty.v b/cf/Dec_Empty.v new file mode 100644 index 0000000..776bef1 --- /dev/null +++ b/cf/Dec_Empty.v @@ -0,0 +1,114 @@ +Require Export Derivation Symbols. + +Section Dec_Emptys. + Variable G : grammar. + + (** * Productive variables *) + + Inductive productive (G : grammar) : symbol -> Prop := + | TProd (a : ter) : productive G (Ts a) + | VProd A u : R A u el G -> (forall s, s el u -> productive G s) -> productive G (Vs A). + Hint Constructors productive. + + Lemma derf_productive u v : + derf G u v -> (forall s, s el v -> productive G s) -> forall s, s el u -> productive G s. + Proof. + intros D H. + induction D ; intros s' E ; auto ; destruct E as [E | E] ; try destruct E ; subst ; eauto. + Qed. + + Lemma productive_derf s : + productive G s -> exists x, derf G [s] x /\ terminal x. + Proof. + induction 1 as [a | A u H0 H1 IH]. + - exists [Ts a]. split ; auto. + intros s [H | H] ; [subst ; exists a ; auto | destruct H]. + - cut (exists y, derf G u y /\ terminal y). + + intros [y [H2 H3]]. exists y. split ; eauto. + + clear H1 H0. induction u as [| s u IHu]. + * exists []. split ; auto. intros s []. + * assert (H0 : forall s, s el u -> exists x : phrase, derf G [s] x /\ terminal x) by auto. + destruct (IHu H0) as [y [H1 H2]]. + assert (H3 : s el s :: u) by auto. + destruct (IH s H3) as [x [IH0 IH1]]. + exists (x ++ y). split ; auto. + intros s' T. apply in_app_iff in T. destruct T as [T | T] ; auto. + Qed. + + Lemma productive_derWord_equi A : + (exists w, der G A w /\ terminal w) <-> productive G (Vs A). + Proof. + split ; intro H. + - destruct H as [w [H1 H2]]. + apply derf_der_equiv in H1. + eapply derf_productive ; eauto. + intros s W. + destruct (H2 s W) as [t H3] ; subst ; auto. + - apply productive_derf in H. + destruct H as [w H]. + exists w. now rewrite <- derf_der_equiv. + Qed. + + (** ** Compute productive variables *) + Definition step (M : list symbol) s := + (exists a, s = Ts a) \/ + exists A u, s = Vs A /\ + R A u el G /\ + forall s', s' el u -> s' el M. + + Instance step_dec M s : dec (step M s). + Proof. + destruct s as [a | A]. + - left. left. exists a. auto. + - decide (exists u, R A u el G /\ forall s', s' el u -> s' el M) as [D | D]. + + left. right. destruct D as [u [D0 D1]]. exists A, u. repeat split ; auto. + + right. intros [[a H0] | [A' [u [H0 [H1 H2]]]]] ; inversion H0 as [H3] ; subst. + apply D. exists u. auto. + Defined. + + Definition P : list symbol := + FCI.C (step := step) (symbs G). + + (** ** Correctness *) + Lemma productive_P s : + s el symbs G -> productive G s -> s el P. + Proof. + intros E H. + induction H ; apply FCI.closure ; auto. + - left. exists a. auto. + - right. exists A, u. repeat split ; auto. + intros s' H2. apply H1 ; auto. + apply symbs_inv. + exists A, u. split ; auto. + Qed. + + Lemma P_productive s : + s el P -> productive G s. + Proof. + apply FCI.ind. + intros M x H0 H1 H2. + destruct H2 as [[a H2] | [A [u [H2 [H3 H4]]]]] ; rewrite H2 ; eauto. + Qed. + + Lemma P_productive_equiv s : + s el symbs G -> (s el P <-> productive G s). + Proof. intros H. split ; [apply P_productive | now apply productive_P]. Qed. + +End Dec_Emptys. + +(** * Decidability of emptiness *) + +Instance productive_dec : forall G s, dec (productive G s). +Proof. + intros G [a | A]. + - left. constructor. + - decide (Vs A el symbs G) as [D | D]. + + decide ((Vs A) el P G) ; [left | right] ; now rewrite <- P_productive_equiv. + + right. intros H. inversion H as [| ? u H1 H2] ; subst. apply D, symbs_inv. exists A, u. split ; auto. +Defined. + +Instance exists_dec : forall G A, dec (exists u, language G A u). +Proof. + intros G A. + decide (productive G (Vs A)) as [P | P] ; rewrite <- productive_derWord_equi in P ; [left | right] ; auto. +Defined. \ No newline at end of file diff --git a/cf/Dec_Word.v b/cf/Dec_Word.v new file mode 100644 index 0000000..791a35e --- /dev/null +++ b/cf/Dec_Word.v @@ -0,0 +1,221 @@ +Require Export Derivation. + +Definition item := prod symbol phrase. +Definition items G u : list item := product pair (symbs G) (segms u). + +(** * Computation of item list *) + +Section Dec_Word. + Variable G : grammar. + Variable u : phrase. + + Definition step (M : list item) i := + match i with + (s, v) => v = [s] \/ match s with + Vs A => exists M', M' <<= M /\ R A (fsts M') el G /\ v = concat (snds M') + | _ => False + end + end. + + (** ** Decidability of step *) + Fixpoint fsts_comb X Y (D : eq_dec X) (M : list (X * Y)) (v : list X) : (list (list (X * Y))) := + match v with + [] => [ [] ] + | s :: v => + let + M' := fsts_comb D M v + in let + S := filter (fun e => match e with (s', _) => s = s' end) M + in + product (fun s M => s :: M) S M' + end. + Arguments fsts_comb {X} {Y} {D} M v. + + Lemma fsts_comb_corr1 X Y (D : eq_dec X) (M : list (X * Y)) (v : list X) (l : list (X * Y)) : + l el fsts_comb M v -> fsts l = v /\ l <<= M. + Proof. + revert l. + induction v as [| s v IHv] ; intros l H ; simpl in *. + - destruct H ; try tauto. + rewrite <- H. split ; simpl ; auto. + - apply prod_corr in H. + destruct H as [[s' x] [M' [H0 [H1 H2]]]]. + apply in_filter_iff in H1. + destruct H1 as [H1 H3] ; subst. + destruct (IHv M' H2) as [H4 H5] ; subst. + split ; auto. + Qed. + + Lemma fsts_comb_corr2 X Y (D : eq_dec X) (M : list (X * Y)) (v : list X) (l : list (X * Y)) : + fsts l = v /\ l <<= M -> l el fsts_comb M v. + Proof. + revert l. + induction v as [| s v IHv] ; intros l [H0 H1] ; simpl in *. + - destruct l as [|[s x]] ; auto. inv H0. + - apply prod_corr. + destruct l as [|[s' x]] ; simpl in H0 ; inv H0. + assert (H0 : fsts l = fsts l /\ l <<= M) by firstorder. + specialize (IHv l H0). + exists (s, x), l. repeat split ; auto. + apply in_filter_iff. split ; auto. + Qed. + + Lemma fsts_comb_corr X Y (D : eq_dec X) (M : list (X * Y)) (v : list X) (l : list (X * Y)) : + l el fsts_comb M v <-> fsts l = v /\ l <<= M. + Proof. + split ; [apply fsts_comb_corr1 | apply fsts_comb_corr2]. + Qed. + + Instance step_dec' (M : list item) A v : + dec (exists M', M' <<= M /\ R A (fsts M') el G /\ v = concat (snds M')). + Proof. + induction G as [| [B w] Gr IHGr]. + - right. intros [M' [_ [[] _]]]. + - destruct IHGr as [IHG | IHG]. + + left. destruct IHG as [M' [H0 [H1 H2]]]. + exists M'. repeat split ; auto. + + decide (A = B) as [D | D] ; subst. + * decide (exists M', M' el (fsts_comb M w) /\ v = concat (snds M')) as [D0 | D0]. + { left. destruct D0 as [M' [H0 H1]]. + exists M'. apply fsts_comb_corr in H0. + destruct H0 as [H0 H2]. rewrite H0. repeat split ; auto. } + { right. intros [M' [H0 [H1 H2]]]. + destruct H1. + - inv H. apply D0. + exists M'. split ; auto. + apply fsts_comb_corr. auto. + - apply IHG. exists M'. split ; auto. } + * right. intros [M' [H0 [H1 H2]]]. + apply IHG. destruct H1 as [H1 | H1] ; try (inv H1 ; tauto). + exists M'. repeat split ; auto. + Defined. + + Instance step_dec M i : dec (step M i). + Proof. + destruct i as (s, x). + simpl. decide (x = [s]) ; try now (left ; auto). + destruct s ; auto. + Defined. + + Definition DW := FCI.C (step := step) (items G u). + + Lemma items_refl s v : + s el symbs G -> (s, v) el items G v. + Proof. + intros H. + apply prod_corr. + exists s, v. repeat split ; auto. + apply segms_corr, segment_refl. auto. + Qed. + + (** ** only-if-part *) + Lemma derf_DW v w : + (forall s, s el v -> s el symbs G) -> segment u w -> derf G v w -> exists M, v = fsts M + /\ w = concat (snds M) + /\ M <<= DW. + Proof. + intros U Sg. + induction 1 as [v | A v w' H0 H IHv | s v w' u0 H IH0 H0 IH1]. + - induction v as [| s v IHv]. + + exists []. repeat split ; simpl ; auto. + + assert (U' : forall s : symbol, s el v -> s el symbs G) by auto. + assert (Sg' : segment u v). { + apply segment_trans with (ys := s :: v) ; auto. + exists [s], []. simpl. now rewrite app_nil_r. } + destruct (IHv U' Sg') as [M [H0 [H1 H2]]]. + exists ((s, [s]) :: M). repeat split ; simpl ; rewrite H0, H1 in * ; auto. + intros s0 [H3 | H3]. + * inv H3. apply FCI.closure ; [| now left]. + apply prod_corr. exists s, [s]. repeat split ; auto. + apply segms_corr. apply segment_trans with (ys := (s :: concat (snds M))) ; auto. + exists [], (concat (snds M)). auto. + * now apply H2. + - exists [(Vs A, w')]. + repeat split ; simpl ; try now rewrite app_nil_r. + intros s [H1 | H1] ; [ | destruct H1]. + subst. apply FCI.closure. + + apply prod_corr. exists (Vs A), w'. repeat split ; auto. now apply segms_corr. + + assert (U' : forall s, s el v -> s el symbs G). { + intros s E. apply symbs_inv. exists A, v. split ; auto. } + destruct (IHv U' Sg) as [M [H3 [H4 H5]]]. + right. exists M. repeat split ; rewrite H3 in * ; auto. + - assert (U' : forall s0 : symbol, s0 el [s] -> s0 el symbs G) by (intros s0 E ; inv E ; now apply U). + assert (U'' : forall s0 : symbol, s0 el v -> s0 el symbs G) by auto. + assert (Sg' : segment u w'). { + apply segment_trans with (ys := w' ++ u0) ; auto. + exists [], u0. auto. } + assert (Sg'' : segment u u0). { + apply segment_trans with (ys := w' ++ u0) ; auto. + exists w', []. now rewrite app_nil_r. } + destruct (IH0 U' Sg') as [Ms [Hs0 [Hs1 Hs2]]]. + destruct (IH1 U'' Sg'') as [Mu [Hu0 [Hu1 Hu2]]]. + exists (Ms ++ Mu). repeat split ; auto. + + now rewrite fsts_split, <- Hs0, Hu0. + + now rewrite snds_split, concat_split, <- Hu1, <- Hs1. +Qed. + + (** ** if-part *) + + Lemma DW_derf' : + inclp DW (fun i => match i with (s, v) => derf G [s] v end). + Proof. + apply FCI.ind. + intros M [[a | A] v] IH X S ; simpl in S ; destruct S ; try tauto ; try (rewrite H ; constructor). + destruct H as [M' [H0 [H1 H2]]]. + econstructor 2 ; eauto. + unfold inclp in IH. + clear H1 X. revert H2. revert v. + induction M' as [| [s x] Mr IHM] ; intros v H2 ; rewrite H2 ; simpl in * ; eauto. + constructor 3 ; firstorder. + assert (H3 : (s, x) el M) by auto. + specialize (IH (s, x) H3). auto. + Qed. + + Lemma DW_der_equiv' s v : + s el symbs G -> ((s,v) el DW <-> derf G [s] v /\ segment u v). + Proof. + intros Ss. split ; intros H. + - dupapply H DW_derf' H'. + split ; auto. + pose (H0 :=FCI.incl H). + apply prod_corr in H0. + destruct H0 as [? [? [H0 [H1 H2]]]] ; inv H0. + now apply segms_corr in H2. + - destruct H as [H0 H1]. + assert (H2 : forall s', s' el [s] -> s' el symbs G) by (intros s' [H2 | []] ; subst ; auto). + destruct (derf_DW H2 H1 H0) as [M [D0 [D1 D2]]]. + apply D2. subst. + assert (H3 : M = [(s, concat (snds M))]). { + destruct M as [| (s', v') M]. + - inv D0. + - simpl in D0. destruct M as [| (s'', v'') M] ; inv D0. + simpl. now rewrite app_nil_r. } + rewrite H3. simpl. rewrite app_nil_r. auto. + Qed. + + Lemma DW_der_equiv A : + Vs A el symbs G -> (der G A u <-> (Vs A, u) el DW). + Proof. + intros Ss. rewrite <- derf_der_equiv. + split ; intros H ; apply DW_der_equiv' ; try split ; auto using segment_refl. + Qed. + +End Dec_Word. + +(** * Decidability of word problem *) + +Instance der_dec G A u : dec (der G A u). +Proof. + decide (Vs A el symbs G). + - decide ((Vs A, u) el DW G u) as [D | D]. + + left. now apply DW_der_equiv. + + right. intros H. apply D. apply DW_der_equiv ; auto. + - decide (u = [Vs A]) as [D | D]. + + left. rewrite D. constructor. + + right. intros H0. apply D. eapply symbs_der ; eauto. +Defined. + +Instance lang_dec G A u : dec (language G A u). +Proof. + auto. +Qed. \ No newline at end of file diff --git a/cf/Definitions.v b/cf/Definitions.v new file mode 100644 index 0000000..6e82d42 --- /dev/null +++ b/cf/Definitions.v @@ -0,0 +1,84 @@ +Require Export Lists. + +(** * Definitions of grammars *) + +Ltac dupapply H1 lemma H2 := pose (H2:= H1) ; apply lemma in H2. + +Inductive ter : Type := +| T : nat -> ter. + +Inductive var : Type := +| V : nat -> var. + +Inductive symbol : Type := +| Ts : ter -> symbol +| Vs : var -> symbol. + +Definition phrase := list symbol. + +Inductive rule : Type := +| R : var -> phrase -> rule. + +Definition grammar := list rule. + +(** * Decidability instances *) + +Instance var_eq_dec : eq_dec var. +Proof. intros A B. unfold dec. repeat decide equality. Defined. + +Instance rule_eq_dec : eq_dec rule. +Proof. intros A B. unfold dec. repeat decide equality. Defined. + +Instance symbol_eq_dec : eq_dec symbol. +Proof. intros A B. unfold dec. repeat decide equality. Defined. + +Instance exists_rule_dec G p {D : forall A u, dec (p A u)} : dec (exists A u, R A u el G /\ p A u). +Proof. + induction G as [| [A u] Gr IHGr]. + - right. intros [A [u [H0 H1]]]. destruct H0. + - destruct IHGr as [IH | IH]. + + left. destruct IH as [A' [u' [H0 H1]]]. + exists A', u'. auto. + + destruct (D A u) as [D' | D']. + * left. exists A, u. auto. + * right. intros [A' [u' [H0 H1]]]. + destruct H0 ; try now inv H. + apply IH. exists A', u'. auto. +Defined. + +Instance exists_phrase_dec G A p : (forall x, dec (p x)) -> dec (exists u , R A u el G /\ p u). +Proof with (intros H1 ; destruct H1 as [u [[H1 | H1] H2]] ; [inv H1 |] ; firstorder). + intros H. + induction G as [| [B v] Gr IHGr] ; try (now right ; intros [u [H0 H1]] ; destruct H0). + destruct IHGr as [IHGr | IHGr] ; try now (left ; firstorder). + decide (A = B) as [D | D] ; subst. + - decide (p v) as [D0 | D0]. + + left. exists v. split ; auto. + + right... + - right... +Defined. + +Instance symbol_ter_dec : forall s, dec (exists a, s = Ts a). +Proof. + intros [s|s] ; [ left ; now exists s | right ; intros [a H] ; inv H]. +Defined. + +Instance phrase_var_dec u : dec (exists A, u = [Vs A]). +Proof with (try now (right ; intros [? H] ; inv H)). + destruct u as [| [t | A] ur]... + destruct ur as [| s ur]... + left. now (exists A). +Defined. + +Instance phrase_char_dec u : dec (exists a, u = [Ts a]). +Proof. + destruct u as [| [a | A] [| s u]] ; try now (right ; intros [b H] ; inv H). + left. exists a. auto. +Qed. + +Instance filter_rule_dec (p : phrase -> Prop) {D : forall u, dec (p u)} : forall r, (dec ((fun r => match r with R A u => p u end) r)). +Proof. + destruct r ; auto. +Defined. + + diff --git a/cf/Derivation.v b/cf/Derivation.v new file mode 100644 index 0000000..a744bdb --- /dev/null +++ b/cf/Derivation.v @@ -0,0 +1,219 @@ +Require Export Symbols. + +(** * Derivability and languages *) + +Inductive der (G : grammar) (A : var) : list symbol -> Prop := +| vDer : der G A [Vs A] +| rDer l : (R A l) el G -> der G A l +| replN B u w v : der G A (u ++ [Vs B] ++ w) -> der G B v -> der G A (u ++ v ++ w). +Hint Constructors der. + +Definition terminal (u : phrase) : Prop := + forall s, s el u -> exists t, s = Ts t. + +Lemma terminal_split u v : + terminal (u ++ v) -> terminal u /\ terminal v. +Proof. + intros H. + split ; intros s T ; apply H ; auto. +Qed. + +Definition language (G : grammar) (A : var) (u : phrase) : Prop := + der G A u /\ terminal u. + +(** * Alternative characterizations of derivability *) +Inductive derL (G : grammar) (A : var) : list symbol -> Prop := +| sDer : derL G A [Vs A] +| gDer B u v w : (R B v) el G -> derL G A (u ++ [Vs B] ++ w) -> derL G A (u ++ v ++ w). +Hint Constructors derL. + +Inductive derT (G : grammar) : list symbol -> list symbol -> Prop := +| derTRefl u : derT G u u +| derTRule A u : R A u el G -> derT G [Vs A] u +| derTTrans u v w x y : derT G x (u ++ y ++ w) -> derT G y v -> derT G x (u++v++w). +Hint Constructors derT. + +Inductive derf (G : grammar) : phrase -> phrase -> Prop := +| fRefl u : derf G u u +| fRule A u v : R A u el G -> derf G u v -> derf G [Vs A] v +| fCons s u v w : derf G [s] v -> derf G u w -> derf G (s :: u) (v ++ w). +Hint Constructors derf. + +Inductive derI (G : grammar) : phrase -> phrase -> Prop := +| derIRefl u : derI G u u +| derIRule A u v w : R A v el G -> derI G (u ++ [Vs A] ++ w) (u ++ v ++ w) +| derITrans u v w : derI G u v -> derI G v w -> derI G u w. +Hint Constructors derI. + +(** ** Linear equivalences *) +Lemma derL_der_equiv (G : grammar) (A : var) (u : list symbol) : + der G A u <-> derL G A u. +Proof. + split. + - induction 1 as [| ? l | A B u w v H IHder1 H0 IHder2] ; eauto. + + replace l with ([] ++ l ++ []) by apply app_nil_r. + econstructor 2 ; eauto using derL. + + clear H H0. + induction IHder2 as [| C x y z] ; auto. + replace (u ++ (x ++ y ++ z) ++ w) with ((u ++ x) ++ y ++ (z ++ w)) by now repeat rewrite app_assoc. + econstructor 2 ; eauto. + now replace ((u++x) ++ [Vs C] ++ (z ++ w)) with ((u ++ (x ++ [Vs C] ++ z) ++ w)) by now repeat rewrite app_assoc. + - induction 1 ; eauto using der. +Qed. + +Lemma derT_der_equiv (G : grammar) (A : var) (u : list symbol) : + der G A u <-> derT G [Vs A] u. +Proof. + split. + - induction 1 ; eauto using derT. + - remember ([Vs A]) as v. + induction 1 as [ | | u v w x y H IHderT1 H0 IHderT2] ; try injection Heqv ; try intros He ; subst ; eauto. + specialize (IHderT1 eq_refl). + clear H IHderT2. + revert IHderT1. revert u w. + induction H0 as [| | u v w x y ? IHderT1 ? IHderT2] ; intros u' w' IH1 ; eauto. + replace (u' ++ (u ++ v ++ w) ++ w') with ((u' ++ u) ++ v ++ (w ++ w')) by now repeat rewrite app_assoc. + apply IHderT2. + replace ((u' ++ u) ++ y ++ w ++ w') with (u' ++ (u ++ y ++ w) ++ w') by now repeat rewrite app_assoc. + now apply IHderT1. +Qed. + +(** ** Properties of derivation predicates *) +Lemma derf_concat G u1 u2 v1 v2 : + derf G u1 v1 -> derf G u2 v2 -> derf G (u1 ++ u2) (v1 ++ v2). +Proof. + intros D0 D1. + induction D0 as [u | | ] ; simpl ; eauto. + - induction u as [|s u] ; auto. simpl. + replace (s :: u ++ v2) with ([s] ++ u ++ v2) ; auto. + - rewrite <- app_assoc. auto. +Qed. + +Lemma derf_split G u u1 u2 v : + derf G u v -> u = u1 ++ u2 -> exists v1 v2, v = v1 ++ v2 /\ derf G u1 v1 /\ derf G u2 v2. +Proof. + intros D. revert u1 u2. + induction D as [ | | s u v w ? IHD1 ? IHD2] ; intros u1 u2 U. + - revert U. revert u1 u2. induction u as [| s u] ; intros u1 u2 U. + + symmetry in U. apply app_eq_nil in U. + destruct U as [U1 U2] ; subst. + exists [], []. repeat split ; auto. + + destruct u1 ; simpl in U ; subst. + * destruct (IHu [] u) as [v1 [v2 [IH0 [IH1 IH2]]]] ; auto. + exists [], (s :: u). repeat split ; auto. + * inv U. destruct (IHu u1 u2) as [v1 [v2 [IH0 [IH1 IH2]]]] ; auto. + exists (s0 :: u1), u2. repeat split ; auto. + - destruct u1 ; simpl in U ; subst. + + exists [], v. repeat split ; eauto. + + inversion U as [[H0 H1]] ; subst. symmetry in H1. + apply app_eq_nil in H1. + destruct H1 as [H1 H1']. subst. + exists v, []. repeat split ; eauto using app_nil_r. + - destruct u1 ; simpl in U ; subst. + + exists [], (v ++ w). repeat split ; auto. + + inversion U as [[H0 H1]]. destruct (IHD2 u1 u2 H1) as [v1 [v2 [IH0 [IH1 IH2]]]] ; subst. + exists (v ++ v1), v2. rewrite <- app_assoc. repeat split ; auto. +Qed. + +Lemma derf_trans G u v w : + derf G u v -> derf G v w -> derf G u w. +Proof. + intros D0. revert w. + induction D0 as [| | ? ? v w] ; intros w' D1 ; eauto. + apply derf_split with (u1 := v) (u2 := w) in D1 ; auto. + destruct D1 as [v1 [v2 [D1 [D2 D3]]]]. + rewrite D1. eauto. +Qed. + +(** ** Remaining equivalences *) + +Lemma derf_derT G u v : + derf G u v -> derT G u v. +Proof. + induction 1 as [ | A u v | s u v w ? ? ? ?] ; eauto. + - replace v with ([] ++ v ++ []) by (simpl ; auto using app_nil_r). + econstructor 3 ; eauto. + constructor 2. simpl. rewrite app_nil_r. eauto. + - replace (s :: u) with ([s] ++ u) by auto. + rewrite <- app_nil_r. rewrite <- app_assoc. + replace ([s] ++ u) with ([s] ++ u ++ []) by now rewrite app_nil_r. + econstructor 3 ; eauto. + repeat rewrite app_nil_r. + rewrite <- app_nil_l. + replace ([s] ++ u) with ([] ++ [s] ++ u) by auto using app_nil_l. + constructor 3 with (y := [s]) ; eauto. +Qed. + +Lemma derT_derI G u v : + derT G u v -> derI G u v. +Proof. + induction 1 as [| A u | ? ? ? ? ? H IHderT1 H0 IHderT2] ; eauto. + - rewrite <- app_nil_r, <- app_nil_l. + replace [Vs A] with ([] ++ [Vs A] ++ []) ; eauto. + - clear H H0. + induction IHderT2 ; auto. + repeat rewrite <- app_assoc in *. + rewrite app_assoc in * ; eauto. +Qed. + +Lemma derI_derf G u v : + derI G u v -> derf G u v. +Proof. + induction 1 ; eauto using derf_concat, derf_trans. +Qed. + +(** ** Inferred equivlaneces and properties *) +Lemma derf_der_equiv G A u : + derf G [Vs A] u <-> der G A u. +Proof. + split ; intros H. + - now apply derT_der_equiv, derf_derT. + - now apply derI_derf, derT_derI, derT_der_equiv. +Qed. + +Lemma derT_trans (G : grammar) (u v w : list symbol) : + derT G u v -> derT G v w -> derT G u w. +Proof. + intros H1 H2. + replace w with ([] ++ w ++ []) by now rewrite <- app_nil_r. + econstructor 3 ; eauto. + now rewrite app_nil_l, app_nil_r. +Qed. + +Lemma derT_concat G u u' v v' : + derT G u v -> derT G u' v' -> derT G (u ++ u') (v ++ v'). +Proof. + intros H0 H1. + apply derf_derT. + apply derT_derI, derI_derf in H0. + apply derT_derI, derI_derf in H1. + apply derf_concat ; auto. +Qed. + +Lemma der_subset G1 G2 A u : + G1 <<= G2 -> der G1 A u -> der G2 A u. +Proof. + induction 2 ; eauto. +Qed. + +(** ** Further Properties *) + +Lemma der_equiv_G G1 G2 A u : + G1 === G2 -> (der G1 A u <-> der G2 A u). +Proof. + intros H. split ; apply der_subset ; destruct H ; auto. +Qed. + +Lemma symbs_der G A u : + ~ Vs A el symbs G -> der G A u -> u = [Vs A]. +Proof. + intros V D. + induction D as [ | A l | A B u v w D IHD1 D0 IHD2] ; auto. + - exfalso. apply V. apply symbs_inv. exists A, l. split ; auto. + - specialize (IHD1 V). + symmetry in IHD1. + apply list_unit in IHD1. + destruct IHD1 as [H0 [H1 H2]] ; injection H2 ; intros H3 ; subst. + rewrite app_nil_r, app_nil_l. + now apply IHD2. +Qed. \ No newline at end of file diff --git a/cf/ElimE.v b/cf/ElimE.v new file mode 100644 index 0000000..48b222c --- /dev/null +++ b/cf/ElimE.v @@ -0,0 +1,288 @@ +Require Export Dec_Word. + +(** * Nullable Variables *) +Inductive nullable (G : grammar) (s : symbol) : Prop := +| Null A u : s = Vs A -> R A u el G -> (forall s', s' el u -> nullable G s') -> nullable G s. +Hint Constructors nullable. + +Lemma derE_nullable (G : grammar) (A : var) (u : phrase) : + der G A u -> (forall s, s el u -> nullable G s) -> nullable G (Vs A). +Proof with (apply U, in_or_app ; (try now left) ; (right ; apply in_or_app ; (try now left) ; try now right)). + intros H U. + induction H as [| u H | A B u w v H IH0 H0 IH1] ; eauto. + apply IH0. + intros s E. + apply in_app_or in E. + destruct E as [E | E]. + + auto... + + destruct E as [E | E]. + * rewrite <- E. apply IH1. intros s' V. auto... + * apply in_app_or in E. destruct E as [E | E] ; firstorder. auto... +Qed. + +Lemma nullable_derE (G : grammar) (s : symbol) : + nullable G s -> exists A, s = Vs A /\ der G A []. +Proof. + induction 1 as [s A u H H0 H1 IH]. + exists A. split ; auto. + clear H H1 s. + apply rDer in H0. + induction u as [|s u IHu] ; auto. + apply IHu ; auto. + assert (H3: s el s::u) by auto. + destruct (IH s H3) as [B [H4 H5]]. rewrite H4 in *. + replace u with ([] ++ [] ++ u) ; eauto. +Qed. + +Lemma nullable_derE_equi (G : grammar) (s : symbol) : + (exists A, s = Vs A /\ der G A []) <-> nullable G s. +Proof. + split ; intro H. + - destruct H as [A [H0 H1]]. + rewrite H0 in *. + eapply derE_nullable ; eauto. firstorder. + - now dupapply H nullable_derE H0. +Qed. + +Instance nullable_dec G s : dec (nullable G s). +Proof. + destruct s as [a | A]. + - right. rewrite <- nullable_derE_equi. intros [A [H0 H1]]. inv H0. + - decide (der G A []) ; [left | right] ; rewrite <- nullable_derE_equi. + + exists A. split ; auto. + + intros [A' [H0 H1]]. inv H0. tauto. +Defined. + +(** * Epsilon closure *) + +Definition efree G := forall A u, R A u el G -> u <> []. + +Fixpoint closure (p : symbol -> Prop) {pdec : forall x, dec (p x)} (G : grammar) := + match G with + [] => [] + | R A u :: Gr => + let + u' := slists p u + in let + G' := map (R A) u' + in G' ++ closure Gr + end. +Arguments closure p {pdec} G. + +Section EClosure. + Variable G : grammar. + + Definition eclosure G:= closure (nullable G) G. + Definition eclosed G := forall A u, R A u el G -> forall v, slist (nullable G) v u -> R A v el G. + + Lemma closure_slist A v (p : symbol -> Prop) {pdec : forall s, dec (p s)} : + R A v el closure p G -> exists u, R A u el G /\ slist p v u. + Proof. + intros H. + induction G as [| [B w] Gr IHGr] ; simpl in H ; [tauto|]. + apply in_app_or in H. + destruct H as [H | H]. + - apply in_map_iff in H. + destruct H as [x [H0 H1]]. + inv H0. exists w. split ; auto. + now apply slists_slist. + - destruct (IHGr H) as [u [H0 H1]]. exists u ; auto. + Qed. + + Lemma slist_closure A v (p : symbol -> Prop) {pdec : forall s, dec (p s)} : + (exists u, R A u el G /\ slist p v u) -> R A v el closure p G. + Proof. + intros [u [H0 H1]]. + induction G as [| [B w] Gr IHGr] ; simpl in H0 ; auto. + destruct H0 as [H0 | H0] ; simpl ; apply in_or_app. + - inv H0. left. apply in_map_iff. + exists v. split ; auto. now apply slists_slist. + - right. auto. + Qed. + + Lemma slist_closure_equiv A v (p : symbol -> Prop) {pdec : forall s, dec (p s)} : + R A v el closure p G <-> exists u, R A u el G /\ slist p v u. + Proof. + split ; [apply closure_slist | apply slist_closure]. + Qed. + + (** ** Epsilon closure is epsilon-closed **) + Lemma nullable_eclosure s : + nullable (eclosure G) s <-> nullable G s. + Proof. + split ; intros H. + - induction H as [? ? ? ? H1 ? ?]. + apply slist_closure_equiv in H1. + destruct H1 as [u' [H3 H4]]. + esplit ; eauto. + eapply slist_inv ; eauto. + - induction H as [? ? u ? ? ? ?]. + esplit ; eauto. + apply slist_closure_equiv. + exists u. split ; auto. apply slist_id. + Qed. + + Lemma eclosed_eclosure : eclosed (eclosure G). + Proof. + intros A u H0 v H1. + apply slist_closure_equiv in H0. + apply slist_closure_equiv. + destruct H0 as [u' [H2 H3]]. + exists u'. split ; auto. + eapply (slist_equiv_pred nullable_eclosure) in H1. + eapply slist_trans ; eauto. + Qed. + + (** ** Epsilon closure preserves languages **) + + Lemma derT_slist u v : + slist (nullable G) v u -> derT G u v. + Proof. + induction 1 as [| ? v u H0 ? ? | s v u ? ?]. + - constructor. + - apply nullable_derE_equi in H0. + destruct H0 as [A [H1 H2]]. + apply derT_der_equiv in H2. + rewrite H1. + assert (H3 : derT G (Vs A :: u) ([] ++ [Vs A] ++ u)) by constructor. + apply derT_trans with (v := [] ++ [] ++ u) ; eauto. + - replace (s :: u) with ([s] ++ u) by auto. + replace (s :: v) with ([s] ++ v) by auto. + apply derT_concat ; eauto. + Qed. + + Lemma eclosure_der u v : + derT (eclosure G) u v -> derT G u v. + Proof. + intros H. + induction H as [| ? ? H |] ; eauto using derT. + apply slist_closure_equiv in H. + destruct H as [u' [H1 H2]]. + apply derTRule in H1. + apply derT_slist in H2. + eapply derT_trans ; eauto. + Qed. + + Lemma der_eclosure_equiv u v : + derT G u v <-> derT (eclosure G) u v. + Proof. + split. + - induction 1 as [| A u |] ; eauto using derT. + constructor 2. + apply slist_closure_equiv. + exists u. split ; auto. apply slist_id. + - apply eclosure_der. + Qed. + +End EClosure. + +(** * Deletion of epsilon rules *) + +Section DelE. + Variable G : grammar. + + Definition delE G := filter (fun r => match r with R A u => u <> [] end) G. + + (** ** delE is epsilon-free *) + Lemma delE_efree : efree (delE G). + Proof. + intros A u H. + induction G as [| [B v] Gr] ; simpl in H. + - tauto. + - decide (v <> []) ; (try destruct H as [H|H]) ; (try now inv H) ; auto. + Qed. + + (** ** delE preserves languages (except for epsion) *) + + Lemma delE_preserveG A u : + R A u el G -> u <> [] -> R A u el delE G. + Proof. + intros H1 H2. + induction G as [| [B v] Gr] ; simpl in H1 ; [tauto|]. + simpl. destruct H1 as [H1 | H1]. + - inv H1. decide (u <> []) ; [auto | contradiction]. + - decide (v <> []) ; [right |] ; auto. + Qed. + + Lemma delE_rules A u : + R A u el (delE G) -> R A u el G. + Proof. + intros H. + induction G as [| [B v] Gr] ; simpl in H ; [tauto|]. + decide (v <> []) ; try destruct H ; try (inv H ; now left) ; try (right ; auto). + Qed. + + Lemma der_G_delE A u v : + eclosed G -> der G A u -> slist (nullable G) v u -> v <> [] -> der (delE G) A v. + Proof. + intros E D Ss U. + apply derL_der_equiv in D. + apply derL_der_equiv. + revert Ss U. revert v. + induction D as [| B u v w H H0 IHD] ; intros v' Ss U. + - assert (H0 : v' = [] \/ v' = [Vs A]). { + inversion Ss as [| ? ? ? H H0 u' | ? u' ? H0] ; subst ; inv H0 ; auto. } + destruct H0 ; subst ; [ tauto | eauto ]. + - apply slist_split with (xs1 := u) (xs2 := v ++ w) in Ss ; auto. + destruct Ss as [u1 [hu [Ss0 [Ss1 Ss2]]]]. + apply slist_split with (xs1 := v) (xs2 := w) in Ss1 ; auto. + destruct Ss1 as [v1 [w1 [Ss3 [Ss4 Ss5]]]]. + rewrite Ss2, Ss5 in *. + assert (H1 : R B v1 el G) by eauto. + decide (v1 = []) as [D0 | D0]. + + rewrite D0 in *. + assert (H2 : nullable G (Vs B)). { + apply nullable_derE_equi. + exists B. split ; eauto. } + apply IHD ; auto. + repeat apply slist_append ; auto. + + constructor 2 with (B := B) ; auto using delE_preserveG. + assert (H2 : slist (nullable G) (u1 ++ [Vs B] ++ w1) (u ++ [Vs B] ++ w)). { + repeat apply slist_append ; auto. } + apply IHD ; auto. + intros H3. destruct u1 ; inv H3. + Qed. + + Lemma delE_der_equiv A u : + eclosed G -> (der G A u /\ u <> [] <-> der (delE G) A u). + Proof. + intros E. + split ; intros H. + - destruct H as [H U]. + assert (H0 : slist (nullable G) u u) by apply slist_id. + eapply der_G_delE ; eauto. + - induction H as [| ? ? H | ? ? u v w H IH1 H0 IH2]. + + split ; [constructor | congruence]. + + split. + * constructor 2. now apply delE_rules. + * now apply delE_efree in H. + + destruct IH1 as [IH11 IH12], IH2 as [IH21 IH22]. + split ; eauto. + destruct u, v, w ; simpl ; congruence. + Qed. + +End DelE. + +(** * Epsilon elimination *) + +Definition elimE G := delE (eclosure G). + +(** Epsilon elimination is epsilon-free *) +Lemma efree_elimE G : + efree (elimE G). +Proof. + apply delE_efree. +Qed. + +(** Epsilon elimination preserves languages (except for epsilon) *) +Lemma elimE_language G A u : + u <> [] -> (language G A u <-> language (elimE G) A u). +Proof. + intros U. split ; intros [H1 H2] ; split ; auto. + - apply (delE_der_equiv A u (eclosed_eclosure (G := G))). + split ; auto. + apply derT_der_equiv. now apply derT_der_equiv, der_eclosure_equiv in H1. + - apply (delE_der_equiv A u (eclosed_eclosure (G := G))) in H1. + destruct H1 as [H1 H3]. + apply derT_der_equiv. now apply derT_der_equiv, der_eclosure_equiv in H1. +Qed. diff --git a/cf/ElimU.v b/cf/ElimU.v new file mode 100644 index 0000000..901cd86 --- /dev/null +++ b/cf/ElimU.v @@ -0,0 +1,186 @@ +Require Export Derivation. + +(** alternative definiton of Domain, with other type than dom *) +Fixpoint domV G : list var := + match G with + [] => [] + | R A u :: Gr => A :: domV Gr + end. + +Lemma dom_domV G A : + A el (domV G) <-> Vs A el (dom G). +Proof. + induction G as [| [B u] Gr] ; simpl ; [tauto|]. + rewrite IHGr. split ; intros [H | H] ; try inv H ; auto. +Qed. + +Lemma rule_domVG G A u : + R A u el G -> A el domV G. +Proof. + rewrite dom_domV. + apply rule_domG. +Qed. + +Lemma domVG_rule G A : + A el (domV G) -> exists u, R A u el G. +Proof. + intros H. + apply dom_domV, domG_rule in H. + destruct H as [A' [u [H0 H1]]]. + exists u. now inv H0. +Qed. + +(** * Elimination of Unit Rules *) + +Definition unitfree G := forall A, ~ exists B, R A [Vs B] el G. + +Section UnitRules. + Variable G : grammar. + + Definition rules (u : list var) (v : list phrase) := product R u v. + Definition N : grammar := rules (domV G) (ran G). + + Definition step M s := + match s with + R A u => (~ (exists B, u = [Vs B]) /\ R A u el G) + \/ (exists B, R A [Vs B] el G /\ R B u el M) + end. + + Instance step_dec' G' M A u : dec (exists B, R A [Vs B] el G' /\ R B u el M). + Proof. + induction M as [| [C w] Mr IHMr]. + - right. intros [B [H0 []]]. + - destruct IHMr as [IH | IH]. + + left. destruct IH as [B [H0 H1]]. + exists B. split ; auto. + + decide (R A [Vs C] el G' /\ w = u) as [D | D]. + * left. exists C. destruct D as [D0 D1]. rewrite D1. split ; auto. + * right. intros [B [H0 [H1 | H1]]]. + { apply D. inv H1. auto. } + { apply IH. exists B. split ; auto. } + Defined. + + Instance step_dec M s : dec (step M s). + Proof. + destruct s as [A u]. + simpl. induction G as [| [B v] Gr IHGr]. + - right. intros [[H0 H1] | [B [H1 H2]]] ; try now inv H1. + - destruct IHGr as [IH | IH]. + + left. destruct IH as [[IH0 IH1] | [C [IH0 IH1]]]. + * left. split ; auto. + * right. exists C. split ; auto. + + decide (R A u = R B v /\ ~ (exists C, u = [Vs C])) as [D | D]. + * left. destruct D as [H0 H1]. + left. inv H0. split ; auto. + * decide (exists B0 : var, R A [Vs B0] el R B v :: Gr /\ R B0 u el M) as [D0 | D0]. + { left. now right. } + { right. intros [[H0 [H1 | H1]] | H0] ; try inv H1 ; try split ; auto. } + Defined. + + Definition elimU : grammar := + FCI.C (step := step) N. + + (** ** elimU is unit-free *) + + Lemma unitfree_elimU' : + inclp elimU (fun i => match i with R A u => ~ exists B, u = [Vs B] end). + Proof. + apply FCI.ind. + intros M [A u] Icl VG S. + destruct S as [[S0 S1] | [C [S0 S1]]] ; [|specialize (Icl (R C u) S1) ; simpl] ; auto. + Qed. + + Lemma unitfree_elimU : + unitfree elimU. + Proof. + intros A [B H]. apply (unitfree_elimU' H). now (exists B). + Qed. + + (** ** elimU preserves languages *) + Lemma elimU_corr A u : + R A u el G -> (~ exists B, u = [Vs B]) -> R A u el elimU. + Proof. + intros H0 H1. + apply FCI.closure. + - apply prod_corr. exists A, u. + repeat split ; eauto using rule_domVG, rule_ranG. + - left. split ; auto. + Qed. + + Lemma ran_elimU_G u : + u el ran elimU -> u el ran G. + Proof. + intros H. + apply ranG_rule in H. destruct H as [A H]. + unfold elimU in H. apply FCI.incl, prod_corr in H. + destruct H as [? [? [H0 [_ ?]]]]. now inv H0. + Qed. + + Lemma elimU_corr2 A B u : + R A [Vs B] el G -> R B u el elimU -> R A u el elimU. + Proof. + intros H0 H1. + apply FCI.closure. + - apply prod_corr. + exists A, u. repeat split ; auto. + + eapply rule_domVG ; eauto. + + apply rule_ranG in H1. now apply ran_elimU_G in H1. + - simpl. right. exists B. split ; auto. + Qed. + + (** rules in elimU can be simulated by a derivation *) + Lemma elimU_corr3' : + inclp elimU (fun i => match i with R A u => derf G [Vs A] u end). + Proof. + unfold elimU. apply FCI.ind. + intros M [A u] Icl V S. + destruct S as [[S0 S1] | [B [S0 S1]]] ; [|specialize (Icl (R B u) S1)] ; eauto. + Qed. + + Lemma elimU_corr3 A u : + R A u el elimU -> derf G [Vs A] u. + Proof. intros elimU. exact (elimU_corr3' elimU). Qed. + + (** completeness of derivability *) + Lemma derfG_derfelimU u v : + terminal v -> derf G u v -> derf elimU u v. + Proof. + intros T D. + induction D as [| A u v H H0 IHD|] ; auto. + - specialize (IHD T). + decide (exists B, u = [Vs B]) as [D | D]. + + destruct D as [B U']. + assert (H1 : exists v', R B v' el elimU /\ derf elimU v' v). { + induction IHD as [| | ? ? ? ? IH0 IHD0 IH1 IHD1] ; subst. + - assert (H1 : Vs B el [Vs B]) by auto. + destruct (T (Vs B) H1) as [t T']. inv T'. + - exists u. split ; inv U' ; auto. + - inv U'. inv IH1. rewrite app_nil_r in *. apply IHD0 ; auto. } + destruct H1 as [v' [H1 H2]]. subst. + apply (elimU_corr2 H) in H1 ; eauto. + + apply elimU_corr in H ; eauto. + - apply terminal_split in T. + destruct T as [T0 T1]. eauto. + Qed. + + (** soundness of derivability *) + Lemma derfelimU_derfG u v : + derf elimU u v -> derf G u v. + Proof. + induction 1 ; eauto using elimU_corr3, derf_trans. + Qed. + + Lemma elimU_der_equiv u v : + terminal v -> (derf G u v <-> derf elimU u v). + Proof. + intros H. split ; auto using derfelimU_derfG, derfG_derfelimU. + Qed. + + Lemma unit_language A u : + language G A u <-> language elimU A u. + Proof. + split ; intros [L0 L1] ; split ; auto ; apply derf_der_equiv ; apply derf_der_equiv in L0 ; [rewrite <- elimU_der_equiv | rewrite elimU_der_equiv] ; auto. + Qed. + +End UnitRules. + diff --git a/cf/Inlining.v b/cf/Inlining.v new file mode 100644 index 0000000..ce65248 --- /dev/null +++ b/cf/Inlining.v @@ -0,0 +1,233 @@ +Require Export Derivation. + +(** * Substitution in grammars *) +Definition substG G s u := map (fun r => match r with R B v => R B (substL v s u) end) G. + +Lemma substG_split G1 G2 s u : + substG (G1 ++ G2) s u = substG G1 s u ++ substG G2 s u. +Proof. + induction G1 as [| [A v] G1] ; simpl ; f_equal ; auto. +Qed. + +Lemma substG_skipRule G A s u v : + ~ s el u -> substG (R A u :: G) s v = R A u :: (substG G s v). +Proof. + intros U. + induction G as [| [C w] Gr IHGr] ; simpl in *. + - rewrite substL_skip ; auto. + - inversion IHGr as [H0]. f_equal. now do 2 rewrite H0. +Qed. + +Lemma substG_skip G s u : + ~ s el symbs G -> substG G s u = G. +Proof with (intros H0 ; apply H ; simpl ; auto). + intros H. + induction G as [| [A v] Gr IHGr] ; [simpl ; auto|]. + rewrite substG_skipRule ; [f_equal ; apply IHGr | ]... +Qed. + +(** substitution of a fresh variable is reversible *) +Lemma substG_undo G B s : + fresh G (Vs B) -> substG (substG G s [Vs B]) (Vs B) [s] = G. +Proof. + intros N. + induction G as [| [A u] Gr IHGr] ; simpl ; auto. + assert (N' : fresh Gr (Vs B)). { + intros s' H. apply N. apply symbs_subset with (G := Gr) ; auto. } + rewrite (IHGr N'). + do 2 f_equal. apply substL_undo. + intros H. + assert (H0 : (Vs B) el symbs (R A u :: Gr)) by (simpl ; auto). + specialize (N (Vs B) H0). unfold sless' in N. destruct B ; simpl in N ; omega. +Qed. + +(** substitution can be simulated by derivability *) +Lemma substL_der G B u v : + R B v el G -> derT G u (substL u (Vs B) v). +Proof. + intros H. + induction u as [| s u IHu] ; simpl ; eauto. + decide (s = Vs B) as [D | D]. + - rewrite D in *. + replace (Vs B :: u) with ([Vs B] ++ u) by auto. + apply derT_concat ; eauto. + - change (derT G ([s] ++ u) ([s] ++ substL u (Vs B) v)). + apply derT_concat ; eauto. +Qed. + +(** correctness lemma of substG *) +Lemma substG_inG G A s u v : + R A u el G -> R A (substL u s v) el (substG G s v). +Proof. + intros H. + induction G as [| [C w] Gr IHGr] ; simpl ; auto. + destruct H as [H | H] ; [ inv H ; left | right] ; auto. +Qed. + +(** substitution preserves domain *) +Lemma substG_dom G s u : + dom (substG G s u) = dom G. +Proof. + induction G as [| [B v] Gr IHGr] ; simpl in * ; auto. + now f_equal. +Qed. + + +(** * Elimination of a deterministic rule *) + +(** ** if part **) +Lemma in_substG_der G A B u v : + R A u el (substG G (Vs B) v) -> der (R B v :: G) A u. +Proof. + intros H. unfold substG in H. + apply in_map_iff in H. + destruct H as [[B' v'] [H0 H1]]. + inv H0. apply derT_der_equiv. + assert (H2 : R B v el (R B v :: G)) by auto. + apply substL_der with (u := v') in H2. + apply derT_trans with (v := v') ; eauto. +Qed. + +Lemma der_substG_G G A B u v : + der (substG G (Vs B) v) A u -> der (R B v :: G) A u. +Proof. + induction 1 ; eauto. + now apply in_substG_der. +Qed. + +(** ** only-if-part **) +Lemma der_G_substG' G A B u v : + A <> B -> ~ Vs B el dom G -> ~ Vs B el v -> derL (R B v :: G) A u -> derL (substG G (Vs B) v) A (substL u (Vs B) v). +Proof. + intros U S V D. + induction D as [| B' u v' w H H0 IHD]. + - simpl. decide (Vs A = Vs B) as [D | D] ; [inv D ; tauto | constructor]. + - destruct H ; [inv H | ] ; + do 2 rewrite substL_split in IHD ; + do 2 rewrite substL_split ; + simpl in IHD. + + decide (Vs B' = Vs B') as [DV | DV ] ; try tauto. + replace (substL v' (Vs B') v') with v' by (rewrite substL_skip ; auto). + now rewrite app_nil_r in IHD. + + assert (H1 : Vs B' <> Vs B) by (apply rule_domG in H ; intros H1 ; inv H1 ; tauto). + decide (Vs B' = Vs B) ; [tauto | ] ; eauto using substG_inG. +Qed. + +Lemma der_G_substG G A B u v : + A <> B -> ~ Vs B el (dom G) -> ~ Vs B el v -> ~ Vs B el u -> der (R B v :: G) A u -> der (substG G (Vs B) v) A u. +Proof. + intros S V U H D. + apply derL_der_equiv, der_G_substG' in D ; auto. + apply derL_der_equiv. + rewrite substL_skip in D ; auto. +Qed. + +(** corollary **) +Lemma der_substG_G_equiv G u v A B : + A <> B -> ~ Vs B el (dom G) -> ~ Vs B el v -> ~ Vs B el u -> (der (R B v :: G) A u <-> der (substG G (Vs B) v) A u). +Proof. + intros H H0 H1 H2. split ; intros D ; [apply der_G_substG | apply der_substG_G] ; auto. +Qed. + +Lemma inl_language_equiv G A B u v : + A <> B -> ~ Vs B el (dom G) -> ~ Vs B el v -> (language (substG G (Vs B) v) A u <-> language (R B v :: G) A u). +Proof. + intros H H0 H1. + split ; intros [L0 L1] ; split ; auto ; apply der_substG_G_equiv ; auto ; intros H2 ; destruct (L1 (Vs B) H2) as [a T] ; inv T. +Qed. + + +(** * Elimination of a list of deterministic rules *) + +Fixpoint inlL L G := + match L with + [] => G + | R A u :: Lr => substG (inlL Lr G) (Vs A) u + end. + +Inductive inlinable (G : grammar) : grammar -> Prop := +| inN : inlinable G nil +| inR A u Gr : + ~ Vs A el u -> ~ Vs A el dom Gr -> ~ Vs A el dom G -> disjoint u (dom Gr) -> + inlinable G Gr -> inlinable G (R A u :: Gr). +Hint Constructors inlinable. + +Lemma inlinable_cons M G A u : + ~ Vs A el dom M -> inlinable G M -> inlinable (R A u :: G) M. +Proof. + intros V IL. + induction IL as [| B v Gr H H0 H1 H2 H3 IH] ; simpl in * ; eauto. + econstructor 2 ; eauto. + intros [D | D] ; [inv D| ] ; auto. +Qed. + +(** ** if-part **) + +Lemma der_inlL_G' M G A u : + R A u el (inlL M G) -> der (M ++ G) A u. +Proof. + revert G u. + induction M as [| [B v] Mr IHMr] ; intros G u D ; simpl in * ; eauto. + unfold substG in D. + apply in_map_iff in D. + destruct D as [[B' u'] [D1 D2]]. + inv D1. specialize (IHMr G u' D2). + eapply der_subset with (G2 := R B v :: Mr ++ G) in IHMr ; auto. + rewrite derT_der_equiv in *. + eapply derT_trans ; eauto. + now apply substL_der. +Qed. + +Lemma der_inlL_G M G A u : + der (inlL M G) A u -> der (M ++ G) A u. +Proof. + induction 1 ; eauto using der_inlL_G'. +Qed. + +(** ** only-if-part **) + +Lemma inlL_skip G Gr A u : + disjoint u (dom G) -> inlL G (R A u :: Gr) = R A u :: inlL G Gr. +Proof. + intros D. + induction G as [| [B v] G' IHG'] ; simpl in * ; auto. + assert (H0 : disjoint u (dom G')) by (intros [s [U1 U2]] ; apply D ; exists s ; auto). + rewrite (IHG' H0). + assert (H1 : ~ Vs B el u) by (intros U ; apply D ; exists (Vs B) ; auto). + now apply substG_skipRule. +Qed. + +Lemma inlL_dom M G : + dom (inlL M G) = dom G. +Proof. + induction M as [| [A u] Mr IHMr] ; simpl in * ; auto. + now rewrite substG_dom. +Qed. + +Lemma der_G_inlL M G A u : + inlinable G M -> Vs A el dom G -> disjoint u (dom M) -> der (M ++ G) A u -> der (inlL M G) A u. +Proof. + revert G. + induction M as [| [B v] Mr IHMr] ; intros G IL V T D ; simpl in * ; auto. + inversion IL as [|B' v' G' H H0 H1 H2 H3] ; subst. + apply der_G_substG ; auto. + - intros E ; subst. tauto. + - now rewrite inlL_dom. + - intros N. apply T. exists (Vs B). auto. + - rewrite <- inlL_skip ; auto. + apply IHMr ; simpl ; auto using inlinable_cons. + + intros [s [U1 U2]]. apply T. exists s. auto. + + eapply der_subset ; try exact D ; auto. +Qed. + +(** corollary **) + +Lemma inlL_langauge_equiv G M A u : + inlinable G M -> Vs A el dom G -> (language (M ++ G) A u <-> language (inlL M G) A u). +Proof. + intros H0 H1. + split ; intros [L0 L1] ; split ; auto ; [apply der_G_inlL | apply der_inlL_G] ; auto. + intros [x [D0 D1]]. apply domG_rule in D1. + destruct D1 as [B [v [D1 D2]]]. subst. + destruct (L1 (Vs B) D0) as [t T]. inv T. +Qed. \ No newline at end of file diff --git a/cf/Lists.v b/cf/Lists.v new file mode 100644 index 0000000..08d31c0 --- /dev/null +++ b/cf/Lists.v @@ -0,0 +1,363 @@ +Require Export Base. + +(** * Decidability instances *) + +Instance eq_dec_prod X Y (Dx : eq_dec X) (Dy : eq_dec Y) : + eq_dec (X * Y). +Proof. + intros [x y] [x' y']. + decide (x = x') ; decide (y = y') ; try (right ; intros H ; inv H ; tauto). + left. f_equal ; auto. +Defined. + +Instance filter_prod_dec X Y {D : eq_dec X} (x : X) : + forall (e : X * Y) , dec ((fun e : X * Y => match e with (xe, _) => x = xe end) e). +Proof. + intros [xe _]. auto. +Defined. + +Instance splitList_dec X (D : eq_dec X) (xs ys : list X) : dec (exists zs, xs = ys ++ zs). +Proof. + revert xs. + induction ys as [| s ys IHv]; intros xs. + - left. exists xs. auto. + - destruct xs as [|s' xs]. + + right. intros [zs H]. inv H. + + decide (s = s') as [DS | DS]. + * rewrite DS. + destruct (IHv xs) as [IH | IH]. + { left. destruct IH as [zs IH]. exists zs. rewrite IH. auto. } + { right. intros [zs H]. simpl in H. + apply IH. exists zs. now inv H. } + * right. intros [zs H]. inv H. tauto. +Defined. + +(** * Sublists **) + +Fixpoint slists (X : Type) (p : X -> Prop) (pdec : forall x, dec (p x)) (xs : list X) : list (list X) := + match xs with + | [] => [[]] + | s::xs' => + let + ys := slists pdec xs' + in let + zs := map (cons s) ys + in + if decision (p s) then ys ++ zs else zs + end. +Arguments slists {X} p {pdec} xs. + +Inductive slist (X : Type) (p : X -> Prop) {pdec : forall x, dec (p x)} : list X -> list X -> Prop := +| subnil : slist nil nil +| subconsp s ys xs: p s -> slist ys xs -> slist ys (s :: xs) +| subcons s ys xs : slist ys xs -> slist (s :: ys) (s :: xs). +Arguments slist {X} p {pdec} ys xs. +Hint Constructors slist. + +Lemma slists_slist (X : Type) (xs ys : list X) (p : X -> Prop) (D : forall x, dec (p x)) : + ys el slists p xs <-> slist p ys xs. +Proof with (apply in_map_iff in H ; destruct H as [ys' [H0 H1]] ; subst ; auto). + split. + - revert ys. + induction xs as [| s xs' IHu] ; intros ys H ; simpl in H. + + destruct H as [H | H] ; [ rewrite <- H ; constructor | tauto ]. + + decide (p s) ; [ apply in_app_iff in H ; destruct H as [H | H] | ] ; auto... + - induction 1 as [| s ys xs H H0 IH | s ys xs H IH] ; simpl ; auto. + * decide (p s) ; firstorder. + * assert (H1: exists ys', s::ys' = s::ys /\ ys' el (slists p xs)) by firstorder. + rewrite <- in_map_iff in H1. + decide (p s) ; [ apply in_app_iff | ] ; auto. +Qed. + +(** ** Properties of sublists **) + +Lemma slist_id (X : Type) (xs : list X) (p : X -> Prop) {pdec : forall x, dec (p x)} : + slist p xs xs. +Proof. + induction xs ; auto. +Qed. + +Lemma slist_trans (X : Type) (xs ys zs : list X) (p : X -> Prop) {pdec : forall x, dec (p x)} : + slist p zs ys -> slist p ys xs -> slist p zs xs. +Proof with (remember (s :: xs) as zs ; induction H2 ; [congruence | | inv Heqzs ] ; auto). + intros H1. revert xs. + induction H1 as [| s ys xs H H0 IH | s ys xs H IH] ; intros xs' H2 ; try now auto ; auto... +Qed. + +Lemma slist_append (X : Type) (xs1 xs2 ys1 ys2 : list X) (p : X -> Prop) {pdec : forall x, dec (p x)} : + slist p ys1 xs1 -> slist p ys2 xs2 -> slist p (ys1 ++ ys2) (xs1 ++ xs2). +Proof. + induction 1 ; simpl ; auto. +Qed. + +Lemma slist_equiv_pred (X : Type) (xs ys : list X) (p : X -> Prop) {pdec : forall x, dec (p x)} (p' : X -> Prop) {pdec' : forall x, dec (p' x)}: + (forall x, p x <-> p' x) -> slist p xs ys -> slist p' xs ys. +Proof. + induction 2 ; auto. + constructor 2 ; firstorder. +Qed. + +Lemma slist_inv (X : Type) (xs ys : list X) (p : X -> Prop) {pdec : forall x, dec (p x)} : + slist p ys xs -> (forall s, s el ys -> p s) -> forall s, s el xs -> p s. +Proof with (destruct E as [E | E] ; try rewrite <- E ; auto). + intros H0 H1 s E. + induction H0 ; auto... +Qed. + +Lemma slist_split (X : Type) (xs ys : list X) (p : X -> Prop) {pdec : forall x, dec (p x)} : + slist p ys xs -> forall xs1 xs2, xs = xs1 ++ xs2 -> exists ys1 ys2, slist p ys1 xs1 /\ slist p ys2 xs2 /\ ys = ys1 ++ ys2. +Proof with (repeat split ; auto ; try inv IH0 ; auto). + induction 1 as [ | s ys xs H H0 IH | s ys xs H IH] ; intros xs1 xs2 U. + - exists [], []. + symmetry in U. + apply app_eq_nil in U ; destruct U as [H1 U]. + rewrite H1, U. repeat split ; auto. + - destruct xs1, xs2 ; simpl in U ; (try now inv U) ; injection U ; intros U0 U1 ; subst. + + destruct (IH [] xs2 eq_refl) as [ys1 [ys2 [IH0 [IH1 IH2]]]]. exists ys1, ys2... + + destruct (IH xs1 [] eq_refl) as [ys1 [ys2 [IH0 [IH1 IH2]]]]. exists ys1, ys2... + + destruct (IH xs1 (x0 :: xs2) eq_refl) as [ys1 [ys2 [IH0 [IH1 IH2]]]]. exists ys1, ys2... + - destruct xs1, xs2 ; simpl in U ; (try now inv U) ; injection U ; intros U0 U1 ; subst. + + destruct (IH [] xs2 eq_refl) as [ys1 [ys2 [IH0 [IH1 IH2]]]]. exists ys1, (x :: ys2)... + + destruct (IH xs1 [] eq_refl) as [ys1 [ys2 [IH0 [IH1 IH2]]]]. exists (x :: ys1), ys2... + + destruct (IH xs1 (x0 :: xs2) eq_refl) as [ys1 [ys2 [IH0 [IH1 IH2]]]]. exists (x :: ys1), ys2... +Qed. + + +Lemma slist_subsumes X (p : X -> Prop) {D : forall x, dec (p x)} xs ys : + slist p xs ys -> xs <<= ys. +Proof. + induction 1 ; auto. +Qed. + +Lemma slist_length X (p : X -> Prop) {D : forall x, dec (p x)} (xs ys : list X) : + slist p xs ys -> |xs| <= |ys|. +Proof. + induction 1 ; simpl ; omega. +Qed. + +Lemma slist_pred X (p p' : X -> Prop) {D : forall x, dec (p' x)} (xs ys : list X) : + slist p' xs ys -> (forall y, y el ys -> p y) -> forall x, x el xs -> p x. +Proof. + intros Ss P. + induction Ss ; intros x' E ; auto. + destruct E as [E | E] ; auto. + rewrite <- E. now apply P. +Qed. + + +(** * Segments *) + +Definition segment X (xs ys : list X) := exists xs1 xs2, xs = xs1 ++ ys ++ xs2. + +Fixpoint segms X (D : eq_dec X) (xs : list X) := + match xs with + [] => [ [] ] + | s :: xs => + let + Ss :=segms D xs + in + map (cons s) (filter (fun ys => exists zs, xs = ys ++ zs) Ss) ++ Ss + end. +Arguments segms {X} {D} xs. + +(** ** Properties of segments *) + +Lemma segment_nil X {D : eq_dec X} (xs : list X) : + segment xs []. +Proof. + exists xs, []. now rewrite app_nil_r. +Qed. + +Lemma segment_refl X {D : eq_dec X} (xs : list X) : + segment xs xs. +Proof. + exists [], []. rewrite app_nil_r. auto. +Qed. + +Lemma segment_trans X {D : eq_dec X} (xs ys zs : list X) : + segment ys zs -> segment xs ys -> segment xs zs. +Proof. + intros [w1 [w2 H0]] [ys1 [ys2 H1]]. + exists (ys1 ++ w1), (w2 ++ ys2). rewrite H1, H0. + now repeat rewrite <- app_assoc. +Qed. + +(** ** Equivalence of segment characterizations *) + +Lemma segms_corr1 X {D : eq_dec X} (xs ys : list X) : + segment xs ys -> ys el segms xs. +Proof. + revert ys. + induction xs as [| s xs IHxs] ; intros ys [ys1 [ys2 H]]. + - simpl. symmetry in H. + apply app_eq_nil in H. + destruct H as [H0 H]. apply app_eq_nil in H. + destruct H as [H1 H2]. subst. auto. + - destruct ys1 as [| sys1 ys1] ; simpl in H. + + destruct ys as [| sys ys] ; simpl in H. + { simpl. apply in_or_app. right. apply IHxs. now apply segment_nil. } + { injection H ; intros H0 H1 ; subst. + simpl. apply in_or_app. left. apply in_map_iff. + exists ys. split ; auto. apply in_filter_iff. split. + - apply IHxs. exists [], ys2. auto. + - now (exists ys2). } + + injection H ; intros H0 H1 ; subst. + simpl. apply in_or_app. right. apply IHxs. + now (exists ys1, ys2). +Qed. + +Lemma segms_corr2 X {D : eq_dec X} (xs ys : list X) : + ys el segms xs -> segment xs ys. +Proof. + intros H. + induction xs as [| s xs IHxs] ; simpl in H. + - destruct H as [H | H] ; [subst | tauto]. + now (exists [], []). + - apply in_app_iff in H. + destruct H as [H | H]. + + apply in_map_iff in H. destruct H as [x [H0 H1]]. + apply in_filter_iff in H1. destruct H1 as [H1 [zs H2]]. + rewrite <- H0, H2 in *. + exists [], zs. auto. + + destruct (IHxs H) as [x [z IH]]. + exists (s :: x), z. rewrite IH. auto. +Qed. + +Lemma segms_corr X {D : eq_dec X} (xs ys : list X) : + ys el segms xs <-> segment xs ys. +Proof. + split ; intros Ss ; [eapply segms_corr2 | eapply segms_corr1] ; eauto. +Qed. + + +(** * General functions on lists *) + +(** ** Product *) + +Fixpoint product X Y Z (f : X -> Y -> Z) (xs : list X) (ys : list Y) : list Z := + match xs with + [] => [] + | s :: xs => map (f s) ys ++ product f xs ys + end. + +Lemma prod_corr1 X Y Z (f : X -> Y -> Z) (xs : list X) (ys : list Y) (z : Z) : + z el product f xs ys -> exists sxs sys, f sxs sys = z /\ sxs el xs /\ sys el ys. +Proof. + intros H. + induction xs as [| s xs IHxs ] ; simpl in H ; try tauto. + apply in_app_iff in H. + destruct H as [H | H]. + - apply in_map_iff in H. + destruct H as [x [H0 H1]]. + exists s, x. repeat split ; auto. + - destruct (IHxs H) as [sxs [sys [H0 [H1 H2]]]]. + exists sxs, sys. auto. +Qed. + +Lemma prod_corr2 X Y Z (f : X -> Y -> Z) (xs : list X) (ys : list Y) (z : Z) : + (exists sxs sys, f sxs sys = z /\ sxs el xs /\ sys el ys) -> z el product f xs ys. +Proof. + intros [sxs [sys [H0 [H1 H2]]]]. + induction xs as [| s xs IHxs ] ; try now inv H1. + simpl. apply in_app_iff. + destruct H1 as [H1 | H1]. + - rewrite H1 in *. left. apply in_map_iff. exists sys. auto. + - right. auto. +Qed. + +Lemma prod_corr X Y Z (f : X -> Y -> Z) (xs : list X) (ys : list Y) (z : Z) : + z el product f xs ys <-> exists sxs sys, f sxs sys = z /\ sxs el xs /\ sys el ys. +Proof. + split ; [apply prod_corr1 | apply prod_corr2]. +Qed. + +(** ** Projection **) +Fixpoint fsts X Y (xs : list (X * Y)) := + match xs with + [] => [] + | (x, y) :: xs => x :: fsts xs + end. + +Lemma fsts_split X Y (xs ys : list (X * Y)) : + fsts (xs ++ ys) = fsts xs ++ fsts ys. +Proof. + induction xs as [| [s1 s2] xs IHxs] ; simpl ; auto. + now rewrite IHxs. +Qed. + +Fixpoint snds X Y (xs : list (X * Y)) := + match xs with + [] => [] + | (x, y) :: xs => y :: snds xs + end. + +Lemma snds_split X Y (xs ys : list (X * Y)) : + snds (xs ++ ys) = snds xs ++ snds ys. +Proof. + induction xs as [| [s1 s2] xs IHxs] ; simpl ; auto. + now rewrite IHxs. +Qed. + +(** ** Concat*) +Fixpoint concat X (xs : list (list X)) := + match xs with + [] => [] + | ys :: xs => ys ++ (concat xs) + end. + +Lemma concat_split X (xs ys : list (list X)) : + concat (xs ++ ys) = concat xs ++ concat ys. +Proof. + induction xs ; simpl ; [| rewrite IHxs] ; auto using app_assoc. +Qed. + +(** ** Substitution**) +Fixpoint substL X {D : eq_dec X} (xs : list X) (y : X) (ys : list X) := + match xs with + [] => [] + | x :: xs => if decision (x = y) then ys ++ substL xs y ys else x :: substL xs y ys + end. + +Lemma substL_split X {D : eq_dec X} (xs1 xs2 : list X) (y : X) (ys : list X) : + substL (xs1 ++ xs2) y ys = substL xs1 y ys ++ substL xs2 y ys. +Proof. + induction xs1 as [| sxs1 xs1 IHxs1] ; simpl ; try (decide (sxs1 = y) ; rewrite IHxs1) ; auto using app_assoc. +Qed. + +Lemma substL_skip X {D : eq_dec X} (xs : list X) (y : X) (ys : list X) : + ~ y el xs -> substL xs y ys = xs. +Proof. + intros U. + induction xs as [| x xs IHxs] ; simpl in * ; auto. + decide (x = y) as [D0 | D0]. + - exfalso. apply U ; auto. + - f_equal. apply IHxs. + intros H. apply U. auto. +Qed. + +Lemma substL_length_unit X {D : eq_dec X} (xs : list X) (x x' : X) : + (|xs|) = | substL xs x [x'] |. +Proof. + induction xs as [| y xr IHxr] ; simpl ; try decide (y = x) ; simpl ; auto. +Qed. + +Lemma substL_undo X {D : eq_dec X} (xs : list X) (x x' : X) : + ~ x' el xs -> substL (substL xs x [x']) x' [x] = xs. +Proof. + intros H. + induction xs as [| y xr IHxr] ; simpl ; auto. + simpl. decide (y = x) as [D0 | D0] ; subst ; simpl. + - decide (x' = x') ; try tauto. f_equal. auto. + - decide (y = x') ; subst. + + exfalso. now apply H. + + f_equal. auto. +Qed. + +(** ** General lemmas on lists **) +Lemma list_unit (X : Type) (xs zs : list X) (x y : X) : + [x] = xs ++ y :: zs -> xs = [] /\ zs = [] /\ x = y. +Proof. + intros H. + destruct xs, zs ; (try now inv H ; auto) ; (injection H ; intros H0 H1 ; subst; + symmetry in H0 ; apply app_eq_nil in H0 ; destruct H0 ; congruence). +Qed. \ No newline at end of file diff --git a/cf/Separate.v b/cf/Separate.v new file mode 100644 index 0000000..79c5c53 --- /dev/null +++ b/cf/Separate.v @@ -0,0 +1,239 @@ +Require Export Inlining. + +Definition charfree u := forall s, s el u -> exists A, s = Vs A. +Definition uniform G := forall A u, R A u el G -> forall a, Ts a el u -> u = [Ts a]. + +Instance dec_charfree u : dec (charfree u). +Proof. + unfold charfree. + induction u as [| [a | A] u IHu]. + - left. intros s H. destruct H. + - right. intros H. + assert (H0 : Ts a el (Ts a :: u)) by auto. + destruct (H (Ts a) H0) as [A H']. inv H'. + - destruct IHu as [IH | IH]. + + left. intros s [H | H] ; [ exists A |] ; auto. + + right. intros H. apply IH. + intros s H0. apply H. auto. +Defined. + +Lemma pickChar u : + ~ charfree u -> { a | Ts a el u}. +Proof. + intros H. + induction u as [| [a | A] u IHu]. + - exfalso. apply H. intros s H0. destruct H0. + - exists a. auto. + - assert (H0 : ~ charfree u). { + intros H0. apply H. + intros s H1. destruct H1 as [H1 | H1] ; [exists A| ] ; auto. } + destruct (IHu H0) as [a H1]. exists a. auto. +Qed. + +Lemma pickCharRule G : + { a | exists A u, R A u el G /\ (Ts a) el u /\ |u| >= 2} + uniform G. +Proof. + induction G as [| [A u] Gr IHGr]. + - right. intros A u []. + - destruct IHGr as [[a IH] | IH]. + + left. exists a. destruct IH as [A' [u' [H0 [H1 H2]]]]. + exists A', u'. repeat split ; auto. + + decide (charfree u) as [D | D]. + * right. intros A' u' [H0 | H0] a H1 ; eauto. + inv H0. destruct (D (Ts a) H1) as [b T]. inv T. + * { apply pickChar in D. destruct D as [a D]. + destruct u as [| [b | B] [| s u]]. + - exfalso. destruct D as []. + - right. intros A' u' [H0 | H0] c H1 ; eauto. + inv H0. destruct H1 as [H1 | H1] ; now inv H1. + - left. exists a, A, (Ts b :: s :: u). repeat split ; simpl ; auto ; omega. + - exfalso. destruct D as [D | D] ; inv D. + - left. exists a, A, (Vs B :: s :: u). repeat split ; simpl ; auto ; omega. } +Qed. + +Definition step (G : grammar) : grammar. + destruct (pickCharRule G) as [[a H] | H ]. + - destruct (pickFresh G) as [B N]. + exact (R B [Ts a] :: substG G (Ts a) [Vs B]). + - exact G. +Defined. + +Fixpoint count_chars u := + match u with + [] => 0 + | Vs A :: ur => count_chars ur + | Ts t :: ur => S (count_chars ur) + end. + +Fixpoint count_sep G := + match G with + [] => 0 + | R A u :: Gr => if decision (|u| < 2) then count_sep Gr + else count_chars u + count_sep Gr + end. + +Definition sep G := it step (count_sep G) G. + +(** * Separation yields uniform grammar *) + +Lemma count_sep_split G G' : + count_sep (G ++ G') = count_sep G + count_sep G'. +Proof. + induction G as [| [A u] Gr IHGr] ; simpl ; try decide (| u | < 2) ; auto. + rewrite <- plus_assoc. now f_equal. +Qed. + +Lemma count_chars_substL u a B : + count_chars u >= count_chars (substL u (Ts a) [Vs B]). +Proof. + induction u as [| [b | A] u] ; simpl ; auto. + decide (Ts b = Ts a) ; simpl ; omega. +Qed. + +Lemma count_sep_substL G a B : + count_sep G >= count_sep (substG G (Ts a) [Vs B]). +Proof. + induction G as [| [A u] Gr IHGr] ; simpl ; auto. + decide (| u | < 2) as [D | D] ; rewrite substL_length_unit with (x := Ts a) (x' := Vs B) (D := symbol_eq_dec) in D ; + decide (| substL u (Ts a) [Vs B] | < 2) ; try tauto. + cut (count_chars u >= count_chars (substL u (Ts a) [Vs B])) ; try omega. + apply count_chars_substL. +Qed. + +Lemma count_chars_split u1 u2 : + count_chars (u1 ++ u2) = count_chars u1 + count_chars u2. +Proof. + induction u1 as [| [a | A] u1] ; simpl ; auto. +Qed. + +Lemma count_chars_decr B u a : + Ts a el u -> count_chars u > count_chars (substL u (Ts a) [Vs B]). +Proof. + intros H0. + apply in_split in H0. + destruct H0 as [u1 [u2 H0]]. rewrite H0. + replace (u1 ++ Ts a :: u2) with (u1 ++ [Ts a] ++ u2) by auto. + repeat rewrite substL_split. + repeat rewrite count_chars_split. + repeat rewrite plus_assoc. + cut (count_chars [Ts a] > count_chars (substL [Ts a] (Ts a) [Vs B])). + - intros H2. + pose (count_chars_substL u1 a B). + pose (count_chars_substL u2 a B). omega. + - simpl. decide (Ts a = Ts a) ; try tauto. auto. +Qed. + +Lemma count_sep_decr G A B u a : + R A u el G -> Ts a el u -> |u| >= 2 -> count_sep G > count_sep (substG G (Ts a) [Vs B]). +Proof. + intros H U T. + apply in_split in H. + destruct H as [G1 [G2 H]]. rewrite H. + replace (G1 ++ R A u :: G2) with (G1 ++ [R A u] ++ G2) by auto. + do 2 rewrite substG_split. + repeat rewrite count_sep_split. + repeat rewrite plus_assoc. + cut (count_sep [R A u] > count_sep (substG [R A u] (Ts a) [Vs B])). + - intros C. pose (C0 := count_sep_substL G1 a B). + pose (C1 := count_sep_substL G2 a B). omega. + - simpl. decide (| u | < 2) as [D | D] ; try omega. + rewrite substL_length_unit with (x := Ts a) (x' := Vs B) (D := symbol_eq_dec) in D. + decide (| substL u (Ts a) [Vs B] | < 2) ; try tauto. + do 2 rewrite <- plus_n_O. + now apply count_chars_decr. +Qed. + +Lemma count_decr G : + step G <> G -> count_sep G > count_sep (step G). +Proof. + intros St. + unfold step in *. + destruct (pickCharRule G) as [[a [B [v [H0 [H1 H2]]]]] | H ] ; try tauto. + destruct (pickFresh G) as [C N]. + simpl. eapply count_sep_decr ; eauto. +Qed. + +Lemma fp_sep G : + FP step (sep G). +Proof. + apply it_fp. intros n. + decide (step (it step n G) = (it step n G)). + - left. auto. + - right. simpl. now apply count_decr in n0. +Qed. + +Lemma fp_uniform G : + FP step G -> uniform G. +Proof. + intros Ss. + unfold step, FP in Ss. + destruct (pickCharRule G) as [[a [B [v [H0 [H1 H2]]]]] | H ]. + - destruct (pickFresh G) as [C N]. + destruct G ; inversion Ss. + exfalso. assert (H5 : Vs C el symbs (r :: G)) by (rewrite <- Ss ; simpl ; auto). + specialize (N (Vs C) H5). unfold sless' in N. destruct B as [i] ; omega. + - intros A' u' Ru'. specialize (H A' u' Ru') ; auto. +Qed. + +Lemma sep_uniform G : + uniform (sep G). +Proof. + apply fp_uniform, fp_sep. +Qed. + +(** * Separation preserves languages *) + +Lemma substG_der_equiv G A u B s : + fresh G (Vs B) -> A <> B -> s <> Vs B -> terminal u -> (der (R B [s] :: (substG G s [Vs B])) A u <-> der G A u). +Proof. + intros N Do U T. + split ; intros D. + - rewrite <- substG_undo with (G := G) (B := B) (s := s) ; auto. + apply der_G_substG ; auto ; intros H. + + rewrite substG_dom in H. apply symbs_dom in H. + apply fresh_symbs in N. tauto. + + destruct H ; tauto. + + destruct (T (Vs B) H) as [t T']. inv T'. + - rewrite <- substG_undo with (G := G) (B := B) (s := s) in D ; auto. + now apply der_substG_G. +Qed. + +Lemma step_der_equiv G A u : + Vs A el dom G -> terminal u -> (der (step G) A u <-> der G A u). +Proof. + intros Do T. + unfold step. + destruct (pickCharRule G) as [[a [B [v [H0 [H1 H2]]]]] | H ] ; [| firstorder]. + destruct (pickFresh G) as [C N]. + apply substG_der_equiv ; auto. + - intros H. inv H. apply symbs_dom in Do. + specialize (N (Vs C) Do). unfold sless' in N. omega. + - intros H5. inv H5. +Qed. + +Lemma step_dom G : + dom G <<= dom (step G). +Proof. + unfold step. + destruct (pickCharRule G) as [[a [B [v [H0 [H1 H2]]]]] | H ] ; auto. + destruct (pickFresh G) as [C N]. + simpl. rewrite substG_dom. auto. +Qed. + +Lemma sep_der_equiv G A u : + Vs A el dom G -> terminal u -> (der (sep G) A u <-> der G A u). +Proof. + unfold sep. remember (count_sep G) as n. clear Heqn. + revert G. + induction n ; intros G D T ; simpl ; try tauto. + rewrite step_der_equiv ; auto. + apply it_ind ; auto. + intros G' H0. now apply step_dom. +Qed. + +Lemma sep_language G A u : + Vs A el dom G -> (language G A u <-> language (sep G) A u). +Proof. + intros D. + split ; intros [L0 L1] ; split ; try eapply sep_der_equiv ; eauto. +Qed. \ No newline at end of file diff --git a/cf/Symbols.v b/cf/Symbols.v new file mode 100644 index 0000000..b78a9f6 --- /dev/null +++ b/cf/Symbols.v @@ -0,0 +1,194 @@ +Require Export Definitions. + +(** * Domain and range **) +Fixpoint dom (G : grammar) : list symbol := + match G with + |[] => [] + |R A u :: Gr => (Vs A) :: dom Gr + end. + +Fixpoint ran G := + match G with + [] => [] + | R A u :: Gr => u :: ran Gr + end. + +Lemma rule_domG G A u : + R A u el G -> Vs A el dom G. +Proof. + intros H. induction G as [| [B v] Gr] ; simpl ; auto. + destruct H as [H | H] ; [inv H | ] ; auto. +Qed. + +Lemma domG_rule G s : + s el (dom G) -> exists A u, s = Vs A /\ R A u el G. +Proof. + intros H. + induction G as [| [B v] Gr IHGr] ; simpl in * ; try tauto. + destruct H as [H | H]. + - subst. exists B, v. auto. + - destruct (IHGr H) as [A [u [H1 H2]]]. + exists A, u. auto. +Qed. + +Lemma dom_subset G G' : + G <<= G' -> dom G <<= dom G'. +Proof. + intros E s H. + apply domG_rule in H. + destruct H as [A [u [H0 H1]]]. + rewrite H0. eapply rule_domG ; eauto. +Qed. + +Lemma rule_ranG G A u : + R A u el G -> u el ran G. +Proof. + intros H. + induction G as [| [B v] G]. + - inv H. + - simpl. destruct H as [H | H] ; [inv H | ] ; auto. +Qed. + +Lemma ranG_rule G u : + u el ran G -> exists A, R A u el G. +Proof. + intros H. + induction G as [| [B v] Gr IHGr] ; simpl in H ; destruct H. + - subst. exists B. auto. + - destruct (IHGr H) as [A H0]. exists A. auto. +Qed. + +(** * Symbols **) + +Fixpoint symbs G := + match G with + [] => [] + | R A u :: Gr => Vs A :: u ++ symbs Gr + end. + +Lemma symbs_dom G s : + s el dom G -> s el symbs G. +Proof. + intros H. + induction G as [| [A u] Gr IHGr] ; simpl ; auto. + simpl in H. destruct H ; auto. +Qed. + +Lemma symbs_inv G s : + s el symbs G <-> exists A u, R A u el G /\ (s = (Vs A) \/ s el u). +Proof. + split. + - intros E. + induction G as [| [A u] Gr IHGr] ; simpl in E ; try tauto. + destruct E as [E | E] ; [exists A, u ; auto|]. + apply in_app_or in E. destruct E as [E | E] ; [exists A, u ; auto|]. + destruct (IHGr E) as [A' [u' [H0 H1]]]. exists A', u'. auto. + - intros [A [u [H0 H1]]]. + induction G as [| [A' u'] Gr IHGr] ; simpl ; try tauto. + destruct H0 as [H0 | H0]. + + injection H0 ; intros H2 H3 ; subst. destruct H1 as [H1 | H1] ; [left | right] ; auto. + + right. apply in_or_app. right. auto. +Qed. + +Lemma symbs_subset G G' s : + G <<= G' -> s el symbs G -> s el symbs G'. +Proof. + intros H0 H1. + apply symbs_inv in H1. + destruct H1 as [A' [u' [H1 H2]]]. + assert (H3 : R A' u' el G') by auto. + eapply symbs_inv ; eauto. +Qed. + +(** * Fresh variables **) + +(** lift <= and < to symbols *) +Definition getNat s := + match s with + Vs (V i) => i + | Ts (T i) => i + end. + +Definition sless n s := getNat s <= n. +Definition sless' s s' := getNat s < getNat s'. + +Instance sless_dec n s : dec (sless n s). +Proof. + unfold sless. destruct s as [[i] | [i]] ; auto. +Defined. + +Lemma sless_monotone m n s : + m <= n -> sless m s -> sless n s. +Proof. + unfold sless ; destruct s as [[i] | [i]] ; simpl ; omega. +Qed. + +(** compute maximal symbol of a grammar *) + +Fixpoint maxSymbRule (sl : list symbol) := + match sl with + | [] => 0 + | s :: u => let + n := maxSymbRule u + in if decision (sless n s) then n else getNat s + end. + +Fixpoint maxSymb (G : grammar) n := + match G with + | [] => n + | R A u :: Gr => let + (m0, m1) := (maxSymbRule (Vs A :: u), maxSymb Gr n) + in if decision (m0 < m1) then m1 else m0 + end. + +Lemma maxSymbRule_corr u s : + s el u -> sless (maxSymbRule u) s. +Proof. + intros H. + unfold sless. + induction u as [| s' u IHu] ; try now destruct H. + simpl. decide (sless (maxSymbRule u) s') ; destruct H as [H | H] ; try (rewrite <- H) ; auto. + unfold sless in n. + setoid_transitivity (maxSymbRule u) ; auto ; omega. +Qed. + +Lemma maxSymb_corr G s n : + s el symbs G -> sless (maxSymb G n) s. +Proof. + intros H. revert n. + apply symbs_inv in H. + destruct H as [A [u [H0 H1]]]. + induction G as [| [A' u'] Gr IHGr] ; intros n ; simpl in H0 ; try tauto. + change (sless (if decision (maxSymbRule (Vs A' :: u') < maxSymb Gr n) then maxSymb Gr n else maxSymbRule (Vs A' :: u')) s). + destruct H0 as [H0 | H0]. + - injection H0 ; intros H2 H3 ; subst. + assert (H4 : s el (Vs A :: u)) by (destruct H1 as [H1 | H1] ; try rewrite H1 ; auto). + apply maxSymbRule_corr in H4. + decide (maxSymbRule (Vs A :: u) < maxSymb Gr n) ; auto. + apply sless_monotone with (m := maxSymbRule (Vs A :: u)) ; auto ; omega. + - decide (maxSymbRule (Vs A' :: u') < maxSymb Gr n) ; auto. + apply sless_monotone with (m := maxSymb Gr n) ; auto ; omega. +Qed. + +(** fresh variables *) + +Definition fresh G s := forall s', s' el symbs G -> sless' s' s. + +Lemma pickFresh G : + { A | fresh G (Vs A) }. +Proof. + exists (V (S (maxSymb G 0))). + intros s' H. + apply maxSymb_corr with (n := 0) in H. + unfold sless in H. unfold sless'. + destruct s' as [[i] | [i]] ; simpl in * ; omega. +Defined. + +Lemma fresh_symbs G s : + fresh G s -> ~ s el symbs G. +Proof. + intros N Sy. + specialize (N s Sy). + simpl in N. unfold sless' in N. + destruct s as [ [i] | [i] ]; omega. +Qed. From 79b9d792c638b2d92843fb2776f3cffd217d1802 Mon Sep 17 00:00:00 2001 From: Leyla Date: Sat, 22 Apr 2017 21:17:52 +0300 Subject: [PATCH 02/23] Update README.md --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index a42f8eb..4a20aa0 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,4 @@ # YC_in_Coq Formalization of some parts of YC + +Formalization of CF language was taken from Jana Hofmann, Saarland University, http://www.ps.uni-saarland.de/~hofmann/bachelor.php. From a4c1df147389e9ec3e9a01fbfd8d82b804c7a6a2 Mon Sep 17 00:00:00 2001 From: HeyLey Date: Sun, 23 Apr 2017 21:19:30 +0300 Subject: [PATCH 03/23] Some about language --- DFA.v | 86 ++++++++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 65 insertions(+), 21 deletions(-) diff --git a/DFA.v b/DFA.v index b36bf88..c543c44 100644 --- a/DFA.v +++ b/DFA.v @@ -1,4 +1,4 @@ -Require Import List Ensembles. +Require Import List. Require Import Fin. @@ -6,43 +6,82 @@ Require Import Fin. Inductive ter : Type := | T : nat -> ter. +Definition word := list ter. + +Definition language := word -> Prop. (** The type of deterministic finite automata. ***) Record dfa : Type := mkDfa { states_n: nat; start: t states_n; - final: Ensemble (t states_n); + final: list (t states_n); next: (t states_n) -> ter -> (t states_n); }. +Fixpoint final_state (d : dfa) (s: t (states_n d)) (w: word) : t (states_n d) := + match w with + | nil => s + | h :: t => final_state d (next d s h) t + end. -Definition word := list ter. - -Definition language := word -> Prop. +Definition accepts (d : dfa) (s: t (states_n d)) (w: word) : Prop := + In (final_state d s w) (final d). + +(** The type of deterministic finite automata. ***) +Record s_dfa: Type := s_mkDfa { + s_states_n: nat; + s_start: t s_states_n; + s_final: t s_states_n; + s_next: (t s_states_n) -> ter -> (t s_states_n); +}. -Fixpoint accepts (d : dfa) (s: t (states_n d)) (w: word) : Prop := - match w with - | nil => In (t (states_n d)) (final d) s - | h :: t => accepts d (next d s h) t +Fixpoint s_final_state (d : s_dfa) (s: t (s_states_n d)) (w: word) : t (s_states_n d) := + match w with + | nil => s + | h :: t => s_final_state d (s_next d s h) t end. +Definition s_accepts (d : s_dfa) (s: t (s_states_n d)) (w: word) : Prop := + (s_final_state d s w) = (s_final d). + Definition dfa_language (d : dfa) := (accepts d (start d)). +Definition s_dfa_language (d : s_dfa) := (s_accepts d (s_start d)). + + + +Fixpoint split_dfa_list (d : dfa) (f_list : list (t (states_n d))) + : list s_dfa := + match f_list with + | nil => nil + | h :: t => s_mkDfa (states_n d) (start d) h (next d) :: split_dfa_list d t + end. + +Definition split_dfa (d: dfa) := split_dfa_list d (final d). + Definition language_union (l1 l2 : language) := fun w => (l1 w) \/ (l2 w). Definition language_intersection (l1 l2 : language) := fun w => (l1 w) /\ (l2 w). Definition language_eq (l1 l2 : language) := forall w : word, l1 w <-> l2 w. +Lemma mk_laguage_eq : forall (l1 l2 : language), (forall w : word, l1 w -> l2 w) -> (forall w : word, l2 w -> l1 w) -> language_eq l1 l2. +Proof. + intros l1 l2 H1 H2. + unfold language_eq. + intro w. + split. + apply (H1 w). + apply (H2 w). +Qed. + Theorem th1 : forall l1 l2 l3 : language, language_eq (language_intersection l1 (language_union l2 l3)) (language_union (language_intersection l1 l2) (language_intersection l1 l3)). Proof. intros. - unfold language_eq. - intros. - split. - intro. + apply mk_laguage_eq. + intros w H. unfold language_intersection in H. destruct H. unfold language_union in H0. @@ -55,7 +94,7 @@ Proof. unfold language_intersection. intuition. - intros. + intros w H. unfold language_union in H. destruct H. unfold language_intersection in H. @@ -89,10 +128,7 @@ Lemma distr : forall (a b c : Prop), (a /\ c) -> a /\ (b \/ c). Proof. intros. destruct H. - split. - exact H. - right. - exact H0. + auto. Qed. Theorem th2 : forall (l2 : language) (ls : list language), @@ -107,8 +143,7 @@ Proof. intros H0. unfold language_intersection in H0. destruct H0. - simpl in H0. - elim H0. + auto. intros a tail. intro HR. intro LI. @@ -180,4 +215,13 @@ Proof. apply distr. unfold language_intersection in H. exact H. -Qed. \ No newline at end of file +Qed. + +Theorem T21: forall d : dfa, language_eq (dfa_language d) (language_list_union (map (s_dfa_language) (split_dfa d))). +Proof. + intros. + apply mk_laguage_eq. + intros w H1. + unfold dfa_language in H1. + unfold accepts in H1. + unfold split_dfa. \ No newline at end of file From e5c8d408e4358cde00d52b5328390f09164dbaea Mon Sep 17 00:00:00 2001 From: HeyLey Date: Sun, 23 Apr 2017 21:23:31 +0300 Subject: [PATCH 04/23] Some about language --- DFA.v | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/DFA.v b/DFA.v index c543c44..38465da 100644 --- a/DFA.v +++ b/DFA.v @@ -156,57 +156,43 @@ Proof. destruct LI as [l2_w H1]. elim H1. - intro. - left. unfold language_intersection. - apply (conj l2_w H). intro. - right. - apply HR. unfold language_intersection. - apply (conj l2_w H). elim ls. - simpl. intros F; case F. - clear ls. - - intros LA ls H0 LU. + intros LA ls H0 LU. simpl language_list_union in LU. - case LU. intro H1. unfold language_intersection. - unfold language_intersection in H1. destruct H1. split. - exact H. simpl language_list_union. left; exact H1. - intro. - apply H0 in H. unfold language_intersection. From 9097701ff386ff6bfe07d9b4040d6a33420f9fba Mon Sep 17 00:00:00 2001 From: HeyLey Date: Tue, 25 Apr 2017 01:06:11 +0300 Subject: [PATCH 05/23] Lemma start --- DFA.v | 57 ++++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 36 insertions(+), 21 deletions(-) diff --git a/DFA.v b/DFA.v index 38465da..813413d 100644 --- a/DFA.v +++ b/DFA.v @@ -11,54 +11,52 @@ Definition word := list ter. Definition language := word -> Prop. (** The type of deterministic finite automata. ***) -Record dfa : Type := mkDfa { - states_n: nat; - start: t states_n; - final: list (t states_n); - next: (t states_n) -> ter -> (t states_n); +Record dfa { n : nat }: Type := mkDfa { + start: t n; + final: list (t n); + next: (t n) -> ter -> (t n); }. -Fixpoint final_state (d : dfa) (s: t (states_n d)) (w: word) : t (states_n d) := +Fixpoint final_state {n : nat} (d : dfa) (s: t n) (w: word) : t n := match w with | nil => s | h :: t => final_state d (next d s h) t end. -Definition accepts (d : dfa) (s: t (states_n d)) (w: word) : Prop := +Definition accepts (n : nat) (d : dfa) (s: t n) (w: word) : Prop := In (final_state d s w) (final d). (** The type of deterministic finite automata. ***) -Record s_dfa: Type := s_mkDfa { - s_states_n: nat; - s_start: t s_states_n; - s_final: t s_states_n; - s_next: (t s_states_n) -> ter -> (t s_states_n); +Record s_dfa { n : nat }: Type := s_mkDfa { + s_start: t n; + s_final: t n; + s_next: (t n) -> ter -> (t n); }. -Fixpoint s_final_state (d : s_dfa) (s: t (s_states_n d)) (w: word) : t (s_states_n d) := +Fixpoint s_final_state {n : nat} (d : s_dfa) (s: t n) (w: word) : t n := match w with | nil => s | h :: t => s_final_state d (s_next d s h) t end. -Definition s_accepts (d : s_dfa) (s: t (s_states_n d)) (w: word) : Prop := +Definition s_accepts {n : nat} (d : s_dfa (n:=n)) (s: t n) (w: word) : Prop := (s_final_state d s w) = (s_final d). -Definition dfa_language (d : dfa) := (accepts d (start d)). +Definition dfa_language {n : nat} (d : dfa (n:=n)) := (accepts n d (start d)). -Definition s_dfa_language (d : s_dfa) := (s_accepts d (s_start d)). +Definition s_dfa_language {n : nat} (d : s_dfa (n:=n)) := (s_accepts d (s_start d)). +Definition create_s_dfa {n : nat} (d : dfa (n:=n)) (h : t n) := s_mkDfa n (start d) h (next d). - -Fixpoint split_dfa_list (d : dfa) (f_list : list (t (states_n d))) +Fixpoint split_dfa_list {n : nat} (d : dfa) (f_list : list (t n)) : list s_dfa := match f_list with | nil => nil - | h :: t => s_mkDfa (states_n d) (start d) h (next d) :: split_dfa_list d t + | h :: t => create_s_dfa d h :: split_dfa_list d t end. -Definition split_dfa (d: dfa) := split_dfa_list d (final d). +Definition split_dfa {n : nat} (d: dfa (n:=n)) := split_dfa_list d (final d). Definition language_union (l1 l2 : language) := fun w => (l1 w) \/ (l2 w). @@ -147,7 +145,7 @@ Proof. intros a tail. intro HR. intro LI. - + simpl. unfold language_intersection in LI. @@ -203,6 +201,23 @@ Proof. exact H. Qed. +Theorem T0: forall (n:nat) (d: dfa (n:=n)) (st : t n) (e : t n) (w: word), + (final_state d st w) = + (s_final_state (create_s_dfa d e) st w). +Proof. + intros n d st e w. + revert st. + destruct d. + simpl. + unfold create_s_dfa. simpl. + induction w. + simpl. + reflexivity. + simpl. + intro st. + apply IHw. +Qed. + Theorem T21: forall d : dfa, language_eq (dfa_language d) (language_list_union (map (s_dfa_language) (split_dfa d))). Proof. intros. From c2b712a42f8f13cdb2f45807dd1752ca21de4fc4 Mon Sep 17 00:00:00 2001 From: HeyLey Date: Sat, 29 Apr 2017 12:45:04 +0300 Subject: [PATCH 06/23] add simple lemma T0 --- DFA.v | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/DFA.v b/DFA.v index 813413d..617c04e 100644 --- a/DFA.v +++ b/DFA.v @@ -19,13 +19,13 @@ Record dfa { n : nat }: Type := mkDfa { Fixpoint final_state {n : nat} (d : dfa) (s: t n) (w: word) : t n := match w with - | nil => s - | h :: t => final_state d (next d s h) t + | nil => s + | h :: t => final_state d (next d s h) t end. Definition accepts (n : nat) (d : dfa) (s: t n) (w: word) : Prop := - In (final_state d s w) (final d). - + In (final_state d s w) (final d). + (** The type of deterministic finite automata. ***) Record s_dfa { n : nat }: Type := s_mkDfa { @@ -36,8 +36,8 @@ Record s_dfa { n : nat }: Type := s_mkDfa { Fixpoint s_final_state {n : nat} (d : s_dfa) (s: t n) (w: word) : t n := match w with - | nil => s - | h :: t => s_final_state d (s_next d s h) t + | nil => s + | h :: t => s_final_state d (s_next d s h) t end. Definition s_accepts {n : nat} (d : s_dfa (n:=n)) (s: t n) (w: word) : Prop := @@ -57,14 +57,14 @@ Fixpoint split_dfa_list {n : nat} (d : dfa) (f_list : list (t n)) end. Definition split_dfa {n : nat} (d: dfa (n:=n)) := split_dfa_list d (final d). - + Definition language_union (l1 l2 : language) := fun w => (l1 w) \/ (l2 w). Definition language_intersection (l1 l2 : language) := fun w => (l1 w) /\ (l2 w). -Definition language_eq (l1 l2 : language) := forall w : word, l1 w <-> l2 w. +Definition language_eq (l1 l2 : language) := forall w : word, l1 w <-> l2 w. -Lemma mk_laguage_eq : forall (l1 l2 : language), (forall w : word, l1 w -> l2 w) -> (forall w : word, l2 w -> l1 w) -> language_eq l1 l2. +Lemma mk_laguage_eq : forall (l1 l2 : language), (forall w : word, l1 w -> l2 w) -> (forall w : word, l2 w -> l1 w) -> language_eq l1 l2. Proof. intros l1 l2 H1 H2. unfold language_eq. @@ -79,7 +79,7 @@ Theorem th1 : forall l1 l2 l3 : language, language_eq (language_intersection l1 Proof. intros. apply mk_laguage_eq. - intros w H. + intros w H. unfold language_intersection in H. destruct H. unfold language_union in H0. @@ -107,7 +107,7 @@ Proof. unfold language_intersection. destruct H. split. - + exact H. unfold language_union. right. @@ -128,7 +128,7 @@ Proof. destruct H. auto. Qed. - + Theorem th2 : forall (l2 : language) (ls : list language), language_eq (language_intersection l2 (language_list_union ls)) (language_list_union (map (language_intersection l2) ls)). @@ -215,7 +215,7 @@ Proof. reflexivity. simpl. intro st. - apply IHw. + apply IHw. Qed. Theorem T21: forall d : dfa, language_eq (dfa_language d) (language_list_union (map (s_dfa_language) (split_dfa d))). From a118017d9a0753d938007f27f25764037d70113b Mon Sep 17 00:00:00 2001 From: HeyLey Date: Sat, 29 Apr 2017 20:24:32 +0300 Subject: [PATCH 07/23] add proof for lemma 2.1 --- DFA.v | 102 +++++++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 84 insertions(+), 18 deletions(-) diff --git a/DFA.v b/DFA.v index 617c04e..8dad9d3 100644 --- a/DFA.v +++ b/DFA.v @@ -17,14 +17,14 @@ Record dfa { n : nat }: Type := mkDfa { next: (t n) -> ter -> (t n); }. -Fixpoint final_state {n : nat} (d : dfa) (s: t n) (w: word) : t n := +Fixpoint final_state {n : nat} (next_d : (t n) -> ter -> (t n)) (s: t n) (w: word) : t n := match w with | nil => s - | h :: t => final_state d (next d s h) t + | h :: t => final_state next_d (next_d s h) t end. Definition accepts (n : nat) (d : dfa) (s: t n) (w: word) : Prop := - In (final_state d s w) (final d). + In (final_state (next d) s w) (final d). (** The type of deterministic finite automata. ***) @@ -47,16 +47,16 @@ Definition dfa_language {n : nat} (d : dfa (n:=n)) := (accepts n d (start d)). Definition s_dfa_language {n : nat} (d : s_dfa (n:=n)) := (s_accepts d (s_start d)). -Definition create_s_dfa {n : nat} (d : dfa (n:=n)) (h : t n) := s_mkDfa n (start d) h (next d). +Definition create_s_dfa (n : nat) (st_d : t n) (next_d : (t n) -> ter -> (t n)) (h : t n) := s_mkDfa n st_d h next_d. -Fixpoint split_dfa_list {n : nat} (d : dfa) (f_list : list (t n)) +Fixpoint split_dfa_list {n : nat} (st_d : t n) (next_d : (t n) -> ter -> (t n)) (f_list : list (t n)) : list s_dfa := match f_list with | nil => nil - | h :: t => create_s_dfa d h :: split_dfa_list d t + | h :: t => create_s_dfa n st_d next_d h :: split_dfa_list st_d next_d t end. -Definition split_dfa {n : nat} (d: dfa (n:=n)) := split_dfa_list d (final d). +Definition split_dfa {n : nat} (d: dfa (n:=n)) := split_dfa_list (start d) (next d) (final d). Definition language_union (l1 l2 : language) := fun w => (l1 w) \/ (l2 w). @@ -201,15 +201,15 @@ Proof. exact H. Qed. -Theorem T0: forall (n:nat) (d: dfa (n:=n)) (st : t n) (e : t n) (w: word), - (final_state d st w) = - (s_final_state (create_s_dfa d e) st w). + +Theorem T0: forall (n:nat) (start0: t n) (final0 : list (t n)) (next0 : t n -> ter -> t n) (st : t n) (e : t n) (w: word), + (final_state next0 st w) = + (s_final_state (create_s_dfa n start0 next0 e) st w). Proof. - intros n d st e w. + intros. revert st. - destruct d. simpl. - unfold create_s_dfa. simpl. + unfold create_s_dfa. induction w. simpl. reflexivity. @@ -218,11 +218,77 @@ Proof. apply IHw. Qed. -Theorem T21: forall d : dfa, language_eq (dfa_language d) (language_list_union (map (s_dfa_language) (split_dfa d))). + +Theorem T21_1: forall (n : nat) (d : dfa (n:=n)) (w : word), + dfa_language d w -> language_list_union (map s_dfa_language (split_dfa d)) w. Proof. - intros. - apply mk_laguage_eq. - intros w H1. + intros n d w. + destruct d. + set (d := {| start := start0; final := final0; next := next0 |}). + intro H1. + unfold split_dfa. + simpl. unfold dfa_language in H1. + simpl in H1. unfold accepts in H1. - unfold split_dfa. \ No newline at end of file + simpl in H1. + induction final0. + simpl in H1. + elim H1. + simpl in H1. + destruct H1. + simpl. + left. + unfold s_dfa_language. + simpl. + unfold s_accepts. + simpl. + rewrite <- T0. + auto. + auto. + simpl. + right. + apply IHfinal0. + auto. +Qed. + + +Theorem T21_2: forall (n : nat) (d : dfa (n:=n)) (w : word), + language_list_union (map s_dfa_language (split_dfa d)) w -> dfa_language d w. +Proof. + intros n d w. + destruct d. + set (d := {| start := start0; final := final0; next := next0 |}). + unfold split_dfa. + simpl. + unfold dfa_language. + simpl. + unfold accepts. + simpl. + intro H1. + induction final0. + auto. + simpl in H1. + simpl. + destruct H1. + left. + unfold s_dfa_language in H. + simpl in H. + unfold s_accepts in H. + simpl in H. + rewrite T0 with (start0:=start0) (e:=a). + auto. + auto. + right. + apply IHfinal0. + auto. +Qed. + + +Theorem T21: forall (n : nat) (d : dfa (n:=n)), language_eq (dfa_language d) (language_list_union (map (s_dfa_language) (split_dfa d))). +Proof. + intros. + apply mk_laguage_eq. + apply T21_1. + apply T21_2. +Qed. \ No newline at end of file From 46dd51454871f3debf6fd272f5db6f6dc4cc7102 Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Mon, 8 May 2017 14:46:22 +0300 Subject: [PATCH 08/23] Add graph library --- CCFPQ/Graph.v | 195 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 195 insertions(+) create mode 100644 CCFPQ/Graph.v diff --git a/CCFPQ/Graph.v b/CCFPQ/Graph.v new file mode 100644 index 0000000..74eba2a --- /dev/null +++ b/CCFPQ/Graph.v @@ -0,0 +1,195 @@ +Require Import List. +Require Import Definitions. +Import ListNotations. + +Unset Implicit Arguments. +Set Strict Implicit. + +(* --------------------------------------------------------------------- *) +(* GRAPS - DEFINITIONS *) +(* --------------------------------------------------------------------- *) +(* This file moslty borrowed from GrapgBasics lib by Jean Duprat, *) +(* but I've added labels(terminals from Context-free grammar definition) *) +(* on arcs. *) +(* Loation of original lib is: *) +(* http://www.lix.polytechnique.fr/coq/V8.2pl1/contribs/GraphBasics.html *) +(* --------------------------------------------------------------------- *) + +Section Sets. + Variable U : Set. + Definition U_set := U -> Prop. + Inductive Empty : U_set :=. + Inductive Full : U_set := In_full : forall x : U, Full x. + Inductive Single (x : U) : U_set := In_single : Single x x. + Definition Included (E F : U_set) : Prop := forall x : U, E x -> F x. + + Inductive Union (E F : U_set) : U_set := + | In_left : forall x : U, E x -> Union E F x + | In_right : forall x : U, F x -> Union E F x. + Inductive Inter (E F : U_set) : U_set := In_inter : forall x : U, E x -> F x -> Inter E F x. + Inductive Differ (E F : U_set) : U_set := In_differ : forall x : U, E x -> ~ F x -> Differ E F x. + + Lemma Not_union : forall (E1 E2 : U_set) (x : U), ~ E1 x -> ~ E2 x -> ~ Union E1 E2 x. + Proof. + intros; red in |- *; intros. + inversion H1. + elim H; trivial. + elim H0; trivial. + Qed. + + Lemma Single_equal : forall x y : U, Single x y -> x = y. + Proof. + intros; inversion H; trivial. + Qed. +End Sets. + +Section Enumeration. + Variable U : Set. + Definition U_list := list U. + Definition U_enumerable (E : U_set U) := {ul : U_list | forall x : U, E x -> In x ul}. + + Inductive U_canon : U_list -> Prop := + | U_canon_nil : U_canon nil + | U_canon_cons : forall (x : U) (ul : U_list), U_canon ul -> ~ In x ul -> U_canon (x :: ul). +End Enumeration. + +Section Vertices. + Inductive Vertex : Set := idx : nat -> Vertex. + Definition V_list := list Vertex. + Definition V_nil : list Vertex := nil. + Definition V_set := U_set Vertex. + Definition V_empty := Empty Vertex. + Definition V_single := Single Vertex. + Definition V_union := Union Vertex. + + Implicit Types m n x y : nat. + Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}. + Proof. + induction n; induction m; auto. + elim (IHn m); auto. + Defined. + + Lemma V_eq_dec : forall x y : Vertex, {x = y} + {x <> y}. + Proof. + simple destruct x; simple destruct y; intros. + case (eq_nat_dec n n0); intros. + left; rewrite e; trivial. + right; injection; trivial. + Qed. +End Vertices. + +Section Arcs. + Inductive Arc : Set := A_ends : Vertex -> Vertex -> ter -> Arc. + Definition A_tail (a : Arc) : Vertex := match a with A_ends x y l => x end. + Definition A_head (a : Arc) : Vertex := match a with A_ends x y l => y end. + Definition A_set := U_set Arc. + Definition A_list := list Arc. + Definition A_nil : list Arc := nil. + Definition A_empty := Empty Arc. + Definition A_single := Single Arc. + Definition A_union := Union Arc. +End Arcs. + +Section Graph. + Inductive Digraph : V_set -> A_set -> Type := + | D_empty : Digraph V_empty A_empty + | D_vertex : + forall (v : V_set) (a : A_set) (d : Digraph v a) (x : Vertex), + ~ v x -> Digraph (V_union (V_single x) v) a + | D_arc : + forall (v : V_set) (a : A_set) (d : Digraph v a) (x y : Vertex) (l : ter), + v x -> v y -> ~ a (A_ends x y l) -> Digraph v (A_union (A_single (A_ends x y l)) a) + | D_eq : + forall (v v' : V_set) (a a' : A_set), + v = v' -> a = a' -> Digraph v a -> Digraph v' a'. + + Fixpoint DV_list (v : V_set) (a : A_set) (d : Digraph v a) : V_list := match d with + | D_empty => V_nil + | D_vertex v' a' d' x _ => x :: DV_list v' a' d' + | D_arc v' a' d' x y l _ _ _ => DV_list v' a' d' + | D_eq v v' a a' _ _ d => DV_list v a d + end. + + Fixpoint DA_list (v : V_set) (a : A_set) (d : Digraph v a) : A_list := match d with + | D_empty => A_nil + | D_vertex v' a' d' x _ => DA_list v' a' d' + | D_arc v' a' d' x y l _ _ _ => A_ends x y l :: DA_list v' a' d' + | D_eq v v' a a' _ _ d => DA_list v a d + end. +End Graph. + +Section Degrees. + Variable a : A_set. + Definition In_neighbor (x y : Vertex) (l : ter) := a (A_ends y x l). + Definition Out_neighbor (x y : Vertex) (l : ter) := a (A_ends x y l). + + Fixpoint In_neighborhood (x : Vertex) (v : V_set) (a : A_set) (d : Digraph v a) : V_list := + match d with + | D_empty => V_nil + | D_vertex v' a' d' x' _ => In_neighborhood x v' a' d' + | D_arc v' a' d' x' y' l' _ _ _ => + if V_eq_dec x y' + then x' :: In_neighborhood x v' a' d' + else In_neighborhood x v' a' d' + | D_eq v' _ a' _ _ _ d' => In_neighborhood x v' a' d' + end. + + Fixpoint Out_neighborhood (x : Vertex) (v : V_set) + (a : A_set) (d : Digraph v a) {struct d} : V_list := + match d with + | D_empty => V_nil + | D_vertex v' a' d' x' _ => Out_neighborhood x v' a' d' + | D_arc v' a' d' x' y' l' _ _ _ => + if V_eq_dec x x' + then y' :: Out_neighborhood x v' a' d' + else Out_neighborhood x v' a' d' + | D_eq v' _ a' _ _ _ d' => Out_neighborhood x v' a' d' + end. +End Degrees. + +Section Paths. + Variable v : V_set. + Variable a : A_set. + Inductive D_walk : Vertex -> Vertex -> V_list -> A_list -> Set := + | DW_null : forall x : Vertex, v x -> D_walk x x V_nil A_nil + | DW_step : + forall (x y z : Vertex) (vl : V_list) (al : A_list) (l : ter), + D_walk y z vl al -> + a (A_ends x y l) -> + D_walk x z (y :: vl) (A_ends x y l :: al). + Definition D_closed_walk := forall (x : Vertex) (vl : V_list) (al : A_list), D_walk x x vl al. + + Inductive D_trail : Vertex -> Vertex -> V_list -> A_list -> Set := + | DT_null : forall x : Vertex, v x -> D_trail x x V_nil A_nil + | DT_step : + forall (x y z : Vertex) (vl : V_list) (al : A_list) (l : ter), + D_trail y z vl al -> + a (A_ends x y l) -> + ~ In (A_ends x y l) al -> + D_trail x z (y :: vl) (A_ends x y l :: al). + Definition D_closed_trail := forall (x : Vertex) (vl : V_list) (al : A_list), D_trail x x vl al. + + Inductive D_path : Vertex -> Vertex -> V_list -> A_list -> Set := + | DP_null : forall x : Vertex, v x -> D_path x x V_nil A_nil + | DP_step : + forall (x y z : Vertex) (vl : V_list) (al : A_list) (l : ter), + D_path y z vl al -> + a (A_ends x y l) -> + ~ In y vl -> + (In x vl -> x = z) -> + ~ In (A_ends x y l) al -> + D_path x z (y :: vl) (A_ends x y l :: al). + Definition D_cycle := forall (x : Vertex) (vl : V_list) (al : A_list), D_path x x vl al. +End Paths. + +Section Connectivity. + Variable v : V_set. + Variable a : A_set. + Inductive Vertex_conn : Vertex -> Vertex -> Set := + | VC_null : forall x : Vertex, v x -> Vertex_conn x x + | VC_step : + forall (x y z : Vertex) (l : ter), + Vertex_conn y z -> + a (A_ends x y l) -> + Vertex_conn x z. +End Connectivity. From 2a6367c05bf2657383eaff32643cca5a0c59df48 Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Mon, 8 May 2017 14:46:49 +0300 Subject: [PATCH 09/23] Add CCFPQ definition --- CCFPQ/CCFPQ.v | 115 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 115 insertions(+) create mode 100644 CCFPQ/CCFPQ.v diff --git a/CCFPQ/CCFPQ.v b/CCFPQ/CCFPQ.v new file mode 100644 index 0000000..40ec02f --- /dev/null +++ b/CCFPQ/CCFPQ.v @@ -0,0 +1,115 @@ +Require Import Definitions. +Require Import Graph. +Unset Implicit Arguments. +Set Strict Implicit. + +Section CCFPQ. + (* Every conjunct may have "free" variables (vertices that should be in answer), *) + (* or "bound" variables (bound by the existential quantifier), to represent this *) + (* analogue of Haskell Either datatype I use triple with boolean 3rd argument *) + (* which is set to true (when we should look at the first field (vertex)), *) + (* or false (then accordingly look at the second one). *) + Definition EitherVertexNat : Set := prod (prod Vertex nat) bool. + Definition EitherVertexNat_pair := prod EitherVertexNat EitherVertexNat. + Definition var_EitherVertexNat_pair := prod var EitherVertexNat_pair. + + Definition Nat_set := U_set nat. + Definition Nat_union := Union nat. + Definition Nat_single := Single nat. + Definition Nat_empty := Empty nat. + + Definition vertex_placeholder : Vertex := idx 0. + Definition nat_placeholder : nat := 0. + Definition getv (x : Vertex) : EitherVertexNat := pair (pair x nat_placeholder) true. + Definition getn (n : nat) : EitherVertexNat := pair (pair vertex_placeholder n) false. + + (* Construct conjunct of type var_EitherVertexNat_pair from 2 single variables and non-terminal *) + Fixpoint constr_nt_VV (n : var) (a b : Vertex) := pair n (pair (getv a) (getv b)). + Fixpoint constr_nt_VN (n : var) (a : Vertex) (b: nat) := pair n (pair (getv a) (getn b)). + Fixpoint constr_nt_NV (n : var) (a : nat) (b: Vertex) := pair n (pair (getn a) (getv b)). + Fixpoint constr_nt_NN (n : var) (a b : nat) := pair n (pair (getn a) (getn b)). + + Inductive CCFPQ_Builder : V_set -> Nat_set -> list var_EitherVertexNat_pair -> Type := + | Empty : CCFPQ_Builder V_empty Nat_empty [] + | Add_free_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) + (nt : var) (x : Vertex), + CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder (V_union v (V_single x)) n var_evnp_l + | Add_bound_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) + (nt : var) (bv : nat), + CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v (Nat_union n (Nat_single bv)) var_evnp_l + | Add_conj_vertex_vertex : forall v n var_evnp_l nt (x1 x2 : Vertex), + CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((constr_nt_VV nt x1 x2)::var_evnp_l) + | Add_conj_vertex_nat : forall v n var_evnp_l nt (x: Vertex) (bv : nat), + CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((constr_nt_VN nt x bv)::var_evnp_l) + | Add_conj_nat_vertex : forall v n var_evnp_l nt (bv : nat) (x : Vertex), + CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((constr_nt_NV nt bv x)::var_evnp_l) + | Add_conj_nat_nat : forall v n var_evnp_l nt (bv1 bv2: nat), + CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((constr_nt_NN nt bv1 bv2)::var_evnp_l). + + Definition is_empty vs ns var_evnp_l (builder : CCFPQ_Builder vs ns var_evnp_l) := + match builder with + | Empty => True + | _ => False + end. + + Definition get_bound_vars' (evnp: EitherVertexNat_pair) : list nat := + match evnp with + | ((_, n1, false), (_, n2, false)) => n1::n2::[] + | ((_, _, true), (_, n, false)) => n::[] + | ((_, n, false), (_, _, true)) => n::[] + | ((_, _, true), (_, _, true)) => [] + end. + + Fixpoint get_bound_vars (var_evnp_l: list var_EitherVertexNat_pair) : list nat := + match var_evnp_l with + | [] => [] + | var_evnp::tl => get_bound_vars' (snd var_evnp) ++ get_bound_vars tl + end. + + Definition get_free_vars' (evnp: EitherVertexNat_pair) : list Vertex := + match evnp with + | ((_, _, false), (_, _, false)) => [] + | ((v, _, true), (_, _, false)) => v::[] + | ((_, _, false), (v, _, true)) => v::[] + | ((v1, _, true), (v2, _, true)) => v1::v2::[] + end. + + Fixpoint get_free_vars (var_evnp_l: list var_EitherVertexNat_pair) : list Vertex := + match var_evnp_l with + | [] => [] + | var_evnp::tl => get_free_vars' (snd var_evnp) ++ get_free_vars tl + end. + + Record CCFPQ : Type := { + vs : V_set; + ns : Nat_set; + var_evnp_l : list var_EitherVertexNat_pair; + builder : CCFPQ_Builder vs ns var_evnp_l; + + (* CCFPQ is legal when all conditions are met *) + is_not_empty : ~ (is_empty vs ns var_evnp_l builder); + all_bound_vars_exist : forall (n : nat), In n (get_bound_vars var_evnp_l) -> ns n; + all_free_vars_exist : forall (x : Vertex), In x (get_free_vars var_evnp_l) -> vs x; + all_vertices_in_answer: forall (x : Vertex), vs x -> In x (get_free_vars var_evnp_l) + }. + + Fixpoint get_nonterminals (var_evnp_l: list var_EitherVertexNat_pair) : list var := + match var_evnp_l with + | [] => [] + | (nt, _)::tl => nt::get_nonterminals tl + end. + + Fixpoint get_all_vars (G : grammar) : list var := + match G with + | [] => [] + | R A u::Gr => A::(get_all_vars Gr) + end. + + Record CCFPQ_on_grammar : Type := { + ccfpq : CCFPQ; + gr : grammar; + + nonterminals_in_grammar : forall (nt : var), + In nt (get_nonterminals (var_evnp_l ccfpq)) -> In nt (get_all_vars gr) + }. +End CCFPQ. From ea46320af2dd3b6d53ac034a94ca63b773c3dd81 Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Mon, 8 May 2017 14:47:24 +0300 Subject: [PATCH 10/23] Add different semantics of CCFPQ evaluation --- CCFPQ/CCFPQ_Result.v | 80 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 80 insertions(+) create mode 100644 CCFPQ/CCFPQ_Result.v diff --git a/CCFPQ/CCFPQ_Result.v b/CCFPQ/CCFPQ_Result.v new file mode 100644 index 0000000..fe1a4e6 --- /dev/null +++ b/CCFPQ/CCFPQ_Result.v @@ -0,0 +1,80 @@ +Require Import Definitions. +Require Import Derivation. +Require Import Graph. +Require Import CCFPQ. + +Unset Implicit Arguments. +Set Strict Implicit. + +Section CFPQ_Res. + Fixpoint getLabels' (arcs : A_list) : list symbol := match arcs with + | [] => [] + | (A_ends _ _ l)::t => (Ts l)::(getLabels' t) + end. + + Fixpoint getLength' (arcs : A_list) : nat := match arcs with + | [] => 0 + | arc::t => 1 + (getLength' t) + end. + + Variable VL : V_list. + Variable AL : A_list. + Definition getLabels VV AA xl1 xl2 (walk : D_walk VV AA xl1 xl2 VL AL) : list symbol := getLabels' AL. + Definition getLength VV AA xl1 xl2 (walk : D_walk VV AA xl1 xl2 VL AL) : nat := getLength' AL. + + Record CFPQ_Relational_query_result : Type := { + g_ : grammar; + CFPQ_ : var_EitherVertexNat_pair; + V_ : V_set; + A_ : A_set; + Graph_ : Digraph V_ A_; + + ntm_ : var := fst CFPQ_; + evnp_ : EitherVertexNat_pair := snd CFPQ_; + are_connected : exists (x1 x2 : Vertex), exists (conn : Vertex_conn V_ A_ x1 x2), True + }. + + Record CFPQ_Single_path_query_result : Type := { + g : grammar; + CFPQ : var_EitherVertexNat_pair; + V : V_set; + A : A_set; + Graph : Digraph V A; + + ntm : var := fst CFPQ; + evnp : EitherVertexNat_pair := snd CFPQ; + has_path : exists (x1 x2 : Vertex), exists (walk : D_walk V A x1 x2 _ _), + der g ntm (getLabels V A x1 x2 walk) + }. + + Record CFPQ_Single_shortest_path_query_result : Type := { + g' : grammar; + CFPQ' : var_EitherVertexNat_pair; + V' : V_set; + A' : A_set; + Graph' : Digraph V' A'; + + ntm' : var := fst CFPQ'; + evnp' : EitherVertexNat_pair := snd CFPQ'; + has_shortest_path : exists (x1 x2 : Vertex), exists (walk : D_walk V' A' x1 x2 _ _), + der g' ntm' (getLabels V' A' x1 x2 walk) -> + forall (other_walk : D_walk V' A' x1 x2 _ _), + getLength V' A' x1 x2 other_walk >= getLength V' A' x1 x2 walk + }. + + Record CFPQ_All_path_query_result : Type := { + g'' : grammar; + CFPQ'' : var_EitherVertexNat_pair; + V'' : V_set; + A'' : A_set; + Graph'' : Digraph V'' A''; + + ntm'' : var := fst CFPQ''; + evnp'' : EitherVertexNat_pair := snd CFPQ''; + all_paths : exists (all_pairs : list (prod Vertex Vertex)), + forall (pair_of_vertices : (prod Vertex Vertex)), + In pair_of_vertices all_pairs <-> + exists (walk : D_walk V'' A'' (fst pair_of_vertices) (snd pair_of_vertices) _ _), + der g'' ntm'' (getLabels V'' A'' (fst pair_of_vertices) (snd pair_of_vertices) walk) + }. +End CFPQ_Res. From 5c037bb7be4c5e8b1e7af5d4eacec14fe22e4b00 Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Wed, 10 May 2017 01:21:35 +0300 Subject: [PATCH 11/23] Rename constructor and remove unused variables --- CCFPQ/CCFPQ.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/CCFPQ/CCFPQ.v b/CCFPQ/CCFPQ.v index 40ec02f..f360e61 100644 --- a/CCFPQ/CCFPQ.v +++ b/CCFPQ/CCFPQ.v @@ -30,12 +30,12 @@ Section CCFPQ. Fixpoint constr_nt_NN (n : var) (a b : nat) := pair n (pair (getn a) (getn b)). Inductive CCFPQ_Builder : V_set -> Nat_set -> list var_EitherVertexNat_pair -> Type := - | Empty : CCFPQ_Builder V_empty Nat_empty [] + | Empty_query : CCFPQ_Builder V_empty Nat_empty [] | Add_free_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) - (nt : var) (x : Vertex), + (x : Vertex), CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder (V_union v (V_single x)) n var_evnp_l | Add_bound_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) - (nt : var) (bv : nat), + (bv : nat), CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v (Nat_union n (Nat_single bv)) var_evnp_l | Add_conj_vertex_vertex : forall v n var_evnp_l nt (x1 x2 : Vertex), CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((constr_nt_VV nt x1 x2)::var_evnp_l) @@ -48,7 +48,7 @@ Section CCFPQ. Definition is_empty vs ns var_evnp_l (builder : CCFPQ_Builder vs ns var_evnp_l) := match builder with - | Empty => True + | Empty_query => True | _ => False end. From 6f60e84f510c2eeeff8d4ac0cb2adb91916c42f6 Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Wed, 10 May 2017 01:22:23 +0300 Subject: [PATCH 12/23] Avoid apostrophes in names --- CCFPQ/CCFPQ_Result.v | 62 ++++++++++++++++++++++---------------------- 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/CCFPQ/CCFPQ_Result.v b/CCFPQ/CCFPQ_Result.v index fe1a4e6..501f688 100644 --- a/CCFPQ/CCFPQ_Result.v +++ b/CCFPQ/CCFPQ_Result.v @@ -23,15 +23,15 @@ Section CFPQ_Res. Definition getLength VV AA xl1 xl2 (walk : D_walk VV AA xl1 xl2 VL AL) : nat := getLength' AL. Record CFPQ_Relational_query_result : Type := { - g_ : grammar; - CFPQ_ : var_EitherVertexNat_pair; - V_ : V_set; - A_ : A_set; - Graph_ : Digraph V_ A_; + g_r : grammar; + CFPQ_r : var_EitherVertexNat_pair; + V_r : V_set; + A_r : A_set; + Graph_r : Digraph V_r A_r; - ntm_ : var := fst CFPQ_; - evnp_ : EitherVertexNat_pair := snd CFPQ_; - are_connected : exists (x1 x2 : Vertex), exists (conn : Vertex_conn V_ A_ x1 x2), True + ntm_r : var := fst CFPQ_r; + evnp_r : EitherVertexNat_pair := snd CFPQ_r; + are_connected : exists (x1 x2 : Vertex), exists (conn : Vertex_conn V_r A_r x1 x2), True }. Record CFPQ_Single_path_query_result : Type := { @@ -39,42 +39,42 @@ Section CFPQ_Res. CFPQ : var_EitherVertexNat_pair; V : V_set; A : A_set; - Graph : Digraph V A; + Graph : Digraph V A; ntm : var := fst CFPQ; evnp : EitherVertexNat_pair := snd CFPQ; - has_path : exists (x1 x2 : Vertex), exists (walk : D_walk V A x1 x2 _ _), + has_path : exists (x1 x2 : Vertex), exists (walk : D_walk V A x1 x2 _ _), der g ntm (getLabels V A x1 x2 walk) }. Record CFPQ_Single_shortest_path_query_result : Type := { - g' : grammar; - CFPQ' : var_EitherVertexNat_pair; - V' : V_set; - A' : A_set; - Graph' : Digraph V' A'; + g_s : grammar; + CFPQ_s : var_EitherVertexNat_pair; + V_s : V_set; + A_s : A_set; + Graph' : Digraph V_s A_s; - ntm' : var := fst CFPQ'; - evnp' : EitherVertexNat_pair := snd CFPQ'; - has_shortest_path : exists (x1 x2 : Vertex), exists (walk : D_walk V' A' x1 x2 _ _), - der g' ntm' (getLabels V' A' x1 x2 walk) -> - forall (other_walk : D_walk V' A' x1 x2 _ _), - getLength V' A' x1 x2 other_walk >= getLength V' A' x1 x2 walk + ntm_s : var := fst CFPQ_s; + evnp_s : EitherVertexNat_pair := snd CFPQ_s; + has_shortest_path : exists (x1 x2 : Vertex), exists (walk : D_walk V_s A_s x1 x2 _ _), + der g_s ntm_s (getLabels V_s A_s x1 x2 walk) -> + forall (other_walk : D_walk V_s A_s x1 x2 _ _), + getLength V_s A_s x1 x2 other_walk >= getLength V_s A_s x1 x2 walk }. Record CFPQ_All_path_query_result : Type := { - g'' : grammar; - CFPQ'' : var_EitherVertexNat_pair; - V'' : V_set; - A'' : A_set; - Graph'' : Digraph V'' A''; + g_a : grammar; + CFPQ_a : var_EitherVertexNat_pair; + V_a : V_set; + A_a : A_set; + Graph_a : Digraph V_a A_a; - ntm'' : var := fst CFPQ''; - evnp'' : EitherVertexNat_pair := snd CFPQ''; - all_paths : exists (all_pairs : list (prod Vertex Vertex)), + ntm_a : var := fst CFPQ_a; + evnp_a : EitherVertexNat_pair := snd CFPQ_a; + all_paths : exists (all_pairs : list (prod Vertex Vertex)), forall (pair_of_vertices : (prod Vertex Vertex)), In pair_of_vertices all_pairs <-> - exists (walk : D_walk V'' A'' (fst pair_of_vertices) (snd pair_of_vertices) _ _), - der g'' ntm'' (getLabels V'' A'' (fst pair_of_vertices) (snd pair_of_vertices) walk) + exists (walk : D_walk V_a A_a (fst pair_of_vertices) (snd pair_of_vertices) _ _), + der g_a ntm_a (getLabels V_a A_a (fst pair_of_vertices) (snd pair_of_vertices) walk) }. End CFPQ_Res. From b3159e8b652078d051441565f9c4245c94073203 Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Wed, 10 May 2017 01:23:59 +0300 Subject: [PATCH 13/23] Add graph construction examples --- CCFPQ/Examples/Graph_examples.v | 162 ++++++++++++++++++++++++++++++++ 1 file changed, 162 insertions(+) create mode 100644 CCFPQ/Examples/Graph_examples.v diff --git a/CCFPQ/Examples/Graph_examples.v b/CCFPQ/Examples/Graph_examples.v new file mode 100644 index 0000000..f08dada --- /dev/null +++ b/CCFPQ/Examples/Graph_examples.v @@ -0,0 +1,162 @@ +From mathcomp.ssreflect Require Import ssreflect ssrbool ssrnat eqtype ssrfun. +Require Import Graph. +Require Import Definitions. + +(* This file contains sample definitions of graphs and paths. *) + +(* Sets. *) +Definition s1 : U_set nat := Single nat 1. +Definition s2 : U_set nat := Single nat 2. +Definition s12 : U_set nat := Union nat s1 s2. + +Lemma one_in_s12 : s12 1. +Proof. + constructor. + constructor. +Qed. + +(* Vertices. *) +Definition vertex1 : Vertex := idx 1. +Definition vertex2 : Vertex := idx 2. +Definition vertex3 : Vertex := idx 3. +Definition vertices : V_list := [vertex1 ; vertex2 ; vertex3]. +Definition verticesSet : V_set := Union Vertex (Single Vertex vertex3) + (Union Vertex (Single Vertex vertex1) (Single Vertex vertex1)). + +(* Arcs. *) +Definition label12 := T 12. +Definition label21 := T 21. +Definition label23 := T 23. +Definition arc12 : Arc := A_ends vertex1 vertex2 label12. +Definition arc21 : Arc := A_ends vertex2 vertex1 label21. +Definition arc23 : Arc := A_ends vertex2 vertex3 label23. + +Definition arcs : A_set := Single Arc arc12. + +Lemma arc12_in_arcs : arcs arc12. +Proof. + constructor. +Qed. + +(* Graphs. *) +Definition gType := Digraph verticesSet arcs. +Check gType. + +Definition eg := D_empty. +Check eg. + +(* Let's add a vertex to this empty graph. *) +(* First, prove that graph doesn't contain this vertex. *) +Lemma v1_not_in_V_empty : ~ V_empty vertex1. +Proof. + done. +Qed. + +(* And now add it. *) +Definition g1 := D_vertex V_empty A_empty D_empty vertex1 v1_not_in_V_empty. +Check g1. +Definition g1v := (V_union (V_single vertex1) V_empty). + +(* Add one more vertex. *) +Lemma not_in_single : forall v1 v2 : Vertex, v1 <> v2 -> ~ (Single Vertex v1) v2. +Proof. + move => v1 v2 Hv H. + apply Single_equal in H. + contradiction. +Qed. + +Lemma v2_not_in_g1v : ~ (g1v vertex2). +Proof. + rewrite / g1v / V_union / V_empty / V_single. + apply: Not_union. + apply: not_in_single. + done. + done. +Qed. + +Definition g12 := D_vertex g1v A_empty g1 vertex2 v2_not_in_g1v. +Definition g12v := (V_union (V_single vertex2) g1v). + +(* Add more. *) +Lemma v3_not_in_g12v: ~ (g12v vertex3). +Proof. + rewrite / g12v / V_union / V_empty / V_single / g1v / V_union / V_empty / V_single. + apply: Not_union. + apply: not_in_single. + done. + apply: Not_union. + apply: not_in_single. + done. + done. +Qed. + +Definition g123 := D_vertex g12v A_empty g12 vertex3 v3_not_in_g12v. +Definition g123v := (V_union (V_single vertex3) g12v). + +(* Check funcions, that collects vertices and arcs. *) +Eval compute in DV_list g123v A_empty g123. +Eval compute in DA_list g123v A_empty g123. + +(* Now add an arc. *) +Lemma v1_in_g123v: g123v vertex1. +Proof. + rewrite / g123v / g12v / g1v. + constructor 2. + constructor 2. + constructor 1. + done. +Qed. + +Lemma v2_in_g123v: g123v vertex2. +Proof. + rewrite / g123v / g12v. + constructor 2. + constructor 1. + done. +Qed. + +Lemma arc_not_in_A_empty : ~ A_empty (A_ends vertex1 vertex2 label12). +Proof. + done. +Qed. + +Definition g123v12a := D_arc g123v A_empty g123 vertex1 vertex2 label12 + v1_in_g123v v2_in_g123v arc_not_in_A_empty. +Check g123v12a. + +Definition g123v12arcs := (A_union (A_single (A_ends vertex1 vertex2 label12)) A_empty). + +(* Check funcions again. *) +Eval compute in DV_list g123v g123v12arcs g123v12a. +Eval compute in DA_list g123v g123v12arcs g123v12a. + +(* Define a paths in our graph. *) +Definition ep := DP_null g123v g123v12arcs vertex2 v2_in_g123v. + +Lemma arc_in_arcs : g123v12arcs (A_ends vertex1 vertex2 label12). +Proof. + constructor. + done. +Qed. + +Lemma not_in_nil_V : ~ In vertex2 V_nil. +Proof. + rewrite / V_nil. + done. +Qed. + +Lemma not_in_nil_A : ~ In (A_ends vertex1 vertex2 label12) A_nil. +Proof. + rewrite / A_nil. + done. +Qed. + +Lemma v1_eq_v2 : In vertex1 V_nil -> vertex1 = vertex2. +Proof. + move => H. + done. +Qed. + +Definition p12 := DP_step g123v g123v12arcs vertex1 vertex2 vertex2 V_nil A_nil label12 + ep arc_in_arcs not_in_nil_V v1_eq_v2 not_in_nil_A. +Check p12. From 3bc3bd5a4dbe50bace8f3f1ce7f02289383e79e8 Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Wed, 10 May 2017 01:24:16 +0300 Subject: [PATCH 14/23] Add cfg construction examples --- CCFPQ/Examples/CFG_examples.v | 85 +++++++++++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 CCFPQ/Examples/CFG_examples.v diff --git a/CCFPQ/Examples/CFG_examples.v b/CCFPQ/Examples/CFG_examples.v new file mode 100644 index 0000000..8d73a5e --- /dev/null +++ b/CCFPQ/Examples/CFG_examples.v @@ -0,0 +1,85 @@ +From mathcomp.ssreflect Require Import ssreflect ssrbool ssrnat eqtype ssrfun. +Require Import Definitions. +Require Import Derivation. +Require Import List. +Import ListNotations. + +(* This file contains sample definitions of cf grammars. *) +(* In this sample we define grammar for well-formed *) +(* parentheses with 2 types of brackets. *) + +(* Define terminals at first. *) +Definition t1 : ter := T 1. +Definition t2 := T 2. +Definition t3 := T 3. +Definition t4 := T 4. + +(* Now define non-terminals. *) +Definition v1 : var := V 1. + +Definition st1 : symbol := Ts t1. +Definition st2 := Ts t2. +Definition st3 := Ts t3. +Definition st4 := Ts t4. +Definition sv1 := Vs v1. + +Definition phrase1 : phrase := [sv1 ; sv1]. +Definition phrase2 := [st1 ; st2]. +Definition phrase3 := [st1 ; sv1 ; st2]. +Definition phrase4 := [st3 ; st4]. +Definition phrase5 := [st3 ; sv1 ; st4]. + +Definition rule1 : rule := R v1 phrase1. +Definition rule2 := R v1 phrase2. +Definition rule3 := R v1 phrase3. +Definition rule4 := R v1 phrase4. +Definition rule5 := R v1 phrase5. + +(* Define grammar. *) +Definition grammar := [rule1 ; rule2 ; rule3 ; rule4 ; rule5]. +Eval compute in grammar. + +(* Example of derivation. *) + +(* Derives "()" *) +Lemma derives1 : der grammar v1 [st1 ; st2]. +Proof. + constructor. + constructor 2. + constructor. + done. +Qed. + +(* Derives "[]" *) +Lemma derives2 : der grammar v1 [st3 ; st4]. +Proof. + constructor. + constructor 2. + constructor 2. + constructor 2. + constructor. + rewrite / rule4. + rewrite / phrase4. + done. +Qed. + +(* Derives "(S)" *) +Lemma derives3 : der grammar v1 [st1 ; sv1 ; st2]. +Proof. + constructor. + constructor 2. + constructor 2. + constructor. + rewrite / rule3. + rewrite / phrase3. + done. +Qed. + +(* Derives "([])" *) +Lemma derives' : der grammar v1 ([st1] ++ [st3; st4] ++ [st2]). +Proof. + move: derives2. + apply: replN. + move: derives3. + done. +Qed. From c5f149f4be5261bf8260eb5d746292abed9dd181 Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Wed, 10 May 2017 01:24:38 +0300 Subject: [PATCH 15/23] Add ccfpq construction examples --- CCFPQ/Examples/CCFPQ_Examples.v | 128 ++++++++++++++++++++++++++++++++ 1 file changed, 128 insertions(+) create mode 100644 CCFPQ/Examples/CCFPQ_Examples.v diff --git a/CCFPQ/Examples/CCFPQ_Examples.v b/CCFPQ/Examples/CCFPQ_Examples.v new file mode 100644 index 0000000..5794fb2 --- /dev/null +++ b/CCFPQ/Examples/CCFPQ_Examples.v @@ -0,0 +1,128 @@ +From mathcomp.ssreflect Require Import ssreflect ssrbool ssrnat eqtype ssrfun. +Require Import Definitions. +Require Import CCFPQ. +Require Import Graph. +Require Import List. +Import ListNotations. + +(* Let's build an example query. *) +Definition empty := Empty_query. +(* Now quiery is empty: Q() -> ... *) + +(* Add new vertex to the answer. *) +Definition v1 : Vertex := idx 1. +Definition q1 := Add_free_var V_empty Nat_empty [] v1 empty. +(* Now query is: Q(v1) -> ... *) + +(* Add new vertex to the answer. *) +Definition v2 : Vertex := idx 2. +Definition q2 := Add_free_var (V_union V_empty (V_single v1)) Nat_empty [] v2 q1. +(* Now query is: Q(v1, v2) -> ... *) +Definition v1v2 : V_set := (V_union (V_union V_empty (V_single v1)) (V_single v2)). + +(* Add new variable to the right side. *) +Definition q3 := Add_bound_var v1v2 Nat_empty [] 1 q2. +(* Now query is: Q(v1, v2) -> exists 1: ... *) +Definition n1 := (Nat_union Nat_empty (Nat_single 1)). + +(* Add first conjunct. *) +Definition nt1 : var := V 1. +Definition q4 := Add_conj_vertex_nat v1v2 n1 [] nt1 v1 1 q3. +(* Now query is: Q(v1, v2) -> exists 1: nt1(v1, 1). *) +Definition conjuncts := [constr_nt_VN nt1 v1 1]. + +(* Add second conjunct. *) +Definition nt2 : var := V 2. +Definition q5 := Add_conj_nat_vertex v1v2 n1 conjuncts nt2 1 v2 q4. +(* Now query is: Q(v1, v2) -> exists 1: [nt1(v1, 1), nt2(1, v2)]. *) +Definition conjuncts' := (constr_nt_NV nt2 1 v2 :: conjuncts). + +(* Now prove that this query is legal. *) +Lemma l1 : ~(is_empty v1v2 n1 conjuncts' q5). +Proof. + simpl. + done. +Qed. + +Lemma or_false : forall (p: Prop) (p1: Prop), p \/ p1 \/ False -> p \/ p1. +Proof. + firstorder. +Qed. + +Lemma or_false_inv : forall (p: Prop) (p1: Prop), p \/ p1 -> p \/ p1 \/ False . +Proof. + firstorder. +Qed. + +Lemma x_or_x : forall (p: Prop), p \/ p -> p. +Proof. + firstorder. +Qed. + +Lemma l2 : forall n : nat, n el get_bound_vars conjuncts' -> n1 n. +Proof. + move => n. + simpl. + move => Hn. + apply or_false in Hn. + apply x_or_x in Hn. + constructor 2. + rewrite / Nat_single. + rewrite Hn. + done. +Qed. + +Lemma l3 : forall x : Vertex, x el get_free_vars conjuncts' -> v1v2 x. +Proof. + move => x. + simpl. + move => Hn. + apply or_false in Hn. + destruct Hn as [H1 | H2]. + + constructor 2. + rewrite / V_single. + rewrite H1. + done. + + constructor 1. + constructor 2. + rewrite / V_single. + rewrite H2. + done. +Qed. + +Lemma l4 : forall x : Vertex, (V_union (V_union V_empty (V_single v1)) (V_single v2)) x -> x el get_free_vars conjuncts'. +Proof. + simpl. + move => x Hx. + apply or_false_inv. + case Hx. + + move => x1 Hx1. + + case Hx1. + move => x0 Hx0. + done. + + move => x0 Hx0. + apply Single_equal in Hx0. + right. + exact Hx0. + + move => x0 Hx0. + apply Single_equal in Hx0. + left. + exact Hx0. +Qed. + +Definition query : CCFPQ := {| + vs := v1v2; + ns := n1; + var_evnp_l := conjuncts'; + builder := q5; + is_not_empty := l1; + all_bound_vars_exist := l2; + all_free_vars_exist := l3; + all_vertices_in_answer := l4 +|}. From bf0a7c36f4ad4990d3a310c2a3cb4168b2ad3e99 Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Wed, 10 May 2017 12:42:08 +0300 Subject: [PATCH 16/23] Fix definition of CCFPQ_result with relational semantics --- CCFPQ/CCFPQ_Result.v | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/CCFPQ/CCFPQ_Result.v b/CCFPQ/CCFPQ_Result.v index 501f688..622bed0 100644 --- a/CCFPQ/CCFPQ_Result.v +++ b/CCFPQ/CCFPQ_Result.v @@ -2,6 +2,8 @@ Require Import Definitions. Require Import Derivation. Require Import Graph. Require Import CCFPQ. +Require Import List. +Import ListNotations. Unset Implicit Arguments. Set Strict Implicit. @@ -22,6 +24,35 @@ Section CFPQ_Res. Definition getLabels VV AA xl1 xl2 (walk : D_walk VV AA xl1 xl2 VL AL) : list symbol := getLabels' AL. Definition getLength VV AA xl1 xl2 (walk : D_walk VV AA xl1 xl2 VL AL) : nat := getLength' AL. + Fixpoint grammar_has_ter (g: grammar) (tr : ter) : Prop := + match g with + | [] => False + | (R _ ph)::t => or (In (Ts tr) ph) (grammar_has_ter t tr) + end. + + Inductive Derivability_relation : grammar -> V_set -> A_set -> + Vertex -> Vertex -> symbol -> Prop := + | Empty_rule : forall (g : grammar) (V : V_set) (A : A_set) (x: Vertex) (s: symbol), + V x -> (exists (v: var), Vs v = s -> In (R v []) g) -> Derivability_relation g V A x x s + | Arc_with_ter_label : forall (g : grammar) (V : V_set) (A : A_set) (x1 x2: Vertex) (s: symbol), + V x1 -> V x2 -> (exists (t: ter), Ts t = s -> grammar_has_ter g t -> A (A_ends x1 x2 t)) -> + Derivability_relation g V A x1 x2 s + (* Given a non-terminal, check that exist list of vertices, that every symbol in right *) + (* hand side of a rule (for given non-terminal) consists in this derivability relation *) + (* with appropriate pair of vertices, i.e. symbol at i-th position should consist in *) + (* derivability relation with i-th and (i+1)-th vertices accordingly. *) + | Rule_application : forall (g : grammar) (V : V_set) (A : A_set) (x1 x2: Vertex) (s: symbol), + V x1 -> V x2 -> + (exists (v: var) (ph : phrase) (vl : V_list), + Vs v = s -> In (R v ph) g -> 1 + length vl = length ph -> + (forall (idx : nat), idx < length ph -> ( + exists (x1' x2' : Vertex) (s' : symbol), + nth_error (x1::vl ++ [x2]) idx = Some x1' -> + nth_error (x1::vl ++ [x2]) (idx + 1) = Some x2' -> + nth_error ph idx = Some s' -> + Derivability_relation g V A x1' x2' s'))) -> + Derivability_relation g V A x1 x2 s. + Record CFPQ_Relational_query_result : Type := { g_r : grammar; CFPQ_r : var_EitherVertexNat_pair; @@ -31,7 +62,8 @@ Section CFPQ_Res. ntm_r : var := fst CFPQ_r; evnp_r : EitherVertexNat_pair := snd CFPQ_r; - are_connected : exists (x1 x2 : Vertex), exists (conn : Vertex_conn V_r A_r x1 x2), True + are_in_derivability_relation : exists (x1 x2 : Vertex), + Derivability_relation g_r V_r A_r x1 x2 (Vs ntm_r) }. Record CFPQ_Single_path_query_result : Type := { From ab0533cbeb801ecc4c270f9c9eea19c68b6085fd Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Wed, 17 May 2017 16:28:14 +0300 Subject: [PATCH 17/23] Add definition of CFG in CNF --- CCFPQ/CF_Definitions.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 CCFPQ/CF_Definitions.v diff --git a/CCFPQ/CF_Definitions.v b/CCFPQ/CF_Definitions.v new file mode 100644 index 0000000..26eb250 --- /dev/null +++ b/CCFPQ/CF_Definitions.v @@ -0,0 +1,24 @@ +Require Import List. +Import ListNotations. + +(* This file contains definition of context-free grammar in Chomsky normal form. *) + +Inductive ter : Type := T : nat -> ter. +Inductive var : Type := V : nat -> var. +Inductive eps : Type := E : eps. + +Inductive Rule : Type := + | Rt : var -> ter -> Rule + | Rv : var -> var -> var -> Rule + | Re : var -> eps -> Rule. + +Definition Grammar := list Rule. + +Inductive Der_ter_list : Grammar -> var -> list ter -> Prop := + | Der_eps : forall (g : Grammar) (v : var) (e : eps), + In (Re v e) g -> Der_ter_list g v [] + | Der_ter : forall (g : Grammar) (v : var) (t : ter), + In (Rt v t) g -> Der_ter_list g v [t] + | Der_var : forall (g : Grammar) (v v1 v2 : var) (tl1 tl2 : list ter), + In (Rv v v1 v2) g -> Der_ter_list g v1 tl1 -> + Der_ter_list g v2 tl2 -> Der_ter_list g v (tl1 ++ tl2). From 095f85f7a4bedc13499e294cbaffa2cea364c3ee Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Wed, 17 May 2017 16:29:23 +0300 Subject: [PATCH 18/23] Remove paths from Graph lib --- CCFPQ/Graph.v | 69 ++++++++------------------------------------------- 1 file changed, 11 insertions(+), 58 deletions(-) diff --git a/CCFPQ/Graph.v b/CCFPQ/Graph.v index 74eba2a..9fdcc1d 100644 --- a/CCFPQ/Graph.v +++ b/CCFPQ/Graph.v @@ -1,19 +1,19 @@ +Require Import CF_Definitions. Require Import List. -Require Import Definitions. Import ListNotations. Unset Implicit Arguments. Set Strict Implicit. -(* --------------------------------------------------------------------- *) -(* GRAPS - DEFINITIONS *) -(* --------------------------------------------------------------------- *) -(* This file moslty borrowed from GrapgBasics lib by Jean Duprat, *) -(* but I've added labels(terminals from Context-free grammar definition) *) -(* on arcs. *) -(* Loation of original lib is: *) -(* http://www.lix.polytechnique.fr/coq/V8.2pl1/contribs/GraphBasics.html *) -(* --------------------------------------------------------------------- *) +(* ---------------------------------------------------------------------- *) +(* GRAPS - DEFINITIONS *) +(* ---------------------------------------------------------------------- *) +(* This file moslty borrowed from GrapgBasics lib by Jean Duprat, *) +(* but I've added labels (terminals from Context-free grammar definition) *) +(* on arcs. *) +(* Loation of original lib is: *) +(* http://www.lix.polytechnique.fr/coq/V8.2pl1/contribs/GraphBasics.html *) +(* ---------------------------------------------------------------------- *) Section Sets. Variable U : Set. @@ -79,7 +79,7 @@ Section Vertices. End Vertices. Section Arcs. - Inductive Arc : Set := A_ends : Vertex -> Vertex -> ter -> Arc. + Inductive Arc : Set := A_ends : Vertex -> Vertex -> ter -> Arc. Definition A_tail (a : Arc) : Vertex := match a with A_ends x y l => x end. Definition A_head (a : Arc) : Vertex := match a with A_ends x y l => y end. Definition A_set := U_set Arc. @@ -146,50 +146,3 @@ Section Degrees. | D_eq v' _ a' _ _ _ d' => Out_neighborhood x v' a' d' end. End Degrees. - -Section Paths. - Variable v : V_set. - Variable a : A_set. - Inductive D_walk : Vertex -> Vertex -> V_list -> A_list -> Set := - | DW_null : forall x : Vertex, v x -> D_walk x x V_nil A_nil - | DW_step : - forall (x y z : Vertex) (vl : V_list) (al : A_list) (l : ter), - D_walk y z vl al -> - a (A_ends x y l) -> - D_walk x z (y :: vl) (A_ends x y l :: al). - Definition D_closed_walk := forall (x : Vertex) (vl : V_list) (al : A_list), D_walk x x vl al. - - Inductive D_trail : Vertex -> Vertex -> V_list -> A_list -> Set := - | DT_null : forall x : Vertex, v x -> D_trail x x V_nil A_nil - | DT_step : - forall (x y z : Vertex) (vl : V_list) (al : A_list) (l : ter), - D_trail y z vl al -> - a (A_ends x y l) -> - ~ In (A_ends x y l) al -> - D_trail x z (y :: vl) (A_ends x y l :: al). - Definition D_closed_trail := forall (x : Vertex) (vl : V_list) (al : A_list), D_trail x x vl al. - - Inductive D_path : Vertex -> Vertex -> V_list -> A_list -> Set := - | DP_null : forall x : Vertex, v x -> D_path x x V_nil A_nil - | DP_step : - forall (x y z : Vertex) (vl : V_list) (al : A_list) (l : ter), - D_path y z vl al -> - a (A_ends x y l) -> - ~ In y vl -> - (In x vl -> x = z) -> - ~ In (A_ends x y l) al -> - D_path x z (y :: vl) (A_ends x y l :: al). - Definition D_cycle := forall (x : Vertex) (vl : V_list) (al : A_list), D_path x x vl al. -End Paths. - -Section Connectivity. - Variable v : V_set. - Variable a : A_set. - Inductive Vertex_conn : Vertex -> Vertex -> Set := - | VC_null : forall x : Vertex, v x -> Vertex_conn x x - | VC_step : - forall (x y z : Vertex) (l : ter), - Vertex_conn y z -> - a (A_ends x y l) -> - Vertex_conn x z. -End Connectivity. From 0010f32b48ad1a1ea249c8db6732d2e15b9911b5 Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Wed, 17 May 2017 16:32:19 +0300 Subject: [PATCH 19/23] Use CFG in CNF in definition of CCFPQ --- CCFPQ/CCFPQ.v | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/CCFPQ/CCFPQ.v b/CCFPQ/CCFPQ.v index f360e61..36d1503 100644 --- a/CCFPQ/CCFPQ.v +++ b/CCFPQ/CCFPQ.v @@ -1,5 +1,8 @@ -Require Import Definitions. +Require Import CF_Definitions. Require Import Graph. +Require Import List. +Import ListNotations. + Unset Implicit Arguments. Set Strict Implicit. @@ -31,10 +34,10 @@ Section CCFPQ. Inductive CCFPQ_Builder : V_set -> Nat_set -> list var_EitherVertexNat_pair -> Type := | Empty_query : CCFPQ_Builder V_empty Nat_empty [] - | Add_free_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) + | Add_free_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) (x : Vertex), CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder (V_union v (V_single x)) n var_evnp_l - | Add_bound_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) + | Add_bound_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) (bv : nat), CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v (Nat_union n (Nat_single bv)) var_evnp_l | Add_conj_vertex_vertex : forall v n var_evnp_l nt (x1 x2 : Vertex), @@ -99,15 +102,16 @@ Section CCFPQ. | (nt, _)::tl => nt::get_nonterminals tl end. - Fixpoint get_all_vars (G : grammar) : list var := + Fixpoint get_all_vars (G : Grammar) : list var := match G with | [] => [] - | R A u::Gr => A::(get_all_vars Gr) + | (Rv A v1 v2)::Gr => A::(get_all_vars Gr) + | x::Gr => get_all_vars Gr end. Record CCFPQ_on_grammar : Type := { ccfpq : CCFPQ; - gr : grammar; + gr : Grammar; nonterminals_in_grammar : forall (nt : var), In nt (get_nonterminals (var_evnp_l ccfpq)) -> In nt (get_all_vars gr) From 46e6efd2e0b4d1cdac63ad4dd95d9dbdbc72b67e Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Wed, 17 May 2017 16:35:29 +0300 Subject: [PATCH 20/23] Add parse tree and 3 semantics of evaluation of CCFPQ; plus theorems for them --- CCFPQ/CCFPQ_Result.v | 589 +++++++++++++++++++++++++++++++++++-------- 1 file changed, 489 insertions(+), 100 deletions(-) diff --git a/CCFPQ/CCFPQ_Result.v b/CCFPQ/CCFPQ_Result.v index 622bed0..3a9cb17 100644 --- a/CCFPQ/CCFPQ_Result.v +++ b/CCFPQ/CCFPQ_Result.v @@ -1,5 +1,6 @@ -Require Import Definitions. -Require Import Derivation. +From mathcomp.ssreflect Require Import ssreflect ssrbool ssrnat eqtype ssrfun. + +Require Import CF_Definitions. Require Import Graph. Require Import CCFPQ. Require Import List. @@ -8,105 +9,493 @@ Import ListNotations. Unset Implicit Arguments. Set Strict Implicit. -Section CFPQ_Res. - Fixpoint getLabels' (arcs : A_list) : list symbol := match arcs with +(* The main goal is to show that 3 sematics of CCFPQ evaluation can be *) +(* derived from parse tree of a graph. *) + +Inductive Parse_tree : Grammar -> V_set -> A_set -> Vertex -> + Vertex -> var -> Prop := + | Leaf : forall (g : Grammar) (V : V_set) (A : A_set) (x1 x2 : Vertex) + (v : var) (t : ter), + V x1 -> V x2 -> In (Rt v t) g -> A (A_ends x1 x2 t) -> + Parse_tree g V A x1 x2 v + | Empty_leaf : forall (g : Grammar) (V : V_set) (A : A_set) (x : Vertex) + (v : var) (e : eps), + V x -> In (Re v e) g -> Parse_tree g V A x x v + | Node : forall (g : Grammar) (V : V_set) (A : A_set) (x1 x2 x3 : Vertex) + (v v1 v2 : var), + V x1 -> V x2 -> V x3 -> In (Rv v v1 v2) g -> + Parse_tree g V A x1 x2 v1 -> Parse_tree g V A x2 x3 v2 -> + Parse_tree g V A x1 x3 v. + +(* First semantic is relation. *) + +Inductive Derivability_relation : Grammar -> V_set -> A_set -> + Vertex -> Vertex -> var -> Prop := + | Empty_rule : forall (g : Grammar) (V : V_set) (A : A_set) (x: Vertex) + (v: var) (e: eps), + V x -> In (Re v e) g -> Derivability_relation g V A x x v + | Arc_with_ter_label : forall (g : Grammar) (V : V_set) (A : A_set) + (x1 x2 : Vertex) (v : var) (t : ter), + V x1 -> V x2 -> In (Rt v t) g -> A (A_ends x1 x2 t) -> + Derivability_relation g V A x1 x2 v + | Rule_application : forall (g : Grammar) (V : V_set) (A : A_set) + (x1 x2: Vertex) (v v1 v2 : var), + (exists (x' : Vertex), V x1 -> V x2 -> V x' -> In (Rv v v1 v2) g -> + Derivability_relation g V A x1 x' v1 /\ + Derivability_relation g V A x' x2 v2) -> + Derivability_relation g V A x1 x2 v. + +Theorem Parse_tree_to_relation : forall (g : Grammar) (V : V_set) (A : A_set) + (x1 x2 : Vertex) (v : var), + Parse_tree g V A x1 x2 v -> Derivability_relation g V A x1 x2 v. +Proof. + move => _g _V _A _x1 _x2 _v pt. + induction pt. + + + apply: Arc_with_ter_label. + done. + done. + exact: H1. + done. + + + apply: Empty_rule. + done. + done. + + + apply: Rule_application. + exists x2. + move => vx1 vx3 vx2 hasRule. + split. + exact: IHpt1. + exact: IHpt2. +Qed. + +(* Second semantic is single path. *) + +Fixpoint get_labels (arcs : list Arc) : list ter := match arcs with + | [] => [] + | (A_ends _ _ l)::t => l::(get_labels t) +end. + +Inductive D_walk : Vertex -> Vertex -> list Vertex -> list Arc -> Prop := + | DW_null : forall (x : Vertex), D_walk x x V_nil A_nil + | DW_step : forall (x y z : Vertex) + (vl : list Vertex) (al : list Arc) (l : ter), + D_walk y z vl al -> D_walk x z (y :: vl) (A_ends x y l :: al). + +Lemma D_walk_append: + forall (x y z : Vertex) (vl1 vl2 : list Vertex) (al1 al2 : list Arc), + D_walk x y vl1 al1 -> D_walk y z vl2 al2 -> + D_walk x z (vl1 ++ vl2) (al1 ++ al2). +Proof. + intros x y z vl vl' el el' Hw; elim Hw; simpl in |- *; intros. + trivial. + apply DW_step; auto. +Qed. + +Definition get_labels_from_walk x1 x2 vl al (walk : D_walk x1 x2 vl al) + : list ter := get_labels al. + +Inductive Single_path_semantics : forall (g : Grammar) (V : V_set) (A : A_set) + (v : var) (x1 x2 : Vertex) (vl : list Vertex) (al : list Arc), + D_walk x1 x2 vl al -> Prop := + | Empty_path : forall (g : Grammar) (V : V_set) (A : A_set) (x : Vertex) + (v : var) (e : eps), + V x -> In (Re v e) g -> + Single_path_semantics g V A v x x V_nil A_nil (DW_null x) + | One_arc_path : forall (g : Grammar) (V : V_set) (A : A_set) + (x1 x2 : Vertex) (v : var) (t : ter), + V x1 -> V x2 -> In (Rt v t) g -> A (A_ends x1 x2 t) -> + Single_path_semantics g V A v x1 x2 [x2] [A_ends x1 x2 t] + (DW_step x1 x2 x2 V_nil A_nil t (DW_null x2)) + | Combine_path : forall (g : Grammar) (V : V_set) (A : A_set) + (x1 x2 x3 : Vertex) (v v1 v2 : var) + (al1 al2 : list Arc) (vl1 vl2 : list Vertex) + (dw1 : D_walk x1 x2 vl1 al1) (dw2 : D_walk x2 x3 vl2 al2), + V x1 -> V x2 -> V x3 -> In (Rv v v1 v2) g -> + Single_path_semantics g V A v1 x1 x2 vl1 al1 dw1 -> + Single_path_semantics g V A v2 x2 x3 vl2 al2 dw2 -> + Single_path_semantics g V A v x1 x3 (vl1 ++ vl2) (al1 ++ al2) + (D_walk_append x1 x2 x3 vl1 vl2 al1 al2 dw1 dw2). + +Lemma get_labels_is_linear : forall (al1 al2 : list Arc), + get_labels (al1 ++ al2) = get_labels al1 ++ get_labels al2. +Proof. + move => al1 al2. + induction al1. + + + simpl. + done. + + + simpl. + case (a). + move => v1 v2 t. + rewrite IHal1. + done. +Qed. + +Theorem Derives_single_path : forall (g : Grammar) (V : V_set) (A : A_set) + (v : var) (x1 x2 : Vertex) (vl : list Vertex) (al : list Arc) + (dw : D_walk x1 x2 vl al) + (p : Single_path_semantics g V A v x1 x2 vl al dw), + Der_ter_list g v (get_labels_from_walk x1 x2 vl al dw). +Proof. + move => g V A v x1 x2 vla la dw sps. + induction sps. + + + rewrite / get_labels_from_walk. + simpl. + apply: Der_eps. + done. + + + rewrite / get_labels_from_walk. + simpl. + apply: Der_ter. + done. + + + rewrite / get_labels_from_walk. + rewrite get_labels_is_linear. + apply: Der_var. + exact H2. + done. + done. +Qed. + +Theorem Parse_tree_to_single_path : forall (g : Grammar) (V : V_set) + (A : A_set) (x1 x2 : Vertex) (v : var), + Parse_tree g V A x1 x2 v -> + exists (vl : list Vertex) (al : list Arc) (dw : D_walk x1 x2 vl al), + Single_path_semantics g V A v x1 x2 vl al dw. +Proof. + move => g V A x1 x2 v pt. + induction pt. + + + exists [x2], + [A_ends x1 x2 t], + (DW_step x1 x2 x2 V_nil A_nil t (DW_null x2)). + apply One_arc_path. + done. + done. + done. + done. + + + exists [], + [], + (DW_null x). + apply: Empty_path. + done. + done. + + + destruct IHpt1 as [vl1 [al1 [dw1 IHpt1]]]. + destruct IHpt2 as [vl2 [al2 [dw2 IHpt2]]]. + exists (vl1 ++ vl2), + (al1 ++ al2), + (D_walk_append x1 x2 x3 vl1 vl2 al1 al2 dw1 dw2). + apply: Combine_path. + done. + done. + done. + exact H2. + done. + done. +Qed. + +(* Third semantic is all paths. *) + +Fixpoint get_pairs (al : list Arc) (all : list (list Arc)) : list (list Arc) := + match all with + | [] => [] + | l::t => (al ++ l)::(get_pairs al t) + end. + +Fixpoint get_all_pairs (all1 all2 : list (list Arc)) : list (list Arc) := + match all1 with | [] => [] - | (A_ends _ _ l)::t => (Ts l)::(getLabels' t) + | l::t => (get_pairs l all2) ++ (get_all_pairs t all2) end. - Fixpoint getLength' (arcs : A_list) : nat := match arcs with - | [] => 0 - | arc::t => 1 + (getLength' t) - end. +Inductive All_path_semantics : forall (g : Grammar) (V : V_set) (A : A_set) + (v : var) (x1 x2 : Vertex) (all : list (list Arc)), Prop := + | Empty_paths : forall (g : Grammar) (V : V_set) (A : A_set) (x : Vertex) + (v : var) (e : eps), + V x -> In (Re v e) g -> All_path_semantics g V A v x x [[]] + | One_arc_paths : forall (g : Grammar) (V : V_set) (A : A_set) + (x1 x2 : Vertex) (v : var) (t : ter), + V x1 -> V x2 -> In (Rt v t) g -> A (A_ends x1 x2 t) -> + All_path_semantics g V A v x1 x2 [[A_ends x1 x2 t]] + | Combine_paths : forall (g : Grammar) (V : V_set) (A : A_set) + (x1 x2 x3 : Vertex) (v v1 v2 : var) + (all1 all2 : list (list Arc)), + V x1 -> V x2 -> V x3 -> In (Rv v v1 v2) g -> + All_path_semantics g V A v1 x1 x2 all1 -> + All_path_semantics g V A v2 x2 x3 all2 -> + All_path_semantics g V A v x1 x3 (get_all_pairs all1 all2). + +Theorem Parse_tree_to_all_path : forall (g : Grammar) (V : V_set) + (A : A_set) (x1 x2 : Vertex) (v : var), + Parse_tree g V A x1 x2 v -> + exists (all : list (list Arc)), All_path_semantics g V A v x1 x2 all. +Proof. + move => g V A x1 x2 v pt. + induction pt. + + + exists [[A_ends x1 x2 t]]. + apply One_arc_paths. + done. + done. + done. + done. + + + exists [[]]. + eapply Empty_paths. + done. + exact H0. + + + destruct IHpt1 as [all1 aps1]. + destruct IHpt2 as [all2 aps2]. + exists (get_all_pairs all1 all2). + eapply Combine_paths. + done. + exact H0. + done. + exact H2. + done. + done. +Qed. + +Lemma app_is_associative_inside_in : + forall (x : list Arc) (a b c : list (list Arc)), + In x (a ++ b ++ c) -> In x ((a ++ b) ++ c). +Proof. + move => x a b c. + remember (a ++ b ++ c) as abc. + rewrite app_assoc in Heqabc. + rewrite Heqabc. + done. +Qed. + +Lemma app_is_associative_inside_in' : + forall (x : list Arc) (a b c : list (list Arc)), + In x ((a ++ b) ++ c) -> In x (a ++ b ++ c). +Proof. + move => x a b c. + remember (a ++ b ++ c) as abc. + rewrite app_assoc in Heqabc. + rewrite Heqabc. + done. +Qed. + +Lemma app_nil_inside_in : forall (x : list Arc) (a b c : list (list Arc)), + In x (a ++ b ++ c) -> In x (a ++ b ++ c ++ []). +Proof. + move => x a b c. + remember (a ++ b ++ c ++ []) as abcn. + rewrite app_nil_r in Heqabcn. + rewrite Heqabcn. + done. +Qed. + +Lemma in_cons_disj : forall (l a : list Arc) (ll : list (list Arc)), + In l ll \/ a = l -> In l (a :: ll). +Proof. + move => l a ll stm. + destruct stm as [l_in_ll | a_is_l]. + simpl. + right. + done. + simpl. + left. + done. +Qed. + +Lemma in_app_cons_disj : forall (x b0 : list Arc) (a b : list (list Arc)), + In x (a ++ b) \/ In x (a ++ [b0]) -> In x (a ++ b0 :: b). +Proof. + move => x b0 a. + induction a. + + + move => b. + simpl. + firstorder. + + + move => b stm. + destruct stm as [x_in_aa0'b | x_im aa0'b0]. + firstorder. + firstorder. +Qed. + +Lemma app_is_commutative_inside_in2 : + forall (x : list Arc) (a b : list (list Arc)), + In x (a ++ b) -> In x (b ++ a). +Proof. + move => x a. + induction a. + + + move => b. + simpl. + move => x_in_b. + remember (b ++ []) as bn. + rewrite app_nil_r in Heqbn. + rewrite Heqbn. + done. + + + move => b x_in. + simpl in x_in. + destruct x_in as [x_is_a | x_in_a0b]. + apply in_or_app. + right. + apply in_cons_disj. + right. + done. + apply IHa in x_in_a0b. + apply in_app_cons_disj. + left. + done. +Qed. + +Lemma app_is_commutative_inside_in3 : + forall (x : list Arc) (a b c : list (list Arc)), + In x (a ++ b ++ c) -> In x (b ++ c ++ a). +Proof. + move => x a b c x_in_abc. + apply app_is_commutative_inside_in2 in x_in_abc. + apply app_is_associative_inside_in' in x_in_abc. + done. +Qed. + +Lemma get_all_pairs_cons : forall (l x : list Arc) (ll1 ll2 : list (list Arc)), + In x (get_all_pairs (l::ll1) ll2) -> + In x (get_all_pairs ll1 ll2) \/ In x (get_all_pairs [l] ll2). +Proof. + move => l x ll1. + induction ll1. + + + move => ll2 conc. + simpl. + right. + done. + + + move => ll2 conc. + simpl. + simpl in conc. + apply in_app_or. + apply app_is_associative_inside_in. + apply app_nil_inside_in. + apply app_is_commutative_inside_in3. + done. +Qed. + +Lemma get_all_pairs_single : forall (a x : list Arc) (ll : list (list Arc)), + In x (get_all_pairs [a] ll) -> + (exists (b : list Arc), In b ll /\ (x = (a ++ b))). +Proof. + move => a x ll. + induction ll. + + + move => stm. + simpl in stm. + done. + + + move => stm. + simpl in stm. + destruct stm as [x_is_sum | x_in_concat]. + exists a0. + split. + apply in_cons_disj. + right. + done. + done. + simpl in IHll. + apply IHll in x_in_concat. + destruct x_in_concat as [b bstm]. + destruct bstm as [b_in_ll x_is_sum]. + exists b. + split. + apply in_cons_disj. + left. + done. + done. +Qed. + +Lemma exists_in_get_all_pairs : + forall (l : list Arc) (ll1 ll2 : list (list Arc)), + In l (get_all_pairs ll1 ll2) -> + (exists (l1 l2 : list Arc), In l1 ll1 /\ In l2 ll2 /\ l = (l1 ++ l2)). +Proof. + move => l ll1. + induction ll1. + + + move => ll2 conc_in_pairs. + simpl in conc_in_pairs. + done. + + + move => ll2 conc_in_pairs. + apply get_all_pairs_cons in conc_in_pairs. + destruct conc_in_pairs as [in1 | in2]. + apply IHll1 in in1. + destruct in1 as [l1 [l2 stm]]. + destruct stm as [l1_in [l2_in l_is_sum]]. + exists l1. + exists l2. + split. + apply in_cons_disj. + left. + done. + split. + done. + done. + apply get_all_pairs_single in in2. + destruct in2 as [l' stm]. + destruct stm as [l'_in l_is_sum]. + exists a. + exists l'. + split. + apply in_cons_disj. + right. + done. + split. + done. + done. +Qed. + +Theorem derives_all_path : forall (g : Grammar) (V : V_set) (A : A_set) + (v : var) (x1 x2 : Vertex) (all : list (list Arc)) + (aps : All_path_semantics g V A v x1 x2 all), + forall (al : list Arc), In al all -> Der_ter_list g v (get_labels al). +Proof. + move => g V A v x1 x2 all aps. + induction aps. + + + move => conc contains. + case contains. + move => empty. + rewrite <- empty. + simpl. + apply: Der_eps. + done. + rewrite / In. + done. + + + move => conc contains. + case contains. + move => al_is. + rewrite <- al_is. + simpl. + apply: Der_ter. + done. + rewrite / In. + done. - Variable VL : V_list. - Variable AL : A_list. - Definition getLabels VV AA xl1 xl2 (walk : D_walk VV AA xl1 xl2 VL AL) : list symbol := getLabels' AL. - Definition getLength VV AA xl1 xl2 (walk : D_walk VV AA xl1 xl2 VL AL) : nat := getLength' AL. - - Fixpoint grammar_has_ter (g: grammar) (tr : ter) : Prop := - match g with - | [] => False - | (R _ ph)::t => or (In (Ts tr) ph) (grammar_has_ter t tr) - end. - - Inductive Derivability_relation : grammar -> V_set -> A_set -> - Vertex -> Vertex -> symbol -> Prop := - | Empty_rule : forall (g : grammar) (V : V_set) (A : A_set) (x: Vertex) (s: symbol), - V x -> (exists (v: var), Vs v = s -> In (R v []) g) -> Derivability_relation g V A x x s - | Arc_with_ter_label : forall (g : grammar) (V : V_set) (A : A_set) (x1 x2: Vertex) (s: symbol), - V x1 -> V x2 -> (exists (t: ter), Ts t = s -> grammar_has_ter g t -> A (A_ends x1 x2 t)) -> - Derivability_relation g V A x1 x2 s - (* Given a non-terminal, check that exist list of vertices, that every symbol in right *) - (* hand side of a rule (for given non-terminal) consists in this derivability relation *) - (* with appropriate pair of vertices, i.e. symbol at i-th position should consist in *) - (* derivability relation with i-th and (i+1)-th vertices accordingly. *) - | Rule_application : forall (g : grammar) (V : V_set) (A : A_set) (x1 x2: Vertex) (s: symbol), - V x1 -> V x2 -> - (exists (v: var) (ph : phrase) (vl : V_list), - Vs v = s -> In (R v ph) g -> 1 + length vl = length ph -> - (forall (idx : nat), idx < length ph -> ( - exists (x1' x2' : Vertex) (s' : symbol), - nth_error (x1::vl ++ [x2]) idx = Some x1' -> - nth_error (x1::vl ++ [x2]) (idx + 1) = Some x2' -> - nth_error ph idx = Some s' -> - Derivability_relation g V A x1' x2' s'))) -> - Derivability_relation g V A x1 x2 s. - - Record CFPQ_Relational_query_result : Type := { - g_r : grammar; - CFPQ_r : var_EitherVertexNat_pair; - V_r : V_set; - A_r : A_set; - Graph_r : Digraph V_r A_r; - - ntm_r : var := fst CFPQ_r; - evnp_r : EitherVertexNat_pair := snd CFPQ_r; - are_in_derivability_relation : exists (x1 x2 : Vertex), - Derivability_relation g_r V_r A_r x1 x2 (Vs ntm_r) - }. - - Record CFPQ_Single_path_query_result : Type := { - g : grammar; - CFPQ : var_EitherVertexNat_pair; - V : V_set; - A : A_set; - Graph : Digraph V A; - - ntm : var := fst CFPQ; - evnp : EitherVertexNat_pair := snd CFPQ; - has_path : exists (x1 x2 : Vertex), exists (walk : D_walk V A x1 x2 _ _), - der g ntm (getLabels V A x1 x2 walk) - }. - - Record CFPQ_Single_shortest_path_query_result : Type := { - g_s : grammar; - CFPQ_s : var_EitherVertexNat_pair; - V_s : V_set; - A_s : A_set; - Graph' : Digraph V_s A_s; - - ntm_s : var := fst CFPQ_s; - evnp_s : EitherVertexNat_pair := snd CFPQ_s; - has_shortest_path : exists (x1 x2 : Vertex), exists (walk : D_walk V_s A_s x1 x2 _ _), - der g_s ntm_s (getLabels V_s A_s x1 x2 walk) -> - forall (other_walk : D_walk V_s A_s x1 x2 _ _), - getLength V_s A_s x1 x2 other_walk >= getLength V_s A_s x1 x2 walk - }. - - Record CFPQ_All_path_query_result : Type := { - g_a : grammar; - CFPQ_a : var_EitherVertexNat_pair; - V_a : V_set; - A_a : A_set; - Graph_a : Digraph V_a A_a; - - ntm_a : var := fst CFPQ_a; - evnp_a : EitherVertexNat_pair := snd CFPQ_a; - all_paths : exists (all_pairs : list (prod Vertex Vertex)), - forall (pair_of_vertices : (prod Vertex Vertex)), - In pair_of_vertices all_pairs <-> - exists (walk : D_walk V_a A_a (fst pair_of_vertices) (snd pair_of_vertices) _ _), - der g_a ntm_a (getLabels V_a A_a (fst pair_of_vertices) (snd pair_of_vertices) walk) - }. -End CFPQ_Res. + + move => conc contains. + apply exists_in_get_all_pairs in contains. + destruct contains as [l1 [l2 contains]]. + destruct contains as [l1_in_all1 [l2_in_all2 contains]]. + rewrite contains. + rewrite get_labels_is_linear. + apply: Der_var. + exact H2. + apply IHaps1. + done. + apply IHaps2. + done. +Qed. From 969e9a2496814f5ee89b0c946acabe648107126b Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Sat, 20 May 2017 19:16:18 +0300 Subject: [PATCH 21/23] Update examples according new defenitions --- CCFPQ/Examples/CCFPQ_Examples.v | 9 +-- CCFPQ/Examples/CFG_examples.v | 120 ++++++++++++++++---------------- CCFPQ/Examples/Graph_examples.v | 36 ++-------- 3 files changed, 68 insertions(+), 97 deletions(-) diff --git a/CCFPQ/Examples/CCFPQ_Examples.v b/CCFPQ/Examples/CCFPQ_Examples.v index 5794fb2..67b82e5 100644 --- a/CCFPQ/Examples/CCFPQ_Examples.v +++ b/CCFPQ/Examples/CCFPQ_Examples.v @@ -1,5 +1,5 @@ From mathcomp.ssreflect Require Import ssreflect ssrbool ssrnat eqtype ssrfun. -Require Import Definitions. +Require Import CF_Definitions. Require Import CCFPQ. Require Import Graph. Require Import List. @@ -59,7 +59,7 @@ Proof. firstorder. Qed. -Lemma l2 : forall n : nat, n el get_bound_vars conjuncts' -> n1 n. +Lemma l2 : forall n : nat, In n (get_bound_vars conjuncts') -> n1 n. Proof. move => n. simpl. @@ -72,7 +72,7 @@ Proof. done. Qed. -Lemma l3 : forall x : Vertex, x el get_free_vars conjuncts' -> v1v2 x. +Lemma l3 : forall x : Vertex, In x (get_free_vars conjuncts') -> v1v2 x. Proof. move => x. simpl. @@ -92,7 +92,8 @@ Proof. done. Qed. -Lemma l4 : forall x : Vertex, (V_union (V_union V_empty (V_single v1)) (V_single v2)) x -> x el get_free_vars conjuncts'. +Lemma l4 : forall (x : Vertex), (V_union (V_union V_empty (V_single v1)) (V_single v2)) x -> + In x (get_free_vars conjuncts'). Proof. simpl. move => x Hx. diff --git a/CCFPQ/Examples/CFG_examples.v b/CCFPQ/Examples/CFG_examples.v index 8d73a5e..293b12c 100644 --- a/CCFPQ/Examples/CFG_examples.v +++ b/CCFPQ/Examples/CFG_examples.v @@ -1,85 +1,83 @@ -From mathcomp.ssreflect Require Import ssreflect ssrbool ssrnat eqtype ssrfun. -Require Import Definitions. -Require Import Derivation. +Require Import CF_Definitions. Require Import List. Import ListNotations. -(* This file contains sample definitions of cf grammars. *) -(* In this sample we define grammar for well-formed *) -(* parentheses with 2 types of brackets. *) +(* This file contains sample definition of cf grammar. *) +(* Let's define grammar for well-formed parentheses. *) (* Define terminals at first. *) -Definition t1 : ter := T 1. -Definition t2 := T 2. -Definition t3 := T 3. -Definition t4 := T 4. +Definition tOp : ter := T 1. +Definition tCl := T 2. (* Now define non-terminals. *) -Definition v1 : var := V 1. +Definition vS : var := V 0. +Definition vA : var := V 1. +Definition vB : var := V 2. +Definition vD : var := V 3. -Definition st1 : symbol := Ts t1. -Definition st2 := Ts t2. -Definition st3 := Ts t3. -Definition st4 := Ts t4. -Definition sv1 := Vs v1. - -Definition phrase1 : phrase := [sv1 ; sv1]. -Definition phrase2 := [st1 ; st2]. -Definition phrase3 := [st1 ; sv1 ; st2]. -Definition phrase4 := [st3 ; st4]. -Definition phrase5 := [st3 ; sv1 ; st4]. - -Definition rule1 : rule := R v1 phrase1. -Definition rule2 := R v1 phrase2. -Definition rule3 := R v1 phrase3. -Definition rule4 := R v1 phrase4. -Definition rule5 := R v1 phrase5. +(* And now define rules. *) +Definition rule1 : Rule := Rv vS vS vS. +Definition rule2 := Rv vS vB vA. +Definition rule3 := Rv vS vB vD. +Definition rule4 := Rv vA vS vD. +Definition rule5 := Rt vB tOp. +Definition rule6 := Rt vD tCl. (* Define grammar. *) -Definition grammar := [rule1 ; rule2 ; rule3 ; rule4 ; rule5]. +Definition grammar := [rule1 ; rule2 ; rule3 ; rule4 ; rule5 ; rule6]. Eval compute in grammar. -(* Example of derivation. *) +(* Examples of derivations. *) +Lemma spl1 : forall (t1 : ter) (tl : list ter), t1::tl = [t1] ++ tl. +Proof. + tauto. +Qed. + +Lemma spl2 : forall (t1 t2 : ter) (tl : list ter), t1::t2::tl = [t1 ; t2] ++ tl. +Proof. + tauto. +Qed. -(* Derives "()" *) -Lemma derives1 : der grammar v1 [st1 ; st2]. +Lemma spl4 : forall (t1 t2 t3 t4 : ter) (tl : list ter), + t1::t2::t3::t4::tl = [t1 ; t2 ; t3 ; t4] ++ tl. Proof. - constructor. - constructor 2. - constructor. - done. + tauto. Qed. -(* Derives "[]" *) -Lemma derives2 : der grammar v1 [st3 ; st4]. +(* Derives "()" *) +Lemma derives1 : Der_ter_list grammar vS [tOp ; tCl]. Proof. - constructor. - constructor 2. - constructor 2. - constructor 2. - constructor. - rewrite / rule4. - rewrite / phrase4. - done. + rewrite spl1. + eapply Der_var. + + compute. + right. right. left. tauto. + + apply Der_ter. compute. firstorder. + + apply Der_ter. compute. firstorder. Qed. -(* Derives "(S)" *) -Lemma derives3 : der grammar v1 [st1 ; sv1 ; st2]. +(* Derives "(())" *) +Lemma derives2 : Der_ter_list grammar vS [tOp ; tOp ; tCl ; tCl]. Proof. - constructor. - constructor 2. - constructor 2. - constructor. - rewrite / rule3. - rewrite / phrase3. - done. + rewrite spl1. + eapply Der_var. + + compute. + right. left. tauto. + + apply Der_ter. compute. firstorder. + + rewrite spl2. + eapply Der_var. + compute. + right. right. right. left. tauto. + - apply derives1. + - apply Der_ter. compute. firstorder. Qed. -(* Derives "([])" *) -Lemma derives' : der grammar v1 ([st1] ++ [st3; st4] ++ [st2]). +(* Derives "(())()" *) +Lemma derives3 : Der_ter_list grammar vS [tOp ; tOp ; tCl ; tCl ; tOp ; tCl]. Proof. - move: derives2. - apply: replN. - move: derives3. - done. + rewrite spl4. + eapply Der_var. + + compute. + left. tauto. + + apply derives2. + + apply derives1. Qed. diff --git a/CCFPQ/Examples/Graph_examples.v b/CCFPQ/Examples/Graph_examples.v index f08dada..2d9a951 100644 --- a/CCFPQ/Examples/Graph_examples.v +++ b/CCFPQ/Examples/Graph_examples.v @@ -1,6 +1,9 @@ From mathcomp.ssreflect Require Import ssreflect ssrbool ssrnat eqtype ssrfun. Require Import Graph. -Require Import Definitions. +Require Import CF_Definitions. +Require Import CCFPQ_Result. +Require Import List. +Import ListNotations. (* This file contains sample definitions of graphs and paths. *) @@ -129,34 +132,3 @@ Definition g123v12arcs := (A_union (A_single (A_ends vertex1 vertex2 label12)) A (* Check funcions again. *) Eval compute in DV_list g123v g123v12arcs g123v12a. Eval compute in DA_list g123v g123v12arcs g123v12a. - -(* Define a paths in our graph. *) -Definition ep := DP_null g123v g123v12arcs vertex2 v2_in_g123v. - -Lemma arc_in_arcs : g123v12arcs (A_ends vertex1 vertex2 label12). -Proof. - constructor. - done. -Qed. - -Lemma not_in_nil_V : ~ In vertex2 V_nil. -Proof. - rewrite / V_nil. - done. -Qed. - -Lemma not_in_nil_A : ~ In (A_ends vertex1 vertex2 label12) A_nil. -Proof. - rewrite / A_nil. - done. -Qed. - -Lemma v1_eq_v2 : In vertex1 V_nil -> vertex1 = vertex2. -Proof. - move => H. - done. -Qed. - -Definition p12 := DP_step g123v g123v12arcs vertex1 vertex2 vertex2 V_nil A_nil label12 - ep arc_in_arcs not_in_nil_V v1_eq_v2 not_in_nil_A. -Check p12. From 3fcc0871ba5caf0a200858068f8795b7a4624b89 Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Mon, 22 May 2017 12:01:51 +0300 Subject: [PATCH 22/23] Make names more understandable --- CCFPQ/CCFPQ.v | 28 +++++++++---------- CCFPQ/CCFPQ_Result.v | 64 ++++++++++++++++++-------------------------- CCFPQ/Graph.v | 24 ++++++++--------- 3 files changed, 52 insertions(+), 64 deletions(-) diff --git a/CCFPQ/CCFPQ.v b/CCFPQ/CCFPQ.v index 36d1503..8891bb8 100644 --- a/CCFPQ/CCFPQ.v +++ b/CCFPQ/CCFPQ.v @@ -23,31 +23,31 @@ Section CCFPQ. Definition vertex_placeholder : Vertex := idx 0. Definition nat_placeholder : nat := 0. - Definition getv (x : Vertex) : EitherVertexNat := pair (pair x nat_placeholder) true. - Definition getn (n : nat) : EitherVertexNat := pair (pair vertex_placeholder n) false. + Definition get_vertex (x : Vertex) : EitherVertexNat := pair (pair x nat_placeholder) true. + Definition get_var (n : nat) : EitherVertexNat := pair (pair vertex_placeholder n) false. (* Construct conjunct of type var_EitherVertexNat_pair from 2 single variables and non-terminal *) - Fixpoint constr_nt_VV (n : var) (a b : Vertex) := pair n (pair (getv a) (getv b)). - Fixpoint constr_nt_VN (n : var) (a : Vertex) (b: nat) := pair n (pair (getv a) (getn b)). - Fixpoint constr_nt_NV (n : var) (a : nat) (b: Vertex) := pair n (pair (getn a) (getv b)). - Fixpoint constr_nt_NN (n : var) (a b : nat) := pair n (pair (getn a) (getn b)). + Fixpoint construct_var_vertex_vertex (n : var) (a b : Vertex) := pair n (pair (get_vertex a) (get_vertex b)). + Fixpoint construct_var_vertex_var (n : var) (a : Vertex) (b: nat) := pair n (pair (get_vertex a) (get_var b)). + Fixpoint construct_var_var_vertex (n : var) (a : nat) (b: Vertex) := pair n (pair (get_var a) (get_vertex b)). + Fixpoint construct_var_var_var (n : var) (a b : nat) := pair n (pair (get_var a) (get_var b)). - Inductive CCFPQ_Builder : V_set -> Nat_set -> list var_EitherVertexNat_pair -> Type := + Inductive CCFPQ_Builder : Vertex_set -> Nat_set -> list var_EitherVertexNat_pair -> Type := | Empty_query : CCFPQ_Builder V_empty Nat_empty [] - | Add_free_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) + | Add_free_var : forall (v : Vertex_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) (x : Vertex), CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder (V_union v (V_single x)) n var_evnp_l - | Add_bound_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) + | Add_bound_var : forall (v : Vertex_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) (bv : nat), CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v (Nat_union n (Nat_single bv)) var_evnp_l | Add_conj_vertex_vertex : forall v n var_evnp_l nt (x1 x2 : Vertex), - CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((constr_nt_VV nt x1 x2)::var_evnp_l) + CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((construct_var_vertex_vertex nt x1 x2)::var_evnp_l) | Add_conj_vertex_nat : forall v n var_evnp_l nt (x: Vertex) (bv : nat), - CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((constr_nt_VN nt x bv)::var_evnp_l) + CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((construct_var_vertex_var nt x bv)::var_evnp_l) | Add_conj_nat_vertex : forall v n var_evnp_l nt (bv : nat) (x : Vertex), - CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((constr_nt_NV nt bv x)::var_evnp_l) + CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((construct_var_var_vertex nt bv x)::var_evnp_l) | Add_conj_nat_nat : forall v n var_evnp_l nt (bv1 bv2: nat), - CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((constr_nt_NN nt bv1 bv2)::var_evnp_l). + CCFPQ_Builder v n var_evnp_l -> CCFPQ_Builder v n ((construct_var_var_var nt bv1 bv2)::var_evnp_l). Definition is_empty vs ns var_evnp_l (builder : CCFPQ_Builder vs ns var_evnp_l) := match builder with @@ -84,7 +84,7 @@ Section CCFPQ. end. Record CCFPQ : Type := { - vs : V_set; + vs : Vertex_set; ns : Nat_set; var_evnp_l : list var_EitherVertexNat_pair; builder : CCFPQ_Builder vs ns var_evnp_l; diff --git a/CCFPQ/CCFPQ_Result.v b/CCFPQ/CCFPQ_Result.v index 3a9cb17..ffb12e0 100644 --- a/CCFPQ/CCFPQ_Result.v +++ b/CCFPQ/CCFPQ_Result.v @@ -12,16 +12,16 @@ Set Strict Implicit. (* The main goal is to show that 3 sematics of CCFPQ evaluation can be *) (* derived from parse tree of a graph. *) -Inductive Parse_tree : Grammar -> V_set -> A_set -> Vertex -> +Inductive Parse_tree : Grammar -> Vertex_set -> Arc_set -> Vertex -> Vertex -> var -> Prop := - | Leaf : forall (g : Grammar) (V : V_set) (A : A_set) (x1 x2 : Vertex) + | Leaf : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x1 x2 : Vertex) (v : var) (t : ter), V x1 -> V x2 -> In (Rt v t) g -> A (A_ends x1 x2 t) -> Parse_tree g V A x1 x2 v - | Empty_leaf : forall (g : Grammar) (V : V_set) (A : A_set) (x : Vertex) + | Empty_leaf : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x : Vertex) (v : var) (e : eps), V x -> In (Re v e) g -> Parse_tree g V A x x v - | Node : forall (g : Grammar) (V : V_set) (A : A_set) (x1 x2 x3 : Vertex) + | Node : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x1 x2 x3 : Vertex) (v v1 v2 : var), V x1 -> V x2 -> V x3 -> In (Rv v v1 v2) g -> Parse_tree g V A x1 x2 v1 -> Parse_tree g V A x2 x3 v2 -> @@ -29,23 +29,23 @@ Inductive Parse_tree : Grammar -> V_set -> A_set -> Vertex -> (* First semantic is relation. *) -Inductive Derivability_relation : Grammar -> V_set -> A_set -> +Inductive Derivability_relation : Grammar -> Vertex_set -> Arc_set -> Vertex -> Vertex -> var -> Prop := - | Empty_rule : forall (g : Grammar) (V : V_set) (A : A_set) (x: Vertex) + | Empty_rule : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x: Vertex) (v: var) (e: eps), V x -> In (Re v e) g -> Derivability_relation g V A x x v - | Arc_with_ter_label : forall (g : Grammar) (V : V_set) (A : A_set) + | Arc_with_ter_label : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x1 x2 : Vertex) (v : var) (t : ter), V x1 -> V x2 -> In (Rt v t) g -> A (A_ends x1 x2 t) -> Derivability_relation g V A x1 x2 v - | Rule_application : forall (g : Grammar) (V : V_set) (A : A_set) + | Rule_application : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x1 x2: Vertex) (v v1 v2 : var), (exists (x' : Vertex), V x1 -> V x2 -> V x' -> In (Rv v v1 v2) g -> Derivability_relation g V A x1 x' v1 /\ Derivability_relation g V A x' x2 v2) -> Derivability_relation g V A x1 x2 v. -Theorem Parse_tree_to_relation : forall (g : Grammar) (V : V_set) (A : A_set) +Theorem Parse_tree_to_relation : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x1 x2 : Vertex) (v : var), Parse_tree g V A x1 x2 v -> Derivability_relation g V A x1 x2 v. Proof. @@ -96,19 +96,19 @@ Qed. Definition get_labels_from_walk x1 x2 vl al (walk : D_walk x1 x2 vl al) : list ter := get_labels al. -Inductive Single_path_semantics : forall (g : Grammar) (V : V_set) (A : A_set) +Inductive Single_path_semantics : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (v : var) (x1 x2 : Vertex) (vl : list Vertex) (al : list Arc), D_walk x1 x2 vl al -> Prop := - | Empty_path : forall (g : Grammar) (V : V_set) (A : A_set) (x : Vertex) + | Empty_path : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x : Vertex) (v : var) (e : eps), V x -> In (Re v e) g -> Single_path_semantics g V A v x x V_nil A_nil (DW_null x) - | One_arc_path : forall (g : Grammar) (V : V_set) (A : A_set) + | One_arc_path : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x1 x2 : Vertex) (v : var) (t : ter), V x1 -> V x2 -> In (Rt v t) g -> A (A_ends x1 x2 t) -> Single_path_semantics g V A v x1 x2 [x2] [A_ends x1 x2 t] (DW_step x1 x2 x2 V_nil A_nil t (DW_null x2)) - | Combine_path : forall (g : Grammar) (V : V_set) (A : A_set) + | Combine_path : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x1 x2 x3 : Vertex) (v v1 v2 : var) (al1 al2 : list Arc) (vl1 vl2 : list Vertex) (dw1 : D_walk x1 x2 vl1 al1) (dw2 : D_walk x2 x3 vl2 al2), @@ -134,7 +134,7 @@ Proof. done. Qed. -Theorem Derives_single_path : forall (g : Grammar) (V : V_set) (A : A_set) +Theorem Derives_single_path : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (v : var) (x1 x2 : Vertex) (vl : list Vertex) (al : list Arc) (dw : D_walk x1 x2 vl al) (p : Single_path_semantics g V A v x1 x2 vl al dw), @@ -161,8 +161,8 @@ Proof. done. Qed. -Theorem Parse_tree_to_single_path : forall (g : Grammar) (V : V_set) - (A : A_set) (x1 x2 : Vertex) (v : var), +Theorem Parse_tree_to_single_path : forall (g : Grammar) (V : Vertex_set) + (A : Arc_set) (x1 x2 : Vertex) (v : var), Parse_tree g V A x1 x2 v -> exists (vl : list Vertex) (al : list Arc) (dw : D_walk x1 x2 vl al), Single_path_semantics g V A v x1 x2 vl al dw. @@ -173,31 +173,19 @@ Proof. + exists [x2], [A_ends x1 x2 t], (DW_step x1 x2 x2 V_nil A_nil t (DW_null x2)). - apply One_arc_path. - done. - done. - done. - done. + by apply: One_arc_path. + exists [], [], (DW_null x). - apply: Empty_path. - done. - done. + by apply: Empty_path. + destruct IHpt1 as [vl1 [al1 [dw1 IHpt1]]]. destruct IHpt2 as [vl2 [al2 [dw2 IHpt2]]]. exists (vl1 ++ vl2), (al1 ++ al2), (D_walk_append x1 x2 x3 vl1 vl2 al1 al2 dw1 dw2). - apply: Combine_path. - done. - done. - done. - exact H2. - done. - done. + apply: Combine_path; eauto. Qed. (* Third semantic is all paths. *) @@ -214,16 +202,16 @@ Fixpoint get_all_pairs (all1 all2 : list (list Arc)) : list (list Arc) := | l::t => (get_pairs l all2) ++ (get_all_pairs t all2) end. -Inductive All_path_semantics : forall (g : Grammar) (V : V_set) (A : A_set) +Inductive All_path_semantics : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (v : var) (x1 x2 : Vertex) (all : list (list Arc)), Prop := - | Empty_paths : forall (g : Grammar) (V : V_set) (A : A_set) (x : Vertex) + | Empty_paths : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x : Vertex) (v : var) (e : eps), V x -> In (Re v e) g -> All_path_semantics g V A v x x [[]] - | One_arc_paths : forall (g : Grammar) (V : V_set) (A : A_set) + | One_arc_paths : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x1 x2 : Vertex) (v : var) (t : ter), V x1 -> V x2 -> In (Rt v t) g -> A (A_ends x1 x2 t) -> All_path_semantics g V A v x1 x2 [[A_ends x1 x2 t]] - | Combine_paths : forall (g : Grammar) (V : V_set) (A : A_set) + | Combine_paths : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x1 x2 x3 : Vertex) (v v1 v2 : var) (all1 all2 : list (list Arc)), V x1 -> V x2 -> V x3 -> In (Rv v v1 v2) g -> @@ -231,8 +219,8 @@ Inductive All_path_semantics : forall (g : Grammar) (V : V_set) (A : A_set) All_path_semantics g V A v2 x2 x3 all2 -> All_path_semantics g V A v x1 x3 (get_all_pairs all1 all2). -Theorem Parse_tree_to_all_path : forall (g : Grammar) (V : V_set) - (A : A_set) (x1 x2 : Vertex) (v : var), +Theorem Parse_tree_to_all_path : forall (g : Grammar) (V : Vertex_set) + (A : Arc_set) (x1 x2 : Vertex) (v : var), Parse_tree g V A x1 x2 v -> exists (all : list (list Arc)), All_path_semantics g V A v x1 x2 all. Proof. @@ -458,7 +446,7 @@ Proof. done. Qed. -Theorem derives_all_path : forall (g : Grammar) (V : V_set) (A : A_set) +Theorem derives_all_path : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (v : var) (x1 x2 : Vertex) (all : list (list Arc)) (aps : All_path_semantics g V A v x1 x2 all), forall (al : list Arc), In al all -> Der_ter_list g v (get_labels al). diff --git a/CCFPQ/Graph.v b/CCFPQ/Graph.v index 9fdcc1d..edf5407 100644 --- a/CCFPQ/Graph.v +++ b/CCFPQ/Graph.v @@ -57,7 +57,7 @@ Section Vertices. Inductive Vertex : Set := idx : nat -> Vertex. Definition V_list := list Vertex. Definition V_nil : list Vertex := nil. - Definition V_set := U_set Vertex. + Definition Vertex_set := U_set Vertex. Definition V_empty := Empty Vertex. Definition V_single := Single Vertex. Definition V_union := Union Vertex. @@ -82,7 +82,7 @@ Section Arcs. Inductive Arc : Set := A_ends : Vertex -> Vertex -> ter -> Arc. Definition A_tail (a : Arc) : Vertex := match a with A_ends x y l => x end. Definition A_head (a : Arc) : Vertex := match a with A_ends x y l => y end. - Definition A_set := U_set Arc. + Definition Arc_set := U_set Arc. Definition A_list := list Arc. Definition A_nil : list Arc := nil. Definition A_empty := Empty Arc. @@ -91,26 +91,26 @@ Section Arcs. End Arcs. Section Graph. - Inductive Digraph : V_set -> A_set -> Type := + Inductive Digraph : Vertex_set -> Arc_set -> Type := | D_empty : Digraph V_empty A_empty | D_vertex : - forall (v : V_set) (a : A_set) (d : Digraph v a) (x : Vertex), + forall (v : Vertex_set) (a : Arc_set) (d : Digraph v a) (x : Vertex), ~ v x -> Digraph (V_union (V_single x) v) a | D_arc : - forall (v : V_set) (a : A_set) (d : Digraph v a) (x y : Vertex) (l : ter), + forall (v : Vertex_set) (a : Arc_set) (d : Digraph v a) (x y : Vertex) (l : ter), v x -> v y -> ~ a (A_ends x y l) -> Digraph v (A_union (A_single (A_ends x y l)) a) | D_eq : - forall (v v' : V_set) (a a' : A_set), + forall (v v' : Vertex_set) (a a' : Arc_set), v = v' -> a = a' -> Digraph v a -> Digraph v' a'. - Fixpoint DV_list (v : V_set) (a : A_set) (d : Digraph v a) : V_list := match d with + Fixpoint DV_list (v : Vertex_set) (a : Arc_set) (d : Digraph v a) : V_list := match d with | D_empty => V_nil | D_vertex v' a' d' x _ => x :: DV_list v' a' d' | D_arc v' a' d' x y l _ _ _ => DV_list v' a' d' | D_eq v v' a a' _ _ d => DV_list v a d end. - Fixpoint DA_list (v : V_set) (a : A_set) (d : Digraph v a) : A_list := match d with + Fixpoint DA_list (v : Vertex_set) (a : Arc_set) (d : Digraph v a) : A_list := match d with | D_empty => A_nil | D_vertex v' a' d' x _ => DA_list v' a' d' | D_arc v' a' d' x y l _ _ _ => A_ends x y l :: DA_list v' a' d' @@ -119,11 +119,11 @@ Section Graph. End Graph. Section Degrees. - Variable a : A_set. + Variable a : Arc_set. Definition In_neighbor (x y : Vertex) (l : ter) := a (A_ends y x l). Definition Out_neighbor (x y : Vertex) (l : ter) := a (A_ends x y l). - Fixpoint In_neighborhood (x : Vertex) (v : V_set) (a : A_set) (d : Digraph v a) : V_list := + Fixpoint In_neighborhood (x : Vertex) (v : Vertex_set) (a : Arc_set) (d : Digraph v a) : V_list := match d with | D_empty => V_nil | D_vertex v' a' d' x' _ => In_neighborhood x v' a' d' @@ -134,8 +134,8 @@ Section Degrees. | D_eq v' _ a' _ _ _ d' => In_neighborhood x v' a' d' end. - Fixpoint Out_neighborhood (x : Vertex) (v : V_set) - (a : A_set) (d : Digraph v a) {struct d} : V_list := + Fixpoint Out_neighborhood (x : Vertex) (v : Vertex_set) + (a : Arc_set) (d : Digraph v a) {struct d} : V_list := match d with | D_empty => V_nil | D_vertex v' a' d' x' _ => Out_neighborhood x v' a' d' From 6dc9545e5df1c224683dde780af99e1aedb6a25f Mon Sep 17 00:00:00 2001 From: Roman Fedorov Date: Tue, 23 May 2017 11:57:55 +0300 Subject: [PATCH 23/23] Use Graph record instead of (Vertices, Arcs) pair --- CCFPQ/CCFPQ_Result.v | 135 +++++++++++++++++++++++-------------------- 1 file changed, 71 insertions(+), 64 deletions(-) diff --git a/CCFPQ/CCFPQ_Result.v b/CCFPQ/CCFPQ_Result.v index ffb12e0..587b677 100644 --- a/CCFPQ/CCFPQ_Result.v +++ b/CCFPQ/CCFPQ_Result.v @@ -9,47 +9,54 @@ Import ListNotations. Unset Implicit Arguments. Set Strict Implicit. +Record Graph := { + vertices : Vertex_set; + arcs : Arc_set; + digraph : Digraph vertices arcs; +}. + (* The main goal is to show that 3 sematics of CCFPQ evaluation can be *) (* derived from parse tree of a graph. *) -Inductive Parse_tree : Grammar -> Vertex_set -> Arc_set -> Vertex -> +Inductive Parse_tree : Grammar -> Graph -> Vertex -> Vertex -> var -> Prop := - | Leaf : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x1 x2 : Vertex) + | Leaf : forall (g : Grammar) (G : Graph) (x1 x2 : Vertex) (v : var) (t : ter), - V x1 -> V x2 -> In (Rt v t) g -> A (A_ends x1 x2 t) -> - Parse_tree g V A x1 x2 v - | Empty_leaf : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x : Vertex) + (vertices G) x1 -> (vertices G) x2 -> In (Rt v t) g -> + (arcs G) (A_ends x1 x2 t) -> Parse_tree g G x1 x2 v + | Empty_leaf : forall (g : Grammar) (G : Graph) (x : Vertex) (v : var) (e : eps), - V x -> In (Re v e) g -> Parse_tree g V A x x v - | Node : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x1 x2 x3 : Vertex) + (vertices G) x -> In (Re v e) g -> Parse_tree g G x x v + | Node : forall (g : Grammar) (G : Graph) (x1 x2 x3 : Vertex) (v v1 v2 : var), - V x1 -> V x2 -> V x3 -> In (Rv v v1 v2) g -> - Parse_tree g V A x1 x2 v1 -> Parse_tree g V A x2 x3 v2 -> - Parse_tree g V A x1 x3 v. + (vertices G) x1 -> (vertices G) x2 -> (vertices G) x3 -> + In (Rv v v1 v2) g -> Parse_tree g G x1 x2 v1 -> + Parse_tree g G x2 x3 v2 -> Parse_tree g G x1 x3 v. (* First semantic is relation. *) -Inductive Derivability_relation : Grammar -> Vertex_set -> Arc_set -> +Inductive Derivability_relation : Grammar -> Graph -> Vertex -> Vertex -> var -> Prop := - | Empty_rule : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x: Vertex) + | Empty_rule : forall (g : Grammar) (G : Graph) (x: Vertex) (v: var) (e: eps), - V x -> In (Re v e) g -> Derivability_relation g V A x x v - | Arc_with_ter_label : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) + (vertices G) x -> In (Re v e) g -> Derivability_relation g G x x v + | Arc_with_ter_label : forall (g : Grammar) (G : Graph) (x1 x2 : Vertex) (v : var) (t : ter), - V x1 -> V x2 -> In (Rt v t) g -> A (A_ends x1 x2 t) -> - Derivability_relation g V A x1 x2 v - | Rule_application : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) + (vertices G) x1 -> (vertices G) x2 -> In (Rt v t) g -> + (arcs G) (A_ends x1 x2 t) -> Derivability_relation g G x1 x2 v + | Rule_application : forall (g : Grammar) (G : Graph) (x1 x2: Vertex) (v v1 v2 : var), - (exists (x' : Vertex), V x1 -> V x2 -> V x' -> In (Rv v v1 v2) g -> - Derivability_relation g V A x1 x' v1 /\ - Derivability_relation g V A x' x2 v2) -> - Derivability_relation g V A x1 x2 v. + (exists (x' : Vertex), (vertices G) x1 -> (vertices G) x2 -> + (vertices G) x' -> In (Rv v v1 v2) g -> + Derivability_relation g G x1 x' v1 /\ + Derivability_relation g G x' x2 v2) -> + Derivability_relation g G x1 x2 v. -Theorem Parse_tree_to_relation : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) +Theorem Parse_tree_to_relation : forall (g : Grammar) (G : Graph) (x1 x2 : Vertex) (v : var), - Parse_tree g V A x1 x2 v -> Derivability_relation g V A x1 x2 v. + Parse_tree g G x1 x2 v -> Derivability_relation g G x1 x2 v. Proof. - move => _g _V _A _x1 _x2 _v pt. + move => _g _G _x1 _x2 _v pt. induction pt. + apply: Arc_with_ter_label. @@ -96,26 +103,26 @@ Qed. Definition get_labels_from_walk x1 x2 vl al (walk : D_walk x1 x2 vl al) : list ter := get_labels al. -Inductive Single_path_semantics : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) +Inductive Single_path_semantics : forall (g : Grammar) (G : Graph) (v : var) (x1 x2 : Vertex) (vl : list Vertex) (al : list Arc), D_walk x1 x2 vl al -> Prop := - | Empty_path : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x : Vertex) + | Empty_path : forall (g : Grammar) (G : Graph) (x : Vertex) (v : var) (e : eps), - V x -> In (Re v e) g -> - Single_path_semantics g V A v x x V_nil A_nil (DW_null x) - | One_arc_path : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) + (vertices G) x -> In (Re v e) g -> + Single_path_semantics g G v x x V_nil A_nil (DW_null x) + | One_arc_path : forall (g : Grammar) (G : Graph) (x1 x2 : Vertex) (v : var) (t : ter), - V x1 -> V x2 -> In (Rt v t) g -> A (A_ends x1 x2 t) -> - Single_path_semantics g V A v x1 x2 [x2] [A_ends x1 x2 t] + (vertices G) x1 -> (vertices G) x2 -> In (Rt v t) g -> (arcs G) (A_ends x1 x2 t) -> + Single_path_semantics g G v x1 x2 [x2] [A_ends x1 x2 t] (DW_step x1 x2 x2 V_nil A_nil t (DW_null x2)) - | Combine_path : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) + | Combine_path : forall (g : Grammar) (G : Graph) (x1 x2 x3 : Vertex) (v v1 v2 : var) (al1 al2 : list Arc) (vl1 vl2 : list Vertex) (dw1 : D_walk x1 x2 vl1 al1) (dw2 : D_walk x2 x3 vl2 al2), - V x1 -> V x2 -> V x3 -> In (Rv v v1 v2) g -> - Single_path_semantics g V A v1 x1 x2 vl1 al1 dw1 -> - Single_path_semantics g V A v2 x2 x3 vl2 al2 dw2 -> - Single_path_semantics g V A v x1 x3 (vl1 ++ vl2) (al1 ++ al2) + (vertices G) x1 -> (vertices G) x2 -> (vertices G) x3 -> In (Rv v v1 v2) g -> + Single_path_semantics g G v1 x1 x2 vl1 al1 dw1 -> + Single_path_semantics g G v2 x2 x3 vl2 al2 dw2 -> + Single_path_semantics g G v x1 x3 (vl1 ++ vl2) (al1 ++ al2) (D_walk_append x1 x2 x3 vl1 vl2 al1 al2 dw1 dw2). Lemma get_labels_is_linear : forall (al1 al2 : list Arc), @@ -134,13 +141,13 @@ Proof. done. Qed. -Theorem Derives_single_path : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) +Theorem Derives_single_path : forall (g : Grammar) (G : Graph) (v : var) (x1 x2 : Vertex) (vl : list Vertex) (al : list Arc) (dw : D_walk x1 x2 vl al) - (p : Single_path_semantics g V A v x1 x2 vl al dw), + (p : Single_path_semantics g G v x1 x2 vl al dw), Der_ter_list g v (get_labels_from_walk x1 x2 vl al dw). Proof. - move => g V A v x1 x2 vla la dw sps. + move => g G v x1 x2 vla la dw sps. induction sps. + rewrite / get_labels_from_walk. @@ -161,13 +168,13 @@ Proof. done. Qed. -Theorem Parse_tree_to_single_path : forall (g : Grammar) (V : Vertex_set) - (A : Arc_set) (x1 x2 : Vertex) (v : var), - Parse_tree g V A x1 x2 v -> +Theorem Parse_tree_to_single_path : forall (g : Grammar) (G : Graph) + (x1 x2 : Vertex) (v : var), + Parse_tree g G x1 x2 v -> exists (vl : list Vertex) (al : list Arc) (dw : D_walk x1 x2 vl al), - Single_path_semantics g V A v x1 x2 vl al dw. + Single_path_semantics g G v x1 x2 vl al dw. Proof. - move => g V A x1 x2 v pt. + move => g G x1 x2 v pt. induction pt. + exists [x2], @@ -202,29 +209,29 @@ Fixpoint get_all_pairs (all1 all2 : list (list Arc)) : list (list Arc) := | l::t => (get_pairs l all2) ++ (get_all_pairs t all2) end. -Inductive All_path_semantics : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) +Inductive All_path_semantics : forall (g : Grammar) (G : Graph) (v : var) (x1 x2 : Vertex) (all : list (list Arc)), Prop := - | Empty_paths : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) (x : Vertex) + | Empty_paths : forall (g : Grammar) (G : Graph) (x : Vertex) (v : var) (e : eps), - V x -> In (Re v e) g -> All_path_semantics g V A v x x [[]] - | One_arc_paths : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) + (vertices G) x -> In (Re v e) g -> All_path_semantics g G v x x [[]] + | One_arc_paths : forall (g : Grammar) (G : Graph) (x1 x2 : Vertex) (v : var) (t : ter), - V x1 -> V x2 -> In (Rt v t) g -> A (A_ends x1 x2 t) -> - All_path_semantics g V A v x1 x2 [[A_ends x1 x2 t]] - | Combine_paths : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) + (vertices G) x1 -> (vertices G) x2 -> In (Rt v t) g -> (arcs G) (A_ends x1 x2 t) -> + All_path_semantics g G v x1 x2 [[A_ends x1 x2 t]] + | Combine_paths : forall (g : Grammar) (G : Graph) (x1 x2 x3 : Vertex) (v v1 v2 : var) (all1 all2 : list (list Arc)), - V x1 -> V x2 -> V x3 -> In (Rv v v1 v2) g -> - All_path_semantics g V A v1 x1 x2 all1 -> - All_path_semantics g V A v2 x2 x3 all2 -> - All_path_semantics g V A v x1 x3 (get_all_pairs all1 all2). - -Theorem Parse_tree_to_all_path : forall (g : Grammar) (V : Vertex_set) - (A : Arc_set) (x1 x2 : Vertex) (v : var), - Parse_tree g V A x1 x2 v -> - exists (all : list (list Arc)), All_path_semantics g V A v x1 x2 all. + (vertices G) x1 -> (vertices G) x2 -> (vertices G) x3 -> In (Rv v v1 v2) g -> + All_path_semantics g G v1 x1 x2 all1 -> + All_path_semantics g G v2 x2 x3 all2 -> + All_path_semantics g G v x1 x3 (get_all_pairs all1 all2). + +Theorem Parse_tree_to_all_path : forall (g : Grammar) (G : Graph) + (x1 x2 : Vertex) (v : var), + Parse_tree g G x1 x2 v -> + exists (all : list (list Arc)), All_path_semantics g G v x1 x2 all. Proof. - move => g V A x1 x2 v pt. + move => g G x1 x2 v pt. induction pt. + exists [[A_ends x1 x2 t]]. @@ -446,12 +453,12 @@ Proof. done. Qed. -Theorem derives_all_path : forall (g : Grammar) (V : Vertex_set) (A : Arc_set) +Theorem derives_all_path : forall (g : Grammar) (G : Graph) (v : var) (x1 x2 : Vertex) (all : list (list Arc)) - (aps : All_path_semantics g V A v x1 x2 all), + (aps : All_path_semantics g G v x1 x2 all), forall (al : list Arc), In al all -> Der_ter_list g v (get_labels al). Proof. - move => g V A v x1 x2 all aps. + move => g G v x1 x2 all aps. induction aps. + move => conc contains.