Как сделать рекурсивный вызов с уменьшающимся аргументом?

Question

Inductive bar {X : Type} : list X -> Prop :=
  | bar_nil : bar []
  | bar_fst : forall x l, bar (rev l ++ l) -> bar (rev l ++ [x] ++ l)
  | bar_snd : forall x l, bar (rev l ++ [x] ++ l) -> bar (rev l ++ [x; x] ++ l).

Axiom bar_surround :
  forall X x (l : list X),
  bar l -> bar ([x] ++ l ++ [x]).

Inductive list_last {X : Type} : list X -> Prop :=
  | ll_nil : list_last []
  | ll_snoc : forall l x, list_last l -> list_last (l ++ [x]).

Axiom ll_app :
  forall X (a b : list X),
  list_last a -> list_last b -> list_last (a ++ b).

Axiom ll_from_list :
  forall {X} (l : list X),
  list_last l.

Axiom app_head_eq :
  forall X (a b c : list X),
  a ++ c = b ++ c -> a = b.

Theorem foo :
  forall X (l: list X), l = rev l -> bar l.
Proof.
intros.
induction l.
- constructor.
- assert (Hll := ll_from_list l).
  inversion Hll.
  + apply (bar_fst x []). apply bar_nil.
  + rewrite <- H1 in H.
    simpl in H.
    rewrite rev_app_distr in H.
    rewrite <- app_assoc in H.
    simpl in H.
    inversion H.
    apply app_head_eq in H4.
    apply bar_surround.

1 subgoal
X : Type
x : X
l, l0 : list X
x0 : X
H : x :: l0 ++ [x0] = x0 :: rev l0 ++ [x]
IHl : l = rev l -> bar l
Hll : list_last l
H0 : list_last l0
H1 : l0 ++ [x0] = l
H3 : x = x0
H4 : l0 = rev l0
______________________________________(1/1)
bar l0

Я только в шаге от решения этого упражнения, но я не знаю, как сделать вводный шаг. Обратите внимание, что IHl здесь бесполезен, и замена индукции на l на индукцию на Hll приведет к аналогичной проблеме. В обоих случаях индуктивная гипотеза будет ожидать вызова с уменьшением на один шаг, а мне нужно два - один с элементом, взятым как из начала, так и из конца списка с обеих сторон равенства.

Учтите, что тип функции, которую я пытаюсь доказать, - forall X (l: list X), l = rev l -> bar l, и у меня здесь l0 = rev l0 -> bar l0 в цели. l0 - уменьшенный аргумент, что делает рекурсивный вызов безопасным.

Что мне здесь делать?

Answer 1

Вы можете доказать следующий индуктивный предикат:

Inductive delist {A : Type} : list A -> Prop :=
| delist_nil : delist []
| delist_one x : delist [x]
| delist_cons x y l : delist l -> delist (x :: l ++ [y])
.

Theorem all_delist {A} : forall xs : list A, delist xs.

Тогда в вашей последней теореме индукция по delist xs будет разбита на нужные вам случаи.

---

Другое решение заключается в сильной индукции по длине списка:

Lemma foo_len X : forall (n : nat) (l: list X), length l <= n -> l = rev l -> bar l.
Proof.
  induction n.
  (* Nat.le_succ_r from the Arith module is useful here *)
  ...
Qed.

(* Final theorem *)
Theorem foo X : forall (l : list X), l = rev l -> bar l.
Proof.
  intros; apply foo_len; auto.
Qed.

Это более распространенный и систематический принцип, чем delist, но вам нужно будет работать больше, чем приведенный выше специальный индуктивный тип, чтобы использовать гипотезу индукции в основном доказательстве.

Answer 2

Вот как реализовать первую часть того, что было предложено в другом ответе.Я могу подтвердить, что с этим решить упражнение довольно просто.Тем не менее, мне интересно, как решить вышеизложенное с помощью простой индукции.Необходимость реализовать delist и его функции сложнее, чем я бы предпочел.

Inductive delist {A : Type} : list A -> Prop :=
| delist_nil : delist []
| delist_one x : delist [x]
| delist_wrap x y l : delist l -> delist (x :: l ++ [y]).

Theorem delist_cons {A} :
  forall x (l : list A),
  delist l -> delist (x :: l).
Proof.
intros.
generalize dependent x.
induction H; intros.
- constructor.
- replace [x; x0] with (x :: [] ++ [x0]).
  2 : { reflexivity. }
  + apply delist_wrap with (l := []). constructor.
- replace (x0 :: x :: l ++ [y]) with (x0 :: (x :: l) ++ [y]).
  2 : { reflexivity. }
  constructor.
  apply IHdelist.
Qed.

Theorem delist_from_list {A} : 
  forall l : list A,
  delist l.
Proof.
induction l.
- constructor.
- assert (ll := ll_from_list l).
  destruct ll.
  + constructor.
  + apply delist_cons. assumption.
Qed.