## Stream: Beginner Questions

### Topic: How to prove the complement automaton in below way

#### Hongjian Jiang (Jun 05 2023 at 14:29):

I am trying to construct the complement regexp.

First, I construct the NFA automaton, the definition of neg1 automaton takes an automaton and changes its accepts states. I thought it's a straightforward idea.

However, I was stuck by the last lemma, `accepts_neg1`. Any help would be appreciated.

``````type_synonym ('a,'s) na = "'s * 'a set * ('a ⇒'s ⇒ 's set) * ('s ⇒ bool)"

primrec delta :: "('a,'s)na ⇒ 'a list ⇒ 's ⇒ 's set" where
"delta A []    p = {p}" |
"delta A (a#w) p = Union(delta A w ` next A a p)"

definition
accepts :: "('a,'s)na ⇒ 'a list ⇒ bool" where
"accepts A w = (∃q ∈ delta A w (start A). fin A q)"

definition
step :: "('a,'s)na ⇒ 'a ⇒ ('s * 's)set" where
"step A a = {(p,q) . q : next A a p}"

primrec steps :: "('a,'s)na ⇒ 'a list ⇒ ('s * 's)set" where
"steps A [] = Id" |
"steps A (a#w) = step A a  O  steps A w"

lemma steps_append[simp]:
"steps A (v@w) = steps A v  O  steps A w"

lemma in_steps_append[iff]:
"(p,r) : steps A (v@w) = ((p,r) : (steps A v O steps A w))"
apply(rule steps_append[THEN equalityE])
apply blast
done

lemma delta_conv_steps: "⋀p. delta A w p = {q. (p,q) : steps A w}"
by(induct w)(auto simp:step_def)

lemma accepts_conv_steps:
"accepts A w = (∃q. (start A,q) ∈ steps A w ∧ fin A q)"

type_synonym 'a bitsNA = "('a, nat list)na"

definition
neg1 :: "'a bitsNA ⇒ 'a bitsNA" where
"neg1 = (λ(ql,vl1,dl,fl). (ql, vl1, dl, λs. ¬ fl s))"

lemma fin_neg1[iff]:
"⋀L. fin (neg1 L) q = (¬ fin L q)"
done
lemma start_neg1[iff]:
"⋀L. start (neg1 L) = start L"
done
lemma step_neg1[iff]:
"⋀L p. (p, q)∈ step (neg1 L) a = ((p, q) ∈ step L a)"
done

lemma steps_neg1[iff]:
"⋀L p. (p, q)∈ steps (neg1 L) w = ((p, q) ∈ steps L w)"
apply(induct w)
apply simp
apply simp
apply force
done

lemma accepts_neg1: accepts (neg1 L) w ⟹ (¬ accepts L w)"
apply(induct w)
apply simp
sorry
``````

#### Hongjian Jiang (Jun 05 2023 at 14:35):

I just think the way is to universal parameter in the state q, but I don't know how to solve it.

#### Maximilian Schäffeler (Jun 05 2023 at 14:55):

What is you definition of `next`?

#### Hongjian Jiang (Jun 05 2023 at 15:08):

``````definition start :: "'a * 'b * 'c * 'd ⇒ 'a" where "start A = fst A"
definition alp :: "'a * 'b * 'c * 'd ⇒ 'b" where "alp A = fst(snd(A))"
definition "next" :: "'a * 'b * 'c * 'd ⇒ 'c" where "next A = fst(snd(snd(A)))"
definition fin :: "'a * 'b * 'c * 'd ⇒ 'd" where "fin A = snd(snd(snd(A)))"
``````

#### Mathias Fleury (Jun 05 2023 at 17:49):

Please remove the useless `⋀L p.`

#### Mathias Fleury (Jun 05 2023 at 17:50):

And the proof goes through once you realize that you have to generalize over `p` and `q`
wrong lemma

#### Hongjian Jiang (Jun 05 2023 at 18:22):

Once remove the L and p, the steps lemma couldn't pass easily

#### Mathias Fleury (Jun 05 2023 at 18:23):

I though a little bit more about it and it is unclear to me if this holds because NFA means that you could have two paths one reaching a final a state and one reaching a non-final state. So negation would still accept the word.

`````` lemma "accepts (neg1 L) [w] ⟹ (¬ accepts L [w])"
(*
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:
L = ([], {}, λx xa. {[0], []}, UNIV - {[]})
w = a⇩1
*)
``````

#### Mathias Fleury (Jun 05 2023 at 18:23):

Not sure if the counter-example is correct

#### Hongjian Jiang (Jun 05 2023 at 18:28):

My NFA includes the initial state, alphabet, transition states and accept states.

The transition rules take one alphabet and one state, the state is denoted in a list, then return a list set, like the atom automaton below,

``````definition
"atom"  :: "'a ⇒ 'a set ⇒ 'a bitsNA" where
"atom a vs = ([2],vs,
λb s. if s=[2] ∧ b=a ∧ a : vs then {[3]} else {[1]},
λs. case s of [] ⇒ False | left#s ⇒ (left#s) = [3])"
``````

#### Hongjian Jiang (Jun 05 2023 at 18:29):

There is no counterexample in my script.

``````Testing conjecture with Quickcheck-exhaustive...
Quickcheck ran out of time
Quickcheck found no counterexample.
``````

I don't know exactly.

#### Mathias Fleury (Jun 05 2023 at 18:30):

I replace the path w by a path of length 1 `[w]`

#### Hongjian Jiang (Jun 05 2023 at 18:34):

Ahh, I see. From the counterexample, the negation of L cound just accept empty list. That's the inital state and any input character.

Last updated: Sep 11 2024 at 16:22 UTC