CODEWITHSUNDEEP
listagdaunification
Steven Cheung
Steven Cheung

Reputation: 35

Agda unification over a list

I am doing a project that proves some properties of Regular expressions. Here is part of my code

⇨ here means derives, Regexp ⇨ word means a Regexp can derive a word

Σ : Set
Σ* : List Σ

Below defines the case when the concatenation e₁ ∙ e₂ can derive a word w if e₁ ⇨ w₁, e₂ ⇨ w₂ and w ≡ w₁ ++ w₂

data _⇨_ : RegExp Σ → Σ* → Set where
 con : {e₁ e₂ : RegExp Σ}{w w₁ w₂ : Σ*} → w ≡ w₁ ++ w₂ → e₁ ⇨ w₁ → e₂ ⇨ w₂ → e₁ ∙ e₂ ⇨ w

This is proving that if w ≡ w₁ ++ [] and (e₁ cannot derives w₁) than (e₁.e₂ cannot derive w)

¬e₁∙e₂⇨xs[]ˡ : {e₁ e₂ : RegExp Σ}{w w₁ : Σ*} → w ≡ w₁ ++ [] → ¬ (e₁ ⇨ w₁) → ¬ (e₁ ∙ e₂ ⇨ w)
¬e₁∙e₂⇨xs[]ˡ refl ¬e₁⇨w₁ (con {w₂ = []} refl e₁⇨w₁ e₂⇨[]) = ¬e₁⇨w₁ e₁⇨w₁

However, the refl in the con refl e₁⇨w₁ e₂⇨[] does not type check, because Agda cannot unify the w₁ in ¬e₁∙e₂⇨xs[]ˡ with the w₁ in ¬ (e₁ ∙ e₂ ⇨ w) The error message is here:

w₁ != w₂ of type List Σ
when checking that the pattern refl has type w₁ ++ [] ≡ w₂ ++ []

Any help will be appreciated!

Upvotes: 1

Views: 116

Answers (1)

effectfully
effectfully

Reputation: 12715

After you pattern-match on w ≡ w₁ ++ [] you are doomed, because w gets unified with w₁ ++ [], e₁ ∙ e₂ ⇨ w becomes e₁ ∙ e₂ ⇨ w₁ ++ [] and you can't pattern-match on that.

_++_ is not injective and w₁ ++ [] ≡ w₁' ++ w₂' doesn't entail w₁ ≡ w₁' × [] ≡ w₂' — in general there are other ways to unify those two expressions.

Your lemma is isomorphic to

¬e₁∙e₂⇨xs[]ˡ : {e₁ e₂ : RegExp Σ}{w : Σ*} → ¬ (e₁ ⇨ w) → ¬ (e₁ ∙ e₂ ⇨ w)

which looks false to me.

See here for a similar problem.

Upvotes: 3

Related Questions