...
 
Commits (2)
(; plus_ACU, lift_1, max_err
Original system as designed by ASSAF, DOWEK, JOUANNAUD and LIU.
Potential issues are:
- No implementation of lifting k levels.
Can only iterate lifting 1 level.
- 1 + max(i,j) is not convertible with max(1+i, 1+j)
It remains unclear whether this is an issue or not.
;)
(;-------------------------------;)
(; Arithmetic on universes sorts ;)
(;-------------------------------;)
Sort : Type.
0 : Sort.
1 : Sort.
defacu plus [Sort, 0].
def max : Sort -> Sort -> Sort.
[i,j] max i (plus i j) --> plus i j
[i,j] max (plus i j) i --> plus i j.
def rule : Sort -> Sort -> Sort.
[i ] rule i 0 --> 0
[i,j] rule i (plus j 1) --> max i (plus j 1).
(; This rule is missing from the original article. ;)
(; It is required to typecheck one of the rule below. ;)
[i,j] rule i (plus i j) --> plus i j.
(;-------------------------------;)
(; Terms encoding ;)
(;-------------------------------;)
(; Symbols declarations ;)
U : Sort -> Type.
def T : i : Sort -> a : U i -> Type.
u : i : Sort -> U (plus i 1).
lift : i : Sort -> a : U i -> U (plus i 1).
def liftn : i : Sort -> a : U 0 -> U i.
def prod :
i : Sort ->
j : Sort ->
a : U i ->
b : (x : T i a -> U j) ->
U (rule i j).
(; Rewriting rules ;)
[a] liftn 0 a --> a
[i,a] liftn (plus i 1) a --> lift i (liftn i a).
[i] T (plus i 1) (u i) --> U i
[i,a] T (plus i 1) (lift i a) --> T i a
[i,a] T i (liftn i a) --> T 0 a
[i,a,b] T 0 (prod i 0 a b) --> x : T i a -> T 0 (b x)
[i,j,a,b] T (plus i j) (prod i (plus i j) a b)
--> x: T i a -> T (plus i j) (b x)
[i,j,a,b] T (plus (plus i j) 1) (prod (plus (plus i j) 1) (plus j 1) a b)
--> x : T (plus (plus i j) 1) a -> T (plus j 1) (b x).
[i,j,a,b] prod (plus i 1) (plus (plus i j) 1) (lift i a) b
--> prod i (plus (plus i j) 1) a b
[i,j,a,b] prod (plus (plus i j) (plus 1 1)) (plus j 1) (lift (plus (plus i j) 1) a) b
--> lift (plus (plus i j) 1)
(prod (plus (plus i j) 1) (plus j 1) a b)
[i,j,a,b] prod (plus (plus i j) (plus 1 1)) (plus j (plus 1 1)) a (x => lift (plus j 1) (b x))
--> prod (plus (plus i j) (plus 1 1)) (plus j 1) a (x => b x)
(; This rule fails when omitting the added rewrite rule for the "rule" symbol. ;)
(; ( [i+j] should be convertible with [rule i (i+j)] ;)
[i,j,a,b] prod i (plus (plus i j) 1) a (x => lift (plus i j) (b x))
--> lift (plus i j) (prod i (plus i j) a (x => b x))
[a,b] prod 0 1 a (x => lift 0 (b x))
--> lift 0 (prod 0 0 a (x => b x))
[i,a,b] prod (plus i 1) 1 a (x => lift 0 (b x))
--> liftn (plus i 1) (prod (plus i 1) 0 a (x => b x))
[i,a,b] prod (plus i 1) 0 (lift i a) b
--> prod i 0 a b.
fmod LPM is
sort Nat .
sort Term .
sort Type .
op 0 : -> Nat [ctor] .
op 1 : -> Nat [ctor] .
op _+_ : Nat Nat -> Nat [comm assoc id: 0] .
op max : Nat Nat -> Nat .
op rule : Nat Nat -> Nat .
op pred : Nat -> Nat .
op U : Nat -> Type .
op T : Nat Term -> Type .
op u : Nat -> Term .
op lift : Nat Term -> Term .
op liftn : Nat Term -> Term .
op prod : Nat Nat Term Term -> Term .
op Pi : Type Type -> Type .
vars i j k l m x : Nat .
vars a b : Term .
eq max(i, i + j) = i + j .
eq max(i + j, j) = i + j .
eq rule(i, 0) = 0 .
eq rule(i, j + 1) = max(i, j + 1) .
eq rule(i, i + j) = i + j .
eq liftn(0, a) = a .
eq liftn(i + 1, a) = lift(i, liftn(i, a)) .
eq T(i + 1, u(i)) = U(i) .
eq T(i + 1, lift(i, a)) = T(i, a) .
eq T(i, liftn(i, a)) = T(0, a) .
eq T(0, prod(i, 0, a, b)) = Pi(T(i, a), T(0, b)) .
eq T(i + j, prod(i, i + j, a, b)) = Pi(T(i, a), T(i + j, b)) .
eq T(i + j + 1, prod(i + j + 1, j + 1, a, b)) = Pi(T(i + j + 1, a), T(j + 1, b)) .
eq prod(i + 1, i + j + 1, lift(i, a), b) = prod(i, i + j + 1, a, b) .
eq prod(i + j + 1 + 1, j + 1, lift(i + j + 1, a), b) = lift(i + j + 1, prod(i + j + 1, j + 1, a, b)) .
eq prod(i + j + 1 + 1, j + 1 + 1, a, lift(j + 1, b)) = prod(i + j + 1 + 1, j + 1, a, b) .
eq prod(i, i + j + 1, a, lift(i + j, b)) = lift(i + j, prod(i, i + j, a, b)) .
eq prod(i + 1, 1, a, lift(0, b)) = liftn(i + 1, prod(i + 1, 0, a, b)) .
eq prod(0, 1, a, lift(0, b)) = lift(0, prod(0, 0, a, b)) .
eq prod(i + 1, 0, lift(i, a), b) = prod(i, 0, a, b) .
eq max(i + 1, j) = 1 + max(i, pred(j)) .
eq pred(max(i, j)) = max(pred(i), pred(j)) .
eq pred(i + 1) = i .
eq pred(0) = 0 .
endfm
load cc.maude
load /home/gferey/maude/MFE/src/mfe.maude
(select tool CRC .)
(ccr LPM .)
(; lift, constraints ;)
(; Natural numbers ;)
N : Type.
0 : N.
S : N -> N.
def max : N -> N -> N.
[i ] max i 0 --> i.
[j ] max 0 (S j) --> S j.
[i,j] max (S i) (S j) --> S (max i j).
(; Unit type ;)
True : Type.
I : True.
(; Sorts ;)
Sort : Type.
prop : Sort.
type : N -> Sort.
def rule : Sort -> Sort -> Sort.
[s] rule s prop --> s.
[j] rule prop (type j) --> type j.
[i,j] rule (type i) (type j) --> type (max i j).
def axiom : Sort -> Sort.
[] axiom prop --> type 0.
[i] axiom (type i) --> type (S i).
(; Constraints ;)
def Cstr : Sort -> Sort -> Type.
[s] Cstr prop s --> True.
[i] Cstr (type 0) (type i) --> True.
[i,j] Cstr (type (S i)) (type (S j)) --> Cstr (type i) (type j).
(; Terms ;)
U : s1 : Sort -> Type.
def T : s1 : Sort -> a : U s1 -> Type.
def lift' : s1 : Sort -> s2 : Sort -> U s1 -> U s2.
def lift : s1 : Sort -> s2 : Sort -> Cstr s1 s2 -> U s1 -> U s2.
[s1, s2] lift s1 s2 _ --> lift' s1 s2.
univ : s : Sort -> U (axiom s).
def prod : s1 : Sort -> s2 : Sort -> a : U s1 -> (T s1 a -> U s2) -> U (rule s1 s2).
[s,a] lift' s s a --> a.
[s1,s2,a] lift' _ s2 (lift' s1 _ a) --> lift' s1 s2 a.
[s1] T _ (univ s1) --> U s1.
[s1,a] T _ (lift' s1 _ a) --> T s1 a.
[s1,s2,a,b] T _ (prod s1 s2 a b) --> x : T s1 a -> T s2 (b x).
[s1,s2,s3,a,b]
prod _ s2 (lift' s1 s3 a) (x => b x)
--> lift' (rule s1 s2) (rule s3 s2) (prod s1 s2 a (x => b x)).
[s1,s2,s3,a,b]
prod s1 _ a (x => lift' s2 s3 (b x))
--> lift' (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
(; lift, constraints ;)
(;
Same as constrained interpretation encoding except we need
a way to build s1 <= s3 from s1 <= s2 and s2 <= s3
;)
(; Natural numbers ;)
N : Type.
0 : N.
S : N -> N.
def max : N -> N -> N.
[i ] max i 0 --> i.
[j ] max 0 (S j) --> S j.
[i,j] max (S i) (S j) --> S (max i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
type : N -> Sort.
def rule : Sort -> Sort -> Sort.
[s] rule s prop --> s.
[j] rule prop (type j) --> type j.
[i,j] rule (type i) (type j) --> type (max i j).
def axiom : Sort -> Sort.
[] axiom prop --> type 0.
[i] axiom (type i) --> type (S i).
(; Constraints and their constructors ;)
Le : Sort -> Sort -> Type.
Leq : Sort -> Sort -> Type.
LeI : s : Sort -> Leq prop s.
LeT : i : N -> Leq (type 0) (type i).
LeqLe : s1 : Sort -> s2 : Sort -> Le s1 s2 -> Leq s1 s2.
LeqEq : s : Sort -> Leq s s.
LeTrans1 : s1 : Sort -> s2 : Sort -> s3 : Sort -> Leq s1 s2 -> Le s2 s3 -> Le s1 s3.
LeTrans2 : s1 : Sort -> s2 : Sort -> s3 : Sort -> Le s1 s2 -> Leq s2 s3 -> Le s1 s3.
LeqTrans : s1 : Sort -> s2 : Sort -> s3 : Sort -> Leq s1 s2 -> Leq s2 s3 -> Leq s1 s3.
(; Terms ;)
U : s1 : Sort -> Type.
def T : s1 : Sort -> a : U s1 -> Type.
def lift' : s1 : Sort -> s2 : Sort -> U s1 -> U s2.
def lift : s1 : Sort -> s2 : Sort -> Leq s1 s2 -> U s1 -> U s2.
[s1, s2] lift s1 s2 _ --> lift' s1 s2.
univ : s : Sort -> U (axiom s).
def prod : s1 : Sort -> s2 : Sort -> a : U s1 -> (T s1 a -> U s2) -> U (rule s1 s2).
[s,a] lift' s s a --> a.
[s1,s2,a] lift' _ s2 (lift' s1 _ a) --> lift' s1 s2 a.
[s1] T _ (univ s1) --> U s1.
[s1,a] T _ (lift' s1 _ a) --> T s1 a.
[s1,s2,a,b] T _ (prod s1 s2 a b) --> x : T s1 a -> T s2 (b x).
[s1,s2,s3,a,b]
prod _ s2 (lift' s1 s3 a) (x => b x)
--> lift' (rule s1 s2) (rule s3 s2) (prod s1 s2 a (x => b x)).
[s1,s2,s3,a,b]
prod s1 _ a (x => lift' s2 s3 (b x))
--> lift' (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
(; WIP, constraints ;)
(; Code types depend on a universe and associated constraints ;)
(; Natural numbers ;)
N : Type.
......
......@@ -7,14 +7,31 @@ This project contains various implementations of cic.dk
| [./AC/cicup_maxAC.dk](./AC/cicup_maxAC.dk) | | | | | X | | | | | | |
| [./AC/cicup_0elim.dk](./AC/cicup_0elim.dk) | | X | | | X | X | | X | | | |
| [./AC/cicup_0elim_maxplus.dk](./AC/cicup_0elim_maxplus.dk) | | X | | | X | | | | | | |
| [./AC/2-test/cc.dk](./AC/2-test/cc.dk) | | | X | | X | X | | | | | |
| [./private/cic.dk](./private/cic.dk) | | | | | | | | | | | |
| [./nolift/cc.dk](./nolift/cc.dk) | | | | X | | | | | X | | X |
| [./nolift/cic.dk](./nolift/cic.dk) | | | | X | | | | | X | | X |
| [./francois/cic.dk](./francois/cic.dk) | | | | | | | | | | | |
| [./HOAS/HOAS_to_DBAC.dk](./HOAS/HOAS_to_DBAC.dk) | | | | | | | | | X | | |
| [./experimenting/liftplus/cic.dk](./experimenting/liftplus/cic.dk) | | | | | | | | | | | |
| [./experimenting/liftplus/univ/plusACpred/univ.dk](./experimenting/liftplus/univ/plusACpred/univ.dk) | | | | | | | | | | | |
| [./experimenting/liftplus/univ/plusAC/univ.dk](./experimenting/liftplus/univ/plusAC/univ.dk) | | | | | | | | | | | |
| [./experimenting/liftk/cic.dk](./experimenting/liftk/cic.dk) | | | | | | | | | | | |
| [./experimenting/liftk/univ/orig/univ.dk](./experimenting/liftk/univ/orig/univ.dk) | | | | | | | | | | | |
| [./experimenting/liftmax/cic.dk](./experimenting/liftmax/cic.dk) | | | | | | | | | | | |
| [./experimenting/liftmax/univ/orig/univ.dk](./experimenting/liftmax/univ/orig/univ.dk) | | | | | | | | | | | |
| [./experimenting/liftkplus/cic.dk](./experimenting/liftkplus/cic.dk) | | | | | | | | | | | |
| [./experimenting/liftkplus/univ/plusACpred/univ.dk](./experimenting/liftkplus/univ/plusACpred/univ.dk) | | | | | | | | | | | |
| [./experimenting/liftkplus/univ/plusAC/univ.dk](./experimenting/liftkplus/univ/plusAC/univ.dk) | | | | | | | | | | | |
| [./orig/cic_ali.dk](./orig/cic_ali.dk) | | | | | X | | | | | | |
| [./orig/cic_coqine.dk](./orig/cic_coqine.dk) | | | | X | X | | | | | | |
| [./orig/cic.dk](./orig/cic.dk) | | | | | X | | | | | | |
| [./orig/cic_v2.dk](./orig/cic_v2.dk) | X | | | | X | | | | X | | |
| [./orig/cic_minimalist.dk](./orig/cic_minimalist.dk) | | | | | X | | | | | | |
| [./old_to_ACU/cc.dk](./old_to_ACU/cc.dk) | | X | | | X | | | | | | |
| [./Constraints/cc.dk](./Constraints/cc.dk) | | | | | | | | | X | X | |
| [./Constraints/constrained_interp/cic.dk](./Constraints/constrained_interp/cic.dk) | | | | | X | | | | | X | |
| [./Constraints/constrained_types/cic.dk](./Constraints/constrained_types/cic.dk) | | | | | | | | | X | X | |
| [./Constraints/constrained_interp_poly/cic.dk](./Constraints/constrained_interp_poly/cic.dk) | | | | | X | | | | | X | |
| [./AC_with_constraints/cic.dk](./AC_with_constraints/cic.dk) | X | | | | X | | | | X | | |
## Flags
......
#put the path of your dkcheck binary
DKCHECK ?= dkcheck
#put the path of your dkdep binary
DKDEP ?= dkdep
DKOPTIONS = $(DKFLAGS) -nl -errors-in-snf -e
DKCHECK_=$(DKCHECK) $(DKOPTIONS)
.PHONY: default orig cic clean
default: orig cic
orig:
$(DKCHECK_) univ/orig/univ.dk
cp univ/orig/univ.dko ./
cic:
$(DKCHECK_) cic.dk
clean:
rm *.dko
(;-------------------------------;)
(; Aliases for universe system ;)
(;-------------------------------;)
def Sort := univ.Sort.
def axiom := univ.axiom.
def max := univ.max.
def rule := univ.rule.
(;-------------------------------;)
(; CiC encoding ;)
(;-------------------------------;)
Univ : Sort -> Type.
def Term : s : Sort -> a : Univ s -> Type.
univ : s : Sort -> Univ (axiom s).
def prod :
s1 : Sort ->
s2 : Sort ->
a : Univ s1 ->
b : (Term s1 a -> Univ s2) ->
Univ (rule s1 s2).
[s] Term _ (univ s) --> Univ s.
[s1, s2, a, b]
Term _ (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).
def lift1 : s1 : Sort -> Univ s1 -> Univ (axiom s1).
[s1,s2,a] Term _ (lift1 s1 a) --> Term s1 a.
[s1, s2, s3, a]
lift1 _ s3 (lift1 s1 s2 a) -->
lift s1 (max s2 s3) a.
[s1, s2, s3, a, b]
prod _ s2 (lift s1 s3 a) b -->
lift (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
[s1, s2, s3, a, b]
prod s1 _ a (x => lift s2 s3 (b x)) -->
lift (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
Leq : Sort -> Sort -> Type.
refl : s : Sort -> Leq s s.
next : s1 : Sort -> s2 : Sort -> Leq s1 s2 -> Leq s1 (axiom s2).
def lift : s1 : Sort -> s2 : Sort -> Leq s1 s2 -> Univ s1 -> Univ s2.
[s, a] lift _ _ (refl s) a --> a.
[s1,s2,p,a] lift _ _ (next s1 s2 p) a --> lift1 s2 (lift s1 s2 p a).
[s1,s2,a] Term _ (lift s1 s2 _ a) --> Term s1 a.
[s1, s2, s3, a]
lift _ s3 (lift s1 s2 a) -->
lift s1 (max s2 s3) a.
[s1, s2, s3, a, b]
prod _ s2 (lift s1 s3 a) b -->
lift (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
[s1, s2, s3, a, b]
prod s1 _ a (x => lift s2 s3 (b x)) -->
lift (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
(; Natural numbers ;)
Nat : Type.
z : Nat.
s : Nat -> Nat.
def m : Nat -> Nat -> Nat.
[i] m i z --> i.
[j] m z j --> j.
[i, j] m (s i) (s j) --> s (m i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
type : Nat -> Sort.
(; Universe cumulativity ;)
def axiom : Sort -> Sort.
[] axiom prop --> type z.
[i] axiom (type i) --> type (s i).
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort.
[s1] rule s1 prop --> prop.
[s2] rule prop s2 --> s2.
[i,j] rule (type i) (type j) --> type (m i j).
(; Universe subtyping ;)
def max : Sort -> Sort -> Sort.
[s] max s prop --> s
[s] max prop s --> s
[i,j] max (type i) (type j) --> type (m i j).
(; Canonicity rules ;)
[s] max s s --> s.
[s1,s2,s3] max (max s1 s2) s3 --> max s1 (max s2 s3).
[s1,s2,s3] rule (max s1 s3) s2 --> max (rule s1 s2) (rule s3 s2).
[s1,s2,s3] rule s1 (max s2 s3) --> max (rule s1 s2) (rule s1 s3).
#put the path of your dkcheck binary
DKCHECK ?= dkcheck-acu
#put the path of your dkdep binary
DKDEP ?= dkdep-acu
DKOPTIONS = $(DKFLAGS) -nl -errors-in-snf -e
DKCHECK_=$(DKCHECK) $(DKOPTIONS)
.PHONY: default orig cic clean
default: plusAC cic
cic:
$(DKCHECK_) cic.dk
clean:
rm *.dko
plusAC:
$(DKCHECK_) univ/plusAC/univ.dk
cp univ/plusAC/univ.dko ./
plusACpred:
$(DKCHECK_) univ/plusACpred/univ.dk
cp univ/plusACpred/univ.dko ./
(;-------------------------------;)
(; Aliases for universe system ;)
(;-------------------------------;)
def Sort := univ.Sort.
def rule := univ.rule.
(;-------------------------------;)
(; CiC encoding ;)
(;-------------------------------;)
U : Sort -> Type.
def T : i : Sort -> a : U i -> Type.
u : i : Sort -> U (univ.plus i univ.1).
lift : i : Sort -> a : U i -> U (univ.plus i univ.1).
def prod :
i : Sort ->
j : Sort ->
a : U i ->
b : (x : T i a -> U j) ->
U (rule i j).
(; Rewriting rules ;)
[i] T _ (u i) --> U i
[i,a] T _ (lift i a) --> T i a
[i,a,b]
T univ.0 (prod i univ.0 a b) -->
x : T i a -> T univ.0 (b x)
[i,j,a,b]
T (univ.plus i j) (prod i (univ.plus i j) a b) -->
x: T i a -> T (univ.plus i j) (b x)
[i,j,a,b]
T (univ.plus (univ.plus i j) univ.1)
(prod (univ.plus (univ.plus i j) univ.1) (univ.plus j univ.1) a b)
-->
x : T (univ.plus (univ.plus i j) univ.1) a -> T (univ.plus j univ.1) (b x).
[i,j,a,b]
prod (univ.plus i univ.1) (univ.plus (univ.plus i j) univ.1) (lift i a) b -->
prod i (univ.plus (univ.plus i j) univ.1) a b
[i,j,a,b]
prod (univ.plus (univ.plus i j) (univ.plus univ.1 univ.1))
(univ.plus j univ.1)
(lift (univ.plus (univ.plus i j) univ.1) a)
b
-->
lift (univ.plus (univ.plus i j) univ.1)
(prod (univ.plus (univ.plus i j) univ.1) (univ.plus j univ.1) a b)
[i,j,a,b]
prod (univ.plus (univ.plus i j) (univ.plus univ.1 univ.1))
(univ.plus j (univ.plus univ.1 univ.1))
a
(x => lift (univ.plus j univ.1) (b x))
-->
prod (univ.plus (univ.plus i j) (univ.plus univ.1 univ.1)) (univ.plus j univ.1) a (x => b x)
[i,j,a,b]
prod i (univ.plus (univ.plus i j) univ.1) a (x => lift (univ.plus i j) (b x)) -->
lift (univ.plus i j) (prod i (univ.plus i j) a (x => b x))
[a,b]
prod univ.0 univ.1 a (x => lift univ.0 (b x)) -->
lift univ.0 (prod univ.0 univ.0 a (x => b x))
[i,a,b]
prod (univ.plus i univ.1) univ.0 (lift i a) b -->
prod i univ.0 a b.
Leq : Sort -> Sort -> Type.
refl : s : Sort -> Leq s s.
next : s1 : Sort -> s2 : Sort -> Leq s1 s2 -> Leq s1 (univ.plus univ.1 s2).
conc : s1 : Sort -> s2 : Sort -> s3 : Sort -> Leq s1 s2 -> Leq s2 s3 -> Leq s1 s3.
def liftn :
s1 : Sort ->
s2 : Sort ->
p : Leq s1 s2 ->
U s1 -> U s2.
[s,a] liftn _ _ (refl s) a --> a.
[s1,s2,p,a] liftn _ _ (next s1 s2 p) a --> lift s2 (liftn s1 s2 p a).
[s1,s2,s3,p1,p2,a]
liftn _ _ (conc s1 s2 s3 p1 p2) a -->
liftn s2 s3 p2 (liftn s1 s2 p1 a).
fmod LPM is
sort Nat .
sort Term .
sort Type .
op 0 : -> Nat [ctor] .
op 1 : -> Nat [ctor] .
op _+_ : Nat Nat -> Nat [comm assoc id: 0] .
op max : Nat Nat -> Nat .
op rule : Nat Nat -> Nat .
op U : Nat -> Type .
op T : Nat Term -> Type .
op u : Nat -> Term .
op lift : Nat Term -> Term .
op prod : Nat Nat Term Term -> Term .
op Pi : Type Type -> Type .
vars i j k l m x : Nat .
vars a b : Term .
eq max(i, i + j) = i + j .
eq max(i + j, j) = i + j .
eq rule(i, 0) = 0 .
eq rule(i, j + 1) = max(i, j + 1) .
eq rule(i, i + j) = i + j .
eq T(i + 1, u(i)) = U(i) .
eq T(i + 1, lift(i, a)) = T(i, a) .
eq T(0, prod(i, 0, a, b)) = Pi(T(i, a), T(0, b)) .
eq T(i + j, prod(i, i + j, a, b)) = Pi(T(i, a), T(i + j, b)) .
eq T(i + j + 1, prod(i + j + 1, j + 1, a, b)) = Pi(T(i + j + 1, a), T(j + 1, b)) .
eq prod(i + 1, i + j + 1, lift(i, a), b) = prod(i, i + j + 1, a, b) .
eq prod(i + j + 1 + 1, j + 1, lift(i + j + 1, a), b) = lift(i + j + 1, prod(i + j + 1, j + 1, a, b)) .
eq prod(i + j + 1 + 1, j + 1 + 1, a, lift(j + 1, b)) = prod(i + j + 1 + 1, j + 1, a, b) .
eq prod(i, i + j + 1, a, lift(i + j, b)) = lift(i + j, prod(i, i + j, a, b)) .
eq prod(0, 1, a, lift(0, b)) = lift(0, prod(0, 0, a, b)) .
eq prod(i + 1, 0, lift(i, a), b) = prod(i, 0, a, b) .
endfm
load cic.maude
load /home/gferey/maude/MFE/src/mfe.maude
(select tool CRC .)
(ccr LPM .)
Sort : Type.
0 : Sort.
1 : Sort.
defacu plus [Sort, 0].
def max : Sort -> Sort -> Sort.
[i,j] max i (plus i j) --> plus i j
[i,j] max (plus i j) i --> plus i j.
def rule : Sort -> Sort -> Sort.
[i ] rule i 0 --> 0
[i,j] rule i (plus j 1) --> max i (plus j 1).
[i,j] rule i (plus i j) --> plus i j.
Sort : Type.
0 : Sort.
1 : Sort.
defacu plus [Sort, 0].
def max : Sort -> Sort -> Sort.
[i,j] max i (plus i j) --> plus i j
[i,j] max (plus i j) i --> plus i j.
def rule : Sort -> Sort -> Sort.
[i ] rule i 0 --> 0
[i,j] rule i (plus j 1) --> max i (plus j 1).
[i,j] rule i (plus i j) --> plus i j.
def pred : Sort -> Sort.
[] pred 0 --> 0.
[i] pred (plus 1 i) --> i.
[i,j] max (plus 1 i) j --> plus 1 (max i (pred j)).
[i,j] pred (max i j) --> max (pred i) (pred j).
#put the path of your dkcheck binary
DKCHECK ?= dkcheck
#put the path of your dkdep binary
DKDEP ?= dkdep
DKOPTIONS = $(DKFLAGS) -nl -errors-in-snf -e
DKCHECK_=$(DKCHECK) $(DKOPTIONS)
.PHONY: default orig cic clean
default: orig cic
orig:
$(DKCHECK_) univ/orig/univ.dk
cp univ/orig/univ.dko ./
cic:
$(DKCHECK_) cic.dk
clean:
rm *.dko
(;-------------------------------;)
(; Aliases for universe system ;)
(;-------------------------------;)
def Sort := univ.Sort.
def axiom := univ.axiom.
def max := univ.max.
def rule := univ.rule.
(;-------------------------------;)
(; CiC encoding ;)
(;-------------------------------;)
Univ : s : Sort -> Type.
def Term : s : Sort -> a : Univ s -> Type.
univ : s : Sort -> Univ (axiom s).
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (max s1 s2).
def prod :
s1 : Sort ->
s2 : Sort ->
a : Univ s1 ->
b : (Term s1 a -> Univ s2) ->
Univ (rule s1 s2).
[s] Term _ (univ s) --> Univ s.
[s1, s2, a] Term _ (lift s1 s2 a) --> Term s1 a.
[s1, s2, a, b]
Term _ (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).
[s, a] lift s s a --> a.
[s1, s2, s3, a]
lift _ s3 (lift s1 s2 a) -->
lift s1 (max s2 s3) a.
[s1, s2, s3, a, b]
prod _ s2 (lift s1 s3 a) b -->
lift (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
[s1, s2, s3, a, b]
prod s1 _ a (x => lift s2 s3 (b x)) -->
lift (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
(; Natural numbers ;)
Nat : Type.
z : Nat.
s : Nat -> Nat.
def m : Nat -> Nat -> Nat.
[i] m i z --> i.
[j] m z j --> j.
[i, j] m (s i) (s j) --> s (m i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
type : Nat -> Sort.
(; Universe cumulativity ;)
def axiom : Sort -> Sort.
[] axiom prop --> type z.
[i] axiom (type i) --> type (s i).
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort.
[s1] rule s1 prop --> prop.
[s2] rule prop s2 --> s2.
[i,j] rule (type i) (type j) --> type (m i j).
(; Universe subtyping ;)
def max : Sort -> Sort -> Sort.
[s] max s prop --> s
[s] max prop s --> s
[i,j] max (type i) (type j) --> type (m i j).
(; Canonicity rules ;)
[s] max s s --> s.
[s1,s2,s3] max (max s1 s2) s3 --> max s1 (max s2 s3).
[s1,s2,s3] rule (max s1 s3) s2 --> max (rule s1 s2) (rule s3 s2).
[s1,s2,s3] rule s1 (max s2 s3) --> max (rule s1 s2) (rule s1 s3).
#put the path of your dkcheck binary
DKCHECK ?= dkcheck-acu
#put the path of your dkdep binary
DKDEP ?= dkdep-acu
DKOPTIONS = $(DKFLAGS) -nl -errors-in-snf -e
DKCHECK_=$(DKCHECK) $(DKOPTIONS)
.PHONY: default orig cic clean
default: plusAC cic
cic:
$(DKCHECK_) cic.dk
clean:
rm *.dko
plusAC:
$(DKCHECK_) univ/plusAC/univ.dk
cp univ/plusAC/univ.dko ./
plusACpred:
$(DKCHECK_) univ/plusACpred/univ.dk
cp univ/plusACpred/univ.dko ./
(;-------------------------------;)
(; Aliases for universe system ;)
(;-------------------------------;)
def Sort := univ.Sort.
def rule := univ.rule.
(;-------------------------------;)
(; CiC encoding ;)
(;-------------------------------;)
U : Sort -> Type.
def T : i : Sort -> a : U i -> Type.
u : i : Sort -> U (univ.plus i univ.1).
lift : i : Sort -> a : U i -> U (univ.plus i univ.1).
def liftn : i : Sort -> a : U univ.0 -> U i.
def prod :
i : Sort ->
j : Sort ->
a : U i ->
b : (x : T i a -> U j) ->
U (rule i j).
(; Rewriting rules ;)
[a] liftn univ.0 a --> a
[i,a] liftn (univ.plus i univ.1) a --> lift i (liftn i a).
[i] T _ (u i) --> U i
[i,a] T _ (lift i a) --> T i a
[i,a] T _ (liftn i a) --> T univ.0 a
[i,a,b]
T univ.0 (prod i univ.0 a b) -->
x : T i a -> T univ.0 (b x)
[i,j,a,b]
T (univ.plus i j) (prod i (univ.plus i j) a b) -->
x: T i a -> T (univ.plus i j) (b x)
[i,j,a,b]
T (univ.plus (univ.plus i j) univ.1)
(prod (univ.plus (univ.plus i j) univ.1) (univ.plus j univ.1) a b)
-->
x : T (univ.plus (univ.plus i j) univ.1) a -> T (univ.plus j univ.1) (b x).
[i,j,a,b]
prod (univ.plus i univ.1) (univ.plus (univ.plus i j) univ.1) (lift i a) b -->
prod i (univ.plus (univ.plus i j) univ.1) a b
[i,j,a,b]
prod (univ.plus (univ.plus i j) (univ.plus univ.1 univ.1))
(univ.plus j univ.1)
(lift (univ.plus (univ.plus i j) univ.1) a)
b
-->
lift (univ.plus (univ.plus i j) univ.1)
(prod (univ.plus (univ.plus i j) univ.1) (univ.plus j univ.1) a b)
[i,j,a,b]
prod (univ.plus (univ.plus i j) (univ.plus univ.1 univ.1))
(univ.plus j (univ.plus univ.1 univ.1))
a
(x => lift (univ.plus j univ.1) (b x))
-->
prod (univ.plus (univ.plus i j) (univ.plus univ.1 univ.1)) (univ.plus j univ.1) a (x => b x)
[i,j,a,b]
prod i (univ.plus (univ.plus i j) univ.1) a (x => lift (univ.plus i j) (b x)) -->
lift (univ.plus i j) (prod i (univ.plus i j) a (x => b x))
[a,b]
prod univ.0 univ.1 a (x => lift univ.0 (b x)) -->
lift univ.0 (prod univ.0 univ.0 a (x => b x))
[i,a,b]
prod (univ.plus i univ.1) univ.1 a (x => lift univ.0 (b x)) -->
liftn (univ.plus i univ.1) (prod (univ.plus i univ.1) univ.0 a (x => b x))
[i,a,b]
prod (univ.plus i univ.1) univ.0 (lift i a) b -->
prod i univ.0 a b.
Sort : Type.
0 : Sort.
1 : Sort.
defacu plus [Sort, 0].
def max : Sort -> Sort -> Sort.
[i,j] max i (plus i j) --> plus i j
[i,j] max (plus i j) i --> plus i j.
def rule : Sort -> Sort -> Sort.
[i ] rule i 0 --> 0
[i,j] rule i (plus j 1) --> max i (plus j 1).
[i,j] rule i (plus i j) --> plus i j.
Sort : Type.
0 : Sort.
1 : Sort.
defacu plus [Sort, 0].
def max : Sort -> Sort -> Sort.
[i,j] max i (plus i j) --> plus i j
[i,j] max (plus i j) i --> plus i j.
def rule : Sort -> Sort -> Sort.
[i ] rule i 0 --> 0
[i,j] rule i (plus j 1) --> max i (plus j 1).
[i,j] rule i (plus i j) --> plus i j.
def pred : Sort -> Sort.
[] pred 0 --> 0.
[i] pred (plus 1 i) --> i.
[i,j] max (plus 1 i) j --> plus 1 (max i (pred j)).
[i,j] pred (max i j) --> max (pred i) (pred j).
Nat : Type.
z : Nat.
s : Nat -> Nat.
def m : Nat -> Nat -> Nat.
[i] m i z --> i.
[j] m z j --> j.
[i, j] m (s i) (s j) --> s (m i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
type : Nat -> Sort.
(; Universe successors ;)
def succ : Sort -> Sort.
[] succ prop --> type z.
[i] succ (type i) --> type (s i).
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort.
[s1] rule s1 prop --> prop.
[s2] rule prop s2 --> s2.
[i, j] rule (type i) (type j) --> type (m i j).
def max : Sort -> Sort -> Sort.
[s1] max s1 prop --> s1.
[s2] max prop s2 --> s2.
[i, j] max (type i) (type j) --> type (m i j).
[s] max s s --> s.
[s1,s2] succ (max s1 s2) --> max (succ s1) (succ s2).
[s1,s2,s3] max (max s1 s2) s3 --> max s1 (max s2 s3).
[s1,s2,s3] rule s1 (max s2 s3) --> max (rule s1 s2) (rule s1 s3).
[s1,s2,s3] rule (max s1 s2) s3 --> max (rule s1 s3) (rule s2 s3).
(; Types and terms ;)
Univ : Sort -> Type.
def Term : s : Sort -> a : Univ s -> Type.
univ : s : Sort -> Univ (succ s).
def prod : s1 : Sort -> s2 : Sort -> a : Univ s1 -> b : (Term s1 a -> Univ s2) -> Univ (rule s1 s2).
def join : s1 : Sort -> s2 : Sort -> Univ s1 -> Univ s2 -> Univ (max s1 s2).
def cast : s1 : Sort -> s2 : Sort -> a : Univ s1 -> b : Univ s2 -> Term s1 a -> Term (max s1 s2) (join s1 s2 a b).
[s] Term _ (univ s) --> Univ s.
[s, a] Term _ (cast _ _ (univ s) _ a) --> Term s a.
[s1 : Sort, s2 : Sort, a : Univ s1, b : (Term s1 a -> Univ s2)]
Term _ (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).
(; Canonicity rules ;)
[i] join _ _ i i --> i.
[s1,s2] join _ _ (univ s1) (univ s2) --> univ (max s1 s2).
[s1,s2,s3,a,b,c]
join _ _ (prod s1 s2 a b) (prod {s1} s3 {a} c)
--> prod s1 (max s2 s3) a (x : Term s1 a => join s2 s3 (b x) (c x)).
[s1,s2,s3,a,b,c,m,x]
cast _ _ (prod s1 s2 a b) (prod {s1} s3 {a} c) m x
--> cast s2 s3 (b x) (c x) (m x).
[t1,t2,a,t1',t2',a'] join _ _ (cast _ _ (univ t1) (univ t2) a) (cast _ _ (univ t1') (univ t2') a') -->
cast (succ (max t1 t1')) (succ (max t2 t2')) (univ (max t1 t1'))
(univ (max t2 t2')) (join t1 t1' a a').
(; canonicity rules ;)
[t,a] cast _ _ t t a --> a.
[s1,s2,s3,a]
cast _ _ (univ _) (univ s3) (cast _ _ (univ s1) (univ s2) a)
--> cast (succ s1) (succ (max s2 s3)) (univ s1) (univ (max s2 s3)) a.
[s1,s2,s3,a,b]
prod _ s2 (cast _ _ (univ s1) (univ s3) a) (x => b x)
--> cast
(succ (rule s1 s2))
(succ (rule s3 s2))
(univ (rule s1 s2))
(univ (rule s3 s2))
(prod s1 s2 a (x => b x)).
[s1,s2,s3,a,b]
prod s1 _ a (x => cast _ _ (univ s2) (univ s3) (b x))
--> cast
(succ (rule s1 s2))
(succ (rule s1 s3))
(univ (rule s1 s2))
(univ (rule s1 s3))
(prod s1 s2 a (x => b x)).
fmod LPM is
sort Nat .
sort Term .
sort Type .
op z : -> Nat [ctor] .
op s : Nat -> Nat [ctor] .
op max : Nat Nat -> Nat [assoc comm] .
op rule : Nat Nat -> Nat .
op Univ : Nat -> Type .
op T : Nat Term -> Type .
op univ : Nat -> Term .
op prod : Nat Nat Term Term -> Term .
op join : Nat Nat Term Term -> Term .
op cast : Nat Nat Term Term -> Term .
op Pi : Type Type -> Type .
vars i j k l m x : Nat .
vars p q r t : Nat .
vars a b : Term .
eq max(i, z) = i .
eq max(z, i) = i .
--- eq max(s(i), s(j)) = s(m(i, j)) .
eq s(max(i, j)) = max(s(i), s(j)) .
eq rule(i, z) = z .
eq rule(z, j) = j .
eq rule(s(i), s(j)) = s(m(i, j)) .
eq max(i, i) = i .
eq rule(i, max(j, k)) = max(rule(i, j), rule(i, k)) .
eq rule(max(i, j), k) = max(rule(i, k), rule(j, k)) .
eq T(i, univ(j)) = Univ(j) .
--- eq Term(s, cast(s1, s2, univ(s), b, a) = Univ(s) .
endfm
load cic.maude
load /home/gferey/maude/MFE/src/mfe.maude
(select tool CRC .)
---(CRC help .)
(ccr LPM .)
---(show all critical pairs .)
\ No newline at end of file
(; lift ;)
(; Natural numbers ;)
Nat : Type.
z : Nat.
s : Nat -> Nat.
def max : Nat -> Nat -> Nat.
[i] max i z --> i.
[j] max z j --> j.
[i, j] max (s i) (s j) --> s (max i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
type : Nat -> Sort.
(; Universe cumulativity ;)
def axiom : Sort -> Sort.
[] axiom prop --> type z.
[i] axiom (type i) --> type (s i).
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort.
[s1] rule s1 prop --> prop.
[s2] rule prop s2 --> s2.
[i, j] rule (type i) (type j) --> type (max i j).
def sup : Sort -> Sort -> Sort.
[s1] sup s1 prop --> s1.
[s2] sup prop s2 --> s2.
[i, j] sup (type i) (type j) --> type (max i j).
(; Types and terms ;)
Univ : s : Sort -> Type.
def Term : s : Sort -> a : Univ s -> Type.
univ : s : Sort -> Univ (axiom s).
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (sup s1 s2).
def prod : s1 : Sort -> s2 : Sort -> a : Univ s1 -> b : (Term s1 a -> Univ s2) -> Univ (rule s1 s2).
[s] Term _ (univ s) --> Univ s.
[s1, s2, a] Term _ (lift s1 s2 a) --> Term s1 a.
[s1, s2, a, b] Term _ (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).
(; Canonicity rules ;)
[s] sup s s --> s.
[s1, s2, s3] sup (sup s1 s2) s3 --> sup s1 (sup s2 s3).
[s1, s2, s3] rule (sup s1 s3) s2 --> sup (rule s1 s2) (rule s3 s2).
[s1, s2, s3] rule s1 (sup s2 s3) --> sup (rule s1 s2) (rule s1 s3).
[s, a] lift s s a --> a.
[s1, s2, s3, a]
lift _ s3 (lift s1 s2 a) -->
lift s1 (sup s2 s3) a.
[s1, s2, s3, a, b]
prod _ s2 (lift s1 s3 a) b -->
lift (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
[s1, s2, s3, a, b]
prod s1 _ a (x => lift s2 s3 (b x)) -->
lift (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
(; lift ;)
(; Natural numbers ;)
Nat : Type.
z : Nat.
s : Nat -> Nat.
def max : Nat -> Nat -> Nat.
[i] max i z --> i.
[j] max z j --> j.
[i, j] max (s i) (s j) --> s (max i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
type : Nat -> Sort.
(; Universe cumulativity ;)
def axiom : Sort -> Sort.
[] axiom prop --> type z.
[i] axiom (type i) --> type (s i).
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort.
[s1] rule s1 prop --> prop.
[s2] rule prop s2 --> s2.
[i,j] rule (type i) (type j) --> type (max i j).
(; Types and terms ;)
Univ : s : Sort -> Type.
def Term : s : Sort -> a : Univ s -> Type.
univ : s : Sort -> Univ (axiom s).
def lift : s : Sort -> i : Nat -> a : Univ s -> Univ (rule s (type i)).
def prod : s1 : Sort -> s2 : Sort -> a : Univ s1 -> b : (Term s1 a -> Univ s2) -> Univ (rule s1 s2).
[s] Term _ (univ s) --> Univ s.
[s1, s2, a] Term _ (lift s1 s2 a) --> Term s1 a.
[s1, s2, a, b] Term _ (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).
(; Canonicity rules ;)
[i] max i i --> i.
[i, a] lift (type i) i a --> a.
[s,i,j] rule (rule s (type i)) (type j) --> rule s (type (max i j)).
[s,i,j,a]
lift _ i (lift s j a) -->
lift s (max j i) a.
(;
rule (rule s (type j)) (type i)
rule (rule s (type i)) (type (max i j)).
;)
[s, i, a, b]
prod _ prop (lift s i a) b -->
prod s prop a b.
[s,i,j,a,b]
prod _ (type i) (lift s j a) b -->
lift (rule s (type i)) (max i j) (prod s (type i) a b).
[s1, s2, s3, a, b]
prod s1 _ a (x => lift s2 s3 (b x)) -->
lift (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
load cic_v2.maude
load /home/gaspi/maude/MFE/src/mfe.maude
load test.maude
load /home/gferey/maude/MFE/src/mfe.maude
(select tool CRC .)
(CRC help .)
---(CRC help .)
(ccr LPM .)
---(show all critical pairs .)
\ No newline at end of file
fmod LPM is
sort Nat .
sort Term .
sort Type .
op z : -> Nat [ctor] .
op s : Nat -> Nat [ctor] .
op m : Nat Nat -> Nat [comm assoc] .
op rule : Nat Nat -> Nat .
op Univ : Nat -> Type .
op Term : Nat Term -> Type .
op univ : Nat -> Term .
op prod : Nat Nat Term Term -> Term .
op lift : Nat Nat Term -> Term .
op Pi : Type Type -> Type .
vars i j k l m x : Nat .
vars p q r t : Nat .
vars a b : Term .
eq m(i, z) = i .
eq m(z, i) = i .
eq m(i, i) = i .
eq m(s(i),s(j)) = s(m(i, j)) .
eq rule(p, z) = z .
eq rule(z,r) = r .
eq rule(s(i), s(i)) = s(i) .
eq rule(s(i), s(z)) = s(i) .
eq rule(s(i), s(s(j))) = s(rule(i,s(j))) .
eq Term(s(q), univ(q)) = Univ(q) .
eq Term(m(q,r), lift(q,r,a)) = Term(q, a) .
eq Term(rule(q,r), prod(q,r,a,b)) = Pi(Term(q,a),Term(r,b)) .
eq Term(p, univ(q)) = Univ(q) .
eq Term(p, prod(q,r,a,b)) = Pi(Term(q,a),Term(r,b)) .
eq Term(rule(q,s(r)), lift(q,r,a)) = Term(q, a) .
eq Term(p, lift(q,r,a)) = Term(q, a) .
eq Term(s(r), lift(z,r,a)) = Term(z, a) .
eq Term(s(q), lift(s(q),z,a)) = Term(s(q), a) .
eq Term(s(rule(q,s(r))), lift(s(q),s(r),a)) = Term(s(q), a) .
eq lift(s(i),i,a) = a .
eq rule(m(p,q),r) = m(rule(p,r),rule(q,r)) .
eq rule(p,m(q,r)) = m(rule(p,q),rule(p,r)) .
eq lift(m(r,t),q,lift(r,t,a)) = lift(r,m(q,t),a) .
eq prod(m(r,t),q,lift(r,t,a),b) = lift(rule(r,q),rule(t,q),prod(r,q,a,b)) .
eq prod(p,m(r,t),a,lift(r,t,b)) = lift(rule(p,r),rule(p,t),prod(p,r,a,b)) .
--- eq m(r,rule(p,r)) = rule(p,r) .
--- eq lift(r, m(r,t), a) = lift(r,t,a) .
endfm
(; Sorts ;)
Sort : Type.
0 : Sort.
S : Sort -> Sort.
(; Universe cumulativity ;)
True : Type.
I : True.
def cumul : Sort -> Sort -> Type.
[i ] cumul 0 i --> True.
[i,j] cumul (S i) (S j) --> cumul i j.
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort.
[i] rule i 0 --> 0.
[i] rule (S i) (S 0) --> S i.
[i, j] rule (S i) (S j) --> S (rule i j).
(; Types and terms ;)
Univ : s : Sort -> Type.
def Term : s : Sort -> a : Univ s -> Type.
univ : s : Sort -> Univ (S s).
def lift' : s1 : Sort -> s2 : Sort -> Univ s1 -> Univ s2.
def lift : s1 : Sort -> s2 : Sort -> cumul s1 s2 -> a : Univ s1 -> Univ s2.
[s1,s2] lift s1 s2 _ --> lift' s1 s2.
def prod : s1 : Sort -> s2 : Sort -> a : Univ s1 -> b : (Term s1 a -> Univ s2) -> Univ (rule s1 s2).
[s] Term (S s) (univ s) --> Univ s.
[s1, s2, a] Term s2 (lift' s1 s2 a) --> Term s1 a.
[s1, s2, a, b]
Term _ (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).
(; Canonicity rules ;)
[s, a] lift' s s a --> a.
[s1, s2, s3, a] lift' _ s3 (lift' s1 s2 a) --> lift' s1 s3 a.
[s1, s2, s3, a,b]
prod _ s2 (lift' s1 s3 a) b -->
lift' (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
[s1, s2, s3, a,b]
prod s1 _ a (x => lift' s2 s3 (b x)) -->
lift' (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
fmod LPM is
sort Nat .
Sort Cumul .
sort Term .
sort Type .
op z : -> Nat [ctor] .
op s : Nat -> Nat [ctor] .
op cumul : Nat Nat -> Type .
op rule : Nat Nat -> Nat .
op Univ : Nat -> Type .
op T : Nat Term -> Type .
op univ : Nat -> Term .
op prod : Nat Nat Term Term -> Term .
op liftp : Nat Nat Term Term -> Term .
op lift : Nat Nat Cumul Term Term -> Term .
op Pi : Type Type -> Type .
vars i j k l m x : Nat .
vars p q r t : Nat .
vars a b : Term .
eq max(i, z) = i .
eq max(z, i) = i .
--- eq max(s(i), s(j)) = s(m(i, j)) .
eq s(max(i, j)) = max(s(i), s(j)) .
eq rule(i, z) = z .
eq rule(z, j) = j .
eq rule(s(i), s(j)) = s(m(i, j)) .
eq max(i, i) = i .
eq rule(i, max(j, k)) = max(rule(i, j), rule(i, k)) .
eq rule(max(i, j), k) = max(rule(i, k), rule(j, k)) .
eq T(i, univ(j)) = Univ(j) .
--- eq Term(s, cast(s1, s2, univ(s), b, a) = Univ(s) .
(; Sorts ;)
Sort : Type.
0 : Sort.
S : Sort -> Sort.
(; Universe cumulativity ;)
True : Type.
I : True.
def cumul : Sort -> Sort -> Type.
[i ] cumul 0 i --> True.
[i,j] cumul (S i) (S j) --> cumul i j.
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort.
[i] rule i 0 --> 0.
[i] rule (S i) (S 0) --> S i.
[i, j] rule (S i) (S j) --> S (rule i j).
(; Types and terms ;)
Univ : s : Sort -> Type.
def Term : s : Sort -> a : Univ s -> Type.
univ : s : Sort -> Univ (S s).
def lift' : s1 : Sort -> s2 : Sort -> Univ s1 -> Univ s2.
def lift : s1 : Sort -> s2 : Sort -> cumul s1 s2 -> a : Univ s1 -> Univ s2.
[s1,s2] lift s1 s2 _ --> lift' s1 s2.
def prod : s1 : Sort -> s2 : Sort -> a : Univ s1 -> b : (Term s1 a -> Univ s2) -> Univ (rule s1 s2).
[s] Term _ (univ s) --> Univ s.
[s1, s2, a] Term _ (lift' s1 s2 a) --> Term s1 a.
[s1, s2, a, b]
Term _ (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).
(; Canonicity rules ;)
[s, a] lift' s s a --> a.
[s1, s2, s3, a] lift' _ s3 (lift' s1 s2 a) --> lift' s1 s3 a.
[s1, s2, s3, a,b]
prod _ s2 (lift' s1 s3 a) b -->
lift' (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
[s1, s2, s3, a,b]
prod s1 _ a (x => lift' s2 s3 (b x)) -->
lift' (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
endfm
load cic.maude
load /home/gferey/maude/MFE/src/mfe.maude
(select tool CRC .)
---(CRC help .)
(ccr LPM .)
---(show all critical pairs .)
\ No newline at end of file
A : Type.
a : A.
b : A.
def T : A -> Type.
def C : (x : A) -> T x -> Type.
[] C b _ --> A.
[] C a _ --> A.
(; This rule needs itself to type-check, since a must be in T b,
which is true if T b --> C b a --> A but not without any rule to define T ;)
[] T b --> C b a.
(; This rule needs itself to type-check, since a must be of type T a,
which is true if T a --> C a a --> A but not without any rule to define T ;)
[] T a --> C a a.
N : Type.
1 : N.
S : N -> N.
def 2 := S 1.
def 3 := S 2.
def 4 := S 3.
def 5 := S 4.
def 6 := S 5.
def 7 := S 6.
def 8 := S 7.
def 9 := S 8.
def 10:= S 9.
def 11:= S 10.
def 12:= S 11.
def nplus : N -> N -> N.
[x] nplus x 1 --> S x
[y] nplus 1 y --> S y
[x,y] nplus (S x) (S y) --> S (S (nplus x y)).
def ntimes : N -> N -> N.
[x] ntimes x 1 --> x
[y] ntimes 1 y --> y
[x,y] ntimes (S x) (S y) --> S (nplus x (nplus y (ntimes x y))).
def max : N -> N -> N.
[x ] max x 1 --> x.
[ y] max 1 y --> y.
[x,y] max (S x) (S y) --> S (max x y).
def min : N -> N -> N.
[x ] min x 1 --> 1.
[ y] min 1 y --> 1.
[x,y] min (S x) (S y) --> S (min x y).
B : Type.
T : B.
F : B.
def and : B -> B -> B.
[] and T T --> T
[] and T F --> F
[] and F T --> F
[] and F F --> F.
def or : B -> B -> B.
[] or T T --> T
[] or T F --> T
[] or F T --> T
[] or F F --> F.
def not : B -> B.
[] not T --> F
[] not F --> T.
def lt : N -> N -> B.
[x ] lt x 1 --> F
[ y] lt 1 (S y) --> T
[x,y] lt (S x) (S y) --> lt x y.
Z : Type.
pos : N -> Z.
neg : N -> Z.
0 : Z.
defac zplus [Z].
[x] zplus 0 x --> x
[x,y] zplus (pos x) (pos y) --> pos (nplus x y)
[x,y] zplus (neg x) (neg y) --> neg (nplus x y)
[ ] zplus (neg 1 ) (pos 1 ) --> 0
[x ] zplus (neg (S x)) (pos 1 ) --> neg x
[ y] zplus (neg 1 ) (pos (S y)) --> pos y
[x,y] zplus (neg (S x)) (pos (S y)) --> zplus (neg x) (pos y)
[x,y,z] zplus (zplus (pos x) (pos y) ) z --> zplus (pos (nplus x y) ) z
[x,y,z] zplus (zplus (neg x) (neg y) ) z --> zplus (neg (nplus x y) ) z
[ z] zplus (zplus (neg 1 ) (pos 1 )) z --> zplus z 0
[x ,z] zplus (zplus (neg (S x)) (pos 1 )) z --> zplus z (neg x)
[ y,z] zplus (zplus (neg 1 ) (pos (S y))) z --> zplus z (pos y)
[x,y,z] zplus (zplus (neg (S x)) (pos (S y))) z --> zplus z (zplus (neg x) (pos y)).
def ztimes : Z -> Z -> Z.
[ y] ztimes 0 y --> 0
[x ] ztimes x 0 --> 0
[x,y] ztimes (neg x) (neg y) --> pos (ntimes x y)
[x,y] ztimes (pos x) (pos y) --> pos (ntimes x y)
[x,y] ztimes (neg x) (pos y) --> neg (ntimes x y)
[x,y] ztimes (pos x) (neg y) --> neg (ntimes x y).
[a,x,y] ztimes (pos a) (zplus x y) --> zplus (ztimes (pos a) x) (ztimes (pos a) y).
[a,x,y] ztimes (zplus x y) (pos a) --> zplus (ztimes y (pos a)) (ztimes y (pos a)).
[a,x,y] ztimes (neg a) (zplus x y) --> zplus (ztimes (neg a) x) (ztimes (neg a) y).
[a,x,y] ztimes (zplus x y) (neg a) --> zplus (ztimes y (neg a)) (ztimes y (neg a)).
def var : Z -> Z.
[x] var (var x) --> var x
[x,y] var (zplus x y) --> zplus (var x) (var y)
[x,y] var (ztimes x y) --> ztimes (var x) (var y)
[x] var (pos x) --> pos x
[x] var (neg x) --> neg x.
[x,a] ztimes (var x) (pos a) --> ztimes (pos a) (var x).
[x,a] ztimes (var x) (neg a) --> ztimes (neg a) (var x).
[x,a,b] zplus (ztimes a (var x)) (ztimes b (var x))
--> ztimes (zplus a b) (var x).
[x,a,b,z] zplus (zplus (ztimes a (var x)) (ztimes b (var x))) z
--> zplus (ztimes (zplus a b) (var x)) z.
(; x,y |-> 2 + 3.x + y.2+ x.(-1) + (-3) ;)
def t1 :=
x : Z => y : Z => var (
zplus (pos 2)
(zplus (ztimes (pos 3) x )
(zplus (ztimes y (neg 2))
(zplus (ztimes x (neg 1))
(neg 3))))).
(; x,y |-> (-1) + 2.x + (-2).y ;)
def t2 :=
x : Z => y : Z => var (
zplus (neg 1)
(zplus (ztimes (pos 2) x)
(ztimes (neg 2) y))).
#CHECK t1 == t2.
#CHECK t1 (pos 3) == (y : Z => zplus (pos 5) (ztimes (neg 2) (var y))).
def abs : Z -> Z.
[ ] abs 0 --> 0
[x] abs (neg x) --> pos x
[x] abs (pos x) --> pos x.
def inv : Z -> Z.
[] inv 0 --> 0.
[x] inv (pos x) --> neg x.
[x] inv (neg x) --> pos x.
(; |x-y| ;)
def absdiff (x:Z) (y:Z) := abs (zplus (inv x) y).
def gcd : Z -> Z -> Z.
[x] gcd 0 x --> abs x.
[x] gcd x 0 --> abs x.
[x,y] gcd (neg x) y --> gcd (pos x) y.
[x,y] gcd x (neg y) --> gcd x (pos y).
[x,y] gcd (pos x) (pos y) --> gcd (abs (zplus (neg x) (pos y))) (pos (min x y)).