Hi. I had been trying to use the `exists`

tactic like

```
From mathcomp Require Import all_ssreflect.
Goal forall w:seq nat,
exists w1 w2: seq nat, w = (w1 ++ w2)%list /\ (length w)==0%nat -> w = [::].
Proof.
move=>w.
exists [], [].
(*
Syntax error: [ltac_use_default] expected after [tactic] (in [tactic_command]).
*)
```

but that gave error.

A version without ssreflect seems happy with this though:

```
Require Import List.
Import ListNotations.
Goal forall w:list nat,
exists w1 w2: list nat, w = (w1 ++ w2)%list /\ (length w)=0%nat -> w = [].
Proof.
intro w.
exists [], [].
(*
1 subgoal
w : list nat
========================= (1 / 1)
w = [] ++ [] /\ length w = 0 -> w = []
*)
```

I guess the ssreflect way of doing this is different.

How are situations like this usually handled?

The empty list in `[::]`

. Also, you can use `exists {::}. exists [::].`

to instantiate `w1`

and `w2`

.

Ah..

How can we instantiate `w1`

and `w2`

in this modified case:

```
Goal forall w:seq nat,
(exists w1 w2: seq nat, w = (w1 ++ w2)%list /\ (length w)==0%nat) -> w = [::].
Proof.
move=>w.
exists [::], [::].
(*
Not the right number of missing arguments (expected 0).
*)
```

This is basic coq, but I couldn't figure it out.

```
Goal forall w:seq nat,
(exists w1 w2: seq nat, w = (w1 ++ w2)%list /\ (length w)==0%nat) -> w = [::].
Proof.
move=> w [w1 [w2]].
```

Here, `w1`

and `w2`

are provided to you, since the existentially quantified proposition is now an hypothesis in your goal.

I got here:

```
Goal forall w:seq nat,
(exists w1 w2: seq nat, w = (w1 ++ w2)%list /\ (length w)==0%nat) -> w = [::].
Proof.
move=>w.
move=>H.
case: H.
move=>x.
move=>H.
case: H.
move=>x0.
case.
move=>H1 H2.
rewrite -List.length_zero_iff_nil.
(*
1 subgoal
w, x, x0 : seq nat
H1 : w = (x ++ x0)%list
H2 : length w == 0
========================= (1 / 1)
length w = 0
*)
```

which feels like a not-so-great way of going about it.

Pierre Jouvelot said:

Here,

`w1`

and`w2`

are provided to you, since the existentially quantified proposition is now an hypothesis in your goal.

Thanks!

```
Goal forall w:seq nat,
(exists w1 w2: seq nat, w = (w1 ++ w2)%list /\ (length w)==0%nat) -> w = [::].
Proof.
move=> w [w1 [w2]].
case.
by case: w; case: w1; case: w2.
Qed.
```

Another proof could be

```
Goal forall w:seq nat,
(exists w1 w2: seq nat, w = (w1 ++ w2)%list /\ (size w)==0%nat) -> w = [::].
Proof.
move=> w [w1 [w2]] [_].
rewrite size_eq0.
exact/eqP.
Qed.
```

Note that ssreflect uses `size`

instead of `length`

with sequences.

Pierre Jouvelot said:

Here,

`w1`

and`w2`

are provided to you, since the existentially quantified proposition is now an hypothesis in your goal.

How would we handle a goal like this?

```
Goal exists w1 w2: seq nat,
w1++w2 = [3].
Proof.
```

Is doing `exists`

/ `eexists`

the only way?

You can indeed use `exists`

, as in:

```
Goal exists w1 w2: seq nat,
w1++w2 = [:: 3].
Proof. by exists [::]; exists [:: 3]. Qed.
```

Of course, you could also sometimes prove an existential goal such as this one via a more general lemma, such as:

```
Goal exists w1 w2: seq nat,
w1++w2 = [:: 3].
Proof.
have f : forall l, exists w1 w2: seq nat, w1++w2 = l.
by move=> l; exists [::]; exists l.
exact: (f [:: 3]).
Qed.
```

If you are dealing with finite types (see fintype.v), you can also sometimes use contraposition, which would replace your exists with foralls.

Last updated: Jun 22 2024 at 15:01 UTC