Как привести индукцию к другому аргументу? - PullRequest
Новая
       18

Как привести индукцию к другому аргументу?

0 голосов
/ 03 мая 2019

Вот решение проблемы, которую я сделал в Idris. 

data Subseq : List a -> List a -> Type where
    Base : Subseq [] []
    There : Subseq seq l -> Subseq seq (x :: l)
    Here : Subseq seq l -> Subseq (x :: seq) (x :: l)

subseq_trans : Subseq a b -> Subseq b c -> Subseq a c
subseq_trans x Base = x
subseq_trans x (There z) = There (subseq_trans x z)
subseq_trans (There x) (Here z) = There (subseq_trans x z)
subseq_trans (Here x) (Here z) = Here (subseq_trans x z)

С Coq, однако я не знаю, как это доказать.Вчера эта проблема заняла у меня несколько часов, прежде чем я отключил автопилот и попытался неформально рассуждать.Вот как далеко я зашёл. 

Inductive subseq : list nat -> list nat -> Prop :=
  | subseq_base : subseq [] []
  | subseq_there : forall seq l x, subseq seq l -> subseq seq (x :: l)
  | subseq_here : forall seq l x, subseq seq l -> subseq (x :: seq) (x :: l).

Theorem subseq_trans : forall l1 l2 l3,
  subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3.
Proof.
intros.
induction H0.
- apply H.
- apply subseq_there, IHsubseq, H.
- inversion H.
  + apply subseq_there, IHsubseq, H3.
  + 

1 subgoal
l1, seq : list nat
x : nat
H : subseq l1 (x :: seq)
l : list nat
H0 : subseq seq l
IHsubseq : subseq l1 seq -> subseq l1 l
seq0, l0 : list nat
x0 : nat
H3 : subseq seq0 seq
H2 : x0 :: seq0 = l1
H1 : x0 = x
H4 : l0 = seq
______________________________________(1/1)
subseq (x :: seq0) (x :: l)

Чтобы решить этот последний случай, мне действительно нужно, чтобы индуктивная гипотеза была subseq seq0 seq -> subseq seq0 l.Это позволило бы мне представить эквивалент доказательства Идриса.Я застрял.

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

1 Ответ

1 голос
/ 03 мая 2019 
Theorem subseq_trans : forall l1 l2 l3,
  subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3.
Proof.
intros.
generalize dependent l1.
induction H0.
- intros. apply H.
- intros. apply subseq_there, IHsubseq, H.
- intros. inversion H.
  + apply subseq_there, IHsubseq, H3.
  + apply subseq_here, IHsubseq, H3.
Qed.

Я сделал ошибку. Я не думал, что обобщение l1 будет работать здесь по какой-то причине, так как оно было связано с l2 в другой предпосылке. С этим небольшим пониманием решение становится простым.

...