theorem RingLemmas.dialect_f_eq_zero {q : ℕ} {n : ℕ} : (Ideal.Quotient.mk (Ideal.span {f q n})) (f q n) = 0

In the quotient ring, (f q n) = 0.

theorem RingLemmas.dialect_mul_f_eq_zero {q : ℕ} {n : ℕ} (a : R q n) : a * (Ideal.Quotient.mk (Ideal.span {f q n})) (f q n) = 0

Since (f q n) = 0, anything multiplied by it is also zero.

theorem RingLemmas.dialect_add_f_eq {q : ℕ} {n : ℕ} (a : R q n) : a + (Ideal.Quotient.mk (Ideal.span {f q n})) (f q n) = a

Since (f q n) = 0, adding it to any element gives the element itself.

def ExampleComm.lhs {q : ℕ} {n : ℕ} [hq : Fact (q > 1)] : Com (FHE q n) ((Ctxt.snoc [] Ty.polynomialLike).snoc Ty.polynomialLike) EffectKind.pure Ty.polynomialLike

Equations

• ExampleComm.lhs = Com.var (Expr.mk Op.add ⋯ ⋯ (⟨0 + 1, ⋯⟩::ₕ(⟨0, ⋯⟩::ₕHVector.nil)) HVector.nil) (Com.ret ⟨0, ⋯⟩)

def ExampleComm.rhs {q : ℕ} {n : ℕ} [hq : Fact (q > 1)] : Com (FHE q n) ((Ctxt.snoc [] Ty.polynomialLike).snoc Ty.polynomialLike) EffectKind.pure Ty.polynomialLike

Equations

• ExampleComm.rhs = Com.var (Expr.mk Op.add ⋯ ⋯ (⟨0, ⋯⟩::ₕ(⟨0 + 1, ⋯⟩::ₕHVector.nil)) HVector.nil) (Com.ret ⟨0, ⋯⟩)

noncomputable def ExampleComm.p1 {q : ℕ} {n : ℕ} [hq : Fact (q > 1)] : PeepholeRewrite (FHE q n) [Ty.polynomialLike, Ty.polynomialLike] Ty.polynomialLike

Equations

• ExampleComm.p1 = { lhs := ExampleComm.lhs, rhs := ExampleComm.rhs, correct := ⋯ }

@[irreducible]

def irreduciblePow (q : ℕ) (n : ℕ) : ℕ

Equations

• (q**n) = q ^ n

def «term_**_» : Lean.TrailingParserDescr

Equations

• «term_**_» = Lean.ParserDescr.trailingNode `«term_**_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "**") (Lean.ParserDescr.cat `term 51))

noncomputable def a_plus_generator_eq_a {q : ℕ} {n : ℕ} [hq : Fact (q > 1)] : Com (FHE q n) (Ctxt.snoc [] Ty.polynomialLike) EffectKind.pure Ty.polynomialLike

Equations

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

def rhs {q : ℕ} {n : ℕ} [hq : Fact (q > 1)] : Com (FHE q n) (match match (Ctxt.DerivedCtxt.ofCtxt (Ctxt.DerivedCtxt.ofCtxt ∅).ctxt).snoc Ty.polynomialLike with | { ctxt := Γ'', diff := diff } => { ctxt := Γ'', diff := (Ctxt.DerivedCtxt.ofCtxt ∅).diff + diff } with | { ctxt := Γ', diff := diff } => Γ') EffectKind.pure Ty.polynomialLike

Equations

• rhs = Com.ret ⟨0, ⋯⟩

noncomputable def p1 {q : ℕ} {n : ℕ} [hq : Fact (q > 1)] : PeepholeRewrite (FHE q n) [Ty.polynomialLike] Ty.polynomialLike

Equations

• p1 = { lhs := a_plus_generator_eq_a, rhs := rhs, correct := ⋯ }