应用不同领域的功能 [英] applying a function with different field

问题描述

有没有办法对我们在Coq中的目标应用假设？

Is there a way, to apply an hypotesis to our goal in Coq ?

例如：

假设：

1 subgoal
a : nat
l1 : list nat
l2 : list nat
H : Prefix (a :: l1) l2
IHl1 : Prefix l1 l2 -> sum l1 <= sum l2

目标

______________________________________(1/1)
sum (a :: l1) <= sum l2

我知道，如果我可以做到：应用IHl1，我可以得到像Prefix（a :: l1）l2这样的结果，之后我将能够做一个假设！
但我无法执行该申请，因为它给了我这个错误：
错误：不可能将 sum l1< = sum l2与 sum（a :: l1）<统一; = sum l2。

I know that if i could do : apply IHl1 , i could have a result like Prefix (a::l1) l2 and after i will be able to do an assumption ! But i can't do the apply because it's giving me this error : Error: Impossible to unify "sum l1 <= sum l2" with "sum (a :: l1) <= sum l2".

说明

Fixpoint

Fixpoint sum (l: list nat) : nat := match l with
  | nil => 0
  | a::t => a + sum t
  end.

引理

Lemma parte2_1_c : forall l1 l2, Prefix l1 l2 -> sum l1 <= sum l2.
Proof.
intros.
induction l1.
simpl.
SearchAbout(_<=_).
apply le_0_n.
SearchAbout(sum).
(*must continue but do not know how to do it...*)

所以...我怎么能解决这个问题？

So... How may i able to solve this ?

推荐答案

a :: l1 与 l1 不同，因此您将无法使用该假设。

a :: l1 is different from l1 so you won't be able to use that hypothesis.

Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.

Definition Prefix : forall {t1}, list t1 -> list t1 -> Prop := fun _ l1 l2 =>
  exists l3, l1 ++ l3 = l2.

Conjecture C1 : forall t1 (x1 : t1) l1 l2, Prefix (x1 :: l1) l2 -> exists l3, l2 = x1 :: l3.
Conjecture C2 : forall n1 n2 n3, n1 <= n2 -> n3 + n1 <= n3 + n2.
Conjecture C3 : forall t1 (x1 : t1) l1 l2, Prefix (x1 :: l1) (x1 :: l2) -> Prefix l1 l2.
Hint Resolve C1 C2 C3.

Lemma parte2_1_c : forall l1 l2, Prefix l1 l2 -> sum l1 <= sum l2.
Proof.
intros.
induction l1.
simpl.
SearchAbout(_<=_).
apply le_0_n.
assert (H3 : exists l3, l2 = a :: l3) by info_eauto with *.
destruct H3.
subst.
simpl in *.
Abort.

在进行归纳之前，您还引入了太多变量。

You also introduced too many variables before performing induction. That made the induction hypothesis less general.

Lemma parte2_1_c : forall l1 l2, Prefix l1 l2 -> sum l1 <= sum l2.
Proof.
intros l1.
induction l1.
info_eauto with *.
intros.
assert (H3 : exists l3, l2 = a :: l3) by info_eauto with *.
destruct H3.
subst.
simpl in *.
info_eauto with *.
Qed.

这篇关于应用不同领域的功能的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！