------------------------------------------------------------------------ -- The Agda standard library -- -- Some boring lemmas used by the ring solver ------------------------------------------------------------------------ -- Note that these proofs use all "almost commutative ring" properties. {-# OPTIONS --cubical-compatible --safe #-} open import Algebra open import Algebra.Solver.Ring.AlmostCommutativeRing module Algebra.Solver.Ring.Lemmas {r₁ r₂ r₃ r₄} (coeff : RawRing r₁ r₄) (r : AlmostCommutativeRing r₂ r₃) (morphism : coeff -Raw-AlmostCommutative⟶ r) where private module C = RawRing coeff open AlmostCommutativeRing r open import Algebra.Morphism open _-Raw-AlmostCommutative⟶_ morphism open import Relation.Binary.Reasoning.Setoid setoid open import Function.Base using (_⟨_⟩_; _$_) lemma₀ : ∀ a b c x → (a + b) * x + c ≈ a * x + (b * x + c) lemma₀ a b c x = begin (a + b) * x + c ≈⟨ distribʳ _ _ _ ⟨ +-cong ⟩ refl ⟩ (a * x + b * x) + c ≈⟨ +-assoc _ _ _ ⟩ a * x + (b * x + c) ∎ lemma₁ : ∀ a b c d x → (a + b) * x + (c + d) ≈ (a * x + c) + (b * x + d) lemma₁ a b c d x = begin (a + b) * x + (c + d) ≈⟨ lemma₀ _ _ _ _ ⟩ a * x + (b * x + (c + d)) ≈⟨ refl ⟨ +-cong ⟩ sym (+-assoc _ _ _) ⟩ a * x + ((b * x + c) + d) ≈⟨ refl ⟨ +-cong ⟩ (+-comm _ _ ⟨ +-cong ⟩ refl) ⟩ a * x + ((c + b * x) + d) ≈⟨ refl ⟨ +-cong ⟩ +-assoc _ _ _ ⟩ a * x + (c + (b * x + d)) ≈⟨ sym $ +-assoc _ _ _ ⟩ (a * x + c) + (b * x + d) ∎ lemma₂ : ∀ a b c x → a * c * x + b * c ≈ (a * x + b) * c lemma₂ a b c x = begin a * c * x + b * c ≈⟨ lem ⟨ +-cong ⟩ refl ⟩ a * x * c + b * c ≈⟨ sym $ distribʳ _ _ _ ⟩ (a * x + b) * c ∎ where lem = begin a * c * x ≈⟨ *-assoc _ _ _ ⟩ a * (c * x) ≈⟨ refl ⟨ *-cong ⟩ *-comm _ _ ⟩ a * (x * c) ≈⟨ sym $ *-assoc _ _ _ ⟩ a * x * c ∎ lemma₃ : ∀ a b c x → a * b * x + a * c ≈ a * (b * x + c) lemma₃ a b c x = begin a * b * x + a * c ≈⟨ *-assoc _ _ _ ⟨ +-cong ⟩ refl ⟩ a * (b * x) + a * c ≈⟨ sym $ distribˡ _ _ _ ⟩ a * (b * x + c) ∎ lemma₄ : ∀ a b c d x → (a * c * x + (a * d + b * c)) * x + b * d ≈ (a * x + b) * (c * x + d) lemma₄ a b c d x = begin (a * c * x + (a * d + b * c)) * x + b * d ≈⟨ distribʳ _ _ _ ⟨ +-cong ⟩ refl ⟩ (a * c * x * x + (a * d + b * c) * x) + b * d ≈⟨ refl ⟨ +-cong ⟩ ((refl ⟨ +-cong ⟩ refl) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩ (a * c * x * x + (a * d + b * c) * x) + b * d ≈⟨ +-assoc _ _ _ ⟩ a * c * x * x + ((a * d + b * c) * x + b * d) ≈⟨ lem₁ ⟨ +-cong ⟩ (lem₂ ⟨ +-cong ⟩ refl) ⟩ a * x * (c * x) + (a * x * d + b * (c * x) + b * d) ≈⟨ refl ⟨ +-cong ⟩ +-assoc _ _ _ ⟩ a * x * (c * x) + (a * x * d + (b * (c * x) + b * d)) ≈⟨ sym $ +-assoc _ _ _ ⟩ a * x * (c * x) + a * x * d + (b * (c * x) + b * d) ≈⟨ sym $ distribˡ _ _ _ ⟨ +-cong ⟩ distribˡ _ _ _ ⟩ a * x * (c * x + d) + b * (c * x + d) ≈⟨ sym $ distribʳ _ _ _ ⟩ (a * x + b) * (c * x + d) ∎ where lem₁′ = begin a * c * x ≈⟨ *-assoc _ _ _ ⟩ a * (c * x) ≈⟨ refl ⟨ *-cong ⟩ *-comm _ _ ⟩ a * (x * c) ≈⟨ sym $ *-assoc _ _ _ ⟩ a * x * c ∎ lem₁ = begin a * c * x * x ≈⟨ lem₁′ ⟨ *-cong ⟩ refl ⟩ a * x * c * x ≈⟨ *-assoc _ _ _ ⟩ a * x * (c * x) ∎ lem₂ = begin (a * d + b * c) * x ≈⟨ distribʳ _ _ _ ⟩ a * d * x + b * c * x ≈⟨ *-assoc _ _ _ ⟨ +-cong ⟩ *-assoc _ _ _ ⟩ a * (d * x) + b * (c * x) ≈⟨ (refl ⟨ *-cong ⟩ *-comm _ _) ⟨ +-cong ⟩ refl ⟩ a * (x * d) + b * (c * x) ≈⟨ sym $ *-assoc _ _ _ ⟨ +-cong ⟩ refl ⟩ a * x * d + b * (c * x) ∎ lemma₅ : ∀ x → (0# * x + 1#) * x + 0# ≈ x lemma₅ x = begin (0# * x + 1#) * x + 0# ≈⟨ ((zeroˡ _ ⟨ +-cong ⟩ refl) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩ (0# + 1#) * x + 0# ≈⟨ (+-identityˡ _ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩ 1# * x + 0# ≈⟨ +-identityʳ _ ⟩ 1# * x ≈⟨ *-identityˡ _ ⟩ x ∎ lemma₆ : ∀ a x → 0# * x + a ≈ a lemma₆ a x = begin 0# * x + a ≈⟨ zeroˡ _ ⟨ +-cong ⟩ refl ⟩ 0# + a ≈⟨ +-identityˡ _ ⟩ a ∎ lemma₇ : ∀ x → - 1# * x ≈ - x lemma₇ x = begin - 1# * x ≈⟨ -‿*-distribˡ _ _ ⟩ - (1# * x) ≈⟨ -‿cong (*-identityˡ _) ⟩ - x ∎