1
我有一个场景,我想证明一个引理,包括一些字符串和列表变量。可能它需要'归纳',但任何人都可以帮助我证明下面给出的引理。如果需要其他代码,我也可以提供。证明 - Coq - 我需要感应吗?
Definition DLVRI (IA IT : string)
(FA ICL FCL IUL FUL FTL : strlist) : bool :=
match (TestA IA FA),
(TestC ICL FCL),
(TestD IT IUL FUL FTL) with
| true, true, true => true
| _ , _ , _ => false
end.
(**
Lemma TestDL : forall (IA IT : string),
forall (FA ICL FCL IUL FUL FTL : strlist),
(TestA IA FA) = true /\
(TestC ICL FCL) = true /\
(TestD IT IUL FUL FTL) = true.
Proof.
*)
(* OR *)
Lemma TestDL : forall (IA IT : string),
forall (FA ICL FCL IUL FUL FTL : strlist),
(TestA IA FA) = true /\
(TestC ICL FCL) = true /\
(TestD IT IUL FUL FTL) = true
-> DLVRI IA IT FA ICL FCL IUL FUL FTL = true.
它的帮助很大。谢谢罗伯特。 – Khan