Supporting results for pointwise provable equality.
The algebraic consequence of the four witness properties in v36. This file alone makes no assertion about arithmetic or program indices.
theorem
PointwiseComposition.FailureOfComposition.no_quotient_composition_of_noncongruence
{A : Type u}
(s : Setoid A)
(comp : A → A → A)
(f i g : A)
(hfi : Setoid.r f i)
(hcomp : ¬Setoid.r (comp f g) (comp i g))
:
¬∃ (C : Quotient s → Quotient s → Quotient s), ∀ (a b : A), C (Quotient.mk s a) (Quotient.mk s b) = Quotient.mk s (comp a b)
theorem
PointwiseComposition.FailureOfComposition.no_quotient_composition
{A : Type u}
(s : Setoid A)
(comp : A → A → A)
(f i g z : A)
(hfi : Setoid.r f i)
(hfg : Setoid.r (comp f g) z)
(hig : Setoid.r (comp i g) g)
(hgz : ¬Setoid.r g z)
:
¬∃ (C : Quotient s → Quotient s → Quotient s), ∀ (a b : A), C (Quotient.mk s a) (Quotient.mk s b) = Quotient.mk s (comp a b)
def
PointwiseComposition.FailureOfComposition.WeaklyTotal
{A : Type u}
(s : Setoid A)
(comp : A → A → A)
(z e : A)
:
The Weakly Total construction in FailureOfComposition.
Equations
- PointwiseComposition.FailureOfComposition.WeaklyTotal s comp z e = ∀ (d : A), Setoid.r (comp e d) z → Setoid.r d z
Instances For
theorem
PointwiseComposition.FailureOfComposition.weaklyTotal_identity
{A : Type u}
(s : Setoid A)
(comp : A → A → A)
(i z : A)
(hi : ∀ (d : A), Setoid.r (comp i d) d)
:
WeaklyTotal s comp z i
theorem
PointwiseComposition.FailureOfComposition.not_weaklyTotal_guard
{A : Type u}
(s : Setoid A)
(comp : A → A → A)
(f g z : A)
(hfg : Setoid.r (comp f g) z)
(hgz : ¬Setoid.r g z)
:
¬WeaklyTotal s comp z f