Created
January 27, 2014 20:38
-
-
Save rodrigogribeiro/8656836 to your computer and use it in GitHub Desktop.
Problems with data constructor injectivity
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Preliminaries where | |
-- levels | |
postulate Level : Set | |
postulate LZero : Level | |
postulate LSuc : Level -> Level | |
postulate LMax : Level -> Level -> Level | |
{-# BUILTIN LEVEL Level #-} | |
{-# BUILTIN LEVELZERO LZero #-} | |
{-# BUILTIN LEVELSUC LSuc #-} | |
{-# BUILTIN LEVELMAX LMax #-} | |
id : forall {a}{A : Set a} -> A -> A | |
id x = x | |
-- natural numbers | |
data Nat : Set where | |
zero : Nat | |
suc : Nat -> Nat | |
{-# BUILTIN NATURAL Nat #-} | |
{-# BUILTIN ZERO zero #-} | |
{-# BUILTIN SUC suc #-} | |
-- propositional equality | |
data _==_ {l}{A : Set l} (x : A) : A -> Set l where | |
refl : x == x | |
{-# BUILTIN EQUALITY _==_ #-} | |
{-# BUILTIN REFL refl #-} | |
-- utilities about equality | |
cong : forall {a b}{A : Set a}{B : Set b}(f : A -> B){x y}-> x == y -> f x == f y | |
cong f refl = refl | |
cong2 : forall {a b c}{A : Set a}{B : Set b}{C : Set c} | |
(f : A -> B -> C){x y u v} -> x == y -> u == v -> f x u == f y v | |
cong2 f refl refl = refl | |
sym : forall {a}{A : Set a}{x y : A} -> x == y -> y == x | |
sym refl = refl | |
trans : forall {a}{A : Set a}{x y z : A} -> x == y -> y == z -> x == z | |
trans refl refl = refl | |
-- unit type, hidden arguments and steroids. | |
data Unit : Set where | |
unit : Unit | |
Hidden : forall {a} -> Set a -> Set a | |
Hidden A = Unit -> A | |
hide : forall {a b}{A : Set a}{B : A -> Set b} -> ((x : A) -> B x) -> ((x : A) -> Hidden (B x)) | |
hide f x unit = f x | |
reveal : forall {a}{A : Set a} -> Hidden A -> A | |
reveal f = f unit | |
data Reveal_is_ {a} {A : Set a} (x : Hidden A) (y : A) : Set a where | |
[_] : (eq : reveal x == y) -> Reveal x is y | |
inspect : forall {a b} {A : Set a} {B : A -> Set b} | |
(f : (x : A) -> B x) (x : A) -> Reveal (hide f x) is (f x) | |
inspect f x = [ refl ] | |
-- products | |
record Sigma {a b}(A : Set a)(B : A -> Set b) : Set (LMax a b) where | |
constructor _,_ | |
field | |
fst : A | |
snd : B fst | |
exists : forall {a b} -> {A : Set a}(B : A -> Set b) -> Set (LMax a b) | |
exists = Sigma _ | |
-- negation | |
data Empty : Set where | |
not : forall {l}(A : Set l) -> Set l | |
not A = A -> Empty | |
exFalsum : forall {l}{A : Set l} -> Empty -> A | |
exFalsum () | |
-- Lists | |
data List {l}(A : Set l) : Set l where | |
[] : List A | |
_::_ : A -> List A -> List A | |
infixl 4 _::_ | |
-- List membership | |
infixl 4 _<-_ | |
data _<-_ {A : Set} : A -> List A -> Set where | |
here : forall {x xs} -> x <- (x :: xs) | |
there : forall {x y ys} -> x <- ys -> x <- (y :: ys) | |
postulate <-irrev : forall {A : Set}{x : A}{xs : List A} -> (p p' : x <- xs) -> p == p' | |
---------------==================================================================================================== | |
module MySubst where | |
open import Preliminaries | |
-- type definition | |
Vars : Set | |
Vars = List Nat | |
data Ty (C : Vars) : Set where | |
var : forall {x} -> x <- C -> Ty C | |
app : forall (l r : Ty C) -> Ty C | |
con : Nat -> Ty C | |
_-_ : forall {x} -> (C : Vars) -> (v : x <- C) -> Vars | |
[] - () | |
(x :: c) - here = c | |
(x :: c) - (there p) = x :: (c - p) | |
weak : forall {x x' C} -> (p : x <- C) -> (p' : x' <- (C - p)) -> x' <- C | |
weak here p' = there p' | |
weak (there p) here = here | |
weak (there p) (there p') = there (weak p p') | |
infix 4 _<-==_ | |
data _<-==_ {C} : forall {t t'} -> t <- C -> t' <- C -> Set where | |
same : forall {t} (x : t <- C) -> x <-== x | |
diff : forall {t t'} (x : t <- C ) (v : t' <- (C - x)) -> x <-== (weak x v) | |
varDiff : forall {t t' C} -> (x : t <- C) (v : t' <- C) -> x <-== v | |
varDiff here here = same here | |
varDiff here (there v) = diff here v | |
varDiff (there x) here = diff (there x) here | |
varDiff (there x) (there v) with varDiff x v | |
varDiff (there .v) (there v) | same .v = same (there v) | |
varDiff (there x) (there .(weak x v)) | diff .x v = diff (there x) (there v) | |
replace : forall {x C} -> (p : x <- C) -> (t : Ty (C - p)) -> Ty C -> Ty (C - p) | |
replace p t (var x) with varDiff p x | |
replace .x₁ t (var x₁) | same .x₁ = t | |
replace p t (var .(weak p v)) | diff .p v = var v | |
replace p t (app t' t'') = app (replace p t t') (replace p t t'') | |
replace p t (con x) = con x | |
weakTy : forall {x C} -> (p : x <- C) -> (t : Ty (C - p)) -> Ty C | |
weakTy p (var v) = var (weak p v) | |
weakTy p (app t t') = app (weakTy p t) (weakTy p t') | |
weakTy p (con c) = con c | |
weakApp : forall {x C} -> (p : x <- C)(t : Ty (C - p))(t' t'' : Ty C) -> | |
weakTy p t == (app t' t'') -> exists (\ a -> exists (\ b -> t == app a b)) | |
weakApp p (var x₂) t' t'' () | |
weakApp p (app t t₁) .(weakTy p t) .(weakTy p t₁) refl = t , (t₁ , refl) | |
weakApp p (con x₁) t' t'' () | |
postulate thereInv : forall {x C}(r : x <- C)(v : x <- C - r) -> there (weak r v) == there r -> weak r v == r | |
weakLeft : forall {x C}(r : x <- C)(v : x <- C - r) -> not (weak r v == r) | |
weakLeft here v () | |
weakLeft (there r) here () | |
weakLeft (there r) (there v) p = (weakLeft r v) (thereInv r v p) | |
replaceWeakTy : forall {x C} -> (v : x <- C) -> (t : Ty (C - v)) -> t == replace v t (weakTy v t) | |
replaceWeakTy v t with weakTy v t | inspect (weakTy v) t | |
replaceWeakTy v (var x) | (var y) | [ eq ] = {!!} | |
--replaceWeakTy v (var x₂) | var x₄ | [ eq ] with varDiff v x₄ | |
--replaceWeakTy .x₄ (var x₂) | var x₄ | [ eq ] | same .x₄ = refl | |
--replaceWeakTy v (var x₃) | var .(weak v v₁) | [ eq ] | diff .v v₁ = {!exFalsum ?!} | |
replaceWeakTy v (app t t₁) | var x₂ | [ () ] | |
replaceWeakTy v (con x₁) | var x₃ | [ () ] | |
replaceWeakTy v t | app t' t'' | [ eq ] with weakApp v t t' t'' eq | |
replaceWeakTy v (var x₂) | app t' t'' | [ () ] | a , (b , c) | |
replaceWeakTy v (app .a .b) | app .(weakTy v a) .(weakTy v b) | [ refl ] | a , (b , refl) with replaceWeakTy v a | replaceWeakTy v b | |
...| ra | rb = {!!} | |
replaceWeakTy v (con x₁) | app t' t'' | [ () ] | a , (b , c) | |
replaceWeakTy v (var x₂) | con x₃ | [ () ] | |
replaceWeakTy v (app t t₁) | con x₁ | [ () ] | |
replaceWeakTy v (con x₁) | con x₂ | [ eq ] = cong (\ t -> replace v (con x₁) t) eq | |
replaceWeakVar : forall {x y C} -> (p : x <- C)(v : y <- C - p)(t : Ty (C - p)) -> var v == replace p t (var (weak p v)) | |
replaceWeakVar p v t with weak p v | inspect (weak p) v | varDiff p (weak p v) | |
replaceWeakVar .r v t | r | [ eq ] | same .r = exFalsum (weakLeft r v eq) | |
replaceWeakVar p v t | .(weak p v₁) | [ eq ] | diff .p v₁ = cong var (<-irrev v v₁) | |
replace-idem : forall {x C} -> (v : x <- C) -> (t : Ty (C - v)) -> (t' : Ty C) -> replace v t t' == replace v t (weakTy v (replace v t t')) | |
replace-idem p t (var v) with varDiff p v | |
replace-idem .v t (var v) | same .v = replaceWeakTy v t | |
replace-idem p t (var .(weak p v)) | diff .p v = replaceWeakVar p v t | |
replace-idem p t (app t' t'') = cong2 app (replace-idem p t t') (replace-idem p t t'') | |
replace-idem p t (con c) = refl |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment