I'm trying to prove the theorem in CoqIDE.

To me this definition**PRIFIKS**

and need to write dokazateljstvo for theorem**Dokaz1**

The problem is that whatever tactics I didn't isparitel I can't complete dokazateljstvo. How to complete dokazateljstvo or where I made a mistake?

To me this definition

```
Inductive PRIFIKS {A:Type}: list A -> list A -> Prop :=
| pri_nul : forall (l : list A), nil PRIFIKS l
| pri_g : forall x:A, forall (l1 l2 : list A), PRIFIKS l1 l2 -> PRIFIKS (x::l1) (x::l2).
```

and need to write dokazateljstvo for theorem

`Theorem Dokaz1: forall A l1 l2, @PRIFIKS A l1 l2 -> exists l3, l2 = l3 ++ l1.`

The problem is that whatever tactics I didn't isparitel I can't complete dokazateljstvo. How to complete dokazateljstvo or where I made a mistake?

```
Theorem Dokaz1: forall A l1 l2, @PRIFIKS A l1 l2 -> exists l3, l2 = l3 ++ l1.
Proof.
intros.
destruct l1.
- exists l2.
reflexivity.
- exists [].
assert (H2: (a::l1) = [] -> PRIFIKS [] l2).
* intros.
apply pri_nul.
* assert (H3: PRIFIKS [] l2).
apply pri_nul.
```

asked April 8th 20 at 02:36

1 answer

answered on April 8th 20 at 02:38

Lists usually need induction to prove it.

Theorem Dokaz1: forall A l1 l2, @PRIFIKS A l1 l2 -> exists l3, l2 = l3 ++ l1.

Proof.

intros.

induction H.

- l exists.

reflexivity.

- destruct IHPRIFIKS.

exists x0.

simpl.

rewrite H0.

reflexivity.

Qed.

Theorem Dokaz1: forall A l1 l2, @PRIFIKS A l1 l2 -> exists l3, l2 = l3 ++ l1.

Proof.

intros.

induction H.

- l exists.

reflexivity.

- destruct IHPRIFIKS.

exists x0.

simpl.

rewrite H0.

reflexivity.

Qed.

Find more questions by tags Programming languages