Guest User

Untitled

a guest
Sep 22nd, 2020
34
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1.  
  2. @[derive decidable_eq]
  3. inductive val : Type
  4. | nat
  5. | nil
  6. | cons : Π (car : val) (cdr: val), val
  7.  
  8. @[derive decidable_eq]
  9. inductive fn : val -> val -> Type
  10. | zero : fn val.nil val.nat
  11. | succ : fn val.nat val.nat
  12. | car : Π {tcar tcdr: val}, fn (val.cons tcar tcdr) tcar
  13. | cdr : Π {tcar tcdr: val}, fn (val.cons tcar tcdr) tcdr
  14. | nil : Π {tin : val}, fn tin val.nil
  15. | cons : Π {tin tcar tcdr: val} (car : fn tin tcar) (cdr: fn tin tcdr), fn tin (val.cons tcar tcdr)
  16. | comp : Π {tin tint tout: val} (f : fn tint tout) (g: fn tin tint), fn tin tout
  17. | prec : Π {trest tout: val} (z_case : fn trest tout) (s_case: fn (val.cons val.nat (val.cons tout trest)) tout),
  18. fn (val.cons val.nat trest) tout
  19.  
  20. inductive step : Π {tin tout} (f: fn tin tout) (g: fn tin tout), Prop
  21. | proj_car : Π {tin tcar tcdr} {car:fn tin tcar} {cdr: fn tin tcdr},
  22. step (fn.comp fn.car (fn.cons car cdr)) car
  23. | proj_cdr : Π {tin tcar tcdr} {car:fn tin tcar} {cdr: fn tin tcdr},
  24. step (fn.comp fn.cdr (fn.cons car cdr)) cdr
  25. | comp_f : Π {tin tint tout} {f1 f2:fn tint tout} {g: fn tin tint}
  26. (_ : step f1 f2),
  27. step (fn.comp f1 g) (fn.comp f2 g)
  28.  
  29. instance step_decidable :
  30. Π (tin tout) (f: fn tin tout) (g: fn tin tout),
  31. decidable (step f g) :=
  32. begin
  33. intros,
  34. induction f,
  35. case comp {
  36. cases g,
  37. case comp {
  38. by_cases (f_tint = g_tint),
  39. focus {
  40. subst h,
  41. by_cases (f_g = g_g),
  42. focus {
  43. subst h,
  44. cases f_ih_f g_f,
  45. case is_true {
  46. apply (is_true),
  47. constructor,
  48. assumption,
  49. done
  50. },
  51. },
  52. },
  53. apply(is_false),
  54. intro h2,
  55. cases h2,
  56. },
  57. }
  58. end
  59.  
RAW Paste Data