module ArithExprPreservation where open import ArithExprTypeSystem data NValue : Expr -> Set where zero : NValue zero succ : ∀ {nv} → NValue nv → NValue (succ nv) data _⇒_ : Expr → Expr → Set where if-true : ∀ {t2 t3} → if true then t2 else t3 ⇒ t2 if-false : ∀ {t2 t3} → if false then t2 else t3 ⇒ t3 if- : ∀ {t t' t2 t3} → t ⇒ t' → if t then t2 else t3 ⇒ if t' then t2 else t3 succ : ∀ {t t'} → t ⇒ t' → succ t ⇒ succ t' pred-zero : pred zero ⇒ zero pred-succ : ∀ {nv} → NValue nv → pred (succ nv) ⇒ nv pred : ∀ {t t'} → t ⇒ t' → pred t ⇒ pred t' iszero-zero : iszero zero ⇒ true iszero-succ : ∀ {nv} → NValue nv → iszero (succ nv) ⇒ false iszero : ∀ {t t'} → t ⇒ t' → iszero t ⇒ iszero t' preservation : (T : Type) → (t t' : Expr) → t ∈ T → t ⇒ t' → t' ∈ T preservation .bool .true t' true () preservation .bool .false t' false () preservation T ._ t' (if p then p₁ else p₂) if-true = p₁ preservation T ._ t' (if p then p₁ else p₂) if-false = p₂ preservation T ._ ._ (if p then p₁ else p₂) (if- q) = if preservation bool {!!} {!!} p q then p₁ else p₂ preservation .nat .zero t' zero () preservation .nat ._ ._ (succ p) (succ q) = succ (preservation nat {!!} {!!} p q) preservation .nat .(pred zero) .zero (pred p) pred-zero = zero preservation .nat .(pred (succ t')) t' (pred (succ p)) (pred-succ q) = p preservation .nat ._ ._ (pred p) (pred q) = pred (preservation nat ? ? p q) preservation .bool ._ t' (iszero p) q = {!!} {- preservation : ∀ {T t t'} → t ∈ T → t ⇒ t' → t' ∈ T preservation true () -- true does not reduce preservation false () -- false does not reduce preservation (if p then p₁ else p₂) if-true = p₁ -- t = if true then t₁ else t₂ preservation (if p then p₁ else p₂) if-false = p₂ -- t = if false then t₁ else t₂ preservation (if p then p₁ else p₂) (if- q) = if preservation p q then p₁ else p₂ -- t = if t' then t₁ else t₂, p is the proof that t' has a type, q the proof that t' reduces to t'', so preservation p q is the proof that t'' has a type, etc. preservation zero () -- zero does not reduce preservation (succ p) (succ q) = succ (preservation p q) -- t = succ t', p is the proof that t' has a type, and q that it reduces preservation (pred p) pred-zero = p -- t = pred p preservation (pred (succ p)) (pred-succ q) = p preservation (pred p) (pred q) = pred (preservation p q) preservation (iszero p) iszero-zero = true preservation (iszero p) (iszero-succ x) = false preservation (iszero p) (iszero q) = iszero (preservation p q) -}