structure Auto.Embedding.GLift (α : Sort u) : Sort (max u (v + 1))

• up :: (
• down : α

  Extract a value from GLift α

• )

def Auto.Embedding.GLift.down.inj {α : Sort u_1} (x y : GLift α) (H : x.down = y.down) : x = y

Equations

• ⋯ = ⋯

def Auto.Embedding.notLift (p : GLift Prop) : GLift Prop

Equations

• Auto.Embedding.notLift p = { down := ¬p.down }

def Auto.Embedding.andLift (p q : GLift Prop) : GLift Prop

Equations

• Auto.Embedding.andLift p q = { down := p.down ∧ q.down }

def Auto.Embedding.orLift (p q : GLift Prop) : GLift Prop

Equations

• Auto.Embedding.orLift p q = { down := p.down ∨ q.down }

def Auto.Embedding.iffLift (p q : GLift Prop) : GLift Prop

Equations

• Auto.Embedding.iffLift p q = { down := p.down ↔ q.down }

noncomputable def Auto.Embedding.ofPropLift (p : GLift Prop) : GLift Bool

Equations

• Auto.Embedding.ofPropLift p = { down := Auto.Bool.ofProp p.down }

def Auto.Embedding.notbLift (p : GLift Bool) : GLift Bool

Equations

• Auto.Embedding.notbLift p = { down := !p.down }

def Auto.Embedding.andbLift (p q : GLift Bool) : GLift Bool

Equations

• Auto.Embedding.andbLift p q = { down := p.down && q.down }

def Auto.Embedding.orbLift (p q : GLift Bool) : GLift Bool

Equations

• Auto.Embedding.orbLift p q = { down := p.down || q.down }

def Auto.Embedding.naddLift (m n : GLift Nat) : GLift Nat

Equations

• Auto.Embedding.naddLift m n = { down := m.down.add n.down }

def Auto.Embedding.nsubLift (m n : GLift Nat) : GLift Nat

Equations

• Auto.Embedding.nsubLift m n = { down := m.down.sub n.down }

def Auto.Embedding.nmulLift (m n : GLift Nat) : GLift Nat

Equations

• Auto.Embedding.nmulLift m n = { down := m.down.mul n.down }

def Auto.Embedding.ndivLift (m n : GLift Nat) : GLift Nat

Equations

• Auto.Embedding.ndivLift m n = { down := m.down.div n.down }

def Auto.Embedding.nmodLift (m n : GLift Nat) : GLift Nat

Equations

• Auto.Embedding.nmodLift m n = { down := m.down.mod n.down }

def Auto.Embedding.nleLift (m n : GLift Nat) : GLift Prop

Equations

• Auto.Embedding.nleLift m n = { down := m.down.le n.down }

def Auto.Embedding.nltLift (m n : GLift Nat) : GLift Prop

Equations

• Auto.Embedding.nltLift m n = { down := m.down.lt n.down }

def Auto.Embedding.nmaxLift (m n : GLift Nat) : GLift Nat

Equations

• Auto.Embedding.nmaxLift m n = { down := m.down.max n.down }

def Auto.Embedding.nminLift (m n : GLift Nat) : GLift Nat

Equations

• Auto.Embedding.nminLift m n = { down := m.down.min n.down }

def Auto.Embedding.iofNatLift (m : GLift Nat) : GLift Int

Equations

• Auto.Embedding.iofNatLift m = { down := Int.ofNat m.down }

def Auto.Embedding.inegSuccLift (m : GLift Nat) : GLift Int

Equations

• Auto.Embedding.inegSuccLift m = { down := Int.negSucc m.down }

def Auto.Embedding.inegLift (m : GLift Int) : GLift Int

Equations

• Auto.Embedding.inegLift m = { down := m.down.neg }

def Auto.Embedding.iabsLift (m : GLift Int) : GLift Int

Equations

• Auto.Embedding.iabsLift m = { down := if m.down < -m.down then -m.down else m.down }

def Auto.Embedding.iaddLift (m n : GLift Int) : GLift Int

Equations

• Auto.Embedding.iaddLift m n = { down := m.down.add n.down }

def Auto.Embedding.isubLift (m n : GLift Int) : GLift Int

Equations

• Auto.Embedding.isubLift m n = { down := m.down.sub n.down }

def Auto.Embedding.imulLift (m n : GLift Int) : GLift Int

Equations

• Auto.Embedding.imulLift m n = { down := m.down.mul n.down }

def Auto.Embedding.idivLift (m n : GLift Int) : GLift Int

Equations

• Auto.Embedding.idivLift m n = { down := m.down.tdiv n.down }

def Auto.Embedding.imodLift (m n : GLift Int) : GLift Int

Equations

• Auto.Embedding.imodLift m n = { down := m.down.tmod n.down }

def Auto.Embedding.iedivLift (m n : GLift Int) : GLift Int

Equations

• Auto.Embedding.iedivLift m n = { down := m.down.ediv n.down }

def Auto.Embedding.iemodLift (m n : GLift Int) : GLift Int

Equations

• Auto.Embedding.iemodLift m n = { down := m.down.emod n.down }

def Auto.Embedding.ileLift (m n : GLift Int) : GLift Prop

Equations

• Auto.Embedding.ileLift m n = { down := m.down.le n.down }

def Auto.Embedding.iltLift (m n : GLift Int) : GLift Prop

Equations

• Auto.Embedding.iltLift m n = { down := m.down.lt n.down }

def Auto.Embedding.imaxLift (m n : GLift Int) : GLift Int

Equations

• Auto.Embedding.imaxLift m n = { down := max m.down n.down }

def Auto.Embedding.iminLift (m n : GLift Int) : GLift Int

Equations

• Auto.Embedding.iminLift m n = { down := min m.down n.down }

def Auto.Embedding.sappLift (m n : GLift String) : GLift String

Equations

• Auto.Embedding.sappLift m n = { down := m.down.append n.down }

def Auto.Embedding.slengthLift (m : GLift String) : GLift Nat

Equations

• Auto.Embedding.slengthLift m = { down := m.down.length }

def Auto.Embedding.sleLift (m n : GLift String) : GLift Prop

Equations

• Auto.Embedding.sleLift m n = { down := Auto.String.le m.down n.down }

def Auto.Embedding.sltLift (m n : GLift String) : GLift Prop

Equations

• Auto.Embedding.sltLift m n = { down := Auto.String.lt m.down n.down }

def Auto.Embedding.sprefixofLift (m n : GLift String) : GLift Bool

Equations

• Auto.Embedding.sprefixofLift m n = { down := m.down.isPrefixOf n.down }

def Auto.Embedding.srepallLift (s patt rep : GLift String) : GLift String

Equations

• Auto.Embedding.srepallLift s patt rep = { down := s.down.replace patt.down rep.down }

def Auto.Embedding.bvofNatLift (n : Nat) (x : GLift Nat) : GLift (BitVec n)

Equations

• Auto.Embedding.bvofNatLift n x = { down := BitVec.ofNat n x.down }

def Auto.Embedding.bvtoNatLift (n : Nat) (x : GLift (BitVec n)) : GLift Nat

Equations

• Auto.Embedding.bvtoNatLift n x = { down := x.down.toNat }

def Auto.Embedding.bvofIntLift (n : Nat) (x : GLift Int) : GLift (BitVec n)

Equations

• Auto.Embedding.bvofIntLift n x = { down := BitVec.ofInt n x.down }

def Auto.Embedding.bvtoIntLift (n : Nat) (x : GLift (BitVec n)) : GLift Int

Equations

• Auto.Embedding.bvtoIntLift n x = { down := x.down.toInt }

def Auto.Embedding.bvaddLift (n : Nat) (x y : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvaddLift n x y = { down := x.down.add y.down }

def Auto.Embedding.bvsubLift (n : Nat) (x y : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvsubLift n x y = { down := x.down.sub y.down }

def Auto.Embedding.bvnegLift (n : Nat) (x : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvnegLift n x = { down := x.down.neg }

def Auto.Embedding.bvabsLift (n : Nat) (x : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvabsLift n x = { down := x.down.abs }

def Auto.Embedding.bvmulLift (n : Nat) (x y : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvmulLift n x y = { down := x.down.mul y.down }

def Auto.Embedding.bvudivLift (n : Nat) (x y : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvudivLift n x y = { down := x.down.smtUDiv y.down }

def Auto.Embedding.bvuremLift (n : Nat) (x y : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvuremLift n x y = { down := x.down.umod y.down }

def Auto.Embedding.bvsdivLift (n : Nat) (x y : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvsdivLift n x y = { down := x.down.smtSDiv y.down }

def Auto.Embedding.bvsremLift (n : Nat) (x y : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvsremLift n x y = { down := x.down.srem y.down }

def Auto.Embedding.bvsmodLift (n : Nat) (x y : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvsmodLift n x y = { down := x.down.smod y.down }

def Auto.Embedding.bvmsbLift (n : Nat) (x : GLift (BitVec n)) : GLift Bool

Equations

• Auto.Embedding.bvmsbLift n x = { down := x.down.msb }

def Auto.Embedding.bvultLift (n : Nat) (x y : GLift (BitVec n)) : GLift Bool

Equations

• Auto.Embedding.bvultLift n x y = { down := x.down.ult y.down }

def Auto.Embedding.bvuleLift (n : Nat) (x y : GLift (BitVec n)) : GLift Bool

Equations

• Auto.Embedding.bvuleLift n x y = { down := x.down.ule y.down }

def Auto.Embedding.bvsltLift (n : Nat) (x y : GLift (BitVec n)) : GLift Bool

Equations

• Auto.Embedding.bvsltLift n x y = { down := x.down.slt y.down }

def Auto.Embedding.bvsleLift (n : Nat) (x y : GLift (BitVec n)) : GLift Bool

Equations

• Auto.Embedding.bvsleLift n x y = { down := x.down.sle y.down }

def Auto.Embedding.bvpropultLift (n : Nat) (x y : GLift (BitVec n)) : GLift Prop

Equations

• Auto.Embedding.bvpropultLift n x y = { down := x.down.toFin < y.down.toFin }

def Auto.Embedding.bvpropuleLift (n : Nat) (x y : GLift (BitVec n)) : GLift Prop

Equations

• Auto.Embedding.bvpropuleLift n x y = { down := x.down.toFin ≤ y.down.toFin }

def Auto.Embedding.bvpropsltLift (n : Nat) (x y : GLift (BitVec n)) : GLift Prop

Equations

• Auto.Embedding.bvpropsltLift n x y = { down := x.down.toInt < y.down.toInt }

def Auto.Embedding.bvpropsleLift (n : Nat) (x y : GLift (BitVec n)) : GLift Prop

Equations

• Auto.Embedding.bvpropsleLift n x y = { down := x.down.toInt ≤ y.down.toInt }

def Auto.Embedding.bvandLift (n : Nat) (x y : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvandLift n x y = { down := x.down.and y.down }

def Auto.Embedding.bvorLift (n : Nat) (x y : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvorLift n x y = { down := x.down.or y.down }

def Auto.Embedding.bvxorLift (n : Nat) (x y : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvxorLift n x y = { down := x.down.xor y.down }

def Auto.Embedding.bvnotLift (n : Nat) (x : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvnotLift n x = { down := x.down.not }

def Auto.Embedding.bvshlLift (n : Nat) (a : GLift (BitVec n)) (s : GLift Nat) : GLift (BitVec n)

Equations

• Auto.Embedding.bvshlLift n a s = { down := a.down.shiftLeft s.down }

def Auto.Embedding.bvlshrLift (n : Nat) (a : GLift (BitVec n)) (s : GLift Nat) : GLift (BitVec n)

Equations

• Auto.Embedding.bvlshrLift n a s = { down := a.down.ushiftRight s.down }

def Auto.Embedding.bvashrLift (n : Nat) (a : GLift (BitVec n)) (s : GLift Nat) : GLift (BitVec n)

Equations

• Auto.Embedding.bvashrLift n a s = { down := a.down.sshiftRight s.down }

def Auto.Embedding.bvsmtshlLift (n : Nat) (a s : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvsmtshlLift n a s = { down := a.down.shiftLeft s.down.toNat }

def Auto.Embedding.bvsmtlshrLift (n : Nat) (a s : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvsmtlshrLift n a s = { down := a.down.ushiftRight s.down.toNat }

def Auto.Embedding.bvsmtashrLift (n : Nat) (a s : GLift (BitVec n)) : GLift (BitVec n)

Equations

• Auto.Embedding.bvsmtashrLift n a s = { down := a.down.sshiftRight s.down.toNat }

def Auto.Embedding.bvappendLift (n m : Nat) (x : GLift (BitVec n)) (y : GLift (BitVec m)) : GLift (BitVec (n.add m))

Equations

• Auto.Embedding.bvappendLift n m x y = { down := x.down.append y.down }

def Auto.Embedding.bvextractLift (n h l : Nat) (x : GLift (BitVec n)) : GLift (BitVec ((h.sub l).add 1))

Equations

• Auto.Embedding.bvextractLift n h l x = { down := BitVec.extractLsb h l x.down }

def Auto.Embedding.bvrepeatLift (w i : Nat) (x : GLift (BitVec w)) : GLift (BitVec (w.mul i))

Equations

• Auto.Embedding.bvrepeatLift w i x = { down := BitVec.replicate i x.down }

def Auto.Embedding.bvzeroExtendLift (w v : Nat) (x : GLift (BitVec w)) : GLift (BitVec v)

Equations

• Auto.Embedding.bvzeroExtendLift w v x = { down := BitVec.zeroExtend v x.down }

def Auto.Embedding.bvsignExtendLift (w i : Nat) (x : GLift (BitVec w)) : GLift (BitVec i)

Equations

• Auto.Embedding.bvsignExtendLift w i x = { down := BitVec.signExtend i x.down }

def Auto.Embedding.constId {a : Sort u} {b : Sort v} : a → (h : b) → b

Equations

• Auto.Embedding.constId x✝ h = h

@[reducible]

def Auto.Embedding.ImpF (p : Sort u) (q : Sort v) : Sort (imax u v)

Equations

• Auto.Embedding.ImpF p q = (p → q)

def Auto.Embedding.impLift (p : GLift (Sort t)) (q : GLift (Sort u)) : GLift (Sort (imax t u))

Equations

• Auto.Embedding.impLift p q = { down := p.down → q.down }

def Auto.Embedding.LiftTyConv (tyUp : GLift (Sort u)) : Sort (max u (v + 1))

Equations

• Auto.Embedding.LiftTyConv tyUp = Auto.Embedding.GLift tyUp.down

def Auto.Embedding.eqLift {α : Sort u} {β : Sort v} (I : IsomType α β) (x y : β) : GLift Prop

Equations

• Auto.Embedding.eqLift I x y = { down := I.g x = I.g y }

def Auto.Embedding.eqLift_refl {α : Sort u} {β : Sort v} (I : IsomType α β) (x : β) : (eqLift I x x).down

Equations

• ⋯ = ⋯

def Auto.Embedding.eqLift.down {α : Sort u} {β : Sort v} (I : IsomType α β) (x y : β) (H : (eqLift I x y).down) : x = y

Equations

• ⋯ = ⋯

def Auto.Embedding.eqLift.up {α : Sort u} {β : Sort v} (I : IsomType α β) (x y : β) (H : x = y) : (eqLift I x y).down

Equations

• ⋯ = ⋯

structure Auto.Embedding.EqLift (β : Sort u) : Sort (max u (v + 1))

• eqF : β → β → GLift Prop
• down (x y : β) : (self.eqF x y).down → x = y
• up (x y : β) : x = y → (self.eqF x y).down

def Auto.Embedding.EqLift.ofIsomTy {α : Sort u} {β : Sort v} (I : IsomType α β) : EqLift β

Equations

• Auto.Embedding.EqLift.ofIsomTy I = { eqF := Auto.Embedding.eqLift I, down := ⋯, up := ⋯ }

def Auto.Embedding.eqLiftFn (β : Type u) (x y : β) : GLift Prop

Equations

• Auto.Embedding.eqLiftFn β x y = { down := x = y }

def Auto.Embedding.EqLift.default (β : Sort u) : EqLift β

Equations

• Auto.Embedding.EqLift.default β = { eqF := fun (x y : β) => { down := x = y }, down := ⋯, up := ⋯ }

theorem Auto.Embedding.eqGLift_equiv {α : Sort u_1} (a b : α) : ({ down := a } = { down := b }) = (a = b)

theorem Auto.Embedding.neGLift_equiv {α : Sort u_1} (a b : α) : ({ down := a } ≠ { down := b }) = (a ≠ b)

@[reducible]

def Auto.Embedding.forallF {α : Sort u} (p : α → Sort v) : Sort (imax u v)

Equations

• Auto.Embedding.forallF p = ((x : α) → p x)

def Auto.Embedding.forallLift {α : Sort u} {β : Sort v} (I : IsomType α β) (p : β → GLift (Sort w)) : GLift (Sort (imax u w))

Equations

• Auto.Embedding.forallLift I p = { down := (x : α) → (p (I.f x)).down }

def Auto.Embedding.forallLift.down {α : Sort u} {β : Sort v} (I : IsomType α β) (p : β → GLift (Sort w)) (H : (forallLift I p).down) (x : β) : (p x).down

Equations

• Auto.Embedding.forallLift.down I p H x = ⋯ ▸ H (I.g x)

def Auto.Embedding.forallLift.up {α : Sort u} {β : Sort v} (I : IsomType α β) (p : β → GLift (Sort w)) (H : (x : β) → (p x).down) : (forallLift I p).down

Equations

• Auto.Embedding.forallLift.up I p H x = ⋯ ▸ ⋯ ▸ H (I.f x)

structure Auto.Embedding.ForallLift (β : Sort v') : Sort (max (max (max (v + 1) v') (w + 1)) (w' + 1))

• forallF : (β → GLift (Sort w)) → GLift (Sort w')
• down (p : β → GLift (Sort w)) : (self.forallF p).down → (x : β) → (p x).down
• up (p : β → GLift (Sort w)) : ((x : β) → (p x).down) → (self.forallF p).down

def Auto.Embedding.ForallLift.ofIsomTy {α : Sort u} {β : Sort v} (I : IsomType α β) : ForallLift β

Equations

• Auto.Embedding.ForallLift.ofIsomTy I = { forallF := Auto.Embedding.forallLift I, down := Auto.Embedding.forallLift.down I, up := Auto.Embedding.forallLift.up I }

def Auto.Embedding.forallLiftFn (β : Type u) (p : β → GLift Prop) : GLift Prop

Equations

• Auto.Embedding.forallLiftFn β p = { down := ∀ (x : β), (p x).down }

def Auto.Embedding.ForallLift.default (β : Sort v') : ForallLift β

Equations

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

theorem Auto.Embedding.forallGLift_equiv {β : Sort u_1} (p : β → Prop) : (∀ (x : GLift β), p x.down) = ∀ (x : β), p x

def Auto.Embedding.existLift {α : Sort u} {β : Sort v} (I : IsomType α β) (p : β → GLift Prop) : GLift Prop

Equations

• Auto.Embedding.existLift I p = { down := ∃ (x : α), (p (I.f x)).down }

def Auto.Embedding.existLift.down {α : Sort u} {β : Sort v} (I : IsomType α β) (p : β → GLift Prop) (H : (existLift I p).down) : ∃ (x : β), (p x).down

Equations

• ⋯ = ⋯

def Auto.Embedding.existLift.up {α : Sort u} {β : Sort v} (I : IsomType α β) (p : β → GLift Prop) (H : ∃ (x : β), (p x).down) : (existLift I p).down

Equations

• ⋯ = ⋯

structure Auto.Embedding.ExistLift (β : Sort v') : Sort (max (v + 1) v')

• existF : (β → GLift Prop) → GLift Prop
• down (p : β → GLift Prop) : (self.existF p).down → ∃ (x : β), (p x).down
• up (p : β → GLift Prop) : (∃ (x : β), (p x).down) → (self.existF p).down

def Auto.Embedding.ExistLift.ofIsomTy {α : Sort u} {β : Sort v} (I : IsomType α β) : ExistLift β

Equations

• Auto.Embedding.ExistLift.ofIsomTy I = { existF := Auto.Embedding.existLift I, down := ⋯, up := ⋯ }

def Auto.Embedding.existLiftFn (β : Type u) (p : β → GLift Prop) : GLift Prop

Equations

• Auto.Embedding.existLiftFn β p = { down := ∃ (x : β), (p x).down }

def Auto.Embedding.ExistLift.default (β : Sort v') : ExistLift β

Equations

• Auto.Embedding.ExistLift.default β = { existF := fun (p : β → Auto.Embedding.GLift Prop) => { down := ∃ (x : β), (p x).down }, down := ⋯, up := ⋯ }

theorem Auto.Embedding.existGLift_equiv {β : Sort u_1} (p : β → Prop) : (∃ (x : GLift β), p x.down) = ∃ (x : β), p x

noncomputable def Auto.Embedding.iteLift {α : Sort u} {β : Sort v} (I : IsomType α β) (b : GLift Prop) (x y : β) : β

Equations

• Auto.Embedding.iteLift I b x y = I.f (Auto.Bool.ite' b.down (I.g x) (I.g y))

def Auto.Embedding.iteLift.wf {α : Sort u} {β : Sort v} (I : IsomType α β) (p : GLift Prop) (x y : β) : iteLift I p x y = Bool.ite' p.down x y

Equations

• ⋯ = ⋯

structure Auto.Embedding.IteLift (β : Sort v') : Sort (max (v + 1) v')

• iteF : GLift Prop → β → β → β
• wf (b : GLift Prop) (x y : β) : self.iteF b x y = Bool.ite' b.down x y

noncomputable def Auto.Embedding.IteLift.ofIsomTy {α : Sort u} {β : Sort v} (I : IsomType α β) : IteLift β

Equations

• Auto.Embedding.IteLift.ofIsomTy I = { iteF := Auto.Embedding.iteLift I, wf := ⋯ }

noncomputable def Auto.Embedding.iteLiftFn (β : Type u) (b : GLift Prop) (x y : β) : β

Equations

• Auto.Embedding.iteLiftFn β b x y = Auto.Bool.ite' b.down x y

noncomputable def Auto.Embedding.IteLift.default (β : Sort v') : IteLift β

Equations

• Auto.Embedding.IteLift.default β = { iteF := fun (b : Auto.Embedding.GLift Prop) (x y : β) => Auto.Bool.ite' b.down x y, wf := ⋯ }