применение функции с другим полем

Есть ли способ применить гипотез к нашей цели в 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».

Инструкции

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...*)

Итак ... Как я могу решить эту проблему?


coq
person Damiii    schedule 23.05.2014    source источник

Ответы (1)


arrow_upward
0
arrow_downward

a :: l1 отличается от l1, поэтому вы не сможете использовать эту гипотезу.

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.

Вы также ввели слишком много переменных перед индукцией. Это сделало гипотезу индукции менее общей.

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.
person Community    schedule 23.05.2014
comment
Святое дерьмо! xD Я никогда не видел эту функцию info_eauto: O - person Damiii; 24.05.2014
comment
Не волнуйтесь слишком сильно. eauto немного медленный. - person ; 24.05.2014
comment
Я не могу применить: info_eauto с *. получение сообщения об ошибке: Синтаксическая ошибка: '.' или "..." ожидается после [тактика: тактика] (в [subgoal_command]). - person Damiii; 24.05.2014
comment
Вы включили части Require Import, Conjecture и Hint Resolve? eauto - это форма автоматического доказательства теорем. Но в интуиционистской логике зависимого типа более высокого порядка искать доказательства труднее, чем в классической нетипизированной логике первого порядка. - person ; 24.05.2014
comment
хммм, не можем ли мы решить это без автоматической теоремы? Потому что мне бы очень хотелось это увидеть ... Я боюсь, что моему учителю это не понравится (если сделает это автоматически) на экзаменационном тесте - person Damiii; 24.05.2014
comment
Не info_eauto выводит сообщение? Это сообщение - шаги, которые info_eauto предприняли, чтобы доказать вашу цель. Вы можете заменить часть info_eauto содержимым этого сообщения. Между прочим, Conjectures - это факты, которые я позволил себе предположить. Они до сих пор не доказаны. - person ; 24.05.2014
comment
Правильно. (Комментарии должны состоять из 15 символов.) - person ; 24.05.2014