leanexe/Verified/TreeFieldLocs.lean at main · jsmorph/leanexe · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
import Verified.TreeFieldsCode
import Verified.TreeLayout

namespace Verified

theorem treeFieldLocs_length (fields : List Bool) :
    ∀ words children, (treeFieldLocs fields words children).length = fields.length := by
  induction fields with
  | nil => intros; rfl
  | cons bit rest ih => cases bit <;> intros <;> simp only [treeFieldLocs, List.length_cons, ih]

theorem treeFieldLocs_mem (fields : List Bool) :
    ∀ words children loc,
      loc ∈ treeFieldLocs fields words children ↔
        (words ≤ loc ∧ loc < words + fields.count false) ∨
          (children ≤ loc ∧ loc < children + fields.count true) := by
  induction fields with
  | nil => intros; simp [treeFieldLocs]
  | cons bit rest ih =>
    cases bit <;> intro words children loc <;>
      simp only [treeFieldLocs, List.mem_cons, ih] <;>
      simp [List.count_cons] <;> omega

theorem treeFieldLocs_nodup (fields : List Bool) :
    ∀ words children,
      (words + fields.count false ≤ children ∨ children + fields.count true ≤ words) →
      (treeFieldLocs fields words children).Nodup := by
  induction fields with
  | nil => intros; exact List.nodup_nil
  | cons bit rest ih =>
    intro words children hApart
    cases bit <;> simp only [treeFieldLocs, List.nodup_cons]
    · refine ⟨fun hMem => ?_, ih _ _ ?_⟩
      · rw [treeFieldLocs_mem] at hMem
        simp [List.count_cons] at hApart
        omega
      · simp [List.count_cons] at hApart
        omega
    · refine ⟨fun hMem => ?_, ih _ _ ?_⟩
      · rw [treeFieldLocs_mem] at hMem
        simp [List.count_cons] at hApart
        omega
      · simp [List.count_cons] at hApart
        omega

end Verified