[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: JosEdu Solsona <josedusolsona@xxxxxxxxx>*Date*: Sat, 30 May 2020 01:11:15 -0700 (PDT)

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 ?

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/49d1f151-10fe-449d-9fd9-fa7abbf2a4e5%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Proof by induction invoking the SequencesInductionTail theorem***From:*Stephan Merz

- Prev by Date:
**[tlaplus] Specification for tic-tac-toe in PlusCal** - Next by Date:
**Re: [tlaplus] Proof by induction invoking the SequencesInductionTail theorem** - Previous by thread:
**[tlaplus] Specification for tic-tac-toe in PlusCal** - Next by thread:
**Re: [tlaplus] Proof by induction invoking the SequencesInductionTail theorem** - Index(es):