Skip to content

Instantly share code, notes, and snippets.

@khibino
Last active November 16, 2022 08:25
Show Gist options
  • Save khibino/90e0f971b9c922e7df8cbe92ef1e6744 to your computer and use it in GitHub Desktop.
Save khibino/90e0f971b9c922e7df8cbe92ef1e6744 to your computer and use it in GitHub Desktop.
open import Agda.Builtin.Equality using (_≡_; refl)
open import Relation.Binary.PropositionalEquality.Core using (sym; trans; _≢_)
-- open import Data.Nat.Base
open import Data.Nat.Base
using (ℕ; zero; suc; _+_; _*_; s≤s; z≤n; _≤_; _<_; _>_;
Ordering; less; equal; greater; compare)
open import Data.Nat.Properties using (+-identityʳ; +-assoc; ≤-trans; m≤m+n; m≢1+m+n; *-cancelˡ-≡)
open import Data.Empty using (⊥)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; _,_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
infixr 2 _⋀_
_⋀_ : Set -> Set -> Set
_⋀_ = _×_
infixr 1 _⋁_
_⋁_ : Set -> Set -> Set
_⋁_ = _⊎_
-----
compareX : ∀ m n → Ordering m n
compareX zero zero = equal zero
compareX (suc m) zero = greater zero m
compareX zero (suc n) = less zero n
compareX (suc m) (suc n) with compareX m n
... | less m k = less (suc m) k
... | equal m = equal (suc m)
... | greater n k = greater (suc n) k
lt|eq|gt : ∀ {n m} -> Ordering n m -> n < m ⋁ n ≡ m ⋁ n > m
lt|eq|gt {n} {.(suc (n + k))} (less .n k) = inj₁ (s≤s (m≤m+n n k))
lt|eq|gt {n} {.n} (equal .n) = inj₂ (inj₁ refl)
lt|eq|gt {.(suc (m + k))} {m} (greater .m k) = inj₂ (inj₂ (s≤s (m≤m+n m k)))
-----
data QuotRem : ℕ -> ℕ -> ℕ -> ℕ -> Set where
quotRem : ∀ {n m q r} -> n ≡ r + m * q -> 0 ≤ r -> r < m -> QuotRem n m q r
Divisor : ℕ -> ℕ -> ℕ -> Set
Divisor n m q = QuotRem n m q 0
ex1 : QuotRem 5 3 1 2
ex1 = quotRem refl z≤n (s≤s (s≤s (s≤s z≤n)))
ex2 : Divisor 6 3 2
ex2 = quotRem refl z≤n (s≤s z≤n)
toContra : ∀ {ℓ} -> ∀ {A B : Set ℓ} -> (A -> B) -> ¬ B -> ¬ A
toContra f nb a = nb (f a)
contraLemma1 : ∀ n m o -> 1 ≤ n -> n * m ≢ n * suc (m + o)
contraLemma1 (suc n) m o le = toContra (*-cancelˡ-≡ n) (m≢1+m+n m)
uniqueDivisor : ∀ {m q₁ q₂ n : ℕ} -> Divisor n m q₁ -> Divisor n m q₂ -> q₁ ≡ q₂
uniqueDivisor {m} {q₁} {q₂} (quotRem eq₁ _ mp₁) (quotRem eq₂ _ mp₂)
with compare q₁ q₂
... | equal .q₁ = refl
uniqueDivisor {m} {q₁} {q₂} (quotRem eq₁ _ mp₁) (quotRem eq₂ _ mp₂)
| less .q₁ k with contraLemma1 m q₁ k mp₁ (trans (sym eq₁) eq₂)
... | ()
uniqueDivisor {m} {q₁} {q₂} (quotRem eq₁ _ mp₁) (quotRem eq₂ _ mp₂)
| greater .q₂ k with contraLemma1 m q₂ k mp₂ (trans (sym eq₂) eq₁)
... | ()
uniqueQuotRem : ∀ {m q₁ q₂ r₁ r₂ n : ℕ} -> QuotRem n m q₁ r₁ -> QuotRem n m q₂ r₂ -> q₁ ≡ q₂ ⋀ r₁ ≡ r₂
uniqueQuotRem {m} {q₁} {q₂} (quotRem eq₁ _ rm₁) (quotRem eq₂ _ rm₂)
with compare q₁ q₂
... | less .q₁ k = {!!}
... | equal .q₁ = refl , {!!}
... | greater .q₂ k = {!!}
(* Require Import Logic. *)
Require Import Arith.
Inductive Ordering : nat -> nat -> Type :=
| less : forall m k, Ordering m (S (m + k))
| equal : forall m, Ordering m m
| greater : forall m k, Ordering (S (m + k)) m
.
Fixpoint compare (m n : nat) : Ordering m n :=
match n with
| O => match m with
| O => equal O
| S m1 => greater O m1
end
| S n1 => match m with
| O => less O n1
| S m1 => match (compare m1 n1) with
| less m2 k => less (S m2) k
| equal m2 => equal (S m2)
| greater n2 k => greater (S n2) k
end
end
end
.
Print le.
(*
Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m.
*)
Lemma lt_eq_gt : forall n m, Ordering n m -> n < m \/ n = m \/ n > m.
intros n m OH.
inversion OH.
- left.
rewrite <- (plus_Sn_m n k).
exact (le_plus_l (S n) k).
- right. left.
reflexivity.
- right. right.
rewrite <- (plus_Sn_m m k).
exact (le_plus_l (S m) k).
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment