Skip to content

Instantly share code, notes, and snippets.

@Kazark
Created September 18, 2020 19:00
Show Gist options
  • Save Kazark/994e08937009a1e8065d6bd7fba5209f to your computer and use it in GitHub Desktop.
Save Kazark/994e08937009a1e8065d6bd7fba5209f to your computer and use it in GitHub Desktop.
Example of a preorder that is not a partial order
module Length where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; trans)
open import Data.List using (List; _∷_; []; length)
open import Data.Nat using (ℕ; _≤_; s≤s; z≤n)
open import Data.Product using (∃-syntax; _,_; _×_; -,_)
open import Relation.Nullary using (¬_)
_ℕList≤_ : List ℕ → List ℕ → Set
xs ℕList≤ ys = length xs ≤ length ys
ℕList≤-refl : ∀{xs : List ℕ} → xs ℕList≤ xs
ℕList≤-refl {[]} = z≤n
ℕList≤-refl {x ∷ xs} = s≤s (ℕList≤-refl {xs})
ℕList≤-trans : ∀{xs ys zs : List ℕ} → xs ℕList≤ ys → ys ℕList≤ zs → xs ℕList≤ zs
ℕList≤-trans {x ∷ xs} {x₁ ∷ ys} {x₂ ∷ zs} (s≤s xs≤ys) (s≤s ys≤zs) = s≤s (ℕList≤-trans {xs} {ys} {zs} xs≤ys ys≤zs)
ℕList≤-trans {[]} {[]} {_} _ ys≤zs = ys≤zs
ℕList≤-trans {[]} {_ ∷ _} {_ ∷ _} _ _ = z≤n
not-anti-sym-List≤ : ∃[ m ]( ∃[ n ]( (m ℕList≤ n) × (n ℕList≤ m) × (¬ m ≡ n) ) )
not-anti-sym-List≤ = 1 ∷ [] , (2 ∷ [] , s≤s z≤n , s≤s z≤n , (λ ()))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment