module Seance3 where open import Relation.Binary.PropositionalEquality open import Relation.Binary open import Function -- case open import Algebra.FunctionProperties -- open import Data.Nat.Properties open import Data.Nat.Base hiding (_≤_ ; _<_ ; _≰_ ; ≤-pred) open import Data.Product -- hiding (∃ ; ∃-syntax) open import Data.Sum open import Data.Empty Nat : Set Nat = ℕ -- The order on natural infix 4 _≤_ _<_ _≰_ data _≤_ : Nat -> Nat -> Set where z≤n : ∀ {n} -> (0 ≤ n) s≤s : ∀ {m n} -> (m ≤ n) -> (suc m ≤ suc n) _<_ : Nat -> Nat -> Set m < n = suc m ≤ n _≰_ : Nat -> Nat -> Set m ≰ n = (m ≤ n) -> ⊥ -- Some properties ≤-refl : ∀ {x} -> x ≤ x ≤-refl {x} = {!!} ≤-trans : ∀ {x y z} -> (x ≤ y) -> (y ≤ z) -> (x ≤ z) ≤-trans {x} {y} {z} p q = {!!} ≤-antisyx : ∀ {x y} -> (x ≤ y) -> (y ≤ x) -> (x ≡ y) ≤-antisyx p q = {!!} ≤-pred : ∀ {x y} → suc x ≤ suc y → x ≤ y ≤-pred q = {!!} ≤-total : ∀ {x y} → x ≤ y ⊎ y ≤ x ≤-total {x} {y} = {!!} ≤-suc : ∀ {x} -> (x ≤ suc x) ≤-suc {x} = {!!} -- One can check that ≤-refl and ≤-suc offer together an equivalent axiomatization of ≤ {- As defined in library product data ∃ (A : ℕ → Set) : Set where _,_ : (x : ℕ) → A x → ∃ A -- Sugar syntax for the existential quantifier. syntax ∃ (λ x → e) = ∃[ x ] e -} -- SUBSTRACTION -- substraction specification : Minus x y z should be inhabited when x - y = z -- Observe that such a spec yields at most one inhabitant per type instance. data Minus : Nat -> Nat -> Nat -> Set where baseM : (x : Nat) -> Minus x 0 x indM : (x y z : Nat) -> Minus x y z -> Minus (suc x) (suc y) z unicity1 : {x y z z' : Nat} -> Minus x y z -> Minus x y z' -> z ≡ z' unicity1 p q = {!!} unicity2 : {x x' y z : Nat} -> Minus x y z -> Minus x' y z -> x ≡ x' unicity2 p q = {!!} -- for some reason the following is hard to prove unicity3 : {x y y' z : Nat} -> Minus x y z -> Minus x y' z -> y ≡ y' unicity3 p q = {!!} ∃-minus : (x y : Nat) -> (y ≤ x) -> ∃[ z ] Minus x y z ∃-minus x y p = {!!} minus : (x y : Nat) -> (y ≤ x) -> Nat minus x y p = proj₁ (∃-minus x y p) -- EUCLIDIAN DIVISION -- Euclidian division specification : Euclidian m d q r should be inhabited when 0 ≤ r < d and m = d * q + r -- Again, the spec is written in such a way that there is at most one inhabitant per type data Euclidian : Nat -> Nat -> Nat -> Nat -> Set where baseE : ∀ {m d : Nat} -> (m < d) -> Euclidian m d 0 m indE : ∀ {m1 m2 d q r : Nat} -> Minus m2 d m1 -> Euclidian m1 d q r -> Euclidian m2 d (suc q) r