Showing pred(succ t) = t

Stream: new members

[Lia Malato]

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]

#backticks

[Mario Carneiro]

also #mwe

[Mario Carneiro]

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]

try cases h2

[Lia Malato]

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]

No, this is false