Semantic Quotients #
Defining the Quotient of Formulas #
@[instance_reducible]
Equations
- Formula.instSetoid = { r := semEquiv, iseqv := semEquiv.Equivalence }
Defining the Quotient of Programs #
@[instance_reducible]
Equations
- Program.instSetoid = { r := relEquiv, iseqv := relEquiv.Equivalence }
Lifting congruent functions (in general) #
These two should maybe go in mathlib? Or they already exist somewhere?
theorem
congr_liftFun
{α β : Type}
{R : α → α → Prop}
{S : β → β → Prop}
{f : α → β}
(h : ∀ (x y : α), R x y → S (f x) (f y))
:
Relator.LiftFun (fun (x1 x2 : α) => R x1 x2) (fun (x1 x2 : β) => S x1 x2) f f
theorem
congr_liftFun₂
{γ : Sort u_1}
{α β : Type}
[HasEquiv α]
[HasEquiv β]
[HasEquiv γ]
{f : α → β → γ}
(h : ∀ (x₁ x₂ : α) (y₁ y₂ : β), x₁ ≈ x₂ → y₁ ≈ y₂ → f x₁ y₁ ≈ f x₂ y₂)
:
Relator.LiftFun (fun (x1 x2 : α) => x1 ≈ x2) (Relator.LiftFun (fun (x1 x2 : β) => x1 ≈ x2) fun (x1 x2 : γ) => x1 ≈ x2) f
f