# [tlaplus] Proof by induction invoking the SequencesInductionTail theorem

Hello all,

I have a theorem which depends on some lemmas. One of this lemmas is the fact that "the product of two sequence products is the sequence product of their concatenation". That is:

`\A s1, s2 \in Seq(Nat) : SeqProduct[s1] * SeqProduct[s2] = SeqProduct[s1 \o s2]`

where
`SeqProduct[s \in Seq(Nat)] ==  IF   s = <<>>   THEN 1  ELSE LET x  == Head(s)           xs == Tail(s)       IN x * SeqProduct[xs]`

For this one, im planning to reason inductively using the SequencesInductionTail theorem available on module SequenceTheorems (not saying this alone will suffice).
Now, having the following structure:
`LEMMA SomeLemma == \A s1, s2 \in Seq(Nat) : SeqProduct[s1] * SeqProduct[s2] = SeqProduct[s1 \o s2]  <1> DEFINE Prop(s) == \A s2 \in Seq(Nat) : SeqProduct[s] * SeqProduct[s2] = SeqProduct[s \o s2]  <1> SUFFICES \A s1 \in Seq(Nat) : Prop(s1) OBVIOUS    <1>1. Prop(<<>>) PROOF OMITTED  <1>2. \A s \in Seq(Nat) : (s # << >>) /\ Prop(Tail(s)) => Prop(s) PROOF OMITTED    <1> HIDE DEF Prop  <1>3. QED     BY <1>1, <1>2, SequencesInductionTail`

Ignoring now <1>1 and <1>2, for the high level part i was expecting TLAPS to prove the final step <1>3 and it couldn't.
The proof obligation generated is:
`ASSUME Prop(<<>>) ,       \A s \in Seq(Nat) : s # <<>> /\ Prop(Tail(s)) => Prop(s) ,       ASSUME NEW CONSTANT S,              NEW CONSTANT P(_),              P(<<>>) ,              \A s \in Seq(S) : s # <<>> /\ P(Tail(s)) => P(s)        PROVE  \A s \in Seq(S) : P(s) PROVE  \A s1 \in Seq(Nat) : Prop(s1)`

which looks reasonable to me. Also tried the ASSUME ... PROVE form, but the result is the same.

Im missing something here to correctly invoke SequencesInductionTail ?

Thanks.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.