The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT univ-grenoble-alpes.fr>]

More or less folklore in proof theory, usually presented
in sequent calculus.
But not that easy to find references on the web.
Here is one, an expert could provide better answers.
https://lipn.univ-paris13.fr/~mazza/teaching/ProofTheoryNotes-M1.pdf

Jean-Francois


On Fri, Mar 22, 2019 at 07:09:12AM -0300, Beta Ziliani wrote:
>    Out of curiosity,  Gaëtan, where did you get the name "commutative cut"
>    for this? It's the first time I've heard of it.
> 
>    Written from mobile. Excuse my limited communication.
>    On Fri, Mar 22, 2019, 5:28 AM Gaëtan Gilbert
>    
> <[1]gaetan.gilbert AT skyskimmer.net>
>  wrote:
> 
>      The variable x depends on t, so when you match on t if you want to use 
> x
>      at a type depending on the branch you have to do a commutative cut
> 
>      Definition liftVal t : tyDenote t -> exp t :=
>         match t with
>         | Nat => fun x => NatLit x
>         | Nat' => fun x => Nat'Lit x
>         | Bool => fun x => BoolLit x
>         end.
> 
>      Gaëtan Gilbert