applying a function with different field

Question

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

For example:

Hypothesis:

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

Goal

______________________________________(1/1)
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".

Instructions

Fixpoint

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

Lemma

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 ?

Unknown Unknown · Accepted Answer · 2014-05-23T20:13:32

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.

applying a function with different field

1 Answers