Proof by induction invoking the SequencesInductionTail theorem

[JosEdu Solsona]

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.

[Stephan Merz]

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

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/49d1f151-10fe-449d-9fd9-fa7abbf2a4e5%40googlegroups.com.

[JosEdu Solsona]

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.

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

[Stephan Merz]

Hello,

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?.

I recommend "currying" such functions, i.e. using functions of type [Nat -> [Nat -> S]] instead of [Nat \X Nat -> S] for TLAPS. Functions with several arguments are not or very badly supported at the moment (and this limitation has existed for far too long).

Sorry,

Stephan

[JosEdu Solsona]

Ok, i see. Instead of writing something like

Sum[n, m \in Nat] ==
  IF   n = 0
  THEN m
  ELSE Sum[n-1,m] + 1

we write it as:

Sum[n \in Nat] ==
  [m \in Nat |-> IF n = 0
                 THEN m
                 ELSE Sum[n-1][m] + 1 ]

which has type [Nat -> [Nat -> Nat]] and apply the same theorems to prove is well defined.

Thank you.

[JosEdu Solsona]

Well, just to correct myself after trying to do the proof of my own example, the following alternative
currification of sum is needed to match the theorem form:

Sum[n \in Nat] ==

  IF   n = 0
  THEN [m \in Nat |-> m]
  ELSE [m \in Nat |-> Sum[n-1][m] + 1 ]