Commit 8d1ea65b authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Merge branch 'master' of https://git.lsv.fr/genestier/PleinDeDk

parents 5e6c33d3 e0805468
(; Original system as designed by ASSAF, DOWEK, JOUANNAUD and LIU.
(; plus_ACU, lift_1, confluent, max_err
Original system as designed by ASSAF, DOWEK, JOUANNAUD and LIU.
Maude joins all critical pairs.
Potential issues are:
- No implementation of lifting k levels from universe i.
Can only lift k levels from 0 or 1 level from universe i.
- 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.
;)
(;-------------------------------;)
......
#NAME cc.
(; plus_AC, lift_1, confluent, max_err
(; System derived from original.
System derived from original.
Maude joins all critical pairs.
......@@ -8,8 +8,8 @@ This variant implements :
- Use of AC+ 0-elimination (instead of ACU)
Potential issues are:
- No implementation of lifting k levels from universe i.
Can only lift k levels from 0 or 1 level from universe i.
- 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.
......
#NAME cc.
(; plus_AC, lift_1
(; System derived from original.
System derived from original.
Maude requires 23 critical pairs to be joined.
rule(i,k) <-> max(k,rule(i,k))
......@@ -12,9 +12,8 @@ This variant implements :
- Added the i + (max j k) --> max (i+j) (i+k)
Potential issues are:
- No implementation of lifting k levels from universe i.
Can only lift k levels from 0 or 1 level from universe i.
- No implementation of lifting k levels.
Can only iterate lifting 1 level.
;)
(;-------------------------------;)
......
#NAME cc.
(; max_ACU, lift_0
(; System derived from original.
System derived from original.
No Maude test performed.
......@@ -8,9 +8,8 @@ This variant implements :
- Use of ACU for max (not for plus)
Potential issues are:
- No implementation of lifting k levels from universe i.
Can only lift k levels from 0 or 1 level from universe i.
- No implementation of lifting k levels.
Can only iterate lifting 1 level.
;)
(;-------------------------------;)
......
#NAME cc.
(; max_AC, plus_AC, WIP ;)
Sort : Type.
......
#NAME cc.
(; max_AC, lift_0, WIP ;)
Sort : Type.
......
(; WIP, constraints ;)
(; Natural numbers ;)
N : Type.
......
(; This is not a CiC implementation : nocic ;)
def Cstr := cc.Cstr.
def s := cc.s.
def Sort := cc.N.
......
#NAME HOASDB.
(; WIP ;)
N : Type.
0 : N.
......
# All supported flags
FLAGS=max_AC plus_AC plus_ACU cast lift lift_1 max_err confluent WIP constraints varity
DKS=$(shell find ./ -type f -name '*.dk')
all:
@rm -f README.md
@echo "This project contains various implementations of cic.dk\n" >> README.md
@echo -n "| File |" >> README.md
@for fg in $(FLAGS) ; do echo -n " $$fg |" >> README.md ; done
@echo -n "\n" >> README.md
@echo -n "| --- |" >> README.md
@for fg in $(FLAGS) ; do echo -n " --- |" >> README.md ; done
@echo -n "\n" >> README.md
@for dk in $(DKS) ; do \
if [ -z $$(head -q -n 1 $$dk | grep "nocic") ]; then \
echo -n "| [$$dk]($$dk) |" >> README.md ; \
for fg in $(FLAGS) ; do \
if [ -z $$(head -q -n 1 $$dk | grep "[^a-zA-Z0-9]$$fg[^a-zA-Z0-9]") ]; then \
echo -n " |" >> README.md ; \
else \
echo -n " X |" >> README.md ; \
fi ; \
done ; \
echo -n "\n" >> README.md ; \
fi ; \
done
@cat post.txt >> README.md
This project contains various implementations of cic.dk
| File | max_AC | plus_AC | plus_ACU | cast | lift | lift_1 | max_err | confluent | WIP | constraints | varity |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| [./AC/1-original/cc.dk](./AC/1-original/cc.dk) | | | X | | X | X | | X | | | |
| [./AC/maxplusAC.dk](./AC/maxplusAC.dk) | X | X | | | | | | | X | | |
| [./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 | | | | | | |
| [./nolift/cc.dk](./nolift/cc.dk) | | | | X | | | | | X | | X |
| [./nolift/cic.dk](./nolift/cic.dk) | | | | X | | | | | X | | X |
| [./HOAS/HOAS_to_DBAC.dk](./HOAS/HOAS_to_DBAC.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 | | |
| [./old_to_ACU/cc.dk](./old_to_ACU/cc.dk) | | X | | | X | | | | | | |
| [./Constraints/cc.dk](./Constraints/cc.dk) | | | | | | | | | X | X | |
| [./AC_with_constraints/cic.dk](./AC_with_constraints/cic.dk) | X | | | | X | | | | X | | |
## Flags
* **max_AC**: `max` on universe levels is AC
* **plus_AC**: `plus` on universe levels is AC
* **plus_ACU**: `plus` on universe levels is ACU
* **cast**: `cast` term from subtype to supertype is implemented
* **lift**: `lift` type from any universe i to any higher universe j
* **lift_1**: `lift` type from any universe i to (i+1)
* **max_err**: `1 + max(i,j)` is not convertible with `max(1+i, 1+j)`
* **confluent**: Critical pair joinability has been checked using Maude.
* **WIP**: Implementation is still a work in progress (may not even dkcheck)
* **constraints**: Implementation is relying on Coq-like constraints mechanisms
* **varity**: Implementation requires Dedukti to accept rewrite rules of variable arity
#NAME idic.
(; This is not a CiC implementation : nocic ;)
def Top_3 := cc.1.
def Top_48 := cc.2.
......
(; cast, WIP, varity ;)
(; Natural numbers ;)
Nat : Type.
z : Nat.
s : Nat -> Nat.
def max : Nat -> Nat -> Nat.
[i] max i z --> i.
[j] max z (s j) --> s j.
[i,j] max (s i) (s j) --> s (max i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
set : Sort.
type : Nat -> Sort.
def axiom : Sort -> Sort.
[] axiom prop --> axiom set.
[] axiom set --> type (s z).
[i] axiom (type i) --> type (s i).
def rule : Sort -> Sort -> Sort.
[] rule _ prop --> prop.
[] rule prop set --> set.
[] rule set set --> set.
[i] rule set (type i) --> type i.
[i] rule (type i) set --> type i.
[i,j] rule (type i) (type j) --> type (max i j).
def sup : Sort -> Sort -> Sort.
[] sup prop prop --> prop.
[] sup set set --> set.
[] sup prop set --> type z. (; ;)
[] sup set prop --> type z.
[i] sup set (type i) --> type i.
[i] sup prop (type i) --> type i.
[i] sup (type i) set --> type i.
[i] sup (type i) prop --> type i.
[i,j] sup (type i) (type j) --> type (max i j).
(; Canonicity rules ;)
[s1] sup s1 s1 --> s1.
[s1,s2] axiom (sup s1 s2) --> sup (axiom s1) (axiom s2).
[s1,s2,s3] sup (sup s1 s2) s3 --> sup s1 (sup s2 s3).
[s1,s2,s3] rule s1 (sup s2 s3) --> sup (rule s1 s2) (rule s1 s3).
[s1,s2,s3] rule (sup s1 s2) s3 --> sup (rule s1 s3) (rule s2 s3).
(; Primitive ;)
U : Sort -> Type.
def T : s1 : Sort -> a : U s1 -> Type.
u : s : Sort -> U (axiom s).
def prod : s1 : Sort -> s2 : Sort -> a : U s1 -> (T s1 a -> U s2) -> U (rule s1 s2).
def join : s1 : Sort -> s2 : Sort -> U s1 -> U s2 -> U (sup s1 s2).
def cast : s1 : Sort -> s2 : Sort -> a : U s1 -> b : U s2 -> T s1 a -> T (sup s1 s2) (join s1 s2 a b).
(; Defining code interpretation: T ;)
[s] T _ (u s) --> U s.
[s,a] T _ (cast _ _ (u s) _ a) --> T s a.
[s1,s2,a,b] T _ (prod s1 s2 a b) --> x : T s1 a -> T s2 (b x).
(; Defining join ;)
[i] join _ _ i i --> i.
[s1,s2] join _ _ (u s1) (u s2) --> u (sup s1 s2).
[s1,s2,s3,a,b,c]
join _ _ (prod s1 s2 a b) (prod s1 s3 a c)
--> prod s1 (sup s2 s3) a (x : T s1 a => join s2 s3 (b x) (c x)).
(; Defining cast ;)
(;[s1 : Sort, s2 : Sort, s3 : Sort, s4 : Sort, a : U s1, b : U s3, m : T s1 a];)
(;cast {sup s1 s2} {sup s3 s4} (lift s1 s2 a) (lift s3 s4 b) m;)
(;--> cast s1 s3 a b m.;)
[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).
(; Canonicity rules ;)
[t,a] cast _ _ t t a --> a.
[s1,s2,s3,a]
cast (axiom (sup s1 s2)) (axiom s3) (u (sup s1 s2)) (u s3) (cast (axiom s1) (axiom s2) (u s1) (u s2) a)
--> cast (axiom s1) (axiom (sup s2 s3)) (u s1) (u (sup s2 s3)) a.
[s1,s2,s3,a,b]
prod _ s2 (cast _ _ (u s1) (u s3) a) (x => b x)
--> cast
(axiom (rule s1 s2))
(axiom (rule s3 s2))
(u (rule s1 s2))
(u (rule s3 s2))
(prod s1 s2 a (x => b x)).
[s1,s2,s3,a,b]
prod s1 _ a (x => cast _ _ (u s2) (u s3) (b x))
--> cast
(axiom (rule s1 s2))
(axiom (rule s1 s3))
(u (rule s1 s2))
(u (rule s1 s3))
(prod s1 s2 a (x => b x)).
(; Alias for universe casting: lift ;)
def lift : s1 : Sort -> s2 : Sort -> U s1 -> U (sup s1 s2).
[s1,s2,m] lift s1 s2 m --> cast (axiom s1) (axiom s2) (u s1) (u s2) m.
(; Aliases for readibility ;)
def 0 := z.
def 1 := s 0.
def 2 := s 1.
def 3 := s 2.
def 4 := s 3.
def 5 := s 4.
def s0 := type 0.
def s1 := type 1.
def s2 := type 2.
def s3 := type 3.
def s4 := type 4.
def s5 := type 5.
def u0 := u s0.
def u1 := u s1.
def u2 := u s2.
def u3 := u s3.
def u4 := u s4.
def u5 := u s5.
def _prop := u prop.
def _set := u set.
def U0 := U s0.
def U1 := U s1.
def U2 := U s2.
def U3 := U s3.
def U4 := U s4.
def U5 := U s5.
def Prop := U prop.
def Set := U set.
(; cast, WIP, varity ;)
(; Natural numbers ;)
Nat : Type.
z : Nat.
s : Nat -> Nat.
def max : Nat -> Nat -> Nat.
[i] max i z --> i.
[j] max z (s j) --> s j.
[i,j] max (s i) (s j) --> s (max i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
type : Nat -> Sort.
def succ : Sort -> Sort.
[] succ prop --> type z.
[i] succ (type i) --> type (s i).
def rule : Sort -> Sort -> Sort.
[] rule _ prop --> prop.
[i] rule prop (type i) --> type i.
[i,j] rule (type i) (type j) --> type (max i j).
def sup : Sort -> Sort -> Sort.
[] sup prop prop --> prop.
[i] sup prop (type i) --> type i.
[i] sup (type i) prop --> type i.
[i,j] sup (type i) (type j) --> type (max i j).
(; Canonicity rules ;)
[s1] sup s1 s1 --> s1.
[s1,s2] succ (sup s1 s2) --> sup (succ s1) (succ s2).
[s1,s2,s3] sup (sup s1 s2) s3 --> sup s1 (sup s2 s3).
[s1,s2,s3] rule s1 (sup s2 s3) --> sup (rule s1 s2) (rule s1 s3).
[s1,s2,s3] rule (sup s1 s2) s3 --> sup (rule s1 s3) (rule s2 s3).
(; Primitive ;)
U : Sort -> Type.
def T : s1 : Sort -> a : U s1 -> Type.
u : s : Sort -> U (succ s).
def prod : s1 : Sort -> s2 : Sort -> a : U s1 -> (T s1 a -> U s2) -> U (rule s1 s2).
def join : s1 : Sort -> s2 : Sort -> U s1 -> U s2 -> U (sup s1 s2).
def cast : s1 : Sort -> s2 : Sort -> a : U s1 -> b : U s2 -> T s1 a -> T (sup s1 s2) (join s1 s2 a b).
(; Defining code interpretation: T ;)
[s] T _ (u s) --> U s.
[s,a] T _ (cast _ _ (u s) _ a) --> T s a.
[s1,s2,a,b] T _ (prod s1 s2 a b) --> x : T s1 a -> T s2 (b x).
(; Defining join ;)
[i] join _ _ i i --> i.
[s1,s2] join _ _ (u s1) (u s2) --> u (sup s1 s2).
[s1,s2,s3,a,b,c]
join _ _ (prod s1 s2 a b) (prod s1 s3 a c)
--> prod s1 (sup s2 s3) a (x : T s1 a => join s2 s3 (b x) (c x)).
(; Defining cast ;)
(;[s1 : Sort, s2 : Sort, s3 : Sort, s4 : Sort, a : U s1, b : U s3, m : T s1 a];)
(;cast {sup s1 s2} {sup s3 s4} (lift s1 s2 a) (lift s3 s4 b) m;)
(;--> cast s1 s3 a b m.;)
[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).
(; Canonicity rules ;)
[t,a] cast _ _ t t a --> a.
[s1,s2,s3,a]
cast (succ (sup s1 s2)) (succ s3) (u (sup s1 s2)) (u s3) (cast (succ s1) (succ s2) (u s1) (u s2) a)
--> cast (succ s1) (succ (sup s2 s3)) (u s1) (u (sup s2 s3)) a.
[s1,s2,s3,a,b]
prod _ s2 (cast _ _ (u s1) (u s3) a) (x => b x)
--> cast
(succ (rule s1 s2))
(succ (rule s3 s2))
(u (rule s1 s2))
(u (rule s3 s2))
(prod s1 s2 a (x => b x)).
[s1,s2,s3,a,b]
prod s1 _ a (x => cast _ _ (u s2) (u s3) (b x))
--> cast
(succ (rule s1 s2))
(succ (rule s1 s3))
(u (rule s1 s2))
(u (rule s1 s3))
(prod s1 s2 a (x => b x)).
(; Alias for universe casting: lift ;)
def lift : s1 : Sort -> s2 : Sort -> U s1 -> U (sup s1 s2).
[s1,s2,m] lift s1 s2 m --> cast (succ s1) (succ s2) (u s1) (u s2) m.
#NAME cc.
(; plus_AC, lift_1
(; System derived from original.
System derived from original.
This variant implements :
- Use of AC+ 0-elimination (instead of ACU)
;)
......
(; This is not a CiC implementation : nocic ;)
def Nat : Type := cc.Sort.
def z : Nat := cc.0.
def s : Nat -> Nat := x => cc.plus cc.1 x.
def m : Nat -> Nat -> Nat := cc.max.
(; Sorts ;)
def Sort : Type := cc.Sort.
def prop : Sort := cc.0.
def type : Nat -> Sort := s.
def succ : Sort -> Sort := s.
def next : Sort -> Sort := s.
def rule : Sort -> Sort -> Sort := cc.rule.
def max : Sort -> Sort -> Sort := cc.max.
(; Types and terms ;)
def Univ : s : Sort -> Type := cc.U.
def Term : s : Sort -> a : Univ s -> Type := cc.T.
def univ : s : Sort -> Univ (succ s) := cc.u.
def prod : s1 : Sort ->
s2 : Sort ->
a : Univ s1 ->
b : (Term s1 a -> Univ s2) ->
Univ (rule s1 s2) := cc.prod.
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (cc.max s1 s2).
[i,j,a] lift (cc.plus i j) i a --> a.
[i,j,a] lift i (cc.plus i j) a --> cc.liftnk i j a.
#NAME cic.
(; This is not a CiC implementation : nocic ;)
def Nat : Type := cc.Sort.
......@@ -8,9 +8,9 @@ def s : Nat -> Nat := x => cc.plus cc.1 x.
def m : Nat -> Nat -> Nat := cc.max.
#CONV i : Nat => m i z , i : Nat => i.
#CONV j : Nat => m z j , j : Nat => j.
#CONV i : Nat => j : Nat => m (s i) (s j) , i : Nat => j : Nat => s (m i j).
#CHECK (i : Nat => m i z ) == (i : Nat => i).
#CHECK (j : Nat => m z j ) == (j : Nat => j).
#CHECK (i : Nat => j : Nat => m (s i) (s j) ) == (i : Nat => j : Nat => s (m i j)).
(; Sorts ;)
......@@ -21,24 +21,24 @@ def type : Nat -> Sort := s.
(; Universe successors ;)
def succ : Sort -> Sort := s.
#CONV succ prop, type z.
#CONV i : Nat => succ (type i), i : Nat => type (s i).
#CHECK succ prop == type z.
#CHECK (i : Nat => succ (type i)) == i : Nat => type (s i).
(; Universe cumulativity ;)
def next : Sort -> Sort := s.
#CONV next prop, type z.
#CONV i : Nat => next (type i), i : Nat => type (s i).
#CHECK next prop == type z.
#CHECK (i : Nat => next (type i) ) == i : Nat => type (s i).
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort := cc.rule.
#CONV s1 : Sort => rule s1 prop, s1 : Sort => prop.
#CONV s2 : Sort => rule prop s2, s2 : Sort => s2.
#CONV i : Nat => j : Nat => rule (type i) (type j), i : Nat => j : Nat => type (m i j).
#CHECK (s1 : Sort => rule s1 prop) == s1 : Sort => prop.
#CHECK (s2 : Sort => rule prop s2) == s2 : Sort => s2.
#CHECK (i : Nat => j : Nat => rule (type i) (type j)) == i : Nat => j : Nat => type (m i j).
def max : Sort -> Sort -> Sort := cc.max.
#CONV s1 : Sort => max s1 prop, s1 : Sort => s1.
#CONV s2 : Sort => max prop s2, s2 : Sort => s2.
#CONV i : Nat => j : Nat => max (type i) (type j), i : Nat => j : Nat => type (m i j).
#CHECK (s1 : Sort => max s1 prop ) == s1 : Sort => s1.
#CHECK (s2 : Sort => max prop s2 ) == s2 : Sort => s2.
#CHECK (i : Nat => j : Nat => max (type i) (type j) ) == i : Nat => j : Nat => type (m i j).
(; Types and terms ;)
......@@ -50,7 +50,9 @@ def univ : s : Sort -> Univ (succ s) := cc.u.
def plus : Sort -> Sort -> Sort := cc.plus.
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (cc.plus s1 s2) := cc.liftnk.
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (cc.max s1 s2).
[i,j,a] lift (cc.plus i j) i a --> a.
[i,j,a] lift i (cc.plus i j) a --> cc.liftnk i j a.
def prod : s1 : Sort ->
s2 : Sort ->
......@@ -58,38 +60,42 @@ def prod : s1 : Sort ->
b : (Term s1 a -> Univ s2) ->
Univ (rule s1 s2) := cc.prod.
#CONV s : Sort => Term (succ s) (univ s), s : Sort => Univ s.
#SNF s1 : Sort => s2 : Sort => a : Univ s1 => Term (plus s1 s2) (lift s1 s2 a).
#SNF s1 : Sort => s2 : Sort => a : Univ s1 => Term s1 a.
#CONV s1 : Sort => s2 : Sort => a : Univ s1 => Term (plus s1 s2) (lift s1 s2 a),
s1 : Sort => s2 : Sort => a : Univ s1 => Term s1 a.
#CHECK (s : Sort => Term (succ s) (univ s) ) == s : Sort => Univ s.
#CONV s1 : Sort => s2 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) =>
Term (rule s1 s2) (prod s1 s2 a b),
s1 : Sort => s2 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) =>
x : Term s1 a -> Term s2 (b x).
#EVAL[SNF] s1 : Sort => s2 : Sort => a : Univ s1 => Term (max s1 s2) (lift s1 s2 a).
#EVAL[SNF] s1 : Sort => s2 : Sort => a : Univ s1 => Term s1 a.
#CHECK (s1 : Sort => s2 : Sort => a : Univ s1 => Term (max s1 s2) (lift s1 s2 a))
== s1 : Sort => s2 : Sort => a : Univ s1 => Term s1 a.
#CHECK ( s1 : Sort => s2 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) =>
Term (rule s1 s2) (prod s1 s2 a b) )
== s1 : Sort => s2 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) =>
x : Term s1 a -> Term s2 (b x).
(; Canonicity rules ;)
#CONV s : Sort => max s s, s : Sort => s.
#CONV s1 : Sort => s2 : Sort => s3 : Sort => max (max s1 s2) s3,
s1 : Sort => s2 : Sort => s3 : Sort => max s1 (max s2 s3).
#CHECK (s : Sort => max s s ) == s : Sort => s.
#CHECK (s1 : Sort => s2 : Sort => s3 : Sort => max (max s1 s2) s3)
== s1 : Sort => s2 : Sort => s3 : Sort => max s1 (max s2 s3).
#CONV s1 : Sort => s2 : Sort => s3 : Sort => rule (max s1 s3) s2,
s1 : Sort => s2 : Sort => s3 : Sort => max (rule s1 s2) (rule s3 s2).
#CONV s1 : Sort => s2 : Sort => s3 : Sort => rule s1 (max s2 s3),
s1 : Sort => s2 : Sort => s3 : Sort => max (rule s1 s2) (rule s1 s3).
#CHECK (s1 : Sort => s2 : Sort => s3 : Sort => rule (max s1 s3) s2)
== s1 : Sort => s2 : Sort => s3 : Sort => max (rule s1 s2) (rule s3 s2).
#CHECK (s1 : Sort => s2 : Sort => s3 : Sort => rule s1 (max s2 s3))
== s1 : Sort => s2 : Sort => s3 : Sort => max (rule s1 s2) (rule s1 s3).
#CONV s : Sort => a : Univ s => lift s s a,
s : Sort => a : Univ s => a.
#CONV s1 : Sort => s2 : Sort => s3 : Sort => a : Univ s1 => lift (max s1 s2) s3 (lift s1 s2 a),
s1 : Sort => s2 : Sort => s3 : Sort => a : Univ s1 => lift s1 (max s2 s3) a.
#CHECK (s : Sort => a : Univ s => lift s s a)
== s : Sort => a : Univ s => a.
#CHECK (s1 : Sort => s2 : Sort => s3 : Sort => a : Univ s1 =>
lift (max s1 s2) s3 (lift s1 s2 a))
== s1 : Sort => s2 : Sort => s3 : Sort => a : Univ s1 => lift s1 (max s2 s3) a.
#CONV s1 : Sort=> s2 : Sort => s3 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) => prod (max s1 s3) s2 (lift s1 s3 a) b,
s1 : Sort=> s2 : Sort => s3 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) => lift (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
#CHECK (s1 : Sort=> s2 : Sort => s3 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) =>
prod (max s1 s3) s2 (lift s1 s3 a) b)
== s1 : Sort=> s2 : Sort => s3 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) => lift (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
#CONV s1 : Sort => s2 : Sort => s3 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) => prod s1 _ a (x => lift s2 s3 (b x)),
s1 : Sort => s2 : Sort => s3 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) => lift (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
#CHECK (s1 : Sort => s2 : Sort => s3 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) =>
prod s1 _ a (x => lift s2 s3 (b x)))
== s1 : Sort => s2 : Sort => s3 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) => lift (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
#NAME cic.
(; lift ;)
(; Natural numbers ;)
......
#NAME Coq.
(; cast, lift ;)
(; Natural numbers ;)
......
#NAME cic.
(; max_AC, lift, WIP ;)
(; Natural numbers ;)
......
## Flags
* **max_AC**: `max` on universe levels is AC
* **plus_AC**: `plus` on universe levels is AC
* **plus_ACU**: `plus` on universe levels is ACU
* **cast**: `cast` term from subtype to supertype is implemented
* **lift**: `lift` type from any universe i to any higher universe j
* **lift_1**: `lift` type from any universe i to (i+1)
* **max_err**: `1 + max(i,j)` is not convertible with `max(1+i, 1+j)`
* **confluent**: Critical pair joinability has been checked using Maude.
* **WIP**: Implementation is still a work in progress (may not even dkcheck)
* **constraints**: Implementation is relying on Coq-like constraints mechanisms
* **varity**: Implementation requires Dedukti to accept rewrite rules of variable arity
Nat : Type.
0 : Nat.
S : Nat -> Nat.
def plus : Nat -> Nat -> Nat.
[y] plus 0 y --> y.
[x,y] plus (S x) y --> S (plus x y).
def mult : Nat -> Nat -> Nat.
[] mult 0 _ --> 0.
[x,y] mult (S x) y --> plus (mult x y) y.
def g : Nat -> Nat.
def f : Nat -> Nat -> Nat.
[x] f x x --> g x.
[x,y] g (plus (S x) (S y)) --> f (plus (S x) (S y)) (mult (S x) y).
#EVAL g (plus (S (S (S 0))) (S (S (S 0)))).
\ No newline at end of file
Nat : Type.
A : Type.
List : Nat -> Type.
Bool : Type.
0 : Nat.
S : Nat -> Nat.
True : Bool.
False : Bool.
Nil : List 0.
Cons : (n: Nat) -> A -> List n -> List (S n).
def ifthensucc : Bool -> Nat -> Nat.
[n] ifthensucc True n --> S n.
[n] ifthensucc False n --> n.
def compute_length : (A -> Bool) -> (n: Nat) -> List n -> Nat.
def aux_length : Bool -> (A -> Bool) -> (n: Nat) -> List n -> Nat.
[f,n,x,l] compute_length f _ (Cons n x l) --> aux_length (f x) f n l.
[f,n,l] aux_length True f n l --> S (compute_length f n l).
[f,n,l] aux_length False f n l --> compute_length f n l.
def filter : f: (A -> Bool) -> (n: Nat) -> l: List n -> List (compute_length f n l).
def bis : b: Bool -> f: (A -> Bool) -> x: A -> (n: Nat) -> l: List n -> List (aux_length b f n l).
[f,n,x,l] filter f _ (Cons n x l) --> bis (f x) f x n l.
[f,n,x,l] bis True f x n l --> Cons (compute_length f n l) x (filter f n l).
[f,x,n,l] bis False f x n l --> filter f n l.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment