Using Coq Equality Definition

Question

I have an equality definition:

Definition reglang_eq :=
  forall (A : Set)
  (r1 r2 : RegularLanguage A),
  (forall xs : List A,
    EvalInRegLang A r1 xs <-> EvalInRegLang A r2 xs)
  -> r1 = r2
.

and a subgoal:

Concat A (EmptyStr A) r = Concat A r (EmptyStr A)
(* note: Concat is a RegularLanguage constructor *)

and when I try to apply or rewrite reglang_eq, I get an error. If I understand correctly, this should simply be because I don't know the correct syntax, but I've been getting increasingly frustrated because I haven't been able to find documentation that I can understand. (Despite how many months I've been stumbling through proving stuff about RegularLanguages.)

Any help is appreciated, thanks.

Answer 1

If Concat is indeed a regular language constructor, you will not be able to prove your goal. There's two problems going on here:

1. When you wrote down reglang_eq, you defined a proposition, but didn't give any proof of it. What you want to do is to replace the := by just a colon (:), so you can enter proof mode and justify your claim. Once you do that and finish your proof, you'll be able to apply it. But if you tried to do this, you would hit the second issue...

2. In Coq, constructors are always disjoint. This means that the only way your equation can be true is when r = EmptyStr A (assuming the latter is also a constructor). What you probably want here is to define a different representation for regular languages so that concatenation and the empty language become defined operations (I.e. functions defined inside the logic).