Stream: Coq users

Topic: exists with ssreflect


view this post on Zulip Julin Shaji (Oct 27 2023 at 08:06):

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?

view this post on Zulip Pierre Jouvelot (Oct 27 2023 at 08:16):

The empty list in [::]. Also, you can use exists {::}. exists [::]. to instantiate w1 and w2.

view this post on Zulip Julin Shaji (Oct 27 2023 at 08:31):

Ah..

view this post on Zulip Julin Shaji (Oct 27 2023 at 08:33):

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.

view this post on Zulip Pierre Jouvelot (Oct 27 2023 at 08:48):

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.

view this post on Zulip Julin Shaji (Oct 27 2023 at 08:48):

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.


view this post on Zulip Julin Shaji (Oct 27 2023 at 08:50):

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.

view this post on Zulip Pierre Jouvelot (Oct 27 2023 at 08:54):

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 lengthwith sequences.

view this post on Zulip Julin Shaji (Nov 06 2023 at 13:14):

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?

view this post on Zulip Pierre Jouvelot (Nov 06 2023 at 13:37):

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