Re: [tlaplus] Proof by induction invoking the SequencesInductionTail theorem

[JosEdu Solsona <josedusolsona@xxxxxxxxx>]

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.

On Sunday, June 14, 2020 at 9:58:54 AM UTC-3, Stephan Merz wrote:

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

-- 
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/f53fac1a-36a6-45dc-a1d8-d3f16ab0f59eo%40googlegroups.com.