Stream: Coq users

Topic: Hint for Strong Pumping Lemma


view this post on Zulip Julia Dijkstra (Dec 18 2023 at 16:35):

I am really stuck on of the Star Append case for the strong version of the pumping lemma from logic foundations. Do you maybe have a hint for me?

  Lemma pumping : forall T (re : reg_exp T) s,
  s =~ re ->
  pumping_constant re <= length s ->
  exists s1 s2 s3,
    s = s1 ++ s2 ++ s3 /\
    s2 <> [] /\
    length s1 + length s2 <= pumping_constant re /\
    forall m, s1 ++ napp m s2 ++ s3 =~ re.
Proof.
  intros T re s HM. induction HM as [
    | x
    | s1 re1 s2 re2 HM1 IH1 HM2 IH2
    | s1 re1 re2 HM IH
    | re1 s2 re2 HM IH
    | re
    | s1 s2 re HM1 IH1 HM2 IH2
  ].

(* Other Cases *)

(* Star Append *)
  - simpl in *. intros. rewrite length_app in H. destruct (length s1) eqn:Q.
    * apply length_0_nil in Q. rewrite Q. simpl. apply IH2. apply H.
    * exists [], s1, s2. simpl. split.
      + reflexivity.
      + split.
        -- unfold not. intros. rewrite <- length_0_nil in H0. rewrite Q in H0. discriminate.
        -- split.
          ** admit.
          ** intros. apply napp_star.
            ++ apply HM1.
            ++ apply HM2.
Qed.

This proof was mostly copied from my proof for the weak version. I wrote these lemmas to assist me:

Lemma length_app : forall T (s1 s2: list T), length (s1 ++ s2) = length s1 + length s2.
Lemma length_0_nil : forall T (l: list T), length l = 0 <-> l = [].

view this post on Zulip Julia Dijkstra (Dec 18 2023 at 16:38):

I figured I'd also post the proof state at the admit. I don't really see a way of proving it from here.

T : Type
s1, s2 : list T
re : reg_exp T
HM1 : s1 =~ re
HM2 : s2 =~ Star re
n : nat
Q : length s1 = S n
IH1 : pumping_constant re <= S n -> exists s2 s3 s4 : list T, s1 = s2 ++ s3 ++ s4 /\ s3 <> [ ] /\ length s2 + length s3 <= pumping_constant re /\ (forall m : nat, s2 ++ napp m s3 ++ s4 =~ re)
IH2 : pumping_constant re <= length s2 -> exists s1 s3 s4 : list T, s2 = s1 ++ s3 ++ s4 /\ s3 <> [ ] /\ length s1 + length s3 <= pumping_constant re /\ (forall m : nat, s1 ++ napp m s3 ++ s4 =~ Star re)
H : pumping_constant re <= S n + length s2

(1 / 1)
length s1 <= pumping_constant re

view this post on Zulip Paolo Giarrusso (Dec 18 2023 at 17:29):

Is it possible you chose the wrong witnesses when you run exists? You've picked your witness before invoking the induction hypothesis

view this post on Zulip Julia Dijkstra (Dec 18 2023 at 17:37):

That is what I am thinking too. I am not yet sure how to delay that until I have enough information yet though. I'm trying to work it out on paper now :sweat_smile: .

view this post on Zulip Julio Di Egidio (Dec 18 2023 at 17:54):

For the little I can see (mainly from the proof state), your proof is along different lines than mine, so I am not sure if I can help, anyway I suppose I can tell you that for the MStarApp case (and similarly in the MApp case) I have done this:

Proof.
  intros T r s Hr Hp.
  induction Hr
    as [ | x' | s1' r1' s2' r2' H1 I1 H2 I2
         | s1' r1' r2' H I | r1' s2' r2' H I
         | r' | s1' s2' r' H1 I1 H2 I2]
  ; simpl in *.
  - ... various cases ...
  - (* MStarApp *)
    assert (Hd :
      pumping_constant r' <= length s1' \/
      length s1' < pumping_constant r').
    {
      apply or_comm.
      apply lt_ge_cases.
    }
    destruct Hd as [Hd | Hd].
    + (* MStarApp[L] *) ...
    + (* MStarApp[R] *) ...

view this post on Zulip Julia Dijkstra (Dec 19 2023 at 23:26):

I managed to finish my proof :smile: ! Do you have any comments on how this could be written more neatly/concisely?

Lemma pumping : forall T (re : reg_exp T) s,
  s =~ re ->
  pumping_constant re <= length s ->
  exists s1 s2 s3,
    s = s1 ++ s2 ++ s3 /\
    s2 <> [] /\
    length s1 + length s2 <= pumping_constant re /\
    forall m, s1 ++ napp m s2 ++ s3 =~ re.
Proof.
  intros T re s HM. induction HM as [
    | x
    | s1 re1 s2 re2 HM1 IH1 HM2 IH2
    | s1 re1 re2 HM IH
    | re1 s2 re2 HM IH
    | re
    | s1 s2 re HM1 IH1 HM2 IH2
  ].
  (* Empty String *)
  - simpl. intros. inversion H.
  (* Char *)
  - simpl. intros. inversion H. inversion H1.
  (* Append *)
  - simpl. intros. assert (length s1 < pumping_constant re1 \/ length s1 >= pumping_constant re1) as [G|G].
    * apply lt_ge_cases.
    * rewrite length_app in H. apply n_lt_m__n_le_m in G. apply le_trans with (o:=pumping_constant re1 + length s2) in H.
      + apply plus_le_compat_l in H. apply IH2 in H as [p1 [p2 [p3 [H1 [H2 [H3 H4]]]]]]. exists (s1 ++ p1), p2, p3. split.
        -- rewrite <- app_assoc. rewrite H1. reflexivity.
        -- split.
          ** apply H2.
          ** split.
            ++ rewrite length_app. rewrite <- add_assoc. apply le_decompose. split.
              --- apply G.
              --- apply H3.
            ++ intros. rewrite <- app_assoc. apply MApp.
              --- apply HM1.
              --- apply H4.
      + apply le_decompose. split.
        -- apply G.
        -- reflexivity.
    * apply IH1 in G as [p1 [p2 [p3 [H1 [H2 [H3 H4]]]]]]. exists p1, p2, (p3 ++ s2). split.
      + rewrite H1. repeat rewrite <- app_assoc. reflexivity.
      + split.
        -- apply H2.
        -- split.
          ** apply le_plus_trans. apply H3.
          ** intros. repeat rewrite app_assoc. apply MApp.
            ++ rewrite <- app_assoc. apply H4.
            ++ apply HM2.
  (* Union Left *)
  - simpl. intros. apply plus_le in H as [H _]. apply IH in H as [p1 [p2 [p3 [H1 [H2 [H3 H4]]]]]].
    exists p1, p2, p3. split.
    * apply H1.
    * split.
      + apply H2.
      + split.
        -- apply le_plus_trans.  apply H3.
        -- intros. apply MUnionL. apply H4.
  (* Union Right *)
  - simpl. intros. apply plus_le in H as [_ H]. apply IH in H as [p1 [p2 [p3 [H1 [H2 [H3 H4]]]]]].
    exists p1, p2, p3. split.
    * apply H1.
    * split.
      + apply H2.
      + split.
        -- rewrite (add_comm (pumping_constant re1)). apply le_plus_trans. apply H3.
        -- intros. apply MUnionR. apply H4.
  (* Star None *)
  - simpl. intros. inversion H as [G|G]. apply pumping_constant_0_false in G. destruct G.
  (* Star Append *)
  - simpl in *. intros. rewrite length_app in H. assert (length s1 < pumping_constant re \/ length s1 >= pumping_constant re) as [G|G].
    * apply lt_ge_cases.
    * destruct (length s1) eqn:Q.
      + simpl in H. apply IH2 in H as [p1 [p2 [p3 [H1 [H2 [H3 H4]]]]]]. apply length_0_nil in Q. subst s1. exists p1, p2, p3. split.
        -- simpl. rewrite <- H1. reflexivity.
        -- split.
          ** apply H2.
          ** split.
            ++ apply H3.
            ++ apply H4.
      + exists [], s1, s2. split.
        -- simpl. reflexivity.
        -- split.
          ** unfold not. intros. apply length_0_nil in H0. rewrite Q in H0. discriminate.
          ** simpl. split.
            ++ rewrite Q. apply n_lt_m__n_le_m. apply G.
            ++ intros. apply napp_star.
              --- apply HM1.
              --- apply HM2.
    * apply IH1 in G as [p1 [p2 [p3 [H1 [H2 [H3 H4]]]]]]. exists p1, p2, (p3 ++ s2). split.
      + rewrite H1. repeat rewrite <- app_assoc. reflexivity.
      + split.
        -- apply H2.
        -- split.
          ** apply H3.
          ** intros. repeat rewrite app_assoc. apply MStarApp.
            ++ rewrite <- app_assoc. apply H4.
            ++ apply HM2.
Qed.

Lemmas I proved and used:

Lemma length_app : forall T (s1 s2: list T), length (s1 ++ s2) = length s1 + length s2.
Lemma length_0_nil : forall T (l: list T), length l = 0 <-> l = [].
Lemma le_decompose : forall (a b c d: nat), a <= c /\ b <= d -> a + b <= c + d.

view this post on Zulip Julio Di Egidio (Dec 20 2023 at 00:11):

I don't think it is important to agonize too much polishing it, more advanced proof writing techniques are simply going to come later: in fact, IMHO, the real next level is learning how to write effective proof automation, as with auto. Anyway, that said:

At this point your proof matches mine almost 1-to-1, although mine remains slightly simpler/cleaner, in particular the MStarApp case. A couple of differences I can see: 1) at least in one place I was able to prove the case with a simple lia; 2) I have never had to destruct on length _.

More than that, I guess I should simply send you my code in a private message if you want. I won't publish it here and I'd invite you to please delete yours as well (you cannot actually delete the post: just edit and remove the code, that should be enough), since solutions to the exercises in Software Foundations are supposed not to be published...

view this post on Zulip Julia Dijkstra (Dec 20 2023 at 00:19):

What is lia? I don't think I have seen it yet.

view this post on Zulip Julio Di Egidio (Dec 20 2023 at 00:44):

You are right, sorry, Lia is introduced later in LF, in the "Simple Imperative Programs (Imp)" chapter: https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html#lab377
I must have had been looking at other code and documentation at that point... though, as I said, I don't think that matters much: IMO the main lesson of those exercises is that one cannot just brute-force proofs, and then getting into the habit of thinking what terms to actually construct...

FYI, Lia is also documented in the refman here: https://coq.inria.fr/doc/V8.18.0/refman/addendum/micromega.html#lia-a-tactic-for-linear-integer-arithmetic


Last updated: Jun 13 2024 at 21:01 UTC