如何解决长度交替追加定理和子列表长度定理的 coq 列表分配

问题描述

我正在尝试解决关于长度交替追加定理和子列表长度定理的 coq 列表分配。我想通过 coq 证明辅助来证明这些引理。我怎样才能做到这一点？

Fixpoint length (l:natlist) : nat :=
 match l with
| nil => O
| h :: t => S (length t)
end.
Fixpoint alternate (l1 l2 : natlist) : natlist :=
match l1,l2 with
| nil,nil => nil
| nil,_ => l2
| _,nil => l1
| h1 :: t1,h2 :: t2 => h1 :: h2 :: alternate t1 t2 end.
Fixpoint listfind (n: nat)(l: natlist) : bool :=
  match l with
  | nil => false
  | h :: t1 => match eqb h n with
          | true => true
          | false => listfind n t1
          end
  end.
Fixpoint sublistin (l1 l2 : natlist) : bool :=
match l1,l2 with
| _,nil => false
| nil,_ => true
| h1 :: t1,_ => (listfind h1 l2) && (sublistin t1 l2)
end.
Lemma length_alternate_right: forall l1 l2 n,length(alternate l1(n::l2))= S(length (alternate l1 l2)).
Lemma length_alternate_app: forall l1 l2,length (l1 ++ l2) = length (alternate l1 l2).
Theorem sublist in_length: forall l1 l2,sublistin l1 l2 = true -> length l1 <= length l2.

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）

coq-tactic coqide