The Coq mailing list

["1337777.OOO" <1337777.ooo AT gmail.com>]

Proph

https://gitlab.com/1337777/dosen/blob/master/dosenSolution101.v

solves some question of Dosen which is how to program the
logical/particular/rewriting/(one-step) polymorphism/cut-elimination
and the confluence/commutation of this rewriting for the grammatical
polymorph pairing-projections ( "product" ) ...

The computational/total/asymptotic/reduction/(multi-step)
polymorphism/cut-elimination of many polymorph mathematics were
already programmed in the earlier COQ texts : polymorph
reflections/adjunctions , polymorph comonad , polymorph
grammatical-metafunctors , polymorph localizations ... The form of
these programs was the same : primo to define grammatical (multi-step)
reduction relation , then secondo to define some non-structural
recursive grade function from the morphisms to the integers , and
finally tertio to define some non-structural recursive cut-elimination
function from any two-morphisms input ( "topmost cut" ) by choosing
some syntactic-match cases precedence when there are ambiguities ref
which reduction shall apply . Memo that the grade function was linear
arithmetic ( addition , maximum , less than ) over the integers .

Now to proceed to the logical consequences of such things shall
require some alternative logical description : some
logical/particular/rewriting/(one-step) polymorphism/cut-elimination
resolution and the confluence/commutation lemma of this rewriting
which shows that this logical resolution is indeed some alternative
description of the computational function . Memo that the grade
function here will ( necessarily ? ) be non-linear arithmetic (
addition , multiplication , distributivity , less than ) over the
integers which mimic/simulate the constructors of the morphisms , in
particular : the polymorphism ( "distributivity" ) of the
composition/cut constructor over the pairing constructor . More
precisely : grade ( f o> g ) = 3 * grade f * grade g  ;  grade ( 1 ) =
1  ;  grade ( ~_1 o> f ) = 1 + grade f  ;  grade ( ~_2 o> f ) = 1 +
grade f  ;  grade ( << f , g >> ) = 1 + grade f + grade g .

This COQ program and deduction is mostly-automated , and the COQ [nia]
automation-tactic is sufficient for this non-linear arithmetic . The
confluence lemma produce some total of ( ( 7 * 8 ) * ( 7 * 8 ) = 3136
goals ) , but only ( 37 classes of goals) are critical via the
automation-tactics ; moreover the COQ computer ( parallel dual core ,
4 gigabytes memory ) motion-time for ( 93 + 27 = 120 minutes ) .

For instant first impression , the lemma that the « resolved-cut » is
congruent modulo solution-conversion is written as :

#+BEGIN_EXAMPLE
Fixpoint solveCoMod_PolyCoMod_cong_Post_ len {struct len}  :
  forall (B1 : obCoMod) (B1' : obCoMod) (g'Sol g'Sol0 : 'CoMod(0 B1 ~>
B1' )0 %sol)
    ( Hconv : ( g'Sol0 ~~~ g'Sol )%sol_once ),
        forall  B2 (g_Sol : 'CoMod(0 B2 ~> B1 )0 %sol),
        forall (H_gradeParticular : ( (Sol.gradeConv Hconv +
Rewrite.gradeParticular ((Sol.toCoMod g_Sol) o>CoMod (Sol.toCoMod
g'Sol))%poly)%Z <= Z.of_nat len)%Z ),
          ( ( ( g_Sol o>CoMod g'Sol0 ) ~~~ ( g_Sol o>CoMod g'Sol ) ))
%sol %sol_conv .
#+END_EXAMPLE

This file [[1337777.OOO//dosenSolution101.v]] is the epilogue of Dosen
book « Cut-Elimination in Categories » .

Keywords : 1337777.OOO//dosenSolution101.v ; pairing-projections
grammar ; logical cut-elimination ; confluence ; non-linear arithmetic

Outline :

  * Grammatical description of polymorph pairing-projections
  ** Importing the non-linear arithmetic COQ automation-tactics
  ** Common-inductive polymorph morphisms, with overloaded notations
for the composition/cut constructor

  * Solution
  ** Grade of solution-conversion for combined non-structural induction
  ** Destruction of solution-morphisms with inner-instantiation of
object-indexes

  * Congruent-Rewriting relation
  ** Non-linear mimicking grade function
  ** Degradation lemma and the non-linear arithmetic COQ automation-tactic 
[nia]

  * Polymorphism/cut-elimination by congruent-rewriting

  * Confluence
  ** Goals accounting
  ** Unique solution for the logical-rewriting relation

  * Polymorphism conversion
  ** Cut-elimination resolution is congruent from the
polymorphism-terminology to the solution-terminology

-----

PS : Oktoberfest 2017 continues as NovemberSchätz 2017 at the CMU
Schätz weekends 11:37-14:00 until november ...

-----

memory amazon.com/hz/wishlist/ls/28SN02HR4EB8W , eth
0x54810dcb93b37DBE874694407f78959Fa222D920 , paypal
1337777.OOO AT gmail.com
 , wechatpay 
2796386464 AT qq.com
 , irc #OOO1337777