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 = [].
```

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
```

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

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: .

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] *) ...
```

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.
```

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

What is `lia`

? I don't think I have seen it yet.

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