arith.sott

define add : Nat -> Nat -> Nat
as introduce m n,
   use m for _. Nat {
     Zero ->
       use n;
     Succ m add_m_n ->
       use Succ add_m_n;
   }

define test :
  [add 2 2 = 4 : Nat]
as refl

define trans :
  (A : Set)
  (a : A)
  (b : A)(p1 : [a = b : A])
  (c : A)(p2 : [b = c : A]) ->
  [a = c : A]
as introduce A a b p c q,
   coerce(p,[a = b : A],[a = c : A],
          subst(A,z.[a = z : A],b,c,q))

define chain3 :
  (A:Set)
  (a:A)
  (b:A)(p1 : [a = b : A])
  (c:A)(p2 : [b = c : A])
  (d:A)(p3 : [c = d : A]) ->
  [a = d : A]
as introduce A a b p1 c p2 d p3,
   trans A a
     b p1
     d (trans A b c p2 d p3)

define chain4 :
  (A:Set)
  (a:A)
  (b:A)(p1 : [a = b : A])
  (c:A)(p2 : [b = c : A])
  (d:A)(p3 : [c = d : A])
  (e:A)(p4 : [d = e : A]) ->
  [a = e : A]
as introduce A a b p1 c p2 d p3 e p4,
   trans A a b p1 e (chain3 A b c p2 d p3 e p4)

define chain5 :
  (A:Set)
  (a:A)
  (b:A)(p1 : [a = b : A])
  (c:A)(p2 : [b = c : A])
  (d:A)(p3 : [c = d : A])
  (e:A)(p4 : [d = e : A])
  (f:A)(p5 : [e = f : A]) ->
  [a = f : A]
as introduce A a b p1 c p2 d p3 e p4 f p5,
   trans A a b p1
     f (trans A b c p2
         f (trans A c d p3
             f (trans A d e p4 f p5)))

define symm :
  (A : Set)(x : A)(y : A) -> [x = y : A] -> [y = x : A]
as introduce A x y p,
   coerce(refl,[x : A = x : A],[y : A = x : A],
          subst(A,z.[z : A = x : A],x,y,p))

define f_equal :
  (f : Nat -> Nat)(x:Nat)(y:Nat) ->
  [x = y : Nat] ->
  [f x = f y : Nat]
as introduce f x y eq,
   coerce(refl,[f x = f x : Nat],[f x = f y : Nat],
          subst(Nat,z.[f x = f z : Nat],x,y,eq))

define add_n_Zero :
  (n : Nat) -> [add n Zero = n : Nat]
as introduce n,
   use n for n. [add n Zero = n : Nat] {
     Zero ->
       refl;
     Succ n p ->
       f_equal (\n -> Succ n) (add n Zero) n p
   }

define add_Succ :
  (n : Nat)(m : Nat) -> [Succ (add n m) = add n (Succ m) : Nat]
as introduce n m,
   use n for n. [Succ (add n m) = add n (Succ m) : Nat] {
     Zero     -> refl;
     Succ n p -> f_equal (\n -> Succ n) (Succ (add n m)) (add n (Succ m)) p
   }

define add_comm :
  (n : Nat)(m : Nat) -> [add n m : Nat = add m n : Nat]
as introduce n m,
   use n for n. [add n m : Nat = add m n : Nat] {
     Zero -> symm Nat (add m Zero) m (add_n_Zero m);
     Succ n p ->
       trans Nat
          (Succ (add n m))
          (Succ (add m n))
          (f_equal (\n -> Succ n) (add n m) (add m n) p)
          (add m (Succ n))
          (add_Succ m n)
   }

define add_assoc :
  (a : Nat)(b : Nat)(c : Nat) ->
  [add a (add b c) : Nat = add (add a b) c : Nat]
as introduce a b c,
   use a for a. [add a (add b c) : Nat = add (add a b) c : Nat] {
     Zero ->
       refl;
     Succ a p ->
       f_equal (\n -> Succ n) (add a (add b c)) (add (add a b) c) p
   }

define add_assoc_inv :
  (a : Nat)(b : Nat)(c : Nat) ->
  [add (add a b) c  = add a (add b c) : Nat]
as introduce a b c,
   symm Nat (add a (add b c)) (add (add a b) c) (add_assoc a b c)

define add_Zero_n :
  (n : Nat) -> [add Zero n = n : Nat]
as \n -> refl


define Int_carrier : Set
as Nat * Nat

define R : Int_carrier -> Int_carrier -> Set
as \z1 z2 -> [add (z1#fst) (z2#snd) = add (z2#fst) (z1#snd) : Nat]

define negate_ : Int_carrier -> Int_carrier
as \z -> (z#snd, z#fst)

define zero_ : Int_carrier
as (Zero, Zero)

define add_ : Int_carrier -> Int_carrier -> Int_carrier
as \z1 z2 -> (add (z1#fst) (z2#fst), add (z1#snd) (z2#snd))

define negate_lemma :
  (z1 : Int_carrier)(z2 : Int_carrier)(r : R z1 z2) -> R (negate_ z1) (negate_ z2)
as \z1 z2 r ->
      chain3 Nat
        (add (z1#snd) (z2#fst))
        (add (z2#fst) (z1#snd))  (add_comm (z1#snd) (z2#fst))
        (add (z1#fst) (z2#snd))  (symm Nat (add (z1#fst) (z2#snd)) (add (z2#fst) (z1#snd)) r)
        (add (z2#snd) (z1#fst))  (add_comm (z1#fst) (z2#snd))

define interchange :
  (a:Nat)(b:Nat)(c:Nat)(d:Nat) ->
  [add (add a b) (add c d) = add (add a c) (add b d) : Nat]
as introduce a b c d,
   chain5 Nat
            (add (add a b) (add c d))
   (* = *)  (add a (add b (add c d)))   (add_assoc_inv a b (add c d))
   (* = *)  (add a (add (add b c) d))   (f_equal (\x -> add a x)
                                                 (add b (add c d)) (add (add b c) d)
                                                 (add_assoc b c d))
   (* = *)  (add a (add (add c b) d))   (f_equal (\x -> add a (add x d))
                                                 (add b c) (add c b)
                                                 (add_comm b c))
   (* = *)  (add a (add c (add b d)))   (f_equal (\x -> add a x)
                                                 (add (add c b) d) (add c (add b d))
                                                 (add_assoc_inv c b d))
   (* = *)  (add (add a c) (add b d))   (add_assoc a c (add b d))

define add_lemma :
  (z1 : Int_carrier)(z1' : Int_carrier)(r1 : R z1 z1')
  (z2 : Int_carrier)(z2' : Int_carrier)(r2 : R z2 z2') ->
  R (add_ z1 z2) (add_ z1' z2')
as introduce z1 z1' r1 z2 z2' r2,
   chain4 Nat
           (add (add (z1#fst) (z2#fst)) (add (z1'#snd) (z2'#snd)))
   (* = *) (add (add (z1#fst) (z1'#snd)) (add (z2#fst) (z2'#snd))) (interchange (z1#fst) (z2#fst) (z1'#snd) (z2'#snd))
   (* = *) (add (add (z1'#fst) (z1#snd)) (add (z2#fst) (z2'#snd))) (f_equal (\x -> add x (add (z2#fst) (z2'#snd))) (add (z1#fst) (z1'#snd)) (add (z1'#fst) (z1#snd)) r1)
   (* = *) (add (add (z1'#fst) (z1#snd)) (add (z2'#fst) (z2#snd))) (f_equal (\x -> add (add (z1'#fst) (z1#snd)) x) (add (z2#fst) (z2'#snd)) (add (z2'#fst) (z2#snd)) r2)
   (* = *) (add (add (z1'#fst) (z2'#fst)) (add (z1#snd) (z2#snd))) (interchange (z1'#fst) (z1#snd) (z2'#fst) (z2#snd))


define Int : Set
as Int_carrier / R

define zero : Int
as [zero_]

define negate : Int -> Int
as introduce z,
   use z for x. Int {
     [z]      -> [negate_ z];
     z1 z2 zr -> same-class (negate_lemma z1 z2 zr)
   }

define add1 : Int_carrier -> Int -> Int
as introduce z1 z2,
   use z2 for x. Int {
      [z2] ->
        [add_ z1 z2];
      z2 z2' r2 ->
        same-class (add_lemma z1 z1 refl z2 z2' r2)
   }

define lemma :
  (z1:Int_carrier)(z1':Int_carrier)
  (z2:Int_carrier)(z2':Int_carrier)(z2r:R z2 z2') ->
  [ [ add1 z1 [z2] = add1 z1' [z2] : Int]
  = [ add1 z1 [z2'] = add1 z1' [z2'] : Int ] ]
as introduce z1 z1' z2 z2' z2r,
   subst(Int, x. [ add1 z1 x : Int = add1 z1' x : Int],
         [z2], [z2'], same-class(z2r))



define add1_eq :
  (z1:Int_carrier)(z1':Int_carrier)(z1r:R z1 z1')(z2:Int)  ->
  [ add1 z1 z2 = add1 z1' z2: Int ]
as introduce z1 z1' z1r z2,
   use z2 for z2. [ add1 z1 z2 = add1 z1' z2 : Int ] {
     [z2] ->
       same-class (add_lemma z1 z1' z1r z2 z2 refl);
     z2 z2' z2r ->
       (* this relies on proof irrelevance for equality proofs *)
       coherence(lemma z1 z1' z2 z2' z2r)
   }


define add_int : Int -> Int -> Int
as introduce z1 z2,
   use z1 for x.Int {
      [z1] -> add1 z1 z2;
      z1 z1' r1 -> add1_eq z1 z1' r1 z2
   }

define inject : Nat -> Int
as \n -> [(n, Zero)]

define one : Int
as inject (Succ Zero)

define minus_one : Int
as negate one

define unit :
  (z : Int) -> [add_int zero z = z : Int]
as introduce z,
   use z for z. [add_int zero z = z : Int] {
     [z] ->
       use refl;
     z z' zr ->
       use coherence(subst(Int, x. [add_int zero x = x : Int], [z], [z'], same-class(zr)))
   }

define inverses :
  (z : Int) -> [ add_int z (negate z) = zero : Int ]
as introduce z,
   use z for z. [ add_int z (negate z) : Int = zero : Int ] {
     [z] -> same-class(trans Nat
                          (add (add (z#fst) (z#snd)) Zero)
                          (add (z#fst) (z#snd))              (add_n_Zero (add (z#fst) (z#snd)))
                          (add (z#snd) (z#fst))              (add_comm (z#fst) (z#snd)));
     z1 z2 zr ->
        coherence(subst(Int, x. [add_int x (negate x) : Int = zero : Int],
                        [z1], [z2], same-class(zr)))
   }

define comm :
  (z1:Int)(z2:Int) ->
  [ add_int z1 z2 = add_int z2 z1 : Int ]
as introduce z1 z2,
   use z1 for z1. [add_int z1 z2 = add_int z2 z1 : Int] {
     [z1] ->
       use z2 for z2. [add_int [z1] z2 = add_int z2 [z1] : Int] {
         [z2] ->
           same-class(trans Nat
                        (add (add (z1#fst) (z2#fst)) (add (z2#snd) (z1#snd)))
                        (add (add (z2#fst) (z1#fst)) (add (z2#snd) (z1#snd)))
                        (f_equal (\x -> add x (add (z2#snd) (z1#snd))) (add (z1#fst) (z2#fst)) (add (z2#fst) (z1#fst)) (add_comm (z1#fst) (z2#fst)))
                        (add (add (z2#fst) (z1#fst)) (add (z1#snd) (z2#snd)))
                        (f_equal (\x -> add (add (z2#fst) (z1#fst)) x) (add (z2#snd) (z1#snd)) (add (z1#snd) (z2#snd)) (add_comm (z2#snd) (z1#snd))));
         z2 z2' z2r ->
           coherence(subst(Int, x. [add_int [z1] x = add_int x [z1] : Int],
                           [z2], [z2'], same-class(z2r)));
       };
     z1 z1' z1r ->
       coherence(subst(Int, x.[add_int x z2 = add_int z2 x : Int],
                       [z1],[z1'],same-class(z1r)));
   }

define assoc :
  (z1:Int)(z2:Int)(z3:Int) ->
  [ add_int z1 (add_int z2 z3) = add_int (add_int z1 z2) z3: Int ]
as introduce z1 z2 z3,
   use z1 for z1. [ add_int z1 (add_int z2 z3) = add_int (add_int z1 z2) z3: Int ] {
     [z1] ->
       use z2 for z2. [ add_int [z1] (add_int z2 z3) = add_int (add_int [z1] z2) z3: Int ] {
         [z2] ->
           use z3 for z3. [ add_int [z1] (add_int [z2] z3) = add_int (add_int [z1] [z2]) z3: Int ] {
             [z3] ->
               same-class
                 (trans Nat
                    (add (add (z1#fst) (add (z2#fst) (z3#fst))) (add (add (z1#snd) (z2#snd)) (z3#snd)))
                    (add (add (add (z1#fst) (z2#fst)) (z3#fst)) (add (add (z1#snd) (z2#snd)) (z3#snd)))
                    (f_equal (\x -> add x (add (add (z1#snd) (z2#snd)) (z3#snd)))
                             (add (z1#fst) (add (z2#fst) (z3#fst)))
                             (add (add (z1#fst) (z2#fst)) (z3#fst))
                             (add_assoc (z1#fst) (z2#fst) (z3#fst)))
                    (add (add (add (z1#fst) (z2#fst)) (z3#fst)) (add (z1#snd) (add (z2#snd) (z3#snd))))
                    (f_equal (\x -> add (add (add (z1#fst) (z2#fst)) (z3#fst)) x)
                             (add (add (z1#snd) (z2#snd)) (z3#snd))
                             (add (z1#snd) (add (z2#snd) (z3#snd)))
                             (add_assoc_inv (z1#snd) (z2#snd) (z3#snd))));
             z3 z3' z3r ->
               coherence(subst(Int, x. [add_int [z1] (add_int [z2] x) = add_int (add_int [z1] [z2]) x : Int],
                               [z3], [z3'], same-class(z3r)));
           };
         z2 z2' z2r ->
           coherence(subst(Int, x. [add_int [z1] (add_int x z3) = add_int (add_int [z1] x) z3 : Int],
                           [z2], [z2'], same-class(z2r)));
       };
     z1 z1' z1r ->
       coherence(subst(Int, x. [add_int x (add_int z2 z3) = add_int (add_int x z2) z3 : Int],
                       [z1], [z1'], same-class(z1r)))
   }

define Bool : Set as {| `True, `False |}

define F : Int -> Set
as \z -> (b : Bool) * b for x.Set { `True  -> [z = zero : Int];
                                    `False -> [z = one : Int ]  }

define v : F zero
as (`True, refl)

define hofmann2 : F (add_int one (negate one))
as coerce(v, F zero, F (add_int one (negate one)),
          subst(Int,x.F x,zero,add_int one (negate one),
                symm Int (add_int one (negate one)) zero (inverses one)))

define test_canonicity :
  [ hofmann2 = (`True, same-class(refl)) : F (add_int one (negate one)) ]
as refl