У меня есть определенные индуктивные типы:
Inductive InL (A:Type) (y:A) : list A -> Prop :=
| InHead : forall xs:list A, InL y (cons y xs)
| InTail : forall (x:A) (xs:list A), InL y xs -> InL y (cons x xs).
Inductive SubSeq (A:Type) : list A -> list A -> Prop :=
| SubNil : forall l:list A, SubSeq nil l
| SubCons1 : forall (x:A) (l1 l2:list A), SubSeq l1 l2 -> SubSeq l1 (x::l2)
| SubCons2 : forall (x:A) (l1 l2:list A), SubSeq l1 l2 -> SubSeq (x::l1) (x::l2).
Теперь я должен доказать серию свойств того индуктивного типа, но я продолжаю застревать.
Lemma proof1: forall (A:Type) (x:A) (l1 l2:list A), SubSeq l1 l2 -> InL x l1 -> InL x l2.
Proof.
intros.
induction l1.
induction l2.
exact H0.
Qed.
Может кто-то помогать мне совершенствоваться.
На самом деле, проще выполнить индукцию непосредственно по оценке SubSet. Однако вы должны быть как можно более общими, поэтому вот мой совет:
Lemma proof1: forall (A:Type) (x:A) (l1 l2:list A),
SubSeq l1 l2 -> InL x l1 -> InL x l2.
(* first introduce your hypothesis, but put back x and In foo
inside the goal, so that your induction hypothesis are correct*)
intros.
revert x H0. induction H; intros.
(* x In [] is not possible, so inversion will kill the subgoal *)
inversion H0.
(* here it is straitforward: just combine the correct hypothesis *)
apply InTail; apply IHSubSeq; trivial.
(* x0 in x::l1 has to possible sources: x0 == x or x0 in l1 *)
inversion H0; subst; clear H0.
apply InHead.
apply InTail; apply IHSubSeq; trivial.
Qed.
«инверсия» - это тактика, которая проверяет индуктивный член и дает вам все возможные способы построить такой термин !! без какой-либо гипотезы индукции! ! Это только дает вам конструктивные предпосылки.
Вы могли бы сделать это непосредственно индукцией по l1, а затем по l2, но вам придется вручную построить правильный экземпляр инверсии, потому что ваша гипотеза индукции была бы очень слабой.
Надеюсь, это поможет, V.