This file contains a list of theorems required during the implementation of this dsl and the creation of the proof for the otp example. Some of them might actually already exists in the mathlib but i had trouble finding them.

theorem excluded_middle_implication (P Q C : Prop) : (P ∧ Q → C) ∧ (P ∧ ¬Q → C) → P → C

theorem Nat.mod_succ_eq {a b m : ℕ} : a % m = b % m ↔ (a + 1) % m = (b + 1) % m

theorem Nat.le_sub_one_le (n m : ℕ) : n ≤ m → n - 1 ≤ m

theorem Nat.gt_zero_le_one (n : ℕ) : 0 < n ↔ 1 ≤ n

theorem Nat.add_gt_zero_gt_zero (n m : ℕ) : 0 < n → 0 < n + m

theorem Nat.add_gt_zero (n m : ℕ) : n > 0 → n + m > 0

theorem Nat.gt_and_neq_succ_gt_succ (n m : ℕ) : n < m → m ≠ n + 1 → n + 1 < m

theorem Nat.lt_add_cancel_right (n m k : ℕ) : n + k < m + k ↔ n < m

theorem Nat.lt_sub_left (a b c : ℕ) : b < a → a < b + c → a - b < c

theorem Nat.size_sub_lt_size (x l s : ℕ) : l < s → x ≤ l → x ≥ 1 → l - x + 1 < s

theorem UInt64.gt_zero_neq_zero (u : UInt64) : u > 0 → u ≠ 0

theorem UInt64.lt_zero (u : UInt64) : u < 0 ↔ False

theorem UInt64.lt_toNat_iff (u i : UInt64) : u.toNat < i.toNat ↔ u < i

theorem UInt64.le_toNat_iff (u i : UInt64) : u.toNat ≤ i.toNat ↔ u ≤ i

theorem UInt64.add_lt_add (n m k c : UInt64) : n < m ∧ k < c → m.toNat + c.toNat < size → n + k < m + c

theorem UInt64.add_cancel_right_iff (u i k : UInt64) : u + k = i + k ↔ u = i

theorem UInt64.add_cancel_left_iff (u i k : UInt64) : k + u = k + i ↔ u = i

theorem UInt64.add_sub_assoc (p l x : UInt64) : x ≤ l → x > 0 → p + (l - x) + 1 = p + (l - (x - 1))

theorem UInt64.add_right_ne_of_lt (n i l : UInt64) : i < l → n + l ≠ n + i

@[implicit_reducible]

instance instPreorderUInt64LeanPool : Preorder UInt64

Equations

• One or more equations did not get rendered due to their size.

instance instWellFoundedLTUInt64_leanPool : WellFoundedLT UInt64