mirror of https://github.com/nmvdw/HITs-Examples
Added interface of finite stes
This commit is contained in:
Niels
parent
376efbf2e9
commit
d9cde16f5a
|
|
@ -1,98 +0,0 @@
|
||||||
{-# OPTIONS --without-K --rewriting #-}
|
|
||||||
|
|
||||||
open import HoTT
|
|
||||||
|
|
||||||
module CL where
|
|
||||||
|
|
||||||
private
|
|
||||||
data CL' : Set where
|
|
||||||
K' : CL'
|
|
||||||
S' : CL'
|
|
||||||
app' : CL' -> CL' -> CL'
|
|
||||||
|
|
||||||
CL : Set
|
|
||||||
CL = CL'
|
|
||||||
|
|
||||||
K : CL
|
|
||||||
K = K'
|
|
||||||
|
|
||||||
Sc : CL
|
|
||||||
Sc = S'
|
|
||||||
|
|
||||||
app : CL -> CL -> CL
|
|
||||||
app = app'
|
|
||||||
|
|
||||||
postulate
|
|
||||||
KConv : {x y : CL} -> app (app K x) y == x
|
|
||||||
SConv : {x y z : CL} -> app (app (app Sc x) y) z == app (app x z) (app y z)
|
|
||||||
|
|
||||||
CLind : (Y : CL -> Set)
|
|
||||||
(KY : Y K)
|
|
||||||
(SY : Y Sc)
|
|
||||||
(appY : (x y : CL) -> Y x -> Y y -> Y (app x y))
|
|
||||||
(KConvY : (x y : CL) (a : Y x) (b : Y y) -> PathOver Y KConv (appY (app K x) y (appY K x KY a) b) a)
|
|
||||||
(SConvY : (x y z : CL) (a : Y x) (b : Y y) (c : Y z) ->
|
|
||||||
PathOver Y SConv
|
|
||||||
(appY
|
|
||||||
(app (app Sc x) y)
|
|
||||||
z
|
|
||||||
(appY
|
|
||||||
(app Sc x)
|
|
||||||
y
|
|
||||||
(appY Sc x SY a)
|
|
||||||
b
|
|
||||||
)
|
|
||||||
c
|
|
||||||
)
|
|
||||||
(appY (app x z) (app y z) (appY x z a c) (appY y z b c))
|
|
||||||
)
|
|
||||||
(x : CL) -> Y x
|
|
||||||
CLind Y KY SY appY _ _ K' = KY
|
|
||||||
CLind Y KY SY appY _ _ S' = SY
|
|
||||||
CLind Y KY SY appY KConvY SConvY (app' x x₁) = appY x x₁ (CLind Y KY SY appY KConvY SConvY x) (CLind Y KY SY appY KConvY SConvY x₁)
|
|
||||||
|
|
||||||
postulate
|
|
||||||
CLind_βKConv : (Y : CL -> Set)
|
|
||||||
(KY : Y K)
|
|
||||||
(SY : Y Sc)
|
|
||||||
(appY : (x y : CL) -> Y x -> Y y -> Y (app x y))
|
|
||||||
(KConvY : (x y : CL) (a : Y x) (b : Y y) -> PathOver Y KConv (appY (app K x) y (appY K x KY a) b) a)
|
|
||||||
(SConvY : (x y z : CL) (a : Y x) (b : Y y) (c : Y z) ->
|
|
||||||
PathOver Y SConv
|
|
||||||
(appY
|
|
||||||
(app (app Sc x) y)
|
|
||||||
z
|
|
||||||
(appY
|
|
||||||
(app Sc x)
|
|
||||||
y
|
|
||||||
(appY Sc x SY a)
|
|
||||||
b
|
|
||||||
)
|
|
||||||
c
|
|
||||||
)
|
|
||||||
(appY (app x z) (app y z) (appY x z a c) (appY y z b c))
|
|
||||||
)
|
|
||||||
(x y : CL) ->
|
|
||||||
apd (CLind Y KY SY appY KConvY SConvY) KConv == KConvY x y (CLind Y KY SY appY KConvY SConvY x) (CLind Y KY SY appY KConvY SConvY y)
|
|
||||||
CLind_βSConv : (Y : CL -> Set)
|
|
||||||
(KY : Y K)
|
|
||||||
(SY : Y Sc)
|
|
||||||
(appY : (x y : CL) -> Y x -> Y y -> Y (app x y))
|
|
||||||
(KConvY : (x y : CL) (a : Y x) (b : Y y) -> PathOver Y KConv (appY (app K x) y (appY K x KY a) b) a)
|
|
||||||
(SConvY : (x y z : CL) (a : Y x) (b : Y y) (c : Y z) ->
|
|
||||||
PathOver Y SConv
|
|
||||||
(appY
|
|
||||||
(app (app Sc x) y)
|
|
||||||
z
|
|
||||||
(appY
|
|
||||||
(app Sc x)
|
|
||||||
y
|
|
||||||
(appY Sc x SY a)
|
|
||||||
b
|
|
||||||
)
|
|
||||||
c
|
|
||||||
)
|
|
||||||
(appY (app x z) (app y z) (appY x z a c) (appY y z b c))
|
|
||||||
)
|
|
||||||
(x y z : CL) ->
|
|
||||||
apd (CLind Y KY SY appY KConvY SConvY) SConv == SConvY x y z (CLind Y KY SY appY KConvY SConvY x) (CLind Y KY SY appY KConvY SConvY y) (CLind Y KY SY appY KConvY SConvY z)
|
|
||||||
|
|
@ -1,122 +0,0 @@
|
||||||
{-# OPTIONS --without-K --rewriting #-}
|
|
||||||
|
|
||||||
open import HoTT
|
|
||||||
open import CL
|
|
||||||
|
|
||||||
module Thms where
|
|
||||||
|
|
||||||
trans-cst : (A : Set) {x y : A} (B : Set) (p : x == y) (z : B) -> transport (\x -> B) p z == z
|
|
||||||
trans-cst A B idp z = idp
|
|
||||||
|
|
||||||
I : CL
|
|
||||||
I = app (app Sc K) K
|
|
||||||
|
|
||||||
IConv : {x : CL} -> app I x == x
|
|
||||||
IConv {x} = SConv ∙ KConv
|
|
||||||
|
|
||||||
B : CL
|
|
||||||
B = app (app Sc (app K Sc)) K
|
|
||||||
|
|
||||||
BConv : {x y z : CL} -> app (app (app B x) y) z == app x (app y z)
|
|
||||||
BConv {x} {y} {z} =
|
|
||||||
ap (λ p -> app (app p y) z) SConv
|
|
||||||
∙ ap (λ p -> app (app (app (p) (app K x)) y) z) KConv
|
|
||||||
∙ SConv
|
|
||||||
∙ ap (λ p -> app p (app y z)) KConv
|
|
||||||
|
|
||||||
M : CL
|
|
||||||
M = app (app Sc I) I
|
|
||||||
|
|
||||||
MConv : {x : CL} -> app M x == app x x
|
|
||||||
MConv {x} =
|
|
||||||
SConv
|
|
||||||
∙ ap (λ p -> app p (app I x)) IConv
|
|
||||||
∙ ap (app x) IConv
|
|
||||||
|
|
||||||
T : CL
|
|
||||||
T = app (app B (app Sc I)) K
|
|
||||||
|
|
||||||
TConv : {x y : CL} -> app (app T x) y == app y x
|
|
||||||
TConv {x} {y} =
|
|
||||||
ap (λ p -> app p y) BConv
|
|
||||||
∙ SConv
|
|
||||||
∙ ap (λ p -> app p (app (app K x) y)) IConv
|
|
||||||
∙ ap (app y) KConv
|
|
||||||
|
|
||||||
C : CL
|
|
||||||
C =
|
|
||||||
app
|
|
||||||
(app
|
|
||||||
B
|
|
||||||
(app
|
|
||||||
T
|
|
||||||
(app
|
|
||||||
(app
|
|
||||||
B
|
|
||||||
B
|
|
||||||
)
|
|
||||||
T
|
|
||||||
)
|
|
||||||
)
|
|
||||||
)
|
|
||||||
(app
|
|
||||||
(app
|
|
||||||
B
|
|
||||||
B
|
|
||||||
)
|
|
||||||
T
|
|
||||||
)
|
|
||||||
|
|
||||||
CConv : {x y z : CL} -> app (app (app C x) y) z == app (app x z) y
|
|
||||||
CConv {x} {y} {z} =
|
|
||||||
ap (λ p -> app (app p y) z) BConv
|
|
||||||
∙ ap (λ p -> app (app p y) z) TConv
|
|
||||||
∙ ap (λ p -> app (app (app p (app (app B B) T)) y) z) BConv
|
|
||||||
∙ ap (λ p -> app p z) BConv
|
|
||||||
∙ ap (λ p -> app p z) TConv
|
|
||||||
∙ ap (λ p -> app (app p x) z) BConv
|
|
||||||
∙ BConv
|
|
||||||
∙ TConv
|
|
||||||
|
|
||||||
W : CL
|
|
||||||
W = app (app C Sc) I
|
|
||||||
|
|
||||||
WConv : {x y : CL} -> app (app W x) y == app (app x y) y
|
|
||||||
WConv {x} {y} =
|
|
||||||
ap (λ p -> app p y) CConv
|
|
||||||
∙ SConv
|
|
||||||
∙ ap (app (app x y)) IConv
|
|
||||||
|
|
||||||
B' : CL
|
|
||||||
B' = app C B
|
|
||||||
|
|
||||||
B'Conv : {x y z : CL} -> app (app (app B' x) y) z == app y (app x z)
|
|
||||||
B'Conv {x} {y} {z} =
|
|
||||||
ap (λ p -> app p z) CConv
|
|
||||||
∙ BConv
|
|
||||||
|
|
||||||
V : CL
|
|
||||||
V = app (app B C) T
|
|
||||||
|
|
||||||
VConv : {x y z : CL} -> app (app (app V x) y) z == app (app z x) y
|
|
||||||
VConv {x} {y} {z} =
|
|
||||||
ap (λ p -> app (app p y) z) BConv
|
|
||||||
∙ CConv
|
|
||||||
∙ ap (λ p -> app p y) TConv
|
|
||||||
|
|
||||||
Y : CL
|
|
||||||
Y = app (app B' (app B' M)) M
|
|
||||||
|
|
||||||
YConv : {x : CL} -> app Y x == app x (app Y x)
|
|
||||||
YConv {x} =
|
|
||||||
B'Conv
|
|
||||||
∙ MConv
|
|
||||||
∙ B'Conv
|
|
||||||
∙ ap (app x) (! B'Conv)
|
|
||||||
|
|
||||||
fixpoint : (x : CL) -> Σ CL (λ y -> app x y == y)
|
|
||||||
fixpoint x = app Y x , ! YConv
|
|
||||||
|
|
||||||
S' : CL
|
|
||||||
S' = app C Sc
|
|
||||||
|
|
||||||
|
|
@ -1,59 +0,0 @@
|
||||||
{-# OPTIONS --without-K --rewriting #-}
|
|
||||||
|
|
||||||
open import HoTT
|
|
||||||
|
|
||||||
module Expressions where
|
|
||||||
|
|
||||||
private
|
|
||||||
data Exp' : Set where
|
|
||||||
value : Nat -> Exp'
|
|
||||||
addition : Exp' -> Exp' -> Exp'
|
|
||||||
|
|
||||||
Exp : Set
|
|
||||||
Exp = Exp'
|
|
||||||
|
|
||||||
val : Nat -> Exp
|
|
||||||
val = value
|
|
||||||
|
|
||||||
plus : Exp -> Exp -> Exp
|
|
||||||
plus = addition
|
|
||||||
|
|
||||||
postulate
|
|
||||||
add : (n m : Nat) -> plus (val n) (val m) == val (n + m)
|
|
||||||
trunc : is-set Exp
|
|
||||||
|
|
||||||
Exp-ind : (C : Exp -> Set)
|
|
||||||
-> (vC : (n : Nat) -> C (val n))
|
|
||||||
-> (pC : (e₁ e₂ : Exp) -> C e₁ -> C e₂ -> C(plus e₁ e₂))
|
|
||||||
-> (addC : (n m : Nat) -> PathOver C (add n m) (pC (val n) (val m) (vC n) (vC m)) (vC (n + m)))
|
|
||||||
-> (t : (e : Exp) -> is-set (C e))
|
|
||||||
-> (x : Exp) -> C x
|
|
||||||
Exp-ind C vC pC addC t (value n) = vC n
|
|
||||||
Exp-ind C vC pC addC t (addition e₁ e₂) = pC e₁ e₂ (Exp-ind C vC pC addC t e₁) (Exp-ind C vC pC addC t e₂)
|
|
||||||
|
|
||||||
postulate
|
|
||||||
Exp-ind-βadd : (C : Exp -> Set)
|
|
||||||
-> (vC : (n : Nat) -> C (val n))
|
|
||||||
-> (pC : (e₁ e₂ : Exp) -> C e₁ -> C e₂ -> C(plus e₁ e₂))
|
|
||||||
-> (addC : (n m : Nat) -> PathOver C (add n m) (pC (val n) (val m) (vC n) (vC m)) (vC (n + m)))
|
|
||||||
-> (t : (e : Exp) -> is-set (C e))
|
|
||||||
-> (n m : Nat)
|
|
||||||
-> apd (Exp-ind C vC pC addC t) (add n m) == addC n m
|
|
||||||
|
|
||||||
Exp-rec : {C : Set}
|
|
||||||
-> (vC : Nat -> C)
|
|
||||||
-> (pC : C -> C -> C)
|
|
||||||
-> (addC : (n m : Nat) -> pC (vC n) (vC m) == vC (n + m))
|
|
||||||
-> (t : is-set C)
|
|
||||||
-> Exp -> C
|
|
||||||
Exp-rec vC pC addC t (value n) = vC n
|
|
||||||
Exp-rec vC pC addC t (addition e₁ e₂) = pC (Exp-rec vC pC addC t e₁) (Exp-rec vC pC addC t e₂)
|
|
||||||
|
|
||||||
postulate
|
|
||||||
Exp-rec-βadd : {C : Set}
|
|
||||||
-> (vC : Nat -> C)
|
|
||||||
-> (pC : C -> C -> C)
|
|
||||||
-> (addC : (n m : Nat) -> pC (vC n) (vC m) == vC (n + m))
|
|
||||||
-> (t : is-set C)
|
|
||||||
-> (n m : Nat)
|
|
||||||
-> ap (Exp-rec vC pC addC t) (add n m) == addC n m
|
|
||||||
|
|
@ -1,16 +0,0 @@
|
||||||
{-# OPTIONS --without-K --rewriting #-}
|
|
||||||
|
|
||||||
open import HoTT
|
|
||||||
open import Expressions
|
|
||||||
|
|
||||||
module Thms where
|
|
||||||
|
|
||||||
value : (e : Exp) -> Σ Nat (\n -> e == val n)
|
|
||||||
value = Exp-ind
|
|
||||||
(\e -> Σ Nat (\n -> e == val n))
|
|
||||||
(\n -> n , idp)
|
|
||||||
(\e₁ e₂ v₁ v₂ -> fst v₁ + fst v₂ ,
|
|
||||||
(ap (\e -> plus e e₂) (snd v₁) ∙ ap (plus (val (fst v₁))) (snd v₂)) ∙ add (fst v₁) (fst v₂)
|
|
||||||
)
|
|
||||||
(\n m -> from-transp! (\e -> Σ Nat (\n -> e == val n)) (add n m) (pair= {!!} {!!}))
|
|
||||||
(\e -> {!!})
|
|
||||||
|
|
@ -1,32 +0,0 @@
|
||||||
{-# OPTIONS --without-K --rewriting #-}
|
|
||||||
|
|
||||||
open import HoTT
|
|
||||||
open import Syntax
|
|
||||||
|
|
||||||
module Language where
|
|
||||||
|
|
||||||
data Program : Set where
|
|
||||||
fail : Program
|
|
||||||
exec : Syntax -> State -> Program
|
|
||||||
|
|
||||||
postulate
|
|
||||||
assignp : (z : State) (x n : Nat) -> exec (x := n) z == exec skip ( z [ x :== n ])
|
|
||||||
comp₁ : (z : State) (S : Syntax) -> exec (conc skip S) z == exec S z
|
|
||||||
comp₂ : (z z' : State) (S₁ S₂ S₁' : Syntax) -> exec S₁ z == exec S₁' z' -> exec (conc S₁ S₂) z == exec (conc S₁' S₂) z'
|
|
||||||
while₁ : (z : State) (x n : Nat) (S : Syntax) -> defined z x -> equals z x n -> exec (while x == n do S) z == exec (conc S (while x == n do S)) z
|
|
||||||
while₂ : (z : State) (x n : Nat) (S : Syntax) -> defined z x -> unequals z x n -> exec (while x == n do S) z == exec skip z
|
|
||||||
while₃ : (z : State) (x n : Nat) (S : Syntax) -> undefined z x -> exec (while x == n do S) z == fail
|
|
||||||
|
|
||||||
Program-elim :
|
|
||||||
(Y : Set)
|
|
||||||
-> (failY : Y)
|
|
||||||
-> (execY : Syntax -> State -> Y)
|
|
||||||
-> (assignY : (z : State) (x n : Nat) -> execY (x := n) z == execY skip ( z [ x :== n ]) )
|
|
||||||
-> (compY₁ : (z : State) (S : Syntax) -> execY (conc skip S) z == execY S z )
|
|
||||||
-> (compY₂ : (z z' : State) (S₁ S₂ S₁' : Syntax) -> execY S₁ z == execY S₁' z' -> execY (conc S₁ S₂) z == execY (conc S₁' S₂) z')
|
|
||||||
-> (whileY₁ : (z : State) (x n : Nat) (S : Syntax) -> defined z x -> equals z x n -> execY (while x == n do S) z == execY (conc S (while x == n do S)) z)
|
|
||||||
-> (whileY₂ : (z : State) (x n : Nat) (S : Syntax) -> defined z x -> unequals z x n -> execY (while x == n do S) z == execY skip z)
|
|
||||||
-> (whileY₃ : (z : State) (x n : Nat) (S : Syntax) -> undefined z x -> execY (while x == n do S) z == failY)
|
|
||||||
-> Program -> Y
|
|
||||||
Program-elim _ failY _ _ _ _ _ _ _ fail = failY
|
|
||||||
Program-elim _ _ execY _ _ _ _ _ _ (exec s z) = execY s z
|
|
||||||
|
|
@ -1,18 +0,0 @@
|
||||||
{-# OPTIONS --without-K --rewriting #-}
|
|
||||||
|
|
||||||
open import HoTT
|
|
||||||
|
|
||||||
module Semantics where
|
|
||||||
|
|
||||||
data koe : Set where
|
|
||||||
a : koe
|
|
||||||
b : koe
|
|
||||||
|
|
||||||
postulate
|
|
||||||
kek : a ↦ b
|
|
||||||
{-# REWRITE kek #-}
|
|
||||||
|
|
||||||
|
|
||||||
Y : koe -> Set
|
|
||||||
Y a = Nat
|
|
||||||
Y b = Bool
|
|
||||||
|
|
@ -1,66 +0,0 @@
|
||||||
{-# OPTIONS --without-K --rewriting #-}
|
|
||||||
|
|
||||||
open import HoTT
|
|
||||||
|
|
||||||
module Syntax where
|
|
||||||
|
|
||||||
data Maybe (A : Set) : Set where
|
|
||||||
Just : A -> Maybe A
|
|
||||||
Nothing : Maybe A
|
|
||||||
|
|
||||||
eqN : Nat -> Nat -> Bool
|
|
||||||
eqN 0 0 = true
|
|
||||||
eqN 0 _ = false
|
|
||||||
eqN (S _) 0 = false
|
|
||||||
eqN (S n) (S m) = eqN n m
|
|
||||||
|
|
||||||
-- first coordinate represents the variable x_i, second the value
|
|
||||||
State : Set
|
|
||||||
State = List (Nat × Nat)
|
|
||||||
|
|
||||||
_[_:==_] : State -> Nat -> Nat -> State
|
|
||||||
nil [ x :== n ] = (x , n) :: nil
|
|
||||||
((y , m) :: s) [ x :== n ] =
|
|
||||||
if eqN x y
|
|
||||||
then (x , n) :: s
|
|
||||||
else ((y , m) :: (s [ x :== n ]))
|
|
||||||
|
|
||||||
equals : State -> Nat -> Nat -> Set
|
|
||||||
equals nil _ _ = Empty
|
|
||||||
equals ((x , n) :: s) y m =
|
|
||||||
if eqN x y
|
|
||||||
then
|
|
||||||
if eqN n m
|
|
||||||
then Unit
|
|
||||||
else Empty
|
|
||||||
else equals s y m
|
|
||||||
|
|
||||||
unequals : State -> Nat -> Nat -> Set
|
|
||||||
unequals nil _ _ = Unit
|
|
||||||
unequals ((x , n) :: s) y m =
|
|
||||||
if eqN x y
|
|
||||||
then
|
|
||||||
if eqN n m
|
|
||||||
then Empty
|
|
||||||
else Unit
|
|
||||||
else unequals s y m
|
|
||||||
|
|
||||||
defined : State -> Nat -> Set
|
|
||||||
defined nil y = Empty
|
|
||||||
defined ((x , n) :: s) y =
|
|
||||||
if eqN x y
|
|
||||||
then Unit
|
|
||||||
else defined s y
|
|
||||||
|
|
||||||
undefined : State -> Nat -> Set
|
|
||||||
undefined nil y = Unit
|
|
||||||
undefined ((x , n) :: s) y =
|
|
||||||
if eqN x y
|
|
||||||
then Empty
|
|
||||||
else undefined s y
|
|
||||||
|
|
||||||
data Syntax : Set where
|
|
||||||
skip : Syntax
|
|
||||||
_:=_ : Nat -> Nat -> Syntax
|
|
||||||
conc : Syntax -> Syntax -> Syntax
|
|
||||||
while_==_do_ : Nat -> Nat -> Syntax -> Syntax
|
|
||||||
|
|
@ -1,63 +0,0 @@
|
||||||
{-# OPTIONS --without-K --rewriting #-}
|
|
||||||
|
|
||||||
open import HoTT
|
|
||||||
|
|
||||||
module Integers where
|
|
||||||
|
|
||||||
private
|
|
||||||
data Integers : Set where
|
|
||||||
z : Integers
|
|
||||||
S : Integers -> Integers
|
|
||||||
P : Integers -> Integers
|
|
||||||
|
|
||||||
Ints : Set
|
|
||||||
Ints = Integers
|
|
||||||
|
|
||||||
nul : Ints
|
|
||||||
nul = z
|
|
||||||
|
|
||||||
Succ : Ints -> Ints
|
|
||||||
Succ = S
|
|
||||||
|
|
||||||
Pred : Ints -> Ints
|
|
||||||
Pred = P
|
|
||||||
|
|
||||||
postulate
|
|
||||||
invl : (x : Integers) -> P(S x) == x
|
|
||||||
invr : (x : Integers) -> S(P x) == x
|
|
||||||
trunc : is-set Ints
|
|
||||||
|
|
||||||
Zind : (Y : Integers -> Set)
|
|
||||||
-> (zY : Y z)
|
|
||||||
-> (SY : (x : Integers) -> Y x -> Y(S x))
|
|
||||||
-> (PY : (x : Integers) -> Y x -> Y(P x))
|
|
||||||
-> (invYl : (x : Integers) (y : Y x) -> PathOver Y (invl x) (PY (S x) (SY x y)) y)
|
|
||||||
-> (invYr : (x : Integers) (y : Y x) -> PathOver Y (invr x) (SY (P x) (PY x y)) y)
|
|
||||||
-> (t : (x : Integers) -> is-set (Y x))
|
|
||||||
-> (x : Integers) -> Y x
|
|
||||||
Zind Y zY SY PY invYl invYr t z = zY
|
|
||||||
Zind Y zY SY PY invYl invYr t (S x) = SY x (Zind Y zY SY PY invYl invYr t x)
|
|
||||||
Zind Y zY SY PY invYl invYr t (P x) = PY x (Zind Y zY SY PY invYl invYr t x)
|
|
||||||
|
|
||||||
postulate
|
|
||||||
Zind-βinvl :
|
|
||||||
(Y : Integers -> Set)
|
|
||||||
-> (zY : Y z)
|
|
||||||
-> (SY : (x : Integers) -> Y x -> Y(S x))
|
|
||||||
-> (PY : (x : Integers) -> Y x -> Y(P x))
|
|
||||||
-> (invYl : (x : Integers) (y : Y x) -> PathOver Y (invl x) (PY (S x) (SY x y)) y)
|
|
||||||
-> (invYr : (x : Integers) (y : Y x) -> PathOver Y (invr x) (SY (P x) (PY x y)) y)
|
|
||||||
-> (t : (x : Integers) -> is-set (Y x))
|
|
||||||
-> (x : Integers)
|
|
||||||
-> apd (Zind Y zY SY PY invYl invYr t) (invl x) == invYl x (Zind Y zY SY PY invYl invYr t x)
|
|
||||||
|
|
||||||
Zind-βinvr :
|
|
||||||
(Y : Integers -> Set)
|
|
||||||
-> (zY : Y z)
|
|
||||||
-> (SY : (x : Integers) -> Y x -> Y(S x))
|
|
||||||
-> (PY : (x : Integers) -> Y x -> Y(P x))
|
|
||||||
-> (invYl : (x : Integers) (y : Y x) -> PathOver Y (invl x) (PY (S x) (SY x y)) y)
|
|
||||||
-> (invYr : (x : Integers) (y : Y x) -> PathOver Y (invr x) (SY (P x) (PY x y)) y)
|
|
||||||
-> (t : (x : Integers) -> is-set (Y x))
|
|
||||||
-> (x : Integers)
|
|
||||||
-> apd (Zind Y zY SY PY invYl invYr t) (invr x) == invYr x (Zind Y zY SY PY invYl invYr t x)
|
|
||||||
|
|
@ -1,205 +0,0 @@
|
||||||
{-# OPTIONS --without-K --rewriting #-}
|
|
||||||
|
|
||||||
open import HoTT
|
|
||||||
open import Integers
|
|
||||||
|
|
||||||
module Thms where
|
|
||||||
|
|
||||||
paths_set : (A B : Set) (m : is-set B) (f g : A -> B) (a : A) -> is-set (f a == g a)
|
|
||||||
paths_set A B m f g a = \c₁ c₂ q₁ q₂ ->
|
|
||||||
prop-has-level-S
|
|
||||||
(contr-is-prop (m (f a) (g a) c₁ c₂))
|
|
||||||
q₁
|
|
||||||
q₂
|
|
||||||
|
|
||||||
trunc_paths : (A : Set) (Y : A -> Set) {x y : A} (p : x == y) (t : is-prop (Y x)) (c₁ : Y x) (c₂ : Y y) -> PathOver Y p c₁ c₂
|
|
||||||
trunc_paths A Y p t c₁ c₂ = from-transp! Y p ((prop-has-all-paths t) c₁ (transport! Y p c₂))
|
|
||||||
|
|
||||||
trans-cst : (A : Set) {x y : A} (B : Set) (p : x == y) (z : B) -> transport (\x -> B) p z == z
|
|
||||||
trans-cst A B idp z = idp
|
|
||||||
|
|
||||||
plus : Ints -> Ints -> Ints
|
|
||||||
plus n = Zind
|
|
||||||
(\m -> Ints)
|
|
||||||
n
|
|
||||||
(\m -> Succ)
|
|
||||||
(\m -> Pred)
|
|
||||||
(\x y -> from-transp (λ _ → Ints) (invl x) (trans-cst Ints Ints (invl x) (Pred (Succ y)) ∙ invl y))
|
|
||||||
(\x y -> from-transp (λ _ → Ints) (invr x) (trans-cst Ints Ints (invr x) (Succ (Pred y)) ∙ invr y))
|
|
||||||
(\x -> trunc)
|
|
||||||
|
|
||||||
negate : Ints -> Ints
|
|
||||||
negate = Zind
|
|
||||||
(λ _ → Ints)
|
|
||||||
nul
|
|
||||||
(λ _ -> Pred)
|
|
||||||
(λ _ -> Succ)
|
|
||||||
(λ x y -> from-transp (λ _ -> Ints) (invl x) (trans-cst Ints Ints (invl x) (Succ (Pred y)) ∙ invr y))
|
|
||||||
(λ x y -> from-transp (λ _ -> Ints) (invr x) (trans-cst Ints Ints (invr x) (Pred (Succ y)) ∙ invl y))
|
|
||||||
(\x -> trunc)
|
|
||||||
|
|
||||||
min : Ints -> Ints -> Ints
|
|
||||||
min x y = plus x (negate y)
|
|
||||||
|
|
||||||
plus_0n : (x : Ints) -> plus x nul == x
|
|
||||||
plus_0n x = idp
|
|
||||||
|
|
||||||
plus_n0 : (x : Ints) -> plus nul x == x
|
|
||||||
plus_n0 = Zind
|
|
||||||
(\x -> plus nul x == x)
|
|
||||||
idp
|
|
||||||
(\x p -> ap Succ p)
|
|
||||||
(\x p -> ap Pred p)
|
|
||||||
(\x y ->
|
|
||||||
trunc_paths
|
|
||||||
Ints
|
|
||||||
(\m -> plus nul m == m)
|
|
||||||
(invl x)
|
|
||||||
(trunc (plus nul (Pred (Succ x)))
|
|
||||||
(Pred(Succ x)))
|
|
||||||
(ap Pred (ap Succ y))
|
|
||||||
y
|
|
||||||
)
|
|
||||||
(\x y ->
|
|
||||||
trunc_paths
|
|
||||||
Ints
|
|
||||||
(\m -> plus nul m == m)
|
|
||||||
(invr x)
|
|
||||||
(trunc (plus nul (Succ (Pred x)))
|
|
||||||
(Succ(Pred x)))
|
|
||||||
(ap Succ (ap Pred y))
|
|
||||||
y
|
|
||||||
)
|
|
||||||
(\x -> paths_set Ints Ints trunc (\m -> plus nul m) (\m -> m) x)
|
|
||||||
|
|
||||||
plus_assoc : (x y z : Ints) -> plus x (plus y z) == plus (plus x y) z
|
|
||||||
plus_assoc x = Zind
|
|
||||||
(λ y -> (z : Ints) -> plus x (plus y z) == plus (plus x y) z)
|
|
||||||
(
|
|
||||||
Zind
|
|
||||||
(λ z -> plus x (plus nul z) == plus (plus x nul) z)
|
|
||||||
idp
|
|
||||||
(λ x p -> ap Succ p)
|
|
||||||
(λ x p -> ap Pred p)
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
)
|
|
||||||
(λ y p ->
|
|
||||||
Zind
|
|
||||||
(λ z -> plus x (plus (Succ y) z) == plus (plus x (Succ y)) z)
|
|
||||||
(p (Succ nul))
|
|
||||||
(λ y' p' -> ap Succ p')
|
|
||||||
(λ y' p' -> ap Pred p')
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
)
|
|
||||||
(λ y p ->
|
|
||||||
Zind
|
|
||||||
(λ z -> plus x (plus (Pred y) z) == plus (plus x (Pred y)) z)
|
|
||||||
(p (Pred nul))
|
|
||||||
(λ y' p' -> ap Succ p')
|
|
||||||
(λ y' p' -> ap Pred p')
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
)
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
|
|
||||||
plus_Succ : (x y : Ints) -> plus x (Succ y) == Succ(plus x y)
|
|
||||||
plus_Succ x y = idp
|
|
||||||
|
|
||||||
Succ_plus : (x y : Ints) -> plus (Succ x) y == Succ(plus x y)
|
|
||||||
Succ_plus x = Zind
|
|
||||||
(λ y -> plus (Succ x) y == Succ(plus x y))
|
|
||||||
idp
|
|
||||||
(λ y' p -> ap Succ p)
|
|
||||||
(λ y' p -> ap Pred p ∙ invl (plus x y') ∙ ! (invr (plus x y')))
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
|
|
||||||
plus_Pred : (x y : Ints) -> plus x (Pred y) == Pred(plus x y)
|
|
||||||
plus_Pred x y = idp
|
|
||||||
|
|
||||||
Pred_plus : (x y : Ints) -> plus (Pred x) y == Pred(plus x y)
|
|
||||||
Pred_plus x = Zind
|
|
||||||
(λ y -> plus (Pred x) y == Pred(plus x y))
|
|
||||||
idp
|
|
||||||
(λ y' p -> ap Succ p ∙ invr (plus x y') ∙ ! (invl (plus x y')))
|
|
||||||
(λ y' p -> ap Pred p)
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
|
|
||||||
plus_negr : (y : Ints) -> plus y (negate y) == nul
|
|
||||||
plus_negr = Zind
|
|
||||||
(λ y -> plus y (negate y) == nul)
|
|
||||||
idp
|
|
||||||
(λ x p ->
|
|
||||||
Succ_plus x (negate (Succ x))
|
|
||||||
∙ invr (plus x (negate x))
|
|
||||||
∙ p
|
|
||||||
)
|
|
||||||
(λ x p ->
|
|
||||||
Pred_plus x (negate (Pred x))
|
|
||||||
∙ invl (plus x (negate x))
|
|
||||||
∙ p
|
|
||||||
)
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
|
|
||||||
plus_negl : (y : Ints) -> plus (negate y) y == nul
|
|
||||||
plus_negl = Zind
|
|
||||||
(λ y -> plus (negate y) y == nul)
|
|
||||||
idp
|
|
||||||
(λ y' p ->
|
|
||||||
Pred_plus (negate y') (Succ y')
|
|
||||||
∙ invl (plus (negate y') y')
|
|
||||||
∙ p
|
|
||||||
)
|
|
||||||
(λ y' p ->
|
|
||||||
Succ_plus (negate y') (Pred y')
|
|
||||||
∙ invr (plus (negate y') y')
|
|
||||||
∙ p
|
|
||||||
)
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
|
|
||||||
plus_com : (x y : Ints) -> plus x y == plus y x
|
|
||||||
plus_com x = Zind
|
|
||||||
(λ y -> plus x y == plus y x)
|
|
||||||
(plus_0n x ∙ ! (plus_n0 x))
|
|
||||||
(λ y' p ->
|
|
||||||
plus_Succ x y'
|
|
||||||
∙ ap Succ p
|
|
||||||
∙ ! (Succ_plus y' x))
|
|
||||||
(λ y' p ->
|
|
||||||
plus_Pred x y'
|
|
||||||
∙ ap Pred p
|
|
||||||
∙ ! (Pred_plus y' x)
|
|
||||||
)
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
{!!}
|
|
||||||
|
|
||||||
times : Ints -> Ints -> Ints
|
|
||||||
times n = Zind
|
|
||||||
(λ _ → Ints)
|
|
||||||
nul
|
|
||||||
(\x y -> plus y n)
|
|
||||||
(\x y -> min y n)
|
|
||||||
(λ x y -> from-transp (λ _ → Ints) (invl x) (trans-cst Ints Ints (invl x) (min (plus y n) n)
|
|
||||||
∙ ! (plus_assoc y n (negate n))
|
|
||||||
∙ ap (plus y) (plus_negr n)
|
|
||||||
∙ plus_0n y))
|
|
||||||
(λ x y -> from-transp (λ _ → Ints) (invr x) (trans-cst Ints Ints (invr x) (plus (min y n) n)
|
|
||||||
∙ ! (plus_assoc y (negate n) n)
|
|
||||||
∙ ap (λ z -> plus y z) (plus_negl n)
|
|
||||||
∙ plus_0n y))
|
|
||||||
(\x -> trunc)
|
|
||||||
|
|
@ -1,49 +0,0 @@
|
||||||
{-# OPTIONS --without-K --rewriting #-}
|
|
||||||
|
|
||||||
open import HoTT
|
|
||||||
|
|
||||||
module Interval where
|
|
||||||
|
|
||||||
postulate
|
|
||||||
I : Set
|
|
||||||
z : I
|
|
||||||
o : I
|
|
||||||
s : z == o
|
|
||||||
I-ind : (Y : I -> Set)
|
|
||||||
(zY : Y z)
|
|
||||||
(oY : Y o)
|
|
||||||
(sY : PathOver Y s zY oY)
|
|
||||||
(x : I)
|
|
||||||
-> Y x
|
|
||||||
I-ind-βz : (Y : I -> Set)
|
|
||||||
(zY : Y z)
|
|
||||||
(oY : Y o)
|
|
||||||
(sY : PathOver Y s zY oY)
|
|
||||||
-> I-ind Y zY oY sY z ↦ zY
|
|
||||||
{-# REWRITE I-ind-βz #-}
|
|
||||||
I-ind-βo : (Y : I -> Set)
|
|
||||||
(zY : Y z)
|
|
||||||
(oY : Y o)
|
|
||||||
(sY : PathOver Y s zY oY)
|
|
||||||
-> I-ind Y zY oY sY o ↦ oY
|
|
||||||
{-# REWRITE I-ind-βo #-}
|
|
||||||
I-ind-βs : (Y : I -> Set)
|
|
||||||
(zY : Y z)
|
|
||||||
(oY : Y o)
|
|
||||||
(sY : PathOver Y s zY oY)
|
|
||||||
-> apd (I-ind Y zY oY sY) s == sY
|
|
||||||
|
|
||||||
transp-cst : (A : Set) {x y : A} (B : Set) (p : x == y) (z : B) -> transport (\x -> B) p z == z
|
|
||||||
transp-cst A B idp z = idp
|
|
||||||
|
|
||||||
transp-fun : (A B : Set) (a b : A) (p : a == b) (f : A -> B) -> transport (λ _ -> A -> B) p f == transport (λ _ -> B) p (f a)
|
|
||||||
transp-fun = ?
|
|
||||||
|
|
||||||
fe : {A B : Set} (f g : A -> B) -> ( (x : A) -> f x == g x) -> f == g
|
|
||||||
fe {A} {B} f g p =
|
|
||||||
ap
|
|
||||||
(I-ind (λ _ → (x : A) → B) f g
|
|
||||||
(from-transp (λ _ → (x : A) → B) s (
|
|
||||||
{!!}
|
|
||||||
)))
|
|
||||||
s
|
|
||||||
|
|
@ -1,59 +0,0 @@
|
||||||
{-# OPTIONS --without-K --rewriting #-}
|
|
||||||
|
|
||||||
open import HoTT
|
|
||||||
|
|
||||||
module Mod2 where
|
|
||||||
|
|
||||||
private
|
|
||||||
data M' : Set where
|
|
||||||
Zero : M'
|
|
||||||
S : M' -> M'
|
|
||||||
|
|
||||||
M : Set
|
|
||||||
M = M'
|
|
||||||
|
|
||||||
z : M
|
|
||||||
z = Zero
|
|
||||||
|
|
||||||
Succ : M -> M
|
|
||||||
Succ = S
|
|
||||||
|
|
||||||
postulate
|
|
||||||
mod : (n : M) -> n == Succ(Succ n)
|
|
||||||
trunc : is-set M
|
|
||||||
|
|
||||||
M-ind : (C : M -> Set)
|
|
||||||
-> (a : C Zero)
|
|
||||||
-> (sC : (x : M) -> C x -> C (S x))
|
|
||||||
-> (p : (n : M) (c : C n) -> PathOver C (mod n) c (sC (Succ n) (sC n c)))
|
|
||||||
-> (t : (m : M) -> is-set (C m))
|
|
||||||
-> (x : M) -> C x
|
|
||||||
M-ind C a sC _ t Zero = a
|
|
||||||
M-ind C a sC p t (S x) = sC x (M-ind C a sC p t x)
|
|
||||||
|
|
||||||
postulate
|
|
||||||
M-ind-βmod : (C : M -> Set)
|
|
||||||
-> (a : C Zero)
|
|
||||||
-> (sC : (x : M) -> C x -> C (S x))
|
|
||||||
-> (p : (n : M) (c : C n) -> PathOver C (mod n) c (sC (Succ n) (sC n c)))
|
|
||||||
-> (t : (m : M) -> is-set (C m))
|
|
||||||
-> (n : M)
|
|
||||||
-> apd (M-ind C a sC p t) (mod n) == p n (M-ind C a sC p t n)
|
|
||||||
|
|
||||||
M-rec : {C : Set}
|
|
||||||
-> (a : C)
|
|
||||||
-> (sC : C -> C)
|
|
||||||
-> (p : (c : C) -> c == sC (sC c))
|
|
||||||
-> (t : is-set C)
|
|
||||||
-> M -> C
|
|
||||||
M-rec a sC _ _ Zero = a
|
|
||||||
M-rec a sC p t (S x) = sC (M-rec a sC p t x)
|
|
||||||
|
|
||||||
postulate
|
|
||||||
M-rec-βmod : {C : Set}
|
|
||||||
-> (a : C)
|
|
||||||
-> (sC : C -> C)
|
|
||||||
-> (p : (c : C) -> c == sC (sC c))
|
|
||||||
-> (t : is-set C)
|
|
||||||
-> (n : M)
|
|
||||||
-> ap (M-rec a sC p t) (mod n) == p (M-rec a sC p t n)
|
|
||||||
|
|
@ -1,113 +0,0 @@
|
||||||
{-# OPTIONS --without-K --rewriting #-}
|
|
||||||
|
|
||||||
open import HoTT
|
|
||||||
open import Mod2
|
|
||||||
|
|
||||||
module Thms where
|
|
||||||
|
|
||||||
paths_set : (A B : Set) (m : is-set B) (f g : A -> B) (a : A) -> is-set (f a == g a)
|
|
||||||
paths_set A B m f g a = \c₁ c₂ q₁ q₂ ->
|
|
||||||
prop-has-level-S
|
|
||||||
(contr-is-prop (m (f a) (g a) c₁ c₂))
|
|
||||||
q₁
|
|
||||||
q₂
|
|
||||||
|
|
||||||
trunc_paths : (A : Set) (Y : A -> Set) {x y : A} (p : x == y) (t : is-prop (Y x)) (c₁ : Y x) (c₂ : Y y) -> PathOver Y p c₁ c₂
|
|
||||||
trunc_paths A Y p t c₁ c₂ = from-transp! Y p ((prop-has-all-paths t) c₁ (transport! Y p c₂))
|
|
||||||
|
|
||||||
plus : M -> M -> M
|
|
||||||
plus n = M-rec
|
|
||||||
n
|
|
||||||
Succ
|
|
||||||
mod
|
|
||||||
trunc
|
|
||||||
|
|
||||||
plus_0n : (n : M) -> plus z n == n
|
|
||||||
plus_0n = M-ind
|
|
||||||
(\n -> plus z n == n)
|
|
||||||
idp
|
|
||||||
(\x -> \p -> ap Succ p)
|
|
||||||
(\x -> \c ->
|
|
||||||
trunc_paths M (\ n → plus z n == n) (mod x) (trunc (plus z x) x) c (ap Succ (ap Succ c))
|
|
||||||
)
|
|
||||||
(\m ->
|
|
||||||
paths_set M M trunc (\x -> plus z x) (\x -> x) m
|
|
||||||
)
|
|
||||||
|
|
||||||
plus_n0 : (n : M) -> plus n z == n
|
|
||||||
plus_n0 = M-ind
|
|
||||||
(\n -> plus n z == n)
|
|
||||||
idp
|
|
||||||
(\x p -> idp)
|
|
||||||
(\x c ->
|
|
||||||
trunc_paths M (\x -> plus x z == x) (mod x) (trunc x x) c idp
|
|
||||||
)
|
|
||||||
(\m -> paths_set M M trunc (\x -> plus x z) (\x -> x) m )
|
|
||||||
|
|
||||||
plus_Sn : (n m : M) -> plus (Succ n) m == Succ (plus n m)
|
|
||||||
plus_Sn n = M-ind
|
|
||||||
(\m -> plus (Succ n) m == Succ (plus n m))
|
|
||||||
idp
|
|
||||||
(\x p -> ap Succ p)
|
|
||||||
(\x c ->
|
|
||||||
trunc_paths M (\x -> plus (Succ n) x == Succ (plus n x)) (mod x) (trunc (plus (Succ n) x) (Succ (plus n x))) c (ap Succ (ap Succ c))
|
|
||||||
)
|
|
||||||
(\m -> paths_set M M trunc (\x -> plus (Succ x) m) (\x -> Succ(plus x m)) n)
|
|
||||||
|
|
||||||
plus_nS : (n m : M) -> plus n (Succ m) == Succ (plus n m)
|
|
||||||
plus_nS n m = idp
|
|
||||||
|
|
||||||
not : Bool -> Bool
|
|
||||||
not true = false
|
|
||||||
not false = true
|
|
||||||
|
|
||||||
not-not : (x : Bool) -> x == not (not x)
|
|
||||||
not-not true = idp
|
|
||||||
not-not false = idp
|
|
||||||
|
|
||||||
toBool : M -> Bool
|
|
||||||
toBool = M-rec
|
|
||||||
true
|
|
||||||
not
|
|
||||||
((\x -> not-not x))
|
|
||||||
Bool-is-set
|
|
||||||
|
|
||||||
toBoolS : (n : M) -> toBool (Succ n) == not (toBool n)
|
|
||||||
toBoolS = M-ind
|
|
||||||
(\n -> toBool (Succ n) == not (toBool n))
|
|
||||||
idp
|
|
||||||
(\x p -> idp)
|
|
||||||
(\n c ->
|
|
||||||
trunc_paths M (\x -> toBool (Succ x) == not (toBool x)) (mod n) (Bool-is-set (not (toBool n)) (not (toBool n))) c idp)
|
|
||||||
(\m -> paths_set M Bool Bool-is-set (\n -> toBool(Succ n)) (\n -> not(toBool n)) m)
|
|
||||||
|
|
||||||
fromBool : Bool -> M
|
|
||||||
fromBool true = z
|
|
||||||
fromBool false = Succ z
|
|
||||||
|
|
||||||
fromBoolNot : (b : Bool) -> fromBool (not b) == Succ (fromBool b)
|
|
||||||
fromBoolNot true = idp
|
|
||||||
fromBoolNot false = mod z
|
|
||||||
|
|
||||||
iso₁ : (b : Bool) -> toBool (fromBool b) == b
|
|
||||||
iso₁ true = idp
|
|
||||||
iso₁ false = idp
|
|
||||||
|
|
||||||
iso₂ : (n : M) -> fromBool (toBool n) == n
|
|
||||||
iso₂ = M-ind
|
|
||||||
(\n -> fromBool (toBool n) == n)
|
|
||||||
idp
|
|
||||||
(\x p ->
|
|
||||||
ap fromBool (toBoolS x)
|
|
||||||
∙ fromBoolNot (toBool x)
|
|
||||||
∙ ap Succ p)
|
|
||||||
(\n p -> trunc_paths M
|
|
||||||
(λ z₁ → fromBool (toBool z₁) == z₁)
|
|
||||||
(mod n)
|
|
||||||
(trunc (fromBool (toBool n)) n)
|
|
||||||
p
|
|
||||||
(ap fromBool (toBoolS (Succ n))
|
|
||||||
∙ fromBoolNot (toBool (Succ n))
|
|
||||||
∙ ap Succ (ap fromBool (toBoolS n) ∙ fromBoolNot (toBool n) ∙ ap Succ p))
|
|
||||||
)
|
|
||||||
(\m -> paths_set M M trunc (\n -> fromBool (toBool n)) (\n -> n) m)
|
|
||||||
|
|
@ -18,6 +18,7 @@ fsets/monad.v
|
||||||
FSets.v
|
FSets.v
|
||||||
Sub.v
|
Sub.v
|
||||||
representations/T.v
|
representations/T.v
|
||||||
|
implementations/interface.v
|
||||||
implementations/lists.v
|
implementations/lists.v
|
||||||
variations/enumerated.v
|
variations/enumerated.v
|
||||||
variations/k_finite.v
|
variations/k_finite.v
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,43 @@
|
||||||
|
Require Import HoTT.
|
||||||
|
Require Import FSets.
|
||||||
|
|
||||||
|
Section structure.
|
||||||
|
Variable (T : Type -> Type).
|
||||||
|
|
||||||
|
Class hasMembership : Type :=
|
||||||
|
member : forall A : Type, A -> T A -> hProp.
|
||||||
|
|
||||||
|
Class hasEmpty : Type :=
|
||||||
|
empty : forall A, T A.
|
||||||
|
|
||||||
|
Class hasSingleton : Type :=
|
||||||
|
singleton : forall A, A -> T A.
|
||||||
|
|
||||||
|
Class hasUnion : Type :=
|
||||||
|
union : forall A, T A -> T A -> T A.
|
||||||
|
|
||||||
|
Class hasComprehension : Type :=
|
||||||
|
filter : forall A, (A -> Bool) -> T A -> T A.
|
||||||
|
End structure.
|
||||||
|
|
||||||
|
Arguments member {_} {_} {_} _ _.
|
||||||
|
Arguments empty {_} {_} {_}.
|
||||||
|
Arguments singleton {_} {_} {_} _.
|
||||||
|
Arguments union {_} {_} {_} _ _.
|
||||||
|
Arguments filter {_} {_} {_} _ _.
|
||||||
|
|
||||||
|
Section interface.
|
||||||
|
Context `{Univalence}.
|
||||||
|
Variable (T : Type -> Type)
|
||||||
|
(f : forall A, T A -> FSet A).
|
||||||
|
Context `{hasMembership T, hasEmpty T, hasSingleton T, hasUnion T, hasComprehension T}.
|
||||||
|
|
||||||
|
Class sets :=
|
||||||
|
{
|
||||||
|
f_empty : forall A, f A empty = E ;
|
||||||
|
f_singleton : forall A a, f A (singleton a) = L a;
|
||||||
|
f_union : forall A X Y, f A (union X Y) = U (f A X) (f A Y);
|
||||||
|
f_filter : forall A ϕ X, f A (filter ϕ X) = comprehension ϕ (f A X);
|
||||||
|
f_member : forall A a X, member a X = isIn a (f A X)
|
||||||
|
}.
|
||||||
|
End interface.
|
||||||
|
|
@ -1,113 +1,69 @@
|
||||||
(* Implementation of [FSet A] using lists *)
|
(* Implementation of [FSet A] using lists *)
|
||||||
Require Import HoTT HitTactics.
|
Require Import HoTT HitTactics.
|
||||||
Require Import representations.cons_repr FSets.
|
Require Import FSets implementations.interface.
|
||||||
From fsets Require Import operations_cons_repr isomorphism length.
|
|
||||||
|
|
||||||
Section Operations.
|
Section Operations.
|
||||||
Variable A : Type.
|
Context `{Univalence}.
|
||||||
Context {A_deceq : DecidablePaths A}.
|
|
||||||
|
|
||||||
Fixpoint member (l : list A) (a : A) : Bool :=
|
Global Instance list_empty : hasEmpty list := fun A => nil.
|
||||||
|
|
||||||
|
Global Instance list_single : hasSingleton list := fun A a => cons a nil.
|
||||||
|
|
||||||
|
Global Instance list_union : hasUnion list.
|
||||||
|
Proof.
|
||||||
|
intros A l1 l2.
|
||||||
|
induction l1.
|
||||||
|
* apply l2.
|
||||||
|
* apply (cons a IHl1).
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Global Instance list_membership : hasMembership list.
|
||||||
|
Proof.
|
||||||
|
intros A.
|
||||||
|
intros a l.
|
||||||
|
induction l as [ | b l IHl].
|
||||||
|
- apply False_hp.
|
||||||
|
- apply (hor (a = b) IHl).
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Global Instance list_comprehension : hasComprehension list.
|
||||||
|
Proof.
|
||||||
|
intros A ϕ l.
|
||||||
|
induction l as [ | b l IHl].
|
||||||
|
- apply nil.
|
||||||
|
- apply (if ϕ b then cons b IHl else IHl).
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Fixpoint list_to_set A (l : list A) : FSet A :=
|
||||||
match l with
|
match l with
|
||||||
| nil => false
|
| nil => E
|
||||||
| cons b l => if (dec (a = b)) then true else member l a
|
| cons a l => U (L a) (list_to_set A l)
|
||||||
end.
|
|
||||||
|
|
||||||
Fixpoint append (l1 l2 : list A) :=
|
|
||||||
match l1 with
|
|
||||||
| nil => l2
|
|
||||||
| cons a l => cons a (append l l2)
|
|
||||||
end.
|
|
||||||
|
|
||||||
Definition empty : list A := nil.
|
|
||||||
|
|
||||||
Definition singleton (a : A) : list A := cons a nil.
|
|
||||||
|
|
||||||
Fixpoint filter (ϕ : A -> Bool) (l : list A) : list A :=
|
|
||||||
match l with
|
|
||||||
| nil => nil
|
|
||||||
| cons a l => if ϕ a then cons a (filter ϕ l) else filter ϕ l
|
|
||||||
end.
|
|
||||||
|
|
||||||
Fixpoint cardinality (l : list A) : nat :=
|
|
||||||
match l with
|
|
||||||
| nil => 0
|
|
||||||
| cons a l => if member l a then cardinality l else 1 + cardinality l
|
|
||||||
end.
|
end.
|
||||||
|
|
||||||
End Operations.
|
End Operations.
|
||||||
|
|
||||||
Arguments nil {_}.
|
|
||||||
Arguments cons {_} _ _.
|
|
||||||
Arguments member {_} {_} _ _.
|
|
||||||
Arguments singleton {_} _.
|
|
||||||
Arguments append {_} _ _.
|
|
||||||
Arguments empty {_}.
|
|
||||||
Arguments filter {_} _ _.
|
|
||||||
Arguments cardinality {_} {_} _.
|
|
||||||
|
|
||||||
Section ListToSet.
|
Section ListToSet.
|
||||||
Variable A : Type.
|
Variable A : Type.
|
||||||
Context {A_deceq : DecidablePaths A} `{Univalence}.
|
Context `{Univalence}.
|
||||||
|
|
||||||
Fixpoint list_to_setC (l : list A) : FSetC A :=
|
Lemma member_isIn (a : A) (l : list A) :
|
||||||
match l with
|
member a l = isIn a (list_to_set A l).
|
||||||
| nil => Nil
|
|
||||||
| cons a l => Cns a (list_to_setC l)
|
|
||||||
end.
|
|
||||||
|
|
||||||
Definition list_to_set (l : list A) := FSetC_to_FSet(list_to_setC l).
|
|
||||||
|
|
||||||
Lemma list_to_setC_surj : forall X : FSetC A, Trunc (-1) ({l : list A & list_to_setC l = X}).
|
|
||||||
Proof.
|
Proof.
|
||||||
hrecursion ; try (intros ; apply hprop_allpath ; apply (istrunc_truncation (-1) _)).
|
induction l ; unfold member in * ; simpl in *.
|
||||||
- apply tr ; exists nil ; cbn. reflexivity.
|
|
||||||
- intros a x P.
|
|
||||||
simple refine (Trunc_rec _ P).
|
|
||||||
intros [l Q].
|
|
||||||
apply tr.
|
|
||||||
exists (cons a l).
|
|
||||||
simpl.
|
|
||||||
apply (ap (fun y => a;;y) Q).
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma member_isIn (l : list A) (a : A) :
|
|
||||||
member l a = isIn_b a (FSetC_to_FSet (list_to_setC l)).
|
|
||||||
Proof.
|
|
||||||
induction l ; cbn in *.
|
|
||||||
- reflexivity.
|
- reflexivity.
|
||||||
- destruct (dec (a = a0)) ; cbn.
|
- rewrite IHl.
|
||||||
* rewrite ?p. simplify_isIn. reflexivity.
|
unfold hor, merely, lor.
|
||||||
* rewrite IHl. simplify_isIn. rewrite L_isIn_b_false ; auto.
|
apply path_iff_hprop ; intros z ; strip_truncations ; destruct z as [z1 | z2].
|
||||||
|
* apply (tr (inl (tr z1))).
|
||||||
|
* apply (tr (inr z2)).
|
||||||
|
* strip_truncations ; apply (tr (inl z1)).
|
||||||
|
* apply (tr (inr z2)).
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Lemma append_FSetCappend (l1 l2 : list A) :
|
Definition empty_empty : list_to_set A empty = E := idpath.
|
||||||
list_to_setC (append l1 l2) = operations_cons_repr.append (list_to_setC l1) (list_to_setC l2).
|
|
||||||
Proof.
|
|
||||||
induction l1 ; simpl in *.
|
|
||||||
- reflexivity.
|
|
||||||
- apply (ap (fun y => a ;; y) IHl1).
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma append_FSetappend (l1 l2 : list A) :
|
Lemma filter_comprehension (ϕ : A -> Bool) (l : list A) :
|
||||||
list_to_set (append l1 l2) = U (list_to_set l1) (list_to_set l2).
|
list_to_set A (filter ϕ l) = comprehension ϕ (list_to_set A l).
|
||||||
Proof.
|
|
||||||
induction l1 ; cbn in *.
|
|
||||||
- symmetry. apply nl.
|
|
||||||
- rewrite <- assoc.
|
|
||||||
refine (ap (fun y => U {|a|} y) _).
|
|
||||||
rewrite <- append_union.
|
|
||||||
rewrite <- append_FSetCappend.
|
|
||||||
reflexivity.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma empty_empty : list_to_set empty = E.
|
|
||||||
Proof.
|
|
||||||
reflexivity.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma filter_comprehension (l : list A) (ϕ : A -> Bool) :
|
|
||||||
list_to_set (filter ϕ l) = comprehension ϕ (list_to_set l).
|
|
||||||
Proof.
|
Proof.
|
||||||
induction l ; cbn in *.
|
induction l ; cbn in *.
|
||||||
- reflexivity.
|
- reflexivity.
|
||||||
|
|
@ -118,32 +74,33 @@ Section ListToSet.
|
||||||
apply IHl.
|
apply IHl.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Lemma length_sizeC (l : list A) :
|
Definition singleton_single (a : A) : list_to_set A (singleton a) = L a :=
|
||||||
cardinality l = length (list_to_setC l).
|
nr (L a).
|
||||||
Proof.
|
|
||||||
induction l.
|
|
||||||
- cbn.
|
|
||||||
reflexivity.
|
|
||||||
- simpl.
|
|
||||||
rewrite IHl.
|
|
||||||
rewrite member_isIn.
|
|
||||||
reflexivity.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma length_size (l : list A) :
|
Lemma append_union (l1 l2 : list A) :
|
||||||
cardinality l = length_FSet (list_to_set l).
|
list_to_set A (union l1 l2) = U (list_to_set A l1) (list_to_set A l2).
|
||||||
Proof.
|
|
||||||
unfold length_FSet.
|
|
||||||
unfold list_to_set.
|
|
||||||
rewrite repr_iso_id_r.
|
|
||||||
apply length_sizeC.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma singleton_single (a : A) :
|
|
||||||
list_to_set (singleton a) = L a.
|
|
||||||
Proof.
|
Proof.
|
||||||
|
induction l1 ; induction l2 ; cbn.
|
||||||
|
- apply (union_idem _)^.
|
||||||
|
- apply (nl _)^.
|
||||||
|
- rewrite IHl1.
|
||||||
|
apply assoc.
|
||||||
|
- rewrite IHl1.
|
||||||
cbn.
|
cbn.
|
||||||
apply nr.
|
apply assoc.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
End ListToSet.
|
End ListToSet.
|
||||||
|
|
||||||
|
Section lists_are_sets.
|
||||||
|
Context `{Univalence}.
|
||||||
|
|
||||||
|
Instance lists_sets : sets list list_to_set.
|
||||||
|
Proof.
|
||||||
|
split ; intros.
|
||||||
|
- apply empty_empty.
|
||||||
|
- apply singleton_single.
|
||||||
|
- apply append_union.
|
||||||
|
- apply filter_comprehension.
|
||||||
|
- apply member_isIn.
|
||||||
|
Defined.
|
||||||
|
End lists_are_sets.
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue