michael/type-theory
2
0
Fork 0
Code Issues 21 Pull requests Projects 1 Releases 1 Packages Wiki Activity Actions

solve demo file

Browse source
This commit is contained in:
Michael Zhang 2024-10-15 14:31:10 -05:00
parent a56ff16ed9
commit e0c0e56967
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
talks/2024-grads/Demo.agda
View file

@ -1,14 +1,20 @@
module 2024-grads.Demo where
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning)
open import Tactic.RingSolver.Core.AlmostCommutativeRing using (AlmostCommutativeRing)
open import Data.Nat.Tactic.RingSolver
open ≡-Reasoning
sumTo : ℕ → ℕ
sumTo zero = zero
sumTo (suc n) = (suc n) + (sumTo n)
lemma : ∀ (n : ℕ) → 2 * suc n + n * (n + 1) ≡ suc n * (suc n + 1)
lemma = solve-∀
theorem : ∀ (n : ℕ) → 2 * sumTo n ≡ (n * (n + 1))
theorem zero = refl
theorem (suc n) =
@ -21,6 +27,6 @@ theorem (suc n) =
2 * (suc n) + 2 * (sumTo n)
≡⟨ cong (2 * (suc n) +_) IH ⟩
2 * (suc n) + (n * (n + 1))
≡⟨ {! solve-∀ !} ⟩
≡⟨ lemma n ⟩
(suc n) * ((suc n) + 1)
∎
∎