Projects.Util.Bit

source

inductive Bit :

Type

B₀ : Bit
B₁ : Bit

Instances For

source

@[instance_reducible]

instance Bit.instOfNatOfNatNat :

OfNat Bit 0

Equations

Bit.instOfNatOfNatNat = { ofNat := Bit.B₀ }

source

@[instance_reducible]

instance Bit.instOfNatOfNatNat_1 :

OfNat Bit 1

Equations

Bit.instOfNatOfNatNat_1 = { ofNat := Bit.B₁ }

source

@[simp]

theorem Bit.B₀_eq :

B₀ = 0

source

@[simp]

theorem Bit.B₁_eq :

B₁ = 1

source

theorem Bit.bit_ind (R : Bit → Prop) (B0 : R 0) (B1 : R 1) (b : Bit) :

R b

source

@[instance_reducible]

instance Bit.instDecidableEq {a b : Bit} :

Decidable (a = b)

Equations

source

def Bit.not :

Bit → Bit

Equations

Bit.B₀.not = 1
Bit.B₁.not = 0

Instances For

source

def Bit.imp :

Bit → Bit → Bit

Equations

Bit.B₀.imp x✝ = 1
Bit.B₁.imp x✝ = x✝

Instances For

source

def Bit.or :

Bit → Bit → Bit

Equations

Bit.B₀.or x✝ = x✝
Bit.B₁.or x✝ = 1

Instances For

source

def Bit.and :

Bit → Bit → Bit

Equations

Bit.B₀.and x✝ = 0
Bit.B₁.and x✝ = x✝

Instances For

source

def Bit.iff :

Bit → Bit → Bit

Equations

Bit.B₀.iff x✝ = x✝.not
Bit.B₁.iff x✝ = x✝

Instances For

source

def Bit.xor :

Bit → Bit → Bit

Equations

Bit.B₀.xor x✝ = x✝
Bit.B₁.xor x✝ = x✝.not

Instances For

source

def Bit.ofBool (b : Bool) :

Bit

Equations

Bit.ofBool true = 1
Bit.ofBool false = 0

Instances For

source

@[instance_reducible]

instance Bit.instCoeBool :

Coe Bool Bit

Equations

Bit.instCoeBool = { coe := Bit.ofBool }

source

@[instance_reducible]

instance Bit.instCoePropOfDecidable [(p : Prop) → Decidable p] :

Coe Prop Bit

Equations

Bit.instCoePropOfDecidable = { coe := fun (x : Prop) => Bit.ofBool (decide x) }

source

def Bit.ite {α : Type u_1} (b : Bit) (x y : α) :

Equations

Bit.B₁.ite x y = x
Bit.B₀.ite x y = y

Instances For

source

def Bit.toBool (b : Bit) :

Bool

Equations

b.toBool = b.ite true false

Instances For

source

@[instance_reducible]

instance Bit.instCoeBool_1 :

Coe Bit Bool

Equations

Bit.instCoeBool_1 = { coe := Bit.toBool }

source

def Bit.toNat (b : Bit) :

ℕ

Equations

Bit.B₀.toNat = 0
Bit.B₁.toNat = 1

Instances For

source

@[simp]

theorem Bit.eq_zero_or_eq_one {b : Bit} :

b = 0 ∨ b = 1

source

@[simp]

theorem Bit.eq_one_or_eq_zero {b : Bit} :

b = 1 ∨ b = 0

source

@[instance_reducible]

instance Bit.instInhabited :

Inhabited Bit

Equations

Bit.instInhabited = { default := 0 }

source

@[instance_reducible]

instance Bit.instFintype :

Fintype Bit

Equations

Bit.instFintype = { elems := {0, 1}, complete := Bit.instFintype._proof_1 }

source

@[simp]

theorem Bit.default_def :

default = 0

source

@[simp]

theorem Bit.not_0 :

not 0 = 1

source

@[simp]

theorem Bit.not_1 :

not 1 = 0

source

@[simp]

theorem Bit.ne_iff_eq_not {a b : Bit} :

a ≠ b ↔ a = b.not

source

@[simp]

theorem Bit.not_not {b : Bit} :

b.not.not = b

source

@[simp]

theorem Bit.ofBool_false :

ofBool false = 0

source

@[simp]

theorem Bit.ofBool_true :

ofBool true = 1

source

@[simp]

theorem Bit.toBool_0 :

toBool 0 = false

source

@[simp]

theorem Bit.toBool_1 :

toBool 1 = true

source

@[simp]

theorem Bit.ofBool_eq_zero_iff {b : Bool} :

ofBool b = 0 ↔ b = false

source

@[simp]

theorem Bit.ofBool_eq_one_iff {b : Bool} :

ofBool b = 1 ↔ b = true

source

@[simp]

theorem Bit.toBool_eq_false_iff {b : Bit} :

b.toBool = false ↔ b = 0

source

@[simp]

theorem Bit.toBool_eq_true_iff {b : Bit} :

b.toBool = true ↔ b = 1

source

@[simp]

theorem Bit.toBool_ofBool {b : Bool} :

(ofBool b).toBool = b

source

@[simp]

theorem Bit.ofBool_toBool {b : Bit} :

ofBool b.toBool = b

source

@[simp]

theorem Bit.ofBool_eq_iff {b₁ b₂ : Bool} :

ofBool b₁ = ofBool b₂ ↔ b₁ = b₂

source

@[simp]

theorem Bit.toNat_zero :

toNat 0 = 0

source

@[simp]

theorem Bit.toNat_one :

toNat 1 = 1