近死之心 莫使復陽也

example code of sequent1

overview

natural

(eva

 (+ natural (-> type)
    zero (-> natural)
    succ (natural -> natural))

 (~ add (natural natural -> natural)
    (:m zero -> :m)
    (:m :n succ -> :m :n add succ))

 (~ mul (natural natural -> natural)
    (:m zero -> zero)
    (:m :n succ -> :m :n mul :m add))

 (~ factorial (natural -> natural)
    (zero -> zero succ)
    (:n succ -> :n factorial :n succ mul))

 (app (->
       zero succ
       zero succ succ
       add))

 (app (->
       zero succ succ
       zero succ succ
       mul))

 (app (->
       zero succ succ succ
       factorial)))

add/commute by richly-defined add

(eva

 (+ natural (-> type)
    zero (-> natural)
    succ (natural -> natural))

 (~ add (natural natural -> natural)
    (:m zero -> :m)
    (zero :m -> :m)
    (:m succ :n succ -> :m :n add succ succ))

 (+ eq ({:t : type} :t :t -> type)
    refl ({:t : type} {:d : :t} -> :d :d eq))

 (~ eq/test
    (-> zero zero add zero zero add eq)
    (-> refl))

 (~ add/commute ((:m :n : natural) -> :m :n add :n :m add eq)
    (:m zero -> refl)
    (:m :n succ -> refl)))

stack processing

(eva

 (+ natural (-> type)
    zero (-> natural)
    succ (natural -> natural))

 (~ drop (:t ->)
    (:d ->))

 (~ dup (:t -> :t :t)
    (:d -> :d :d))

 (~ over (:t1 :t2 -> :t1 :t2 :t1)
    (:d1 :d2 -> :d1 :d2 :d1))

 (~ tuck (:t1 :t2 -> :t2 :t1 :t2)
    (:d1 :d2 -> :d2 :d1 :d2))

 (~ swap (:t1 :t2 -> :t2 :t1)
    (:d1 :d2 -> :d2 :d1))

 (app (-> zero
          zero succ
          swap
          drop
          dup)))

list

(eva

 (+ natural (-> type)
    zero (-> natural)
    succ (natural -> natural))

 (~ add (natural natural -> natural)
    (:m zero -> :m)
    (:m :n succ -> :m :n add succ))

 (~ mul (natural natural -> natural)
    (:m zero -> zero)
    (:m :n succ -> :m :n mul :m add))

 (+ list (type -> type)
    null (-> :t list)
    cons (:t list :t -> :t list))

 (~ append (:t list :t list -> :t list)
    (:l null -> :l)
    (:l :r :e cons -> :l :r append :e cons))

 (~ length (:t list -> natural)
    (null -> zero)
    (:l :e cons -> :l length succ))

 (app (->
       null
       zero cons
       null
       zero cons
       append))

 (app (->
       null
       zero cons
       zero cons
       null
       zero cons
       zero cons
       append
       length)))

list map

(eva

 (+ natural (-> type)
    zero (-> natural)
    succ (natural -> natural))

 (~ add (natural natural -> natural)
    (:m zero -> :m)
    (:m :n succ -> :m :n add succ))

 (~ mul (natural natural -> natural)
    (:m zero -> zero)
    (:m :n succ -> :m :n mul :m add))

 (+ list (type -> type)
    null (-> :t list)
    cons (:t list :t -> :t list))

 (~ append (:t list :t list -> :t list)
    (:l null -> :l)
    (:l :r :e cons -> :l :r append :e cons))

 (~ map (:t1 list (:t1 -> :t2) -> :t2 list)
    (null :f -> null)
    (:l :e cons :f -> :l :f map :e :f apply cons))

 (app (->
       null
       zero cons
       zero cons
       zero cons
       null
       zero cons
       zero cons
       zero cons
       append
       (zero -> zero succ)
       map))

 (app (->
       null
       zero cons
       zero cons
       (lambda (natural -> natural)
         (zero -> zero succ))
       map))

 (+ has-length (:t list natural -> type)
    null/has-length (-> null zero has-length)
    cons/has-length (:l :n has-length -> :l :a cons :n succ has-length))

 (~ map/has-length (:l :n has-length -> :l :f map :n has-length)
    (null/has-length -> null/has-length)
    (:h cons/has-length -> :h map/has-length cons/has-length)))

vector

(eva

 (+ natural (-> type)
    zero (-> natural)
    succ (natural -> natural))

 (~ add (natural natural -> natural)
    (:m zero -> :m)
    (:m :n succ -> :m :n add succ))

 ;; ;; this can not be used to prove append
 ;; (~ add (natural natural -> natural)
 ;;    (:m zero -> :m)
 ;;    (zero :m -> :m)
 ;;    (:m succ :n succ -> :m :n add succ succ))

 ;; ;; this can be used to prove append
 ;; (~ add (natural natural -> natural)
 ;;    (:m zero -> :m)
 ;;    (zero :m -> :m)
 ;;    (:m succ :n succ -> :m :n add succ succ)
 ;;    (:m :n succ -> :m :n add succ)
 ;;    (:m succ :n -> :m :n add succ))

 (~ mul (natural natural -> natural)
    (:m zero -> zero)
    (:m :n succ -> :m :n mul :m add))

 (+ vector (natural type -> type)
    null (-> zero :t vector)
    cons (:n :t vector :t -> :n succ :t vector))

 (~ append (:m :t vector :n :t vector -> :m :n add :t vector)
    (:l null -> :l)
    (:l :r :e cons -> :l :r append :e cons))

 (app (->
       null
       zero cons
       zero cons
       zero cons
       null
       zero cons
       zero cons
       zero cons
       append)))

vector map

(eva

 (+ natural (-> type)
    zero (-> natural)
    succ (natural -> natural))

 (~ add (natural natural -> natural)
    (:m zero -> :m)
    (:m :n succ -> :m :n add succ))

 (~ mul (natural natural -> natural)
    (:m zero -> zero)
    (:m :n succ -> :m :n mul :m add))

 (+ vector (natural type -> type)
    null (-> zero :t vector)
    cons (:n :t vector :t -> :n succ :t vector))

 (~ append (:m :t vector :n :t vector -> :m :n add :t vector)
    (:l null -> :l)
    (:l :r :e cons -> :l :r append :e cons))

 (~ map (:n :t1 vector (:t1 -> :t2) -> :n :t2 vector)
    (null :f -> null)
    (:l :e cons :f -> :l :f map :e :f apply cons))

 (app (->
       null
       zero cons
       zero cons
       zero cons
       null
       zero cons
       zero cons
       zero cons
       append
       (zero -> zero succ)
       map))

 (app (->
       null
       zero cons
       zero cons
       (lambda (natural -> natural)
         (zero -> zero succ))
       map)))

>< equality

  • I do not know how to handle equality

(eva

 (+ natural (-> type)
    zero (-> natural)
    succ (natural -> natural))

 (+ eq ({:t : type} :t :t -> type)
    refl ({:t : type} {:d : :t} -> :d :d eq))

 ;; success
 (~ eq/test0
    (-> zero succ succ :z eq)
    (-> refl))

 ;; fail
 (~ eq/test1
    (-> :z zero succ succ eq)
    (-> refl)))

fail to cover/data-list:
dl-tsc :
((cons (eq ((cons (succ ((cons (succ ((cons (zero ()))))))))
            (var (#((:z . 3852) ((1 cons (natural ())))) 0))))))

type-dl-sc :
((cons (eq ((var (#((:d . 3856) ((1 var (#((:t . 3857) ((0 var (#((:t . 3858) ((1 cons (type ())))) 0)) (1 cons (type ())))) 0)))) 0))
            (var (#((:d . 3856) ((1 var (#((:t . 3857) ((0 var (#((:t . 3858) ((1 cons (type ())))) 0)) (1 cons (type ())))) 0)))) 0))))))

info-list :
(cover/data
 fail because non-var can never cover var
 (pattern:
   (cons (succ ((cons (succ ((cons (zero ())))))))))
 (data:
   (var (#((:z . 3852) ((1 cons (natural ())))) 0))))

>< associative of add

(eva

 (+ natural (-> type)
    zero (-> natural)
    succ (natural -> natural))

 (~ add (natural natural -> natural)
    (:m zero -> :m)
    (:m :n succ -> :m :n add succ))

 (~ mul (natural natural -> natural)
    (:m zero -> zero)
    (:m :n succ -> :m :n mul :m add))

 (+ eq ({:t : type} :t :t -> type)
    refl ({:t : type} {:d : :t} -> :d :d eq))

 (~ cong
    ({:t1 :t2 : type} {:x :y : :t1}
     :x :y eq (:f : (:t1 -> :t2)) ->
     :x :f apply :y :f apply eq)
    (refl :f -> refl))

 ;; (~ associative
 ;;    ((:x :y :z : natural) ->
 ;;     :x :y add :z add
 ;;     :x :y :z add add eq)
 ;;    (:x :y zero -> refl)
 ;;    (:x :y :z succ ->
 ;;     :x :y :z associative (lambda (natural -> natural) (:n -> :n succ)) cong))

 ;;     (a + b) + S(c)
 ;; =   S((a + b) + c)  [by A2]
 ;; =   S(a + (b + c))  [by the induction hypothesis]
 ;; =   a + S(b + c)    [by A2]
 ;; =   a + (b + S(c))  [by A2]

 ;; :x :y add :z succ add
 ;; :x :y add :z add succ
 ;; :x :y :z add add succ
 ;; :x :y :z add succ add
 ;; :x :y :z succ add add

 (~ t1 ((:x :y :z : natural) ->
        :x :y :z add add succ
        :x :y :z succ add add eq)
    (:x0 :y0 :z0 -> refl))

 (~ t2 (->
        zero succ
        zero succ eq)
    (-> refl (lambda (natural -> natural) (:n -> :n succ)) cong)))

natural-induction

(eva

 (+ natural (-> type)
    zero (-> natural)
    succ (natural -> natural))

 (~ natural-induction ((:p : (natural -> type))
                       zero :p apply
                       ((:k : natural) :k :p apply -> :k succ :p apply)
                       (:x : natural) -> :x :p apply)
    (:q :q/z :q/s zero -> :q/z)
    (:q :q/z :q/s :n succ ->
        :n
        :q :q/z :q/s :n natural-induction
        :q/s apply)))

test recur-check

(eva

 (+ natural (-> type)
    zero (-> natural)
    succ (natural -> natural))

 (~ add (natural natural -> natural)
    (:m zero -> :m)
    (:m :n succ -> :m :n succ add succ)))

(eva

 (+ natural (-> type)
    zero (-> natural)
    succ (natural -> natural))

 (~ add (natural natural -> natural)
    (:m :n -> :m :n add succ)))

torus

(* torus (-> type)
   t (-> torus)
   p (t => t)
   q (t => t)
   h (p q => q p))

(* circle (-> type)
   c (-> circle)
   l (c => c))

(~ ? (circle circle <-> torus)
   t -> )
近死之心 莫使復陽也