Commit 325ca643 authored by Gaspard FEREY's avatar Gaspard FEREY

Fixed cicup_v2. Started working on v3. Moved translation cic to AC in its own folder.

parent 522ffa72
......@@ -17,7 +17,7 @@ Sort : Type.
defac plus [Sort].
[i] plus i 0 --> i.
def max : Sort -> Sort -> Sort.
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
[i ] max i i --> i (; Derived from previous ;)
......@@ -80,13 +80,15 @@ def prod :
--> x: T i a -> T i (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).
--> x : T (plus (plus i j) 1) a -> T (plus j 1) (b x)
(; Derived from previous ;)
[j,a,b] T (plus j 1) (prod (plus j 1) (plus j 1) a b)
--> x : T (plus j 1) a -> T (plus j 1) (b x).
--> x : T (plus j 1) a -> T (plus j 1) (b x)
(; Derived from previous ;)
[i,a,b] T (plus i 1) (prod (plus i 1) 1 a b)
--> x : T (plus i 1) a -> T 1 (b x).
--> x : T (plus i 1) a -> T 1 (b x)
(; Derived from previous ;)
[a,b] T 1 (prod 1 1 a b) --> x : T 1 a -> T 1 (b x).
......@@ -99,6 +101,8 @@ def prod :
(; Derived from previous ;)
[i,a,b] prod (plus i 1) (plus i 1) (lift i a) b
--> prod i (plus i 1) a b
(; Derived from previous ;)
[a,b] prod 1 1 (lift 0 a) b --> prod 0 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)
......@@ -109,6 +113,8 @@ def prod :
(; Derived from previous ;)
[i,a,b] prod (plus i (plus 1 1)) 1 (lift (plus i 1) a) b
--> lift (plus i 1) (prod (plus i 1) 1 a b)
(; Derived from previous ;)
[a,b] prod (plus 1 1) 1 (lift 1 a) b --> lift 1 (prod 1 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))
......@@ -119,6 +125,9 @@ def prod :
(; Derived from previous ;)
[i,a,b] prod (plus i (plus 1 1)) (plus 1 1) a (x => lift 1 (b x))
--> prod (plus i (plus 1 1)) 1 a (x => b x)
(; Derived from previous ;)
[a,b] prod (plus 1 1) (plus 1 1) a (x => lift 1 (b x))
--> prod (plus 1 1) 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)] ;)
......
......@@ -20,7 +20,7 @@ fmod LPM is
op Pi : Type Type -> Type .
vars i j l m x : Nat .
vars i j k l m x : Nat .
vars a b : Term .
eq i + 0 = i .
......@@ -56,22 +56,32 @@ fmod LPM is
eq T(i + j + 1, prod(i + j + 1, j + 1, a, b)) = Pi(T(i + j + 1, a), T(j + 1, b)) .
eq T(j + 1 , prod(j + 1 , j + 1, a, b)) = Pi(T(j + 1, a) , T(j + 1, b)) .
eq T(i + 1 , prod(i + 1 , 1 , a, b)) = Pi(T(i + 1, a) , T(1 , b)) .
--- New equation
eq T( 1 , prod( 1 , 1 , a, b)) = Pi(T( 1, a) , T(1 , b)) .
eq prod(i + 1, i + j + 1, lift(i, a), b) = prod(i, i + j + 1, a, b) .
eq prod( 1, j + 1, lift(0, a), b) = prod(0, j + 1, a, b) .
eq prod(i + 1, i + 1, lift(i, a), b) = prod(i, i + 1, a, b) .
--- New equation
eq prod( 1, 1, lift(0, a), b) = prod(0, 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( j + 1 + 1, j + 1, lift( j + 1, a), b) = lift( j + 1, prod( j + 1, j + 1, a, b)) .
eq prod(i + 1 + 1, 1, lift(i + 1, a), b) = lift(i + 1, prod(i + 1, 1, a, b)) .
--- New equation
eq prod( 1 + 1, 1, lift( 1, a), b) = lift( 1, prod( 1, 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( j + 1 + 1, j + 1 + 1, a, lift(j + 1, b)) = prod( j + 1 + 1, j + 1, a, b) .
eq prod(i + 1 + 1, 1 + 1, a, lift( 1, b)) = prod(i + 1 + 1, 1, a, b) .
--- New equation
eq prod( 1 + 1, 1 + 1, a, lift( 1, b)) = prod( 1 + 1, 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, j + 1, a, lift( j, b)) = lift( j, prod(0, j, a, b)) .
eq prod(i, i + 1, a, lift(i , b)) = lift(i , prod(i, i , a, b)) .
--- New equation
eq prod(0, 1, a, lift(0 , b)) = lift(0 , prod(0, 0 , a, b)) .
eq prod(0, 1, a, lift(0, b)) = lift(0, prod(0, 0, a, b)) .
......
#NAME cc.
(; System derived from original.
This variant implements :
- Use of AC+ 0-elimination (instead of ACU)
- Added the i + (max j k) --> max (i+j) (i+k)
;)
(;-------------------------------;)
(; Arithmetic on universes sorts ;)
(;-------------------------------;)
Sort : Type.
0 : Sort.
1 : Sort.
defac plus [Sort].
[i] plus i 0 --> i.
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
[i ] max i i --> i (; Derived from previous ;)
[i ] max 0 i --> i (; Derived from previous ;)
[i ] max i 0 --> i. (; Derived from previous ;)
[i,j,k] plus i (max j k) --> max (plus i j) (plus i k).
def rule : Sort -> Sort -> Sort.
[i ] rule i 0 --> 0
[i,j] rule i (plus j 1) --> max i (plus j 1)
[i ] rule i 1 --> max i 1. (; Derived from previous ;)
[i,j] rule i (plus i j) --> plus i j
[j ] rule 0 j --> j (; Derived from previous ;)
[i ] rule i i --> i. (; Derived from previous ;)
(;-------------------------------;)
(; 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)
[ a] liftn 1 a --> lift 0 a. (; Derived from previous ;)
[i ] T (plus i 1) (u i) --> U i
[ ] T 1 (u 0) --> U 0 (; Derived from previous ;)
[i,a] T (plus i 1) (lift i a) --> T i a
[ a] T 1 (lift 0 a) --> T 0 a (; Derived from previous ;)
[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)
(; Derived from previous ;)
[j,a,b] T j (prod 0 j a b)
--> x: T 0 a -> T j (b x)
(; Derived from previous ;)
[i,a,b] T i (prod i i a b)
--> x: T i a -> T i (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)
(; Derived from previous ;)
[j,a,b] T (plus j 1) (prod (plus j 1) (plus j 1) a b)
--> x : T (plus j 1) a -> T (plus j 1) (b x)
(; Derived from previous ;)
[i,a,b] T (plus i 1) (prod (plus i 1) 1 a b)
--> x : T (plus i 1) a -> T 1 (b x)
(; Derived from previous ;)
[a,b] T 1 (prod 1 1 a b) --> x : T 1 a -> T 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
(; Derived from previous ;)
[j,a,b] prod 1 (plus j 1) (lift 0 a) b
--> prod 0 (plus j 1) a b
(; Derived from previous ;)
[i,a,b] prod (plus i 1) (plus i 1) (lift i a) b
--> prod i (plus i 1) a b
(; Derived from previous ;)
[a,b] prod 1 1 (lift 0 a) b --> prod 0 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)
(; Derived from previous ;)
[j,a,b] prod (plus j (plus 1 1)) (plus j 1) (lift (plus j 1) a) b
--> lift (plus j 1) (prod (plus j 1) (plus j 1) a b)
(; Derived from previous ;)
[i,a,b] prod (plus i (plus 1 1)) 1 (lift (plus i 1) a) b
--> lift (plus i 1) (prod (plus i 1) 1 a b)
(; Derived from previous ;)
[a,b] prod (plus 1 1) 1 (lift 1 a) b --> lift 1 (prod 1 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)
(; Derived from previous ;)
[j,a,b] prod (plus j (plus 1 1)) (plus j (plus 1 1)) a (x => lift (plus j 1) (b x))
--> prod (plus j (plus 1 1)) (plus j 1) a (x => b x)
(; Derived from previous ;)
[i,a,b] prod (plus i (plus 1 1)) (plus 1 1) a (x => lift 1 (b x))
--> prod (plus i (plus 1 1)) 1 a (x => b x)
(; Derived from previous ;)
[a,b] prod (plus 1 1) (plus 1 1) a (x => lift 1 (b x))
--> prod (plus 1 1) 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))
(; Derived from previous ;)
[j,a,b] prod 0 (plus j 1) a (x => lift j (b x))
--> lift j (prod 0 j a (x => b x))
(; Derived from previous ;)
[i,a,b] prod i (plus i 1) a (x => lift i (b x))
--> lift i (prod i i 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))
(; Derived from previous ;)
[a,b] prod 1 1 a (x => lift 0 (b x))
--> liftn 1 (prod 1 0 a (x => b x))
[i,a,b] prod (plus i 1) 0 (lift i a) b
--> prod i 0 a b
(; Derived from previous ;)
[a,b] prod 1 0 (lift 0 a) b
--> prod 0 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] .
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 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 i + 0 = i .
eq max(i, i + j) = i + j .
eq max(i + j, j) = i + j .
eq max(i, i) = i .
eq max(i, 0) = i .
eq max(0, i) = i .
eq rule(i, 0) = 0 .
eq rule(i, j + 1) = max(i, j + 1) .
eq rule(i, 1) = max(i, 1) .
eq rule(i, i + j) = i + j .
eq rule(0, j) = j .
eq rule(i, i) = i .
eq liftn(0, a) = a .
eq liftn(i + 1, a) = lift(i, liftn(i, a)) .
eq liftn(1 , a) = lift(0, a) .
eq T(i + 1, u(i)) = U(i) .
eq T(1 , u(0)) = U(0) .
eq T(i + 1, lift(i, a)) = T(i, a) .
eq T(1 , lift(0, a)) = T(0, 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(j , prod(0, j , a, b)) = Pi(T(0, a), T(j , b)) .
eq T(i , prod(i, i , a, b)) = Pi(T(i, a), T(i , 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 T(j + 1 , prod(j + 1 , j + 1, a, b)) = Pi(T(j + 1, a) , T(j + 1, b)) .
eq T(i + 1 , prod(i + 1 , 1 , a, b)) = Pi(T(i + 1, a) , T(1 , b)) .
--- New equation
eq T( 1 , prod( 1 , 1 , a, b)) = Pi(T( 1, a) , T(1 , b)) .
eq prod(i + 1, i + j + 1, lift(i, a), b) = prod(i, i + j + 1, a, b) .
eq prod( 1, j + 1, lift(0, a), b) = prod(0, j + 1, a, b) .
eq prod(i + 1, i + 1, lift(i, a), b) = prod(i, i + 1, a, b) .
--- New equation
eq prod( 1, 1, lift(0, a), b) = prod(0, 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( j + 1 + 1, j + 1, lift( j + 1, a), b) = lift( j + 1, prod( j + 1, j + 1, a, b)) .
eq prod(i + 1 + 1, 1, lift(i + 1, a), b) = lift(i + 1, prod(i + 1, 1, a, b)) .
--- New equation
eq prod( 1 + 1, 1, lift( 1, a), b) = lift( 1, prod( 1, 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( j + 1 + 1, j + 1 + 1, a, lift(j + 1, b)) = prod( j + 1 + 1, j + 1, a, b) .
eq prod(i + 1 + 1, 1 + 1, a, lift( 1, b)) = prod(i + 1 + 1, 1, a, b) .
--- New equation
eq prod( 1 + 1, 1 + 1, a, lift( 1, b)) = prod( 1 + 1, 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, j + 1, a, lift( j, b)) = lift( j, prod(0, j, a, b)) .
eq prod(i, i + 1, a, lift(i , b)) = lift(i , prod(i, i , a, b)) .
--- New equation
eq prod(0, 1, a, lift(0 , b)) = lift(0 , prod(0, 0 , a, b)) .
eq prod(0, 1, a, lift(0, b)) = lift(0, prod(0, 0, a, b)) .
eq prod(i + 1, 1, a, lift(0, b)) = liftn(i + 1, prod(i + 1, 0, a, b)) .
eq prod( 1, 1, a, lift(0, b)) = liftn( 1, prod( 1, 0, a, b)) .
eq prod(i + 1, 0, lift(i, a), b) = prod(i, 0, a, b) .
eq prod( 1, 0, lift(0, a), b) = prod(0, 0, a, b) .
eq i + max(j, k) = max(i + j, i + k) .
endfm
......@@ -2,10 +2,157 @@
(; System derived from original.
This variant implements :
- Use of AC+ 0-elimination (instead of ACU)
- Cumulativity compatible with Coq (Prop / Set are both Type_1)
- Use of ACU for max (not for plus)
;)
(;-------------------------------;)
(; Arithmetic on universes sorts ;)
(;-------------------------------;)
Sort : Type.
0 : Sort.
1 : Sort.
defacu max [Sort, 0].
[i,j] max i (plus i j) --> plus i j
def plus : Sort -> Sort -> Sort.
[i ] plus i 0 --> i
[i,j,k] plus i (max j k) --> max (plus i j) (plus i k)
[i,j,k] plus (max j k) i --> max (plus i j) (plus i k).
def rule : Sort -> Sort -> Sort.
[i ] rule i 0 --> 0
[i,j] rule i (plus j 1) --> max i (plus j 1)
[i ] rule i 1 --> max i 1. (; Derived from previous ;)
[i,j] rule i (plus i j) --> plus i j
[j ] rule 0 j --> j (; Derived from previous ;)
[i ] rule i i --> i. (; Derived from previous ;)
(;-------------------------------;)
(; 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)
[ a] liftn 1 a --> lift 0 a. (; Derived from previous ;)
[i ] T (plus i 1) (u i) --> U i
[ ] T 1 (u 0) --> U 0 (; Derived from previous ;)
[i,a] T (plus i 1) (lift i a) --> T i a
[ a] T 1 (lift 0 a) --> T 0 a (; Derived from previous ;)
[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)
(; Derived from previous ;)
[j,a,b] T j (prod 0 j a b)
--> x: T 0 a -> T j (b x)
(; Derived from previous ;)
[i,a,b] T i (prod i i a b)
--> x: T i a -> T i (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)
(; Derived from previous ;)
[j,a,b] T (plus j 1) (prod (plus j 1) (plus j 1) a b)
--> x : T (plus j 1) a -> T (plus j 1) (b x)
(; Derived from previous ;)
[i,a,b] T (plus i 1) (prod (plus i 1) 1 a b)
--> x : T (plus i 1) a -> T 1 (b x)
(; Derived from previous ;)
[a,b] T 1 (prod 1 1 a b) --> x : T 1 a -> T 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
(; Derived from previous ;)
[j,a,b] prod 1 (plus j 1) (lift 0 a) b
--> prod 0 (plus j 1) a b
(; Derived from previous ;)
[i,a,b] prod (plus i 1) (plus i 1) (lift i a) b
--> prod i (plus i 1) a b
(; Derived from previous ;)
[a,b] prod 1 1 (lift 0 a) b --> prod 0 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)
(; Derived from previous ;)
[j,a,b] prod (plus j (plus 1 1)) (plus j 1) (lift (plus j 1) a) b
--> lift (plus j 1) (prod (plus j 1) (plus j 1) a b)
(; Derived from previous ;)
[i,a,b] prod (plus i (plus 1 1)) 1 (lift (plus i 1) a) b
--> lift (plus i 1) (prod (plus i 1) 1 a b)
(; Derived from previous ;)
[a,b] prod (plus 1 1) 1 (lift 1 a) b --> lift 1 (prod 1 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)
(; Derived from previous ;)
[j,a,b] prod (plus j (plus 1 1)) (plus j (plus 1 1)) a (x => lift (plus j 1) (b x))
--> prod (plus j (plus 1 1)) (plus j 1) a (x => b x)
(; Derived from previous ;)
[i,a,b] prod (plus i (plus 1 1)) (plus 1 1) a (x => lift 1 (b x))
--> prod (plus i (plus 1 1)) 1 a (x => b x)
(; Derived from previous ;)
[a,b] prod (plus 1 1) (plus 1 1) a (x => lift 1 (b x))
--> prod (plus 1 1) 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))
(; Derived from previous ;)
[j,a,b] prod 0 (plus j 1) a (x => lift j (b x))
--> lift j (prod 0 j a (x => b x))
(; Derived from previous ;)
[i,a,b] prod i (plus i 1) a (x => lift i (b x))
--> lift i (prod i i 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))
(; Derived from previous ;)
[a,b] prod 1 1 a (x => lift 0 (b x))
--> liftn 1 (prod 1 0 a (x => b x))
[i,a,b] prod (plus i 1) 0 (lift i a) b
--> prod i 0 a b
(; Derived from previous ;)
[a,b] prod 1 0 (lift 0 a) b
--> prod 0 0 a b.
load cicup_v2.maude
load cicup_v22.maude
load /home/gaspi/maude/MFE/src/mfe.maude
(select tool CRC .)
(ccr LPM .)
#NAME cc.
(; Original system as designed by ASSAF, DOWEK, JOUANNAUD and LIU ;)
(;-------------------------------;)
(; 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 liftnk : i : Sort -> j : Sort -> a : U i -> U (plus i j).
def prod :
i : Sort ->
j : Sort ->
a : U i ->
b : (x : T i a -> U j) ->
U (rule i j).
(; Rewriting rules ;)
[i,a] liftnk i 0 a --> a
[i,j,a] liftnk i (plus j 1) a --> lift (plus i j) (liftnk i j a).
def liftn : i : Sort -> a : U 0 -> U i := liftnk 0.
[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.
......@@ -49,7 +49,7 @@ def univ : s : Sort -> Univ (succ s) := cc.u.
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (max s1 s2).
[i ,a] lift i i a --> a
[i,j,a] lift i (cc.plus i j) a --> cc.lnlift i j a
[i,j,a] lift i (cc.plus i j) a --> cc.liftnk i j a
[i,j,a] lift (cc.plus i j) i a --> a.
def prod : s1 : Sort ->
......
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