famubu
/
playground
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

[coq] replicate coq/reglang

This commit is contained in:
Julin S 2024-04-01 17:48:32 +05:30
parent fc4cb83894
commit c23231e006
10 changed files with 940 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.gitignore vendored
View File

@ -71,3 +71,5 @@ bsv/**/bsim
bsv/**/*.h
latex/**/*.pdf
*.opam

21
coq/re-nfa/default.nix Normal file
View File

@ -0,0 +1,21 @@
with import <nixpkgs> {};
let cP = coqPackages.overrideScope' (self: super: {
mathcomp = super.mathcomp.override { version = "2.1.0"; };
});
in
mkShell {
packages = (with cP; [
coq
hierarchy-builder
reglang
]) ++ [
dune_3
opam
ocaml
emacs
];
}

65
coq/re-nfa/dfa.v Normal file
View File

@ -0,0 +1,65 @@
(*
From mathcomp Require Import all_ssreflect.
Set Bullet Behavior "Strict Subproofs".
From aruvi Require state.
From aruvi Require re.
From aruvi Require nfa.
Import state.StateNotations.
Record t {A: Type}: Type := mkDfa {
state: state.tNfa;
start: {sset nfa⟦state⟧};
final: {sset nfa⟦state⟧};
tf: {sset nfa⟦state⟧} -> A -> {sset nfa⟦state⟧}
}.
Arguments t: clear implicits.
Definition of_nfa {A: Type} (n: nfa.t A): t A. refine {|
state := nfa.state n;
start := _; (* [set (nfa.start n)]; *)
(* start := [set [set x] | x in nfa.start n]; (1* [set (nfa.start n)]; *1) *)
final := _;
tf src ch := _
|}.
- Check [set
- Check [set: dfa⟦state.pset (nfa.state n)⟧].
Check [set x | x in [set: dfa⟦state.pset (nfa.state n)⟧]].
Check [set x | x in [set: dfa⟦state.pset (nfa.state n)⟧]].
Check [set x | x in [set: bool]].
Check [set x in [set: bool] | true].
Check [set x in [set: dfa⟦state.pset (nfa.state n)⟧] | true].
Check [set x in [set: _] | true].
Check [set x in [set: {set {set nfa⟦nfa.state n⟧}}] | true].
Search {set _} bool.
Search (set_of _ -> set_of _ -> bool).
Check [set x in [set: {set {set nfa⟦nfa.state n⟧}}] | x :&: _ = false].
Check [set x in [set: dfa⟦state.pset (nfa.state n)⟧] | x :&: _].
(*
[set p | p ∩ n.final != ∅
& p in pset] *)
Check [set true; false].
Check [set true] == set0.
(* [set true; false] : {set Datatypes_bool__canonical__fintype_Finite} *)
- Check [set [set x] | x in nfa.final n].
Check [set: bool].
Check [set: bool].
(* [set: bool] : {set Datatypes_bool__canonical__fintype_Finite} *)
- Check nfa.state n.
exact: [set (nfa.start n)].
Check {set nfa⟦nfa.state n⟧}.
Check [set x | x \in {set nfa⟦nfa.state n⟧}].
Check [set x | set0 \notin (x :&: (nfa.start n)) & x \in {set nfa⟦nfa.state n⟧}].
Check [set x | set0 \notin (x :&: (nfa.start n)) & x \in {set nfa⟦nfa.state n⟧}].
Check [set x | x \in {set nfa⟦state⟧}].
+ exact:
Check [set X | X :&: nfa.final n != set0].
*)

5
coq/re-nfa/dune Normal file
View File

@ -0,0 +1,5 @@
(coq.theory
(name aruvi)
(synopsis "A coq library for streams and their hardware realisation"))
(include_subdirs qualified)

7
coq/re-nfa/dune-project Normal file
View File

@ -0,0 +1,7 @@
(lang dune 3.6)
(using coq 0.6)
(generate_opam_files true)
(package
(name renfa)
(allow_empty))

131
coq/re-nfa/lang.v Normal file
View File

@ -0,0 +1,131 @@
From mathcomp Require Import all_ssreflect.
Set Bullet Behavior "Strict Subproofs".
Section Lang.
Definition t (A: Type) := pred (seq A).
Context {A: Type}.
Definition eps: t A := nilp (T:=A).
Definition char (f: A -> bool): t A := fun w =>
match w with
| [:: x ] => f x
| _ => false
end.
Definition cat (l1 l2: t A): t A := fun w =>
[exists i : 'I_(size w).+1,
l1 (seq.take i w) && l2 (seq.drop i w)].
Definition alt (l1 l2: t A): t A :=
[pred w | (w \in l1) || (w \in l2)].
Definition residual (l: t A) (x: A): t A := fun w =>
l (x :: w).
Definition star (l: t A): t A :=
fix star w :=
match w with
| [:: x & w'] => cat (residual l x) star w'
| [::] => true
end.
Lemma catP (l1 l2: t A) (w: seq A): reflect
(exists w1 w2: seq A,
w = w1 ++ w2 /\
w1 \in l1 /\
w2 \in l2)
(w \in cat l1 l2).
Proof.
apply: (iffP exists_inP).
- move => [i] Hl1 Hl2.
exists (take i w).
exists (drop i w).
rewrite cat_take_drop.
by split.
- move => [w1 [w2 [Hw1w2 [H2 H3]]]].
have Hi : size w1 < (size w).+1.
+ by rewrite Hw1w2 size_cat ltnS leq_addr.
+ exists (Ordinal Hi); subst.
* by rewrite take_size_cat.
* by rewrite drop_size_cat.
Qed.
Lemma cat_eq (l1 l2 l3 l4: t A):
l1 =i l2 ->
l3 =i l4 ->
cat l1 l3 =i cat l2 l4.
Proof.
move => H1 H2 w.
apply: eq_existsb => n.
by rewrite (_ : l1 =1 l2) // (_ : l3 =1 l4).
Qed.
(* Out of all words, there exists a list of words which is part of l and is
not ε.
Concatenation of all words in wl would also be in star l. Clever! *)
Lemma starP (l: t A) (w: seq A): reflect
(exists2 wl: seq (seq A),
all [predD l & eps] wl & w = flatten wl)
(w \in star l).
Proof.
(* TODO: ??? What's _.+1 *)
elim: {w} _.+1 {-2}w (ltnSn (size w)) => //.
move => n IHw.
case => /=.
- move => Hsz.
left.
by exists [::].
- move => ch w Hsz.
apply (iffP (catP _ _ w)).
+ move => [w1] [w2] [Hw1w2] [H1].
case/IHw.
* rewrite -ltnS (leq_trans _ Hsz) //. (* TODO: How ?....? *)
by rewrite Hw1w2 size_cat !ltnS leq_addl.
* move => wl Hall H.
exists ((ch::w1) :: wl); first by apply/andP; split.
by rewrite Hw1w2 H.
+ move => [[|[|ch' w'] wl] //=].
case/andP => Hw' Hall [Hch Hw].
exists w'; exists (flatten wl).
subst.
do 2! split => //.
apply/IHw.
* rewrite -ltnS (leq_trans _ Hsz) //. (* TODO: How ?....? *)
rewrite size_cat.
rewrite 2!ltnS.
apply: leq_addl.
* by exists wl.
Qed.
Lemma star_cat (l: t A) (w1 w2: seq A):
w1 \in l ->
w2 \in (star l) ->
w1 ++ w2 \in star l.
Proof.
case: w1 => [|a w1] // H1 /starP [wl Ha Hf].
apply/starP.
by exists ((a::w1) :: wl); rewrite ?Hf //= H1.
Qed.
Lemma star_eq (l1 l2: t A):
l1 =i l2 -> star l1 =i star l2.
Proof.
move => H w.
apply/starP/starP.
- move => [wl] Hall Hflatten.
exists wl => //.
erewrite eq_all.
eexact Hall.
move => x /=.
by rewrite H.
- move => [wl] Hall Hflatten.
exists wl => //.
erewrite eq_all.
eexact Hall.
move => x /=.
by rewrite H.
Qed.
End Lang.

545
coq/re-nfa/nfa.v Normal file
View File

@ -0,0 +1,545 @@
From mathcomp Require Import all_ssreflect.
Set Bullet Behavior "Strict Subproofs".
From aruvi Require state.
From aruvi Require re.
Import state.StateNotations.
Record t {A: Type}: Type := mkNfa {
state: state.tNfa;
start: {set nfa⟦state⟧};
final: {set nfa⟦state⟧};
tf: nfa⟦state⟧ -> A -> nfa⟦state⟧ -> bool
}.
Arguments t: clear implicits.
Module Enfa.
Record t {A: Type}: Type := mkEnfa {
state: state.tNfa;
start: {set nfa⟦state⟧};
final: {set nfa⟦state⟧};
tf: option A -> nfa⟦state⟧ -> nfa⟦state⟧ -> bool
}.
#[global] Arguments t: clear implicits.
Inductive accept {A: Type} {n: t A}: nfa⟦state n⟧ -> seq A -> Prop :=
| EnfaFin (s: nfa⟦state n⟧)
: s \in final n -> accept s [::]
| EnfaSome (s: nfa⟦state n⟧) (ch: A) (d: nfa⟦state n⟧) (w: seq A)
: (tf n) (Some ch) s d -> accept d w -> accept s (ch::w)
| EnfaNone (s d: nfa⟦state n⟧) (w: seq A)
: (tf n) None s d -> accept d w -> accept s w.
Definition to_lang {A: Type} (n: t A) (w: seq A) :=
exists2 src: nfa⟦state n⟧, src \in (start n) & accept src w.
Definition eps_closure {A: Type} (n: t A)(src: nfa⟦state n⟧) :=
[set dst | connect ((tf n) None) src dst].
Lemma lift_accept {A: Type} (n: t A) (src dst: nfa⟦state n⟧) (w: seq A)
: dst \in eps_closure n src -> accept dst w -> accept src w.
Proof.
rewrite inE => /connectP [s].
elim: s src w dst =>
[ src w dst _ -> //
| dst dsts IHw src w dst' /=].
case/andP => /= Htf Hpath Heq HAccdst'.
have H := IHw dst w dst' Hpath Heq HAccdst'.
exact: (Enfa.EnfaNone src dst w Htf H).
Qed.
End Enfa.
Definition of_enfa {A: Type} (n: Enfa.t A): t A := {|
state := Enfa.state n;
start := \bigcup_(p in Enfa.start n) (Enfa.eps_closure n p);
final := Enfa.final n;
tf p a q := [exists p',
(Enfa.tf n) (Some a) p p' &&
(q \in Enfa.eps_closure n p')]
|}.
Section EnfaFAs.
Context {A: Type}.
Definition ecat (n1 n2: t A): Enfa.t A := {|
Enfa.state := state.NPlus (state n1) (state n2);
Enfa.start := inl @: start n1;
Enfa.final := inr @: final n2;
Enfa.tf ch src dst :=
match src, ch, dst with
| inl s, Some c, inl d => (tf n1) s c d
| inr s, Some c, inr d => (tf n2) s c d
| inl s, None, inr d =>
(s \in (final n1)) && (d \in (start n2))
| _, _, _ => false
end
|}.
Definition estar (n: t A): Enfa.t A := {|
Enfa.state := state.NPlus state.NOne (state n);
Enfa.start := [set (inl tt)];
Enfa.final := [set (inl tt)];
Enfa.tf ch src dst :=
match src, ch, dst with
(* | inl _, None, inl _ => true *)
| inl _, None, inr d => d \in (start n)
| inr s, None, inl _ => s \in (final n)
(* | inr s, None, inr d => s == d *)
| inr s, Some c, inr d => (tf n) s c d
| _, _, _ => false
end
|}.
End EnfaFAs.
Section FAs.
Context {A: Type}.
(* Like 𝟘 *)
Definition nul: t A := {|
state := state.NZero;
start := set0;
final := set0;
tf src ch dst := false
|}.
(* Like 𝟙 *)
Definition eps: t A :={|
state := state.NOne;
start := [set tt];
final := [set tt];
tf src ch dst := false
|}.
Definition char (f: A -> bool): t A := {|
state := state.NPlus state.NOne state.NOne;
start := [set (inl tt)];
final := [set (inr tt)];
tf src ch dst :=
match src, dst with
| inl _, inr _ => f ch
| _, _ => false
end
|}.
Definition alt (n1 n2: t A): t A := {|
state := state.NPlus (state n1) (state n2);
start := [set s |
match s with
| inl s => s \in start n1
| inr s => s \in start n2
end];
final := [set s |
match s with
| inl s => s \in final n1
| inr s => s \in final n2
end];
tf src ch dst :=
match src, dst with
| inl s, inl d => (tf n1) s ch d
| inr s, inr d => (tf n2) s ch d
| _, _ => false
end
|}.
Definition cat (n1 n2: t A): t A := of_enfa (ecat n1 n2).
Definition star (n: t A): t A := of_enfa (estar n).
End FAs.
Section Sem.
Context {A: Type}.
Fixpoint accept (n: t A) (src: nfa⟦state n⟧)
(w: list A): bool :=
match w with
| [::] => src \in (final n)
| [:: ch & w'] =>
[exists (dst | (tf n) src ch dst), accept n dst w']
end.
Definition to_lang (n: t A): lang.t A :=
[pred w | [exists src, (src \in (start n)) && (accept n src w)]].
End Sem.
Section EnfaLemmas.
Context {A: Type}.
Lemma enfa_catIr (n1 n2: t A) (src: nfa⟦state n2⟧) (w: seq A)
: accept n2 src w -> Enfa.accept (n:=ecat n1 n2) (inr src) w.
Proof.
elim: w src.
- move => fin H.
constructor => /=.
by apply: (imset_f inr).
- move => ch w IHw src2 /= /exists_inP [dst2] Htf H.
have HH := IHw dst2 H.
exact: (Enfa.EnfaSome (n:=ecat n1 n2) (inr src2) ch (inr dst2) w Htf HH).
Qed.
Lemma enfa_catIl (n1 n2: t A) (src: nfa⟦state n1⟧) (w1 w2: seq A)
: accept n1 src w1 -> w2 \in to_lang n2 ->
Enfa.accept (n:=ecat n1 n2) (inl src) (w1++w2).
Proof.
elim: w1 src => /=.
- move => fin1 H1.
move/exists_inP => [src2] H2 H3.
apply: ((Enfa.EnfaNone (n:=ecat n1 n2) (inl fin1)) (inr src2) w2); first by rewrite /= H1.
exact: enfa_catIr n1 n2 src2 w2 H3.
- move => ch w IHw src /exists_inP [s] Htf H1 H.
apply: (Enfa.EnfaSome (n:=ecat n1 n2) (inl src) ch (inl s) (w++w2)) => //.
exact: IHw s H1 H.
Qed.
Lemma enfa_catE (n1 n2: t A) (src: nfa⟦Enfa.state (ecat n1 n2)⟧) (w: seq A):
Enfa.accept src w ->
match src with
| inl s => exists w1 w2: seq A,
[/\ w = w1++w2, accept n1 s w1 & w2 \in to_lang n2]
| inr s => accept n2 s w
end.
Proof.
elim => {src w}.
- by move => src /imsetP [dst] Hdst ->.
- move => [src|src] ch [dst|dst] w //.
+ move => /= Htf Hacc [w1] [w2] [H1 H2 H3].
exists (ch::w1).
exists w2.
subst.
split => //.
rewrite /accept.
apply/exists_inP.
by exists dst.
+ move => /= Htf Hacc Heacc.
apply/exists_inP.
by exists dst.
- move => [src|src] [dst|dst] //=.
move => w /andP [H1 H2] Heacc Hacc.
exists [::] => /=.
exists w => //=.
split => //.
apply/exists_inP.
by exists dst.
Qed.
Lemma enfa_catP (n1 n2: t A) (w: seq A): reflect
(Enfa.to_lang (ecat n1 n2) w)
(lang.cat (to_lang n1) (to_lang n2) w).
Proof.
apply: (iffP (lang.catP (to_lang n1) (to_lang n2) w)).
- move => [w1] [w2] [H1 [H2 H3]].
case/exists_inP: H2 => src Hsrc Hacc.
exists (inl src) => /=.
apply: imset_f => //.
rewrite H1.
by apply: enfa_catIl.
- rewrite /Enfa.to_lang.
move => [[src|src]]; last by case/imsetP. (* TODO: How the last ?? *)
move/imsetP => [src1] H1 H2 /enfa_catE [w1] [w2] [H3 H4 H5].
exists w1; exists w2.
split => //; split => //.
apply/exists_inP.
exists src1 => //.
assert (src = src1); first by case: H2.
by rewrite -H.
Qed.
Lemma enfaE {n: Enfa.t A} (w: seq A) (src: nfa⟦Enfa.state n⟧):
(Enfa.accept src w) <->
(exists2 dst : nfa⟦state (of_enfa n)⟧,
dst \in Enfa.eps_closure n src & accept (of_enfa n) dst w).
Proof.
split => /=.
- elim => {src w}
[ fin H
| src ch dst w H H1 [dst' Heps Hacc]
| dst dst' w H H1 [s Heps Hacc]].
+ exists fin => //.
by rewrite inE connect0.
+ exists src => /=; first by rewrite inE.
apply/exists_inP.
exists dst' => //.
apply/exists_inP.
by exists dst.
+ exists s; last by [].
rewrite inE in Heps.
rewrite inE.
exact: (connect_trans (connect1 _) Heps).
- elim: w src => //=.
+ move => src [s] Heps Hfin.
apply: (Enfa.lift_accept n _ s) => //.
by apply: (Enfa.EnfaFin s).
+ move => ch w IH.
move => src [s] Heps.
case/exists_inP.
move => dst.
move/exists_inP => [d Hsd Hdd] H.
apply: (Enfa.lift_accept n src _ (ch::w) Heps).
apply: (Enfa.EnfaSome s ch _ w Hsd).
apply: IH.
by exists dst.
Qed.
Lemma of_enfaP (n: Enfa.t A) (w: seq A)
: reflect (Enfa.to_lang n w) (w \in to_lang (of_enfa n)).
Proof.
apply: (iffP exists_inP).
- move => [src Hin Hacc].
case/bigcupP: Hin => begin H1 H2.
rewrite /Enfa.to_lang.
exists begin => //.
apply/enfaE.
exists src => //.
- rewrite /Enfa.to_lang.
move => [esrc Hestart] /enfaE [src HesrcEps Hacc].
exists src => //.
apply/bigcupP.
by exists esrc.
Qed.
Lemma enfa_star_cat (n: t A) (w1 w2: seq A) (src: nfa⟦Enfa.state (estar n)⟧):
Enfa.accept src w1 ->
Enfa.to_lang (estar n) w2 ->
Enfa.accept src (w1 ++ w2).
Proof.
elim => {src w1}.
- move => src.
rewrite inE => /eqP ->.
rewrite /Enfa.to_lang.
case => s.
by rewrite inE => /eqP ->.
- move => src ch dst w /=.
case src => src' //.
case dst => dst' //.
move => Htf Hacc IH H.
(* Check (Enfa.EnfaSome (n:=estar n) (inr src') ch (inr dst') (ch :: w ++ w2) _). *)
exact: Enfa.EnfaSome (IH H). (* TODO: How .... ? *)
- move => src dst w Htf Hacc IH H.
exact: Enfa.EnfaNone (IH H). (* TODO: How .... ? *)
Qed.
Lemma enfa_starI (n: t A) (w: seq A) (src: nfa⟦state n⟧):
accept n src w ->
Enfa.accept (n:=estar n) (inr src) w.
Proof.
elim: w src => /=.
- move => src Hsrc.
apply: (Enfa.EnfaNone (n:=estar n) (inr src) (inl tt)) => //.
apply: Enfa.EnfaFin.
by rewrite inE.
- move => ch w IHw src.
case/exists_inP => dst Htf /IHw.
by exact: Enfa.EnfaSome.
Qed.
Lemma enfa_star_langI (n: t A) (w: seq A):
w \in to_lang n -> Enfa.accept (n:=estar n) (inl tt) w.
Proof.
case/exists_inP => src Hsrc Hacc.
refine (Enfa.EnfaNone (n:=estar n) (inl tt) (inr src) w _ _) => //.
by apply: enfa_starI.
Qed.
(* Warning!: This is in Prop, not bool *)
Lemma enfa_starE (n: t A) (src: nfa⟦Enfa.state (estar n)⟧) (w: seq A):
Enfa.accept src w ->
match src with
| inl _ => is_true (lang.star (to_lang n) w)
| inr src' => exists w1 w2: seq A,
[/\ w = w1 ++ w2, accept n src' w1 & lang.star (to_lang n) w2]
end.
Proof.
elim => {w src}.
- move => [src|src] //.
by rewrite inE => /eqP.
- move => [src|src] ch [dst|dst] w //= Htf Hacc [w1] [w2] [H1 H2 H3].
exists (ch::w1); exists w2.
rewrite H1 /=.
split => //.
apply/exists_inP.
by exists dst.
(* - move => [src|] [|dst] w //=. *)
- move => [src|src] [dst|dst] w //=.
+ move => Hin Hacc.
move => [w1] [w2] [-> H].
apply: lang.star_cat.
apply/exists_inP.
by exists dst.
+ move => Hin Hacc H.
exists [::] => /=.
by exists w => /=.
Qed.
Lemma enfa_starP (n: t A) (w: seq A): reflect
(Enfa.to_lang (estar n) w)
(lang.star (to_lang n) w).
Proof.
apply: (iffP idP).
- case/lang.starP => wl H ->.
elim: wl H => /=.
+ move => _.
rewrite /Enfa.to_lang.
exists (inl tt).
* by rewrite inE.
* apply: Enfa.EnfaFin => /=.
by rewrite inE.
+ move => w' wl IH /andP [/andP [H1 H2] H3].
rewrite /Enfa.to_lang.
exists (inl tt).
* by rewrite inE.
* apply: enfa_star_cat; first by apply: enfa_star_langI.
by apply: IH.
- rewrite /Enfa.to_lang.
case => src.
rewrite inE => /eqP ->.
exact: enfa_starE.
Qed.
End EnfaLemmas.
Section Correctness.
Context {A: Type}.
Lemma eps_correct:
to_lang (A:=A) eps =i re.to_lang re.Eps.
Proof.
rewrite /= => w.
apply/exists_inP/idP. (* ??? *)
- move => [[_]] //=.
case: w => [|a w'] //=.
by move/exists_inP => [[]].
- case: w => [|a w'] //=.
rewrite /lang.eps unfold_in => _.
by exists tt; rewrite inE.
Qed.
Lemma char_correct (f: A -> bool):
to_lang (char f) =1 re.to_lang (re.Char f).
Proof.
move => w //=.
apply/exists_inP/idP => //=.
- case w => [|a w'].
+ move => [src] //=.
by case: src; case; rewrite !inE.
+ move => [src].
case: src; last by case; rewrite inE.
case.
rewrite inE => _ /= /exists_inP => [[src1]].
case src1; first by case.
case.
case (f a) => [_|]; last by [].
elim: w' => [|a2 w' IH] //=.
move/exists_inP.
by move => [src2].
- rewrite /lang.char /=.
case w => [|a [|b w']]; first by []; last by [].
case (f a) eqn:Hfa => [_|]; last by [].
exists (inl tt); first by rewrite inE.
apply/exists_inP => //=.
rewrite Hfa.
exists (inr tt); first by [].
by rewrite inE.
Qed.
Lemma cat_correct (n1 n2: t A):
to_lang (cat n1 n2) =i lang.cat (to_lang n1) (to_lang n2).
Proof.
move => w.
by apply/of_enfaP/idP; move => H; apply/enfa_catP.
Qed.
Lemma alt_correct (n1 n2: t A):
to_lang (alt n1 n2) =i lang.alt (to_lang n1) (to_lang n2).
Proof.
move => w.
apply/idP/idP.
- case/exists_inP => [[src|src]].
+ rewrite !inE => Hsrc Hacc.
apply/orP.
left.
apply/exists_inP.
exists src => //.
elim: w src {Hsrc} Hacc => /=.
* move => src.
by rewrite inE.
* move => ch w IH src.
case/exists_inP.
move => [|] // s Htf /= /IH H.
apply/exists_inP.
by exists s.
+ rewrite !inE => Hsrc Hacc.
apply/orP.
right.
apply/exists_inP.
exists src => //.
elim: w src {Hsrc} Hacc => /=.
* move => src.
by rewrite inE.
* move => ch w IH src.
case/exists_inP.
move => [|] // s Htf /= /IH H.
apply/exists_inP.
by exists s.
- rewrite !inE.
case/orP.
+ move/exists_inP => [start1] Hstart1 Hacc.
apply/exists_inP.
exists (inl start1).
rewrite inE //.
elim: w start1 {Hstart1} Hacc => //=.
* move => start1 Hstart1.
by rewrite inE.
* move => ch w IH start1.
move/exists_inP => [d] Htf /IH Hacc.
apply/exists_inP.
by exists (inl d).
+ move/exists_inP => [start2] Hstart2 Hacc.
apply/exists_inP.
exists (inr start2).
rewrite inE //.
elim: w start2 {Hstart2} Hacc => //=.
* move => start2 Hstart2.
by rewrite inE.
* move => ch w IH start2.
move/exists_inP => [d] Htf /IH Hacc.
apply/exists_inP.
by exists (inr d).
Qed.
Lemma star_correct (n: t A):
to_lang (star n) =i lang.star (to_lang n).
Proof.
move => w.
apply/of_enfaP/idP => [H|]; by apply/enfa_starP.
Qed.
End Correctness.
Section OfRe.
Context {A: Type}.
Fixpoint of_re (r: re.t A): t A :=
match r with
| re.Eps => eps
| re.Char f => char f
| re.Cat r1 r2 => cat (of_re r1) (of_re r2)
| re.Alt r1 r2 => alt (of_re r1) (of_re r2)
| re.Star rr => star (of_re rr)
end.
Theorem of_re_correctness (r: re.t A):
to_lang (of_re r) =i re.to_lang r.
Proof.
elim: r.
- exact: eps_correct.
- apply: char_correct.
- move => r1 IHr1 r2 IHr2 w /=.
rewrite cat_correct.
exact: lang.cat_eq.
- move => r1 IHr1 r2 IHr2 w /=.
rewrite alt_correct.
rewrite /lang.alt.
rewrite inE IHr1 IHr2.
by rewrite inE.
- move => r IHr /= w.
rewrite star_correct.
by apply: lang.star_eq.
Qed.
End OfRe.

62
coq/re-nfa/re.v Normal file
View File

@ -0,0 +1,62 @@
From mathcomp Require Import all_ssreflect.
Set Bullet Behavior "Strict Subproofs".
From aruvi Require lang.
Inductive t {A: Type}: Type :=
| Eps: t
| Char: (A -> bool) -> t
| Cat: t -> t -> t
| Alt: t -> t -> t
| Star: t -> t.
Arguments t: clear implicits.
Section Combinators.
Context {A: Type}.
Definition any: t A := Char (fun _ => true).
Fixpoint repn (r: t A) (n: nat): t A :=
match n with
| O => Eps
| S n' => Cat r (repn r n')
end.
Definition repnm (r: t A) (low high: nat): t A :=
match Nat.ltb high low with
| true => Eps
| _ =>
let idxs := List.seq 0 ((high-low).+1) in
let rs := List.map (repn r) idxs in
let rn := repn r low in
let rs' := List.map (Cat rn) rs in
List.fold_right (fun x acc => Alt acc x) Eps rs'
end.
End Combinators.
Fixpoint to_lang {A: Type} (r: t A): lang.t A :=
match r with
| Eps => lang.eps
| Char f => lang.char f
| Cat r1 r2 => lang.cat (to_lang r1) (to_lang r2)
| Alt r1 r2 => lang.alt (to_lang r1) (to_lang r2)
| Star rr => lang.star (to_lang rr)
end.
Module ReNotations.
Declare Scope re_scope.
Delimit Scope re_scope with re.
Notation "'↑' c" := (Char c) (at level 25, no associativity): re_scope.
Notation "r '⁎'" := (Star r) (at level 30, right associativity): re_scope.
Infix ";" := Cat (at level 35, right associativity): re_scope.
Infix "│" := Alt (at level 41, right associativity): re_scope.
Notation "'ε'" := Eps: re_scope.
Notation "'⋅'" := any: re_scope.
Notation "r '❴' n '❵'" := (repn r n) (at level 20): re_scope.
Notation "r '❴' low ',' high '❵'" := (repnm r low high)
(at level 20): re_scope.
Notation "'⟦' c '⟧'" := (Char (Nat.eqb c)) (at level 50): re_scope.
Notation "'❮' c '❯'" := (Char (Bool.eqb c)) (at level 50): re_scope.
End ReNotations.

100
coq/re-nfa/state.v Normal file
View File

@ -0,0 +1,100 @@
From mathcomp Require Import all_ssreflect.
Set Bullet Behavior "Strict Subproofs".
Reserved Notation "'dfa⟦' s '⟧'" (at level 20).
Reserved Notation "'nfa⟦' s '⟧'" (at level 20).
Inductive tNfa: Type :=
| NZero: tNfa
| NOne: tNfa
| NPlus: tNfa -> tNfa -> tNfa.
Inductive tDfa: Type :=
| DOne: tDfa
| DPlus: tDfa -> tDfa -> tDfa
| DMult: tDfa -> tDfa -> tDfa.
Fixpoint tNfaDenote (s: tNfa): finType :=
(match s with
| NZero => void
| NOne => unit
| NPlus a b => nfa⟦a⟧ + nfa⟦b⟧
end)%type
where "'nfa⟦' s '⟧'" := (tNfaDenote s).
Fixpoint tDfaDenote (s: tDfa): finType :=
(match s with
| DOne => unit
| DPlus a b => dfa⟦a⟧ + dfa⟦b⟧
| DMult a b => dfa⟦a⟧ * dfa⟦b⟧
end)%type
where "'dfa⟦' s '⟧'" := (tDfaDenote s).
Fixpoint pset (s: tNfa): tDfa :=
match s with
| NZero => DOne
| NOne => DPlus DOne DOne
| NPlus a b => DMult (pset a) (pset b)
end.
(* Fixpoint tNfaEnum (s: tDfa): seq (dfa⟦s⟧). *)
(* refine ( *)
(* match s with *)
(* | DOne => [:: tt] *)
(* | DPlus a b => _ *)
(* | DMult a b => _ *)
(* end) => /=. *)
(* Fixpoint union {n: tNfa}: {set nfa⟦n⟧} -> {set dfa⟦pset n⟧}. *)
(* refine ( *)
(* match n with *)
(* | NZero => fun s => set0 *)
(* | NOne => fun s => _ *)
(* | NPlus a b => fun s => _ *)
(* end) => /=; rewrite /= in s. *)
(* - shelve. *)
(* - *)
(* Check [set x | x in s]. *)
(* Check [set (fun x => x) x | x in s]. *)
(* - refine ([set _ | x in s]). *)
(* Search (set_of _ -> bool). *)
(* Search set0 bool. *)
(* Compute set0 \in set0. *)
(* refine ( *)
(* match x with *)
(* | inl l => inl x' *)
(* | inr r => inr x' *)
(* ref [set *)
(* (match x with *)
(* | inl x' => inl x' *)
(* | inr x' => inr x' *)
(* end) *)
(* | x in s]. *)
(* Check [set *)
(* (match x with *)
(* | inl x' => x *)
(* | inr x' => x *)
(* end) *)
(* | x in s]. *)
(* Search ({set _} -> seq _). *)
(* Search (set_of _ -> seq _). *)
(* Search (set_of _) seq. *)
(* Search (set_of _) bool. *)
(* Check [set *)
Module StateNotations.
Declare Scope state_scope.
Delimit Scope state_scope with state.
Notation "'dfa⟦' s '⟧'" := (tDfaDenote s) (at level 20).
Notation "'nfa⟦' s '⟧'" := (tNfaDenote s) (at level 20).
Notation "{ 'sset' T }" := {set {set T}} (only parsing): type_scope.
End StateNotations.

2
haskell/Music.hs
View File

@ -1,3 +1,5 @@
-- https://www.youtube.com/watch?v=FYTZkE5BZ-0
import qualified Data.ByteString.Lazy as BSL
import qualified Data.ByteString.Builder as BSB
import qualified Data.Foldable