typed-arith.agda

open import Relation.Binary.PropositionalEquality

-- 存在型
data ∃ {A : Set} (B : A → Set) : Set where
     _,_ : (x₁ : A) → B x₁ → ∃ \(x : A) → B x

-- ORの定義
infixl 8  _∨_
data _∨_ (P Q : Set) : Set where
  or-introl : P → P ∨ Q
  or-intror : Q → P ∨ Q

-- OR消去
or-elimination : {A B C : Set} → A ∨ B → (A → C) → (B → C) → C
or-elimination (or-introl x) ac bc = ac x
or-elimination (or-intror x) ac bc = bc x

-- ANDの定義
infixl 10 _∧_
data _∧_ (P Q : Set) : Set where
  and-intro : P -> Q -> P ∧ Q

-- AND消去
and-eliml : forall {P Q} -> P ∧ Q -> P
and-eliml (and-intro y y') = y

and-elimr : forall {P Q} -> P ∧ Q -> Q
and-elimr (and-intro y y') = y'

-- 項の定義
data Term : Set where
  true : Term
  false : Term
  if_then_else_ : Term → Term → Term → Term
  zero : Term
  succ : Term → Term
  pred : Term → Term
  iszero : Term → Term

infix 30 if_then_else_

-- 型の定義
-- p.70
data Type : Set where
  Bool : Type
  Nat : Type

-- 型づけの定義
-- p.70
data _∷_ : Term → Type → Set where
  t-True : true ∷ Bool
  t-False : false ∷ Bool
  t-If : {t₁ t₂ t₃ : Term} {T : Type} →
    t₁ ∷ Bool → t₂ ∷ T → t₃ ∷ T →
      if t₁ then t₂ else t₃ ∷ T
  t-Zero : zero ∷ Nat
  t-Succ : {t₁ : Term} →
    t₁ ∷ Nat →
      (succ t₁) ∷ Nat
  t-Pred : {t₁ : Term} →
    t₁ ∷ Nat →
      (pred t₁) ∷ Nat
  t-IsZero : {t₁ : Term} →
    t₁ ∷ Nat →
      iszero t₁ ∷ Bool
-- ocaml
-- let rec typeof t =
--   match t with
--     TmTrue(fi) -> 
--       TyBool
--   | TmFalse(fi) -> 
--       TyBool
--   | TmIf(fi,t1,t2,t3) ->
--      if (=) (typeof t1) TyBool then
--        let tyT2 = typeof t2 in
--        if (=) tyT2 (typeof t3) then tyT2
--        else error fi "arms of conditional have different types"
--      else error fi "guard of conditional not a boolean"
--   | TmZero(fi) ->
--       TyNat
--   | TmSucc(fi,t1) ->
--       if (=) (typeof t1) TyNat then TyNat
--       else error fi "argument of succ is not a number"
--   | TmPred(fi,t1) ->
--       if (=) (typeof t1) TyNat then TyNat
--       else error fi "argument of pred is not a number"
--   | TmIsZero(fi,t1) ->
--       if (=) (typeof t1) TyNat then TyBool
--       else error fi "argument of iszero is not a number"


-- 数値の値の定義
data is-nval : Term → Set where
  nval-zero : is-nval zero
  nval-succ : {t : Term} → is-nval t → is-nval (succ t)
-- ocaml
-- let rec isnumericval t = match t with
--     TmZero(_) -> true
--   | TmSucc(_,t1) -> isnumericval t1
--   | _ -> false



-- 値の定義
data is-value : Term → Set where
  val-true : is-value true
  val-false : is-value false
  val-zero : is-value zero
  val-succ : {nv : Term} → is-nval nv → is-value (succ nv)
-- ocaml
-- let rec isval t = match t with
--     TmTrue(_)  -> true
--   | TmFalse(_) -> true
--   | t when isnumericval t  -> true
--   | _ -> false


-- 評価の定義
data _⟶_ : Term → Term → Set where
  e-IfTrue : {t₂ t₃ : Term} →
    if true then t₂ else t₃ ⟶ t₂
  e-IfFalse : {t₂ t₃ : Term} →
    if false then t₂ else t₃ ⟶ t₃
  e-If : {t₁ t₁′ t₂ t₃ : Term} →
    t₁ ⟶ t₁′ →
    if t₁ then t₂ else t₃ ⟶ if t₁′ then t₂ else t₃
  e-Succ : {t₁ t₁′ : Term} →
    t₁ ⟶ t₁′ →
    succ t₁ ⟶ succ t₁′
  e-PredZero :
    pred zero ⟶ zero
  e-PredSucc : {nv₁ : Term} →
    is-nval nv₁ →
    pred (succ nv₁) ⟶ nv₁
  e-Pred : {t₁ t₁′ : Term} →
    t₁ ⟶ t₁′ →
    pred t₁ ⟶ pred t₁′
  e-IsZeroZero :
    iszero zero ⟶ true
  e-IsZeroSucc : {nv₁ : Term} →
    is-nval nv₁ →
    iszero (succ nv₁) ⟶ false
  e-IsZero : {t₁ t₁′ : Term} →
    t₁ ⟶ t₁′ →
    iszero t₁ ⟶ iszero t₁′

-- ocaml
-- let rec eval1 t = match t with
--     TmIf(_,TmTrue(_),t2,t3) ->
--       t2
--   | TmIf(_,TmFalse(_),t2,t3) ->
--       t3
--   | TmIf(fi,t1,t2,t3) ->
--       let t1' = eval1 t1 in
--       TmIf(fi, t1', t2, t3)
--   | TmSucc(fi,t1) ->
--       let t1' = eval1 t1 in
--       TmSucc(fi, t1')
--   | TmPred(_,TmZero(_)) ->
--       TmZero(dummyinfo)
--   | TmPred(_,TmSucc(_,nv1)) when (isnumericval nv1) ->
--       nv1
--   | TmPred(fi,t1) ->
--       let t1' = eval1 t1 in
--       TmPred(fi, t1')
--   | TmIsZero(_,TmZero(_)) ->
--       TmTrue(dummyinfo)
--   | TmIsZero(_,TmSucc(_,nv1)) when (isnumericval nv1) ->
--       TmFalse(dummyinfo)
--   | TmIsZero(fi,t1) ->
--       let t1' = eval1 t1 in
--       TmIsZero(fi, t1')
--   | _ -> 
--       raise NoRuleApplies

--- 部分項の定義
data _∈_ : Term → Term → Set where
  sub-if₁    : ∀ {t₁ t₂ t₃} → t₁ ∈ if t₁ then t₂ else t₃
  sub-if₂    : ∀ {t₁ t₂ t₃} → t₂ ∈ if t₁ then t₂ else t₃
  sub-if₃    : ∀ {t₁ t₂ t₃} → t₃ ∈ if t₁ then t₂ else t₃
  sub-succ   : ∀ {t} → t ∈ succ t
  sub-pred   : ∀ {t} → t ∈ pred t
  sub-iszero : ∀ {t} → t ∈ iszero t
  sub-trans  : ∀ {t₁ t₂ t₃} → t₁ ∈ t₂ → t₂ ∈ t₃ → t₁ ∈ t₃

-- 型付け関係の逆転 8.2.2 p.71
reverse-rule-true : ∀ {R : Type} → true ∷ R → R ≡ Bool
reverse-rule-true t-True = refl
reverse-rule-false : ∀ {R : Type} → false ∷ R → R ≡ Bool
reverse-rule-false t-False = refl
reverse-rule-if : ∀ {t₁ t₂ t₃ : Term} {R : Type} → if t₁ then t₂ else t₃ ∷ R → t₁ ∷ Bool ∧ t₂ ∷ R ∧ t₃ ∷ R
reverse-rule-if (t-If t₁-bool t₂-R t₃-R) = and-intro (and-intro t₁-bool t₂-R) t₃-R
reverse-rule-zero : ∀ {R : Type} → zero ∷ R → R ≡ Nat
reverse-rule-zero t-Zero = refl
reverse-rule-succ : ∀ {t₁ : Term} {R : Type} → (succ t₁) ∷ R → R ≡ Nat
reverse-rule-succ (t-Succ t₁-is-Nat) = refl
reverse-rule-pred : ∀ {t₁ : Term} {R : Type} → (pred t₁) ∷ R → R ≡ Nat
reverse-rule-pred (t-Pred t₁-is-Nat) = refl
reverse-rule-is-zero : ∀ {t₁ : Term} {R : Type} → (iszero t₁) ∷ R → R ≡ Bool
reverse-rule-is-zero (t-IsZero t₁-is-Nat) = refl

-- 8.2.3 p.71
-- 型づけられた項の部分項は型づけられている。
sub-term-is-typed : ∀ {t T} → t ∷ T → ∀ s → s ∈ t → ∃ \(T : Type) → s ∷ T
sub-term-is-typed (t-If t₁-is-bool _ _) t₁ sub-if₁ = Bool , t₁-is-bool
sub-term-is-typed (t-If _ t₂-is-T _)    t₂ sub-if₂ = _ , t₂-is-T
sub-term-is-typed (t-If _ _ t₃-is-T)    t₃ sub-if₃ = _ , t₃-is-T
sub-term-is-typed (t-Succ t₁-is-Nat)    t₁ sub-succ = Nat , t₁-is-Nat
sub-term-is-typed (t-Pred t₁-is-Nat)    t₁ sub-pred = Nat , t₁-is-Nat
sub-term-is-typed (t-IsZero t₁-is-Nat)  t₁ sub-iszero = Nat , t₁-is-Nat
sub-term-is-typed t-is-T                t₁ (sub-trans {.t₁} {t₂} {t} t₁-in-t₂ t₂-in-t) = t₃-from-t₂ (sub-term-is-typed t-is-T t₂ t₂-in-t)
  where
    t₃-from-t₂ : (∃ λ T₁ → (t₂ ∷ T₁)) → ∃ λ T₂ → t₁ ∷ T₂
    t₃-from-t₂ (_ , t₂-is-T₁) = sub-term-is-typed t₂-is-T₁ t₁ t₁-in-t₂

-- 型の一意性 8.2.4
type-uniqueness : ∀ {t : Term} {T : Type} → t ∷ T → ∀ (S : Type) → t ∷ S → T ≡ S
type-uniqueness t-True .Bool t-True = refl
type-uniqueness t-False .Bool t-False = refl
type-uniqueness (t-If _ t-is-T _) S (t-If _ t-is-S _) = type-uniqueness t-is-T S t-is-S
type-uniqueness t-Zero .Nat t-Zero = refl
type-uniqueness (t-Succ t-is-T) .Nat (t-Succ t-is-S) = refl
type-uniqueness (t-Pred t-is-T) .Nat (t-Pred t-is-S) = refl
type-uniqueness (t-IsZero t-is-T) .Bool (t-IsZero t-is-S) = refl

-- 標準形 定理 8.3.1 p.72
normal-form-bool : {v : Term} → v ∷ Bool → is-value v → (v ≡ true) ∨ (v ≡ false)
normal-form-bool t-True  is-value-v = or-introl refl
normal-form-bool t-False is-value-v = or-intror refl
normal-form-bool (t-If v-bool v-bool₁ v-bool₂) ()
normal-form-bool (t-IsZero t-is-Nat) ()

normal-form-nat : {v : Term} → v ∷ Nat → is-value v → is-nval v
normal-form-nat t-Zero isval-v             = nval-zero
normal-form-nat (t-Succ vnat) (val-succ x) = nval-succ x
normal-form-nat (t-Pred vnat) ()
normal-form-nat (t-If vnat vnat₁ vnat₂) ()

-- 進行 定理 8.3.2 p.73
-- t ∷ T に関する帰納法
progress : {t : Term} {T : Type} → t ∷ T → is-value t ∨ ∃ \(t′ : Term) → t ⟶ t′
progress {t = true}  t-True  = or-introl val-true
progress {t = false} t-False = or-introl val-false
progress {t = if t₁ then t₂ else t₃}
  (t-If t₁-is-bool t₂-is-T t₃-is-T) = or-elimination (progress t₁-is-bool)
  -- 帰納の仮定より、t₁が値の場合と、進行をもつ場合で条件分岐
  (λ t₁-is-value     → or-intror (or-elimination (normal-form-bool t₁-is-bool t₁-is-value)
                                  (λ t₁=true → if-t₁=true t₁=true)
                                  (λ t₁=false → if-t₁=false t₁=false)))
  (λ {(t₁′ , t₁->t₁′) → or-intror ((if t₁′ then t₂ else t₃) , (e-If t₁->t₁′))})
  where
    if-t₁=true  : {t₁ : Term} → t₁ ≡ true → ∃ \ t′ → (if t₁ then t₂ else t₃) ⟶ t′
    if-t₁=true  refl = t₂ , e-IfTrue
    if-t₁=false : {t₁ : Term} → t₁ ≡ false → ∃ \ t′ → (if t₁ then t₂ else t₃) ⟶ t′
    if-t₁=false refl = t₃ , e-IfFalse
progress {t = zero}    t-Zero = or-introl val-zero
progress {t = succ t₁} (t-Succ t₁-is-Nat) = or-elimination (progress t₁-is-Nat)
  -- 帰納の仮定より、t₁が値の場合と、進行をもつ場合で条件分岐
  (λ t₁-is-value      → or-introl (val-succ (normal-form-nat t₁-is-Nat t₁-is-value)))
  (λ {(t₁′ , t₁->t₁′) → or-intror ((succ t₁′) , (e-Succ t₁->t₁′))})
progress {t = pred t₁} (t-Pred t₁-is-Nat) = or-elimination (progress t₁-is-Nat)
  -- 帰納の仮定より、t₁が値の場合と、進行をもつ場合で条件分岐
  (λ t₁-is-value      → or-intror (if-t₁-is-n-value (normal-form-nat t₁-is-Nat t₁-is-value)))
  (λ {(t₁′ , t₁->t₁′) → or-intror ((pred t₁′) , (e-Pred t₁->t₁′))})
    where
      if-t₁-is-n-value : {t₁ : Term} → is-nval t₁ → ∃ \(t′ : Term) → (pred t₁) ⟶ t′
      if-t₁-is-n-value nval-zero = zero , e-PredZero
      if-t₁-is-n-value {succ t₁}(nval-succ t₁-is-nval) = t₁ , (e-PredSucc t₁-is-nval)
progress {t = iszero t₁} (t-IsZero t₁-is-Nat) = or-elimination (progress t₁-is-Nat)
  -- 帰納の仮定より、t₁が値の場合と、進行をもつ場合で条件分岐
  (λ t₁-is-value      → or-intror (if-t₁-is-n-value (normal-form-nat t₁-is-Nat t₁-is-value)))
  (λ {(t₁′ , t₁->t₁′) → or-intror ((iszero t₁′) , e-IsZero t₁->t₁′)})
    where
      if-t₁-is-n-value : {t₁ : Term} → is-nval t₁ → ∃ \(t′ : Term) → (iszero t₁) ⟶ t′
      if-t₁-is-n-value nval-zero = true , e-IsZeroZero
      if-t₁-is-n-value {succ t₁}(nval-succ t₁-is-nval) = false , (e-IsZeroSucc t₁-is-nval)


pp-sss-z : pred (pred (succ (succ (succ zero)))) ∷ Nat
pp-sss-z = t-Pred (t-Pred (t-Succ (t-Succ (t-Succ t-Zero))))

test-progress1 = progress pp-sss-z
-- or-intror
-- (pred (pred (succ (succ zero))) ,
---  e-Pred (e-PredSucc (nval-succ (nval-succ nval-zero))))

-- 保存 8.3.3 p.73
-- t ∷ T に関する帰納法
preservation : ∀ {t t′ : Term} {T : Type} → t ∷ T → t ⟶ t′ → t′ ∷ T
preservation t-True ()
preservation t-False ()
preservation t-Zero ()
preservation {t = if true then t₂ else t₃} {t′ = .t₂}
  (t-If t₁-is-Bool t₂-is-T t₃-is-T) e-IfTrue  = t₂-is-T
preservation {t = if false then t₂ else t₃}{t′ = .t₃}
  (t-If t₁-is-Bool t₂-is-T t₃-is-T) e-IfFalse = t₃-is-T
preservation {t = if t₁ then t₂ else t₃}   {t′ = if t₁′ then .t₂ else .t₃}
  (t-If t₁-is-Bool t₂-is-T t₃-is-T) (e-If t₁->t₁′) = t-If (preservation t₁-is-Bool t₁->t₁′) t₂-is-T t₃-is-T
preservation {t = succ t₁}       {t′ = succ t₁′}   (t-Succ t₁-is-N) (e-Succ t₁->t₁′) = t-Succ (preservation t₁-is-N t₁->t₁′)
preservation {t = pred zero}     {t′ = zero}       (t-Pred t₁-is-N) e-PredZero     = t-Zero
preservation {t = pred (succ t₁)}{t′ = .t₁}        (t-Pred (t-Succ t₁-is-N)) (e-PredSucc t₁-is-nval) = t₁-is-N
preservation {t = pred t₁}       {t′ = pred t₁′}   (t-Pred t₁-is-N) (e-Pred t₁->t₁′) = t-Pred (preservation t₁-is-N t₁->t₁′)
preservation {t = iszero .zero}  {t′ = true}       (t-IsZero t₁-is-Nat) e-IsZeroZero = t-True
preservation {t = iszero _}      {t′ = false}      (t-IsZero t₁-is-Nat) (e-IsZeroSucc x) = t-False
preservation {t = iszero t₁}     {t′ = iszero t₁′} (t-IsZero t₁-is-Nat) (e-IsZero t->t′) = t-IsZero (preservation t₁-is-Nat t->t′)

-- eval : {t : Term}{T : Type} → t ∷ T → Term
-- eval {t}t-is-T = or-elimination (progress t-is-T)
--  (λ t-is-value → t)
--  (λ {(t′ , t->t′) → eval (preservation t-is-T t->t′)})
-- test-eval = eval pp-sss-z