Browse Source

Add first attempt at extensible equality.

idris
Thomas Kerber 1 year ago
parent
commit
cc79f8fa56
Signed by: Thomas Kerber <tk@drwx.org> GPG Key ID: 8489B911F9ED617B
2 changed files with 37 additions and 0 deletions
  1. +1
    -0
      .gitignore
  2. +36
    -0
      Yggdrasil/Extensible.idr

+ 1
- 0
.gitignore View File

@@ -1,2 +1,3 @@
/dist
/.stack-work
*.ibc

+ 36
- 0
Yggdrasil/Extensible.idr View File

@@ -0,0 +1,36 @@
import Prelude.Cast

infixr 5 ^=

data (^=) : a -> b -> Type where
Refl : x ^= x
Extend : {a : Type} -> {b : Type} -> (f : a -> b) -> (g : a -> b) -> ((x : a) -> f x ^= g x) -> f ^= g

eEqTransitive : a ^= b -> b ^= c -> a ^= c
eEqTransitive Refl eq = eq
eEqTransitive eq Refl = eq
eEqTransitive (Extend a _ prfab) (Extend _ d prfbc) = Extend a d (\x => eEqTransitive (prfab x) (prfbc x))

eEqSymmetric : a ^= b -> b ^= a
eEqSymmetric Refl = Refl
eEqSymmetric (Extend a b prfab) = Extend b a (\x => eEqSymmetric (prfab x))

Cast (a = b) (a ^= b) where
cast Refl = Refl

-- Tests

fiveEqFive : 5 ^= 5
fiveEqFive = Refl

Double1 : Nat -> Nat
Double1 x = x + x

Double2 : Nat -> Nat
Double2 x = 2 * x

doubleEqItems : (x : Nat) -> Double1 x ^= Double2 x
doubleEqItems n = rewrite plusZeroRightNeutral n in Refl

doubleEq : Double1 ^= Double2
doubleEq = Extend Double1 Double2 doubleEqItems

Loading…
Cancel
Save