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

# Re: [tlaplus] Missing theorem

 Hi Frédéric,I see, thanks a lot – in fact, the inability to prove step <4>3 in this context appears to come from an unintended interaction with the set product in the argument to Seq(_) that we'll have to investigate further. Here are two possible fixes in the meanwhile.The first workaround uses lemma SeqDef (the very first lemma in module SequenceTheorems, of which your proposed lemma is an immediate consequence). The step is then proved by Isabelle.<4>1. J \in Nat<4>2. seq \in [ 1 .. J -> ( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) ) ]<4>3. seq \in Seq(( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) ))  BY <4>1, <4>2, SeqDefThe second workaround consists in hiding the product construction: this is a general recipe for handling "complex" expressions that are irrelevant for a given step. Here, the step is proved by SMT using its built-in knowledge of sequences.<4>1. J \in Nat<4>. DEFINE S == ( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) )<4>2. seq \in [ 1 .. J ->  S]<4>. HIDE DEF S<4>3. seq \in Seq(S) BY <4>1, <4>2If you need the definition of S further down in the proof, you may prefer the variant<4>1. J \in Nat<4>. DEFINE S == ( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) )<4>2. seq \in [ 1 .. J ->  S]<4>3. seq \in Seq(S)  <5>. HIDE DEF S  <5>. QED  BY <4>1, <4>2Best regards,StephanP.S.: Using the default settings on my platform, I use cvc3 as the default SMT solver, although any solver should be able to handle this proof. -sOn 07 Nov 2014, at 16:53, fl wrote: If you have an instance of this lemma in the context of a larger proof where the prover was unable to prove such a step, I'd be interested in hearing about it.   <4>1. J \in Nat<4>2. seq \in [ 1 .. J -> ( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) ) ]<4>3. seq \in Seq(( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) )) BY <4>1, <4>2  -- 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+u...@xxxxxxxxxxxxxxxx. To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. Visit this group at http://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout.