## 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.

#backticks

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