From 72feeec46c34c678640341e76958481f4244d8df Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Thu, 12 Jan 2023 17:57:06 +0000 Subject: Provide examples of Obs code. This folder spells out the action of equality and cast for the different type constructors. Ideally the two correctness proofs should given by reflexivity. --- examples/equality/Pi.obs | 46 +++++++++++++++++++++++++++++++++++++++++ examples/equality/Sigma.obs | 47 ++++++++++++++++++++++++++++++++++++++++++ examples/equality/Universe.obs | 31 ++++++++++++++++++++++++++++ examples/equality/template.obs | 22 ++++++++++++++++++++ 4 files changed, 146 insertions(+) create mode 100644 examples/equality/Pi.obs create mode 100644 examples/equality/Sigma.obs create mode 100644 examples/equality/Universe.obs create mode 100644 examples/equality/template.obs diff --git a/examples/equality/Pi.obs b/examples/equality/Pi.obs new file mode 100644 index 0000000..6364e2d --- /dev/null +++ b/examples/equality/Pi.obs @@ -0,0 +1,46 @@ +TypeData : Set 1 +TypeData = (domain : Set) ** (x : domain) -> Set + +domain : (type : TypeData) -> Set +domain = \type => fst type + +codomain : (type : TypeData) -> (x : domain type) -> Set +codomain = \type => snd type + +Value : (type : TypeData) -> Set +Value = \type => (x : domain type) -> codomain type x + +Equality : (left : TypeData) -> (right : TypeData) -> Prop +Equality = \left => \right => + (domainEquality : domain right ~ domain left) ** + (x : domain right) -> + codomain left (cast (domain right) (domain left) domainEquality x) ~ codomain right x + +Cast : + (oldType : TypeData) -> + (newType : TypeData) -> + (equality : Equality oldType newType) -> + (value : Value oldType) -> + Value newType +Cast = \oldType => \newType => \equality => \value => + \x => + cast + (codomain oldType (cast (domain newType) (domain oldType) (fst equality) x)) + (codomain newType x) + (snd equality x) + (value (cast (domain newType) (domain oldType) (fst equality) x)) + +EqualityCorrect : + (left : TypeData) -> + (right : TypeData) -> + Equality left right ~ (Value left ~ Value right) +EqualityCorrect = refl Equality + +CastCorrect : + (oldType : TypeData) -> + (newType : TypeData) -> + (equality : Equality oldType newType) -> + (value : Value oldType) -> + Cast oldType newType equality value ~ + cast (Value oldType) (Value newType) (fst (EqualityCorrect oldType newType) equality) value +CastCorrect = refl Cast diff --git a/examples/equality/Sigma.obs b/examples/equality/Sigma.obs new file mode 100644 index 0000000..f742183 --- /dev/null +++ b/examples/equality/Sigma.obs @@ -0,0 +1,47 @@ +TypeData : Set 1 +TypeData = (index : Set) ** (x : index) -> Set + +index : (type : TypeData) -> Set +index = \type => fst type + +element : (type : TypeData) -> (x : index type) -> Set +element = \type => snd type + +Value : (type : TypeData) -> Set +Value = \type => (x : index type) ** element type x + +Equality : (left : TypeData) -> (right : TypeData) -> Prop +Equality = \left => \right => + (indexEquality : index left ~ index right) ** + (x : index left) -> + element left x ~ element right (cast (index left) (index right) indexEquality x) + +Cast : + (oldType : TypeData) -> + (newType : TypeData) -> + (equality : Equality oldType newType) -> + (value : Value oldType) -> + Value newType +Cast = \oldType => \newType => \equality => \value => + < cast (index oldType) (index newType) (fst equality) (fst value) + , cast + (element oldType (fst value)) + (element newType (cast (index oldType) (index newType) (fst equality) (fst value))) + (snd equality (fst value)) + (snd value) + > + +EqualityCorrect : + (left : TypeData) -> + (right : TypeData) -> + Equality left right ~ (Value left ~ Value right) +EqualityCorrect = refl Equality + +CastCorrect : + (oldType : TypeData) -> + (newType : TypeData) -> + (equality : Equality oldType newType) -> + (value : Value oldType) -> + Cast oldType newType equality value ~ + cast (Value oldType) (Value newType) (fst (EqualityCorrect oldType newType) equality) value +CastCorrect = refl Cast diff --git a/examples/equality/Universe.obs b/examples/equality/Universe.obs new file mode 100644 index 0000000..19a8408 --- /dev/null +++ b/examples/equality/Universe.obs @@ -0,0 +1,31 @@ +TypeData : Prop +TypeData = () + +Value : (type : TypeData) -> Set 1 +Value = \type => Set + +Equality : (left : TypeData) -> (right : TypeData) -> Prop +Equality = \left => \right => () + +Cast : + (oldType : TypeData) -> + (newType : TypeData) -> + (equality : Equality oldType newType) -> + (value : Value oldType) -> + Value newType +Cast = \oldType => \newType => \equality => \value => value + +EqualityCorrect : + (left : TypeData) -> + (right : TypeData) -> + Equality left right ~ (Value left ~ Value right) +EqualityCorrect = refl Equality + +CastCorrect : + (oldType : TypeData) -> + (newType : TypeData) -> + (equality : Equality oldType newType) -> + (value : Value oldType) -> + Cast oldType newType equality value ~ + cast (Value oldType) (Value newType) (fst (EqualityCorrect oldType newType) equality) value +CastCorrect = refl Cast diff --git a/examples/equality/template.obs b/examples/equality/template.obs new file mode 100644 index 0000000..856e05f --- /dev/null +++ b/examples/equality/template.obs @@ -0,0 +1,22 @@ +postulate TypeData : Set 1 +postulate Value : (type : TypeData) -> Set +postulate Equality : (left : TypeData) -> (right : TypeData) -> Prop +postulate Cast : + (oldType : TypeData) -> + (newType : TypeData) -> + (equality : Equality oldType newType) -> + (value : Value oldType) -> + Value newType + +postulate EqualityCorrect : + (left : TypeData) -> + (right : TypeData) -> + Equality left right ~ (Value left ~ Value right) + +postulate CastCorrect : + (oldType : TypeData) -> + (newType : TypeData) -> + (equality : Equality oldType newType) -> + (value : Value oldType) -> + Cast oldType newType equality value ~ + cast (Value oldType) (Value newType) (fst (EqualityCorrect oldType newType) equality) value -- cgit v1.2.3