Hello Stephan,
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 prove
LEMMA
ASSUME 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,
Stephan
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
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 prove
LEMMA
ASSUME 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,
Stephan
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
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 prove
LEMMA
ASSUME 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,
Stephan
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
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.