Использование Определение Coq Равенства

Question

У меня есть определение равенства:

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

и подцель:

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

и когда я пытаюсь применить или переписать reglang_eq, я получаю сообщение об ошибке. Если я правильно понимаю, это должно быть просто потому, что я не знаю правильного синтаксиса, но я все больше расстраиваюсь, потому что не смог найти документацию, которую я могу понять. (Несмотря на то, сколько месяцев я спотыкался, проверяя материал о RegularLanguages.)

Любая помощь приветствуется, спасибо.

Answer 1

Если Concat действительно является конструктором языка, вы не сможете доказать свою цель. Там две проблемы, происходящие здесь:

1. Когда вы записали reglang_eq, вы определили предложение, но не дают никаких доказательств этого. То, что вы хотите сделать, это заменить: = на двоеточие (:), чтобы вы могли войти в режим доказательства и обосновать свои претензии. Когда вы это сделаете и закончите свое доказательство, вы сможете применить его. Но если вы попытаетесь сделать это, вы попадете во второй выпуск ...

2. В Coq конструкторы всегда не пересекаются. Это означает, что единственный способ, которым ваше уравнение может быть истинным, - это когда r = EmptyStr A (предполагая, что последний также является конструктором). Здесь вы, вероятно, хотите определить другое представление для регулярных языков, чтобы конкатенация и пустой язык стали определяемыми операциями (I.e.функциями, определенными внутри логики).