{"header":{"message":"3. Relations","description":null,"timestamp":"2026-01-18T20:05:06Z","authors":[{"email":"tzemanovic@gmail.com","name":"Tomáš Zemanovič"}]},"hash":"YLTANVG3K2CWRDK7IQMF7AQJT5FKOU4ROJAYHHDTILSK7ON5GWPAC","authors":[],"deps":{"hashes":[["YLTANVG3K2CWRDK7IQMF7AQJT5FKOU4ROJAYHHDTILSK7ON5GWPAC","3. Relations"],["AA",null],["SHHLAOUJR4YNATSPEACPP56ITB6353COYJGUDEN47747EFPYJNQAC","Bump sass from 1.89.2 to 1.90.0 (#1124)"]],"deps":["SHHLAOUJR4YNATSPEACPP56ITB6353COYJGUDEN47747EFPYJNQAC"],"known":[]},"hunks":[{"Edit":{"inode":{"change":2,"pos":7761142},"path":"src/plfa/part1/Relations.lagda.md","line":247,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":7769190}],"down_context":[{"change":2,"pos":7769190}],"flag":"BLOCK","start":113,"end":141,"inode":{"change":2,"pos":7761142}}},"contents":[{"Add":"-- Divides relation on ints"}]}},{"Edit":{"inode":{"change":2,"pos":7761142},"path":"src/plfa/part1/Relations.lagda.md","line":254,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":7769289}],"down_context":[{"change":2,"pos":7769289}],"flag":"BLOCK","start":142,"end":170,"inode":{"change":2,"pos":7761142}}},"contents":[{"Add":"-- Divides relation on nats"}]}},{"Replacement":{"inode":{"change":2,"pos":7761142},"path":"src/plfa/part1/Relations.lagda.md","line":368,"ins":{"up_context":[{"change":2,"pos":7773626}],"down_context":[{"change":2,"pos":7773630}],"flag":"BLOCK","start":171,"end":865,"inode":{"change":2,"pos":7761142}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":7773626},"to":{"change":2,"start":7773626,"end":7773630},"introduced_by":2}],"inode":{"change":2,"pos":7761142}},"ins_contents":[{"Add":""},{"Add":"-- Because if one of the implicit arguments (`m` or `n`) is zero, it cannot be greater than anything else that's non-zero"},{"Add":""},{"Add":"≤-antisym' : ∀ {m n : ℕ}"},{"Add":" → m ≤ n"},{"Add":" → n ≤ m"},{"Add":" -----"},{"Add":" → m ≡ n"},{"Add":"≤-antisym' z≤n z≤n = refl"},{"Add":"≤-antisym' (s≤s m≤n) (s≤s n≤m) = cong suc (≤-antisym m≤n n≤m)"},{"Add":"-- The case for the constructor s≤s is impossible"},{"Add":"-- because unification ended with a conflicting equation"},{"Add":"-- suc n ≟ zero"},{"Add":"-- Possible solution: remove the clause, or use an absurd pattern ()."},{"Add":"-- when checking that the pattern s≤s n≤m has type n ≤ zero"},{"Add":"-- ≤-antisym' z≤n (s≤s n≤m) = ?"},{"Add":"-- ≤-antisym' (s≤s n≤m) z≤n = ?"}],"del_contents":[{"Del":"```\n"}]}},{"Edit":{"inode":{"change":2,"pos":7761142},"path":"src/plfa/part1/Relations.lagda.md","line":386,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":7773631}],"down_context":[{"change":2,"pos":7773631}],"flag":"BLOCK","start":866,"end":870,"inode":{"change":2,"pos":7761142}}},"contents":[{"Add":"```"}]}},{"Edit":{"inode":{"change":2,"pos":7761142},"path":"src/plfa/part1/Relations.lagda.md","line":575,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":7780856}],"down_context":[{"change":2,"pos":7780856}],"flag":"BLOCK","start":871,"end":1476,"inode":{"change":2,"pos":7761142}}},"contents":[{"Add":""},{"Add":"*-monoʳ-≤ : ∀ (n p q : ℕ)"},{"Add":" → p ≤ q"},{"Add":" → n * p ≤ n * q"},{"Add":"*-monoʳ-≤ zero p q p≤q = z≤n"},{"Add":"-- Goal: p + n * p ≤ q + n * q"},{"Add":"*-monoʳ-≤ (suc n) p q p≤q ="},{"Add":" let n*p≤n*q = (*-monoʳ-≤ n p q p≤q) in"},{"Add":" +-mono-≤ p q (n * p) (n * q) p≤q n*p≤n*q"},{"Add":""},{"Add":"*-monoˡ-≤ : ∀ (m n p : ℕ)"},{"Add":" → m ≤ n"},{"Add":" → m * p ≤ n * p"},{"Add":"*-monoˡ-≤ m n p m≤n rewrite *-comm m p | *-comm n p = *-monoʳ-≤ p m n m≤n"},{"Add":""},{"Add":"*-mono-≤ : ∀ (m n p q : ℕ)"},{"Add":" → m ≤ n"},{"Add":" → p ≤ q"},{"Add":" → m * p ≤ n * q"},{"Add":"*-mono-≤ m n p q m≤n p≤q = ≤-trans (*-monoˡ-≤ m n p m≤n) (*-monoʳ-≤ n p q p≤q)"},{"Add":""}]}},{"Edit":{"inode":{"change":2,"pos":7761142},"path":"src/plfa/part1/Relations.lagda.md","line":644,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":7782424}],"down_context":[{"change":2,"pos":7782424}],"flag":"BLOCK","start":1477,"end":1623,"inode":{"change":2,"pos":7761142}}},"contents":[{"Add":""},{"Add":"<-trans : ∀ {m n p : ℕ}"},{"Add":" → m < n"},{"Add":" → n < p"},{"Add":" → m < p"},{"Add":"<-trans z_"},{"Add":""},{"Add":"-- NOTE: This does not work as it has incomplete cases"},{"Add":"-- _>_ : ∀ {m n : ℕ} → n < m"},{"Add":"-- _>_ {suc m} {zero} = z_ {suc m} {suc n} = s_ {m} {n})"},{"Add":""},{"Add":"-- NOTE: no relation to `_<_`"},{"Add":"data _>_ : ℕ → ℕ → Set where"},{"Add":" s>z : ∀ {n : ℕ} → suc n > zero"},{"Add":" s>s : ∀ {m n : ℕ} → m > n → suc m > suc n"},{"Add":""},{"Add":"data Trichotomy (m n : ℕ) : Set where"},{"Add":" forward : m > n → Trichotomy m n"},{"Add":" flipped : n > m → Trichotomy m n"},{"Add":" equal : m ≡ n → Trichotomy m n"},{"Add":""},{"Add":"-- NOTE: relation to `_<_`, but seems complicated"},{"Add":"-- data _>_ : ∀ {m n : ℕ} {nz : ∀ {m : ℕ} → _>_ {suc m} {zero} {zs : ∀ {m n : ℕ} → (n_ {suc m} {suc n} {s_ {m} {n} {n_ {n} {m} {m Set where"},{"Add":" one : One (⟨⟩ I)"},{"Add":" suc : ∀ {b : Bin} → One b → One (inc b)"},{"Add":""},{"Add":"-- NOTE: Using a bin-law from Induction.lagda.md"},{"Add":"from-inc-suc-from : ∀ (b : Bin) → from (inc b) ≡ suc (from b)"},{"Add":"from-inc-suc-from ⟨⟩ = refl"},{"Add":"from-inc-suc-from (b O) = refl"},{"Add":"from-inc-suc-from (b I) rewrite cong (\\x → 2 * x) (from-inc-suc-from b) | *-comm 2 (1 + (from b)) | cong (\\x → 2 + x) (*-comm (from b) 2) = refl"},{"Add":""},{"Add":"1≤from-one : ∀ {b : Bin} → One b → 1 ≤ from b"},{"Add":"1≤from-one one = s≤s z≤n"},{"Add":"1≤from-one (suc {b} x) rewrite from-inc-suc-from b = s≤s z≤n"},{"Add":""},{"Add":"data Can : Bin → Set where"},{"Add":" zeroᴮ : Can (⟨⟩ O)"},{"Add":" leading : ∀ {b : Bin} → One b → Can b"},{"Add":""},{"Add":"inc-can : ∀ {b : Bin} → Can b → Can (inc b)"},{"Add":"inc-can zeroᴮ = leading one"},{"Add":"inc-can (leading x) = leading (suc x)"},{"Add":""},{"Add":"to-can : (n : ℕ) → Can (to n)"},{"Add":"to-can zero = zeroᴮ"},{"Add":"to-can (suc n) = inc-can (to-can n)"},{"Add":""}]}}],"owner":"tzemanovic","repo":"plfa","token":"INEcprt8kWorItDpG10dAM1QnbaGYPrR0hAzdvFHPfg=","login":null}

…

Dependencies

Change contents