Zulip Chat Archive

Stream: new members

Topic: Showing pred(succ t) = t


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 19 2021 at 05:07):

#backticks

view this post on Zulip Mario Carneiro (Jan 19 2021 at 05:08):

also #mwe

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 19 2021 at 05:14):

try cases h2

view this post on Zulip 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)?

view this post on Zulip Mario Carneiro (Jan 19 2021 at 10:32):

No, this is false


Last updated: May 18 2021 at 16:25 UTC