I was solving a Coq problem below, and I'm curious how to re-use lemma itself again (as a hypothesis) for the proof.

Inductive lparen : T -> Prop :=
| leps : lparen eps
| lseq : forall (lp: T) (lp': T), lparen lp /\ lparen lp' -> lparen (LPs +++ lp +++ RPs +++ lp').

(* +++ operator concats between parenthesess *)

Lemma lparen_concat : forall l l':T, lparen l -> lparen l' -> lparen (l +++ l').
Proof.
  intros l l' IHl IHl'.
  induction IHl as [|lp lp' [IHHl IHHl']].
  - simpl.
    assumption.
  - rewrite par_assoc.
    apply lseq.
    split.
    + assumption.
    +
Qed.

The remaining goal is following lparen (lp' +++ l'), which can be proved by applying lparen_concat itself again.

l', lp, lp' : T
IHHl : lparen lp
IHHl' : lparen lp'
IHl' : lparen l'
-----------------------
lparen (lp' +++ l')

I was solving a Coq problem below, and I'm curious how to re-use lemma itself again (as a hypothesis) for the proof.

Inductive lparen : T -> Prop :=
| leps : lparen eps
| lseq : forall (lp: T) (lp': T), lparen lp /\ lparen lp' -> lparen (LPs +++ lp +++ RPs +++ lp').

(* +++ operator concats between parenthesess *)

Lemma lparen_concat : forall l l':T, lparen l -> lparen l' -> lparen (l +++ l').
Proof.
  intros l l' IHl IHl'.
  induction IHl as [|lp lp' [IHHl IHHl']].
  - simpl.
    assumption.
  - rewrite par_assoc.
    apply lseq.
    split.
    + assumption.
    +
Qed.

The remaining goal is following lparen (lp' +++ l'), which can be proved by applying lparen_concat itself again.

l', lp, lp' : T
IHHl : lparen lp
IHHl' : lparen lp'
IHl' : lparen l'
-----------------------
lparen (lp' +++ l')

• rocq-prover
• induction

Share Improve this question Follow asked Nov 16, 2024 at 17:46 LiuLiu 5733 bronze badges 2

• Reusing the lemma you are currently proving is just wrong, that's not how proofs work. So.. what are you trying to prove here, and why do you think that assuming the lemma you are trying to prove is a useful idea here? – JoJoModding Commented Nov 17, 2024 at 18:18
• From a different perspective "using the lemma you're currently proving" is how induction works, provided you use it at a "smaller" instantiation. – Naïm Favier Commented Nov 17, 2024 at 18:29

Add a comment  | 

1 Answer 1

Sorted by: Reset to default 3

Note that in your proof, when you do induction IHl as [|lp lp' [IHHl IHHl']], that IHHl and IHHl' are not induction hypotheses. The reason is that you wrote your inductive predicate in an uncanonical way, so Coq's default method for inferring the induction scheme fails.

Instead, try defining your inductive predicate like so:

Inductive lparen : T -> Prop :=
| leps : lparen eps
| lseq : forall (lp: T) (lp': T), lparen lp -> lparen lp' -> lparen (LPs +++ lp +++ RPs +++ lp').

The difference being that we give two preconditions lparen lp and lparen lp', instead of one which is a conjunction. In Coq, this is much more natural (since -> is a primitive).

Then, the induction scheme actually contains induction hypotheses, which makes the proof go through:

Lemma lparen_concat : forall l l':T, lparen l -> lparen l' -> lparen (l +++ l').
Proof.
  intros l l' Hl Hl'.
  induction Hl as [|lp lp' Hlp IHlp  Hlp' IHlp']].
  - simpl.
    assumption.
  - rewrite par_assoc.
    apply lseq.
    split.
    + assumption.
    + apply IHlp'.
Qed.

Note that Hlp corresponds to your IHHl, which you named IH even though it is not an induction hypothesis. What I named IHlp' is what was missing in your proof (and actually is an inductive hypothesis), but is here now, since Coq can now generate useful induction schemes for your predicate.

Similarly, the things introd in the first line are not induction hypotheses and thus not named IH by convention.

Finally, note that I would not say that induction is "assuming the Lemma you are proving." It "assumes" a special case of the Lemma, where one argument is strictly smaller than it is in the goal you are currently proving. This is then usually called the inductive hypothesis. So a better way of asking your question is "how do I get Coq to generate the correct inductive hypothesis here?".