Logiweb(TM)

8.5.18 Curry and Uncurry

Prev Up Next Page 343 of 800 Search internet


The Curry operator A Curry modifies a conclusion of form ( x oplus y ) infer z to x infer y infer z and the uncurry operator A Uncurry does the opposite. As examples of use, consider the following three lemmas and proofs:

lemma ConsLemma : All #x ,, #y : #x infer #y infer ( #x oplus #y ) end lemma

prepare proof indentation,proof of ConsLemma : line L00 : Arbitrary >> #x ,, #y ; line L01 : ( #x oplus #y ) infer ( #x oplus #y ) Init >> ( #x oplus #y ) infer ( #x oplus #y ) ; line L02 : L01 Curry >> #x infer #y infer ( #x oplus #y ) qed

lemma HeadLemma : All #x ,, #y : ( #x oplus #y ) infer #x end lemma

prepare proof indentation,proof of HeadLemma : line L00 : Arbitrary >> #x ,, #y ; line L01 : #x infer #y infer #x Init >> #x infer #y infer #x ; line L02 : L01 Uncurry >> ( #x oplus #y ) infer #x qed

lemma TailLemma : All #x ,, #y : ( #x oplus #y ) infer #y end lemma

prepare proof indentation,proof of TailLemma : line L00 : Arbitrary >> #x ,, #y ; line L01 : #x infer #y infer #y Init >> #x infer #y infer #y ; line L02 : L01 Uncurry >> ( #x oplus #y ) infer #y qed

The construct

lemma ConsLemma : All #x ,, #y : #x infer #y infer ( #x oplus #y ) end lemma

defines the statement aspect of ConsLemma to be All #x ,, #y : #x infer #y infer ( #x oplus #y ). That defines All #x ,, #y : #x infer #y infer ( #x oplus #y ) as a lemma directly in the Logiweb sequent calculus.

A lemma like

Prop lemma M1.8a : #x imply #x end lemma

defines the statement aspect of M1.8a as Prop infer #x imply #x and also defines the unitac aspect of M1.8a suitably. The latter allows to use M1.8a directly in argumentations. In contrast,

lemma ConsLemma : All #x ,, #y : #x infer #y infer ( #x oplus #y ) end lemma

does not define a unitac aspect for ConsLemma. Thus, one cannot use ConsLemma directly in argumentations but must include it using suitable operations as described in the next section.

Prev Up Next Page 343 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05