Commit 26237587 authored by Gaspard FEREY's avatar Gaspard FEREY

Reorganized CiC implementations. Added the proposition from the paper from Gilles, JP et alii.

parent 0c531557
#NAME cc.
(;-------------------------------;)
(; 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).
(;-------------------------------;)
(; 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 llift : 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] llift 0 a --> a
[i,a] llift (plus i 1) a --> lift i (llift 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 (llift 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)
(; Fails here, [i+j] is not 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))
--> llift (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.
......@@ -9,7 +9,6 @@ defac plus [Sort].
[i] plus i 0 --> i.
defac max [Sort].
[i,j,k] max (plus i k) (plus i j) --> plus i (max j k)
[i,j ] max i (plus i j) --> plus i j
[i,j ] max (plus i j) i --> plus i j
[i ] max i i --> i
......@@ -17,12 +16,13 @@ defac max [Sort].
def rule : Sort -> Sort -> Sort.
[i ] rule i 0 --> 0
[j ] rule 0 j --> j
[i ] rule i i --> i
[i,j] rule i (plus 1 j) --> max i (plus 1 j)
[i ] rule i 1 --> max i 1
[i,j] rule i (plus i j) --> plus i j
[i,j] rule (plus 1 i) j --> max (plus 1 i) j.
[j ] rule 0 j --> j
[i ] rule i i --> i.
[i,j,k] max (rule i j) (rule i k) --> rule i (max j k).
[i,j,k] max (rule j i) (rule k i) --> rule (max j k) i.
......
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