# Zulip Chat Archive

## Stream: new members

### Topic: Showing pred(succ t) = t

#### Lia Malato (Jan 19 2021 at 04:59):

I am working through the book "Types and programming" and there is a theorem I can't completely prove. The following is the background information needed to prove the part where I am stuck:

inductive term

| cond : term → term → term → term

| succ : term → term

| pred : term → term

inductive IsNumV : term → Prop

| succ (n : term) : IsNumV (term.succ n)

inductive IsValue : term → Prop

| numv {t : term} : IsNumV t → IsValue t

inductive eval : term → term → Prop

| E_if (t1 t1' t2 t3 : term) : eval t1 t1' → eval (term.cond t1 t2 t3) (term.cond t1' t2 t3)

| E_succ (t1 t1' : term) : eval t1 t1' → eval (term.succ t1) (term.succ t1')

| E_pred_succ (nv1 : term) : IsNumV nv1.succ → eval (term.pred (term.succ nv1)) nv1

| E_pred (t1 t1' : term) : eval t1 t1' → eval (term.pred t1) (term.pred t1')

inductive ttype

| tBool : ttype

| tNat : ttype

open ttype

inductive TypeChecks : term → ttype → Prop

| TCcond {t1 t2 t3 : term} {T : ttype} :

TypeChecks t1 tBool → TypeChecks t2 T → TypeChecks t3 T → TypeChecks (term.cond t1 t2 t3) T

| TCsucc {t1 : term} :

TypeChecks t1 tNat → TypeChecks (term.succ t1) tNat

| TCpred {t1 : term} :

TypeChecks t1 tNat → TypeChecks (term.pred t1) tNat

I want to show the following:

t t' : term

T : ttype

h1 : IsNumV t'.succ

h2 : TypeChecks t'.succ tNat

ih : ∀ {t'_1 : term}, eval t'.succ t'_1 → TypeChecks t'_1 tNat

|- TypeChecks t' tNat

Now it seems to me that I must somehow prove that term.pred (term.succ t') = t', however I haven't been able to. If anyone has some ideas on how to prove this or the above statement, I would be more than glad to discuss your ideas.

#### Mario Carneiro (Jan 19 2021 at 05:07):

#### Mario Carneiro (Jan 19 2021 at 05:08):

also #mwe

#### Mario Carneiro (Jan 19 2021 at 05:09):

like this:

```
inductive term
| cond : term → term → term → term
| succ : term → term
| pred : term → term
inductive IsNumV : term → Prop
| succ (n : term) : IsNumV (term.succ n)
inductive IsValue : term → Prop
| numv {t : term} : IsNumV t → IsValue t
inductive eval : term → term → Prop
| E_if (t1 t1' t2 t3 : term) : eval t1 t1' → eval (term.cond t1 t2 t3) (term.cond t1' t2 t3)
| E_succ (t1 t1' : term) : eval t1 t1' → eval (term.succ t1) (term.succ t1')
| E_pred_succ (nv1 : term) : IsNumV nv1.succ → eval (term.pred (term.succ nv1)) nv1
| E_pred (t1 t1' : term) : eval t1 t1' → eval (term.pred t1) (term.pred t1')
inductive ttype
| tBool : ttype
| tNat : ttype
open ttype
inductive TypeChecks : term → ttype → Prop
| TCcond {t1 t2 t3 : term} {T : ttype} :
TypeChecks t1 tBool → TypeChecks t2 T → TypeChecks t3 T → TypeChecks (term.cond t1 t2 t3) T
| TCsucc {t1 : term} :
TypeChecks t1 tNat → TypeChecks (term.succ t1) tNat
| TCpred {t1 : term} :
TypeChecks t1 tNat → TypeChecks (term.pred t1) tNat
example
(t t' : term)
(T : ttype)
(h1 : IsNumV t'.succ)
(h2 : TypeChecks t'.succ tNat)
(ih : ∀ {t'_1 : term}, eval t'.succ t'_1 → TypeChecks t'_1 tNat) :
TypeChecks t' tNat :=
sorry
```

#### Mario Carneiro (Jan 19 2021 at 05:14):

try `cases h2`

#### Lia Malato (Jan 19 2021 at 10:17):

Thank you very much! I was indeed able to finish the proof. However, is there a way outside of this example, to prove pred(succ t) = t or succ(pred t)?

#### Mario Carneiro (Jan 19 2021 at 10:32):

No, this is false

Last updated: May 18 2021 at 16:25 UTC