1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109
110. 110

import Mathlib

structure SurBase where
  l : List SurBase
  r : List SurBase

  -- h : ∀ x ∈ l, ∀ y ∈ r,

    --match a, b with
    -- | SurBase.mk xl xr _, ⟨yl, yr, _⟩ =>
      -- (∀ a ∈ xl, ¬le ⟨yl, yr⟩ a) ∧ (∀ b ∈ yr, ¬le b ⟨xl, xr⟩))

@[grind]
def SurBase.le (x : SurBase) (y : SurBase) :=
  (∀ a ∈ x.l, ¬le y a) ∧ (∀ b ∈ y.r, ¬le b x)
termination_by sizeOf x + sizeOf y
decreasing_by
  all_goals
    expose_names
    cases x
    cases y
    have := List.sizeOf_lt_of_mem h
    grind [SurBase.mk.sizeOf_spec]

-- structure Sur where
--   l : List Sur
--   r : List Sur
--   h : ∀ x ∈ l, ∀ y ∈ r, SurBase.le ⟨x.l, x.r⟩ ⟨y.l, y.r⟩

@[grind]
def SurBase.correct (x : SurBase) :=
  (∀ a ∈ x.l, ∀ b ∈ x.r, a.le b) ∧ (∀ a ∈ x.l, a.correct) ∧ (∀ b ∈ x.r, b.correct)
decreasing_by
  all_goals
    expose_names
    cases x
    have := List.sizeOf_lt_of_mem h
    grind [SurBase.mk.sizeOf_spec]

def Sur := { x : SurBase // x.correct }

@[grind]
def SurZero : Sur := ⟨⟨[], []⟩, by grind⟩

@[grind]
def SurOne : Sur := ⟨⟨[SurZero.val], []⟩, by grind⟩

@[grind]
def SurNegOne : Sur := ⟨⟨[], [SurZero.val]⟩, by grind⟩

example : SurZero.val.le SurOne.val := by
  grind

example : SurNegOne.val.le SurOne.val := by
  grind

example : SurZero.val.le SurZero.val := by
  grind

example : SurOne.val.le SurOne.val := by
  grind

lemma Sur_trans (x y z : Sur) (hxy : x.val.le y.val) (hyz : y.val.le z.val) : x.val.le z.val := by
  by_contra hxz
  unfold SurBase.le at hxy hyz hxz
  simp at hxz
  by_cases h : ∀ a ∈ x.val.l, ¬z.val.le a
  · obtain ⟨k, hk⟩ := hxz h
    have := Sur_trans ⟨k, by
      have := z.property
      unfold SurBase.correct at this
      exact this.2.2 k hk.1⟩ x y
    grind
  · simp at h
    obtain ⟨k, hk⟩ := h
    have := Sur_trans y z ⟨k, by
      have := x.property
      unfold SurBase.correct at this
      exact this.2.1 k hk.1⟩
    grind
termination_by sizeOf x.val + sizeOf y.val + sizeOf z.val
decreasing_by
  all_goals expose_names
  · cases _ : z.val
    have := List.sizeOf_lt_of_mem hk.1
    grind [SurBase.mk.sizeOf_spec]
  · cases _ : x.val
    have := List.sizeOf_lt_of_mem hk.1
    grind [SurBase.mk.sizeOf_spec]


lemma Sur_refl (x : Sur) : x.val.le x.val := by
  by_contra hx
  unfold SurBase.le at hx
  simp at hx
  by_cases h : ∀ a ∈ x.val.l, ¬x.val.le a
  · obtain ⟨k, hk⟩ := hx h


    grind
  · simp at h
    obtain ⟨k, hk⟩ := h

    grind


  -- have := x.property
  -- unfold SurBase.correct at this
  -- unfold SurBase.le
  -- grind