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

*From*: JosEdu Solsona <josedusolsona@xxxxxxxxx>*Date*: Sat, 13 Jun 2020 16:48:42 -0700 (PDT)*References*: <49d1f151-10fe-449d-9fd9-fa7abbf2a4e5@googlegroups.com> <F30C5582-E77D-4405-A68A-5214D9FA50CA@gmail.com>

Hello Stephan,

On Saturday, May 30, 2020 at 6:16:11 AM UTC-3, Stephan Merz wrote:

On Saturday, May 30, 2020 at 6:16:11 AM UTC-3, Stephan Merz wrote:

On Saturday, May 30, 2020 at 6:16:11 AM UTC-3, Stephan Merz wrote:

-- Thank you for the comprehensive answer. And sorry this late reply, but now i finally have the Z3 backend working as expected and TLAPS

feels more confortable, before i needed to explicitly call CVC4 where necesary (and even this wasn't working 100% ok).

I successfully proved the SeqProduct "split" lemma. Also proved corresponding definition and type lemmas to justify it is a well defined function.

Similarly, i previously had other "primivite recursive" functions over naturals, like Sqrt[n \in Nat] which i was using without proof. Now

i also justified it using the analogous NatInductiveDef theorem from the NaturalsInduction module.

I guess that these useful theorems need adapted versions to be used for recursive functions defined on multiple parameters (e.g. Sum[n, m \in Nat]

where recursion is done on one parameter having the other fixed) because key theorems/definitions like RecursiveFcnOfNat and

NatInductiveDefConclusion are written assuming single parameter functions. I'm right?.

Thanks.

On Saturday, May 30, 2020 at 6:16:11 AM UTC-3, Stephan Merz wrote:

Hello,the proof works if you write`<1>3. QED`

BY <1>1, <1>2, SequencesInductionTail, IsaM("blast")

A little explanation: Isabelle is the only backend useful for proving schematic goals, i.e. those involving some predicate parameters such as Prop and P in your example. The default proof method "auto" combines rewriting and standard logic reasoning, and it so happens that the rewriting it performs is counter-productive here. The "blast" method omits the rewriting and can trivially solve the obligation.Note that since SeqProduct is defined as a recursive function (which introduces a CHOOSE), you will need to prove that it satisfies the expected equation, i.e. you want to proveLEMMAASSUME NEW s \in Seq(Nat)PROVE SeqProduct(s) = IF s = << >> THEN 1 ELSE Head(s) * SeqProduct(Tail(s))in order to be able to prove steps <1>1 and <1>2 of your lemma. The theorem TailInductiveDef (in module SequenceOpTheorems) is designed to prove exactly that, and the theorem TailInductiveDefType may also be useful. You may also want to look at some of the proofs of the library theorems (in modules SequenceTheorems_proofs and SequenceOpTheorems_proofs) if you get stuck in your proofs.Hope this helps,StephanOn 30 May 2020, at 10:11, JosEdu Solsona <josedu...@xxxxxxxxx> wrote: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, SequencesInductionTailIgnoring 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 tla...@googlegroups.com .

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

On Saturday, May 30, 2020 at 6:16:11 AM UTC-3, Stephan Merz wrote:

Hello,the proof works if you write`<1>3. QED`

BY <1>1, <1>2, SequencesInductionTail, IsaM("blast")

A little explanation: Isabelle is the only backend useful for proving schematic goals, i.e. those involving some predicate parameters such as Prop and P in your example. The default proof method "auto" combines rewriting and standard logic reasoning, and it so happens that the rewriting it performs is counter-productive here. The "blast" method omits the rewriting and can trivially solve the obligation.Note that since SeqProduct is defined as a recursive function (which introduces a CHOOSE), you will need to prove that it satisfies the expected equation, i.e. you want to proveLEMMAASSUME NEW s \in Seq(Nat)PROVE SeqProduct(s) = IF s = << >> THEN 1 ELSE Head(s) * SeqProduct(Tail(s))in order to be able to prove steps <1>1 and <1>2 of your lemma. The theorem TailInductiveDef (in module SequenceOpTheorems) is designed to prove exactly that, and the theorem TailInductiveDefType may also be useful. You may also want to look at some of the proofs of the library theorems (in modules SequenceTheorems_proofs and SequenceOpTheorems_proofs) if you get stuck in your proofs.Hope this helps,StephanOn 30 May 2020, at 10:11, JosEdu Solsona <josedu...@xxxxxxxxx> wrote: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, SequencesInductionTailIgnoring 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 tla...@googlegroups.com .

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

On Saturday, May 30, 2020 at 6:16:11 AM UTC-3, Stephan Merz wrote:

Hello,the proof works if you write`<1>3. QED`

BY <1>1, <1>2, SequencesInductionTail, IsaM("blast")

A little explanation: Isabelle is the only backend useful for proving schematic goals, i.e. those involving some predicate parameters such as Prop and P in your example. The default proof method "auto" combines rewriting and standard logic reasoning, and it so happens that the rewriting it performs is counter-productive here. The "blast" method omits the rewriting and can trivially solve the obligation.Note that since SeqProduct is defined as a recursive function (which introduces a CHOOSE), you will need to prove that it satisfies the expected equation, i.e. you want to proveLEMMAASSUME NEW s \in Seq(Nat)PROVE SeqProduct(s) = IF s = << >> THEN 1 ELSE Head(s) * SeqProduct(Tail(s))in order to be able to prove steps <1>1 and <1>2 of your lemma. The theorem TailInductiveDef (in module SequenceOpTheorems) is designed to prove exactly that, and the theorem TailInductiveDefType may also be useful. You may also want to look at some of the proofs of the library theorems (in modules SequenceTheorems_proofs and SequenceOpTheorems_proofs) if you get stuck in your proofs.Hope this helps,StephanOn 30 May 2020, at 10:11, JosEdu Solsona <josedu...@xxxxxxxxx> wrote: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, SequencesInductionTailIgnoring 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 tla...@googlegroups.com .

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

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/b8d0a69a-8f72-4834-bbc0-d40d6c61587bo%40googlegroups.com.

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

**References**:**[tlaplus] Proof by induction invoking the SequencesInductionTail theorem***From:*JosEdu Solsona

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

- Prev by Date:
**Re: [tlaplus] How to Specify a Broadcast Channel** - Next by Date:
**Re: [tlaplus] Proof by induction invoking the SequencesInductionTail theorem** - Previous by thread:
**Re: [tlaplus] Proof by induction invoking the SequencesInductionTail theorem** - Next by thread:
**Re: [tlaplus] Proof by induction invoking the SequencesInductionTail theorem** - Index(es):