Commit 2bfe295f authored by Francois THIRE's avatar Francois THIRE

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

parents d375dc19 5732b598
#NAME cc.
(; Original system as designed by ASSAF, DOWEK, JOUANNAUD and LIU ;)
(; 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 (where k *closed* Sort) from 0 or 1 level from 0.
- 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 ;)
......
......@@ -5,7 +5,7 @@ fmod LPM is
op 0 : -> Nat [ctor] .
op 1 : -> Nat [ctor] .
op _+_ : Nat Nat -> Nat [comm assoc id: 0 ctor] .
op _+_ : Nat Nat -> Nat [comm assoc id: 0] .
op max : Nat Nat -> Nat .
op rule : Nat Nat -> Nat .
......@@ -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 .
......@@ -31,7 +31,6 @@ fmod LPM is
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)) .
......
#NAME cc.
(; System derived from original.
Maude joins all critical pairs.
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 (where k *closed* Sort) from 0 or 1 level from 0.
- 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.
(; System derived from original.
Maude requires 23 critical pairs to be joined.
rule(i,k) <-> max(k,rule(i,k))
j + max(a,b) <-> max(b,j + max(a,b))
...
This variant implements :
- Use of AC+ 0-elimination (instead of ACU)
- 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 (where k *closed* Sort) from 0 or 1 level from 0.
;)
(;-------------------------------;)
......
......@@ -5,8 +5,8 @@ fmod LPM is
op 0 : -> Nat [ctor] .
op 1 : -> Nat [ctor] .
op _+_ : Nat Nat -> Nat [comm assoc] .
op max : Nat Nat -> Nat .
op _+_ : Nat Nat -> Nat [comm assoc ctor] .
op max : Nat Nat -> Nat [comm assoc] .
op rule : Nat Nat -> Nat .
op U : Nat -> Type .
......@@ -19,16 +19,12 @@ fmod LPM is
op Pi : Type Type -> Type .
vars i j k l m x : Nat .
vars j k l m x : Nat .
vars i : 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) .
......@@ -36,7 +32,12 @@ fmod LPM is
eq rule(i, i + j) = i + j .
eq rule(0, j) = j .
eq rule(i, i) = i .
eq rule(max(i,j), k) = max(rule(i,k), rule(j, k)) .
eq rule(i, max(j,k)) = max(rule(i,j), rule(i, k)) .
eq max(i, i + j) = i + j .
eq max(i, i) = i .
eq max(i, 0) = i .
eq liftn(0, a) = a .
eq liftn(i + 1, a) = lift(i, liftn(i, a)) .
......@@ -90,6 +91,4 @@ fmod LPM is
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
#NAME cc.
(; System derived from original.
No Maude test performed.
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 (where k *closed* Sort) from 0 or 1 level from 0.
;)
(;-------------------------------;)
......
load cicup_v22.maude
load cicup_0elim_maxplus.maude
load /home/gaspi/maude/MFE/src/mfe.maude
(select tool CRC .)
(ccr LPM .)
Set Printing Universes.
Definition id {A : Type} (a : A) := a.
About id.
Definition id {A : Type} (a : A) := a.
Polymorphic Definition pid {A : Type} (a : A) := a.
About pid.
Definition pid_id := pid (@id).
Definition pid_id_expl := @pid (forall A:Type,A->A) (@id).
Definition aux := @pid (forall A:Type,A->A) (@id).
Definition pid_pid := pid (@pid).
Definition pid_pid_expl := @pid (forall A:Type,A->A) (@pid). (* identical *)
Print aux.
Polymorphic Definition p_pid_id := pid (@id).
Polymorphic Definition p_pid_id_expl := @pid (forall A:Type,A->A) (@id).
Polymorphic Definition paux := @pid (forall A:Type,A->A) (@id).
Polymorphic Definition p_pid_pid := pid (@pid).
Polymorphic Definition p_pid_pid_expl := @pid (forall A:Type,A->A) (@pid).
Print paux.
Polymorphic Definition paux2 := pid (@id).
Universe i j.
Print paux2.
Definition aux : forall A : Type@{i}, A -> A :=
p_pid_pid.
Print Universes.
Print Sorted Universes.
Print Universes.
\ No newline at end of file
#NAME cc.
(; Original system as designed by ASSAF, DOWEK, JOUANNAUD and LIU ;)
(; System derived from original.
This variant implements :
- Use of AC+ 0-elimination (instead of ACU)
;)
(;-------------------------------;)
(; Arithmetic on universes sorts ;)
(;-------------------------------;)
Sort : Type.
0 : Sort.
1 : Sort.
defacu plus [Sort, 0].
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,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 0 --> 0
[i,j] rule i (plus j 1) --> max i (plus j 1)
[i ] rule i 1 --> max i 1. (; Derived from previous ;)
(; 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.
[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 ;)
(;-------------------------------;)
......@@ -37,7 +48,6 @@ 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 ->
......@@ -48,46 +58,105 @@ def prod :
(; 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 liftnk : i : Sort -> j : Sort -> a : U i -> U (plus i j).
def liftn : i : Sort -> a : U 0 -> U i := liftnk 0.
[i] T (plus i 1) (u i) --> U i
[i, a] liftnk i 0 a --> a
[i,j,a] liftnk i (plus j 1) a --> lift (plus i j) (liftnk i j a)
[i, a] liftnk i 1 a --> lift i 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).
--> 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.
--> prod i 0 a b
(; Derived from previous ;)
[a,b] prod 1 0 (lift 0 a) b
--> prod 0 0 a b.
......@@ -47,10 +47,10 @@ def Term : s : Sort -> a : Univ s -> Type := cc.T.
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.liftnk i j a
[i,j,a] lift (cc.plus i j) i a --> a.
def plus : Sort -> Sort -> Sort := cc.plus.
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (cc.plus s1 s2) := cc.liftnk.
def prod : s1 : Sort ->
s2 : Sort ->
......@@ -59,8 +59,12 @@ def prod : s1 : Sort ->
Univ (rule s1 s2) := cc.prod.
#CONV s : Sort => Term (succ s) (univ s), s : Sort => Univ s.
#CONV s1 : Sort => s2 : Sort => a : Univ s1 => Term (max s1 s2) (lift s1 s2 a),
#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.
#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) =>
......@@ -81,7 +85,11 @@ def prod : s1 : Sort ->
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.
#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).
#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)).
#NAME cic.
(; Natural numbers ;)
Nat : Type.
z : Nat.
......@@ -55,10 +57,13 @@ def prod : s1 : Sort -> s2 : Sort -> a : Univ s1 -> b : (Term s1 a -> Univ s2) -
(; Canonicity rules ;)
[s : Sort] max s s --> s.
[s1 : Sort, s2 : Sort, s3 : Sort] max (max s1 s2) s3 --> max s1 (max s2 s3).
[s1 : Sort, s2 : Sort, s3 : Sort] rule (max s1 s3) s2 --> max (rule s1 s2) (rule s3 s2).
[s1 : Sort, s2 : Sort, s3 : Sort] rule s1 (max s2 s3) --> max (rule s1 s2) (rule s1 s3).
[s : Sort, a : Univ s] lift s s a --> a.
[s1 : Sort, s2 : Sort, s3 : Sort, a : Univ s1]
lift _ s3 (lift s1 s2 a) -->
......
#NAME cic.
(; Natural numbers ;)
Nat : Type.
z : Nat.
s : Nat -> Nat.
defac m [Nat].
[i ] m i z --> i.
[i,j] m (s i) (s j) --> s (m i j).
[i,j,k] m (m (s i) (s j)) k --> m (s (m i j)) k.
(; 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.
[s] rule s prop --> prop.
[s] rule prop s --> s.
[i,j] rule (type i) (type j) --> type (m i j).
defac max [Sort].
[s] max s prop --> s.
[s] max prop s --> s.
[i,j] max (type i) (type j) --> type (m i j).
(; Types and terms ;)
Univ : s : Sort -> Type.
def Term : s : Sort -> a : Univ s -> Type.
univ : s : Sort -> Univ (succ 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).
(; Canonicity rules ;)
[s : Sort] max s s --> s.
[s1 : Sort, s2 : Sort, s3 : Sort] rule (max s1 s3) s2 --> max (rule s1 s2) (rule s3 s2).
[s1 : Sort, s2 : Sort, s3 : Sort] rule s1 (max s2 s3) --> max (rule s1 s2) (rule s1 s3).
[s : Sort, a : Univ s] lift s s a --> a.
[s1 : Sort, s2 : Sort, s3 : Sort, a : Univ s1]
lift _ s3 (lift s1 s2 a) -->
lift s1 (max s2 s3) a.
[s1 : Sort, s2 : Sort, s3 : Sort, a : Univ s1, b : Term s1 a -> Univ s2]
prod _ s2 (lift s1 s3 a) b -->
lift (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
[s1 : Sort, s2 : Sort, s3 : Sort, a : Univ s1, b : Term s1 a -> Univ s2]
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 Term .
sort Type .
op z : -> Nat [ctor] .
op s : Nat -> Nat [ctor] .
--- op m : Nat Nat -> Nat .
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 . --- useless
eq m(i, i) = i .
eq m(s(i),s(j)) = s(m(i, j)) .
--- eq m(s(z),s(j)) = s(j) .
--- eq m(s(i),s(z)) = s(i) .
--- eq m( m(s(i), s(j)), k) = m( s(m(i,j)), k) .
)
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 Term(s(s(q)), lift(s(q),s(z),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
fmod LPM is
sort Nat .
sort Term .
sort Type .
op z : -> Nat [ctor] .
op _+_ : Nat Nat -> Nat .
op 1 : -> 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 lift : Nat Nat Term -> Term .
op prod : 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 m(i, z) = i .
eq m(z, i) = i . --- useless
eq m(i, i) = i .
eq 1 + m(i,j) = m(1 + i, 1 + j) .
--- eq m(s(z),s(j)) = s(j) .
--- eq m(s(i),s(z)) = s(i) .
--- eq m( m(s(i), s(j)), k) = m( s(m(i,j)), k) .
eq m(r,rule(p,r)) = rule(p,r) .
eq m(i, i + j) = i + j .
eq i + (j + k) = (i + j) + k .
eq i + z = i .
eq rule(p, z) = z .
eq rule(i, 1 + j) = m(i, 1 + 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, lift(q,r,a)) = Term(q, a) .
eq Term(p, prod(q,r,a,b)) = Pi(Term(q,a),Term(r,b)) .
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(p,p,a) = a .
eq lift(p,q,lift(r,t,a)) = lift(r,m(q,t),a) .
***(
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 prod(p,q,lift(r,t,a),b) = lift(rule(r,q),rule(t,q),prod(r,q,a,b)) .
eq prod(p,q,a,lift(r,t,b)) = lift(rule(p,r),rule(p,t),prod(p,r,a,b)) .
--- eq lift(r, m(r,t), a) = lift(r,t,a) .
endfm
fmod LPM is
sort Nat .
sort Term .
sort Type .
op z : -> Nat [ctor] .
op s : Nat -> Nat [ctor] .
--- op m : Nat Nat -> Nat .
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 . --- useless
eq m(i, i) = i .
eq m(s(i),s(j)) = s(m(i, j)) .
--- eq m(s(z),s(j)) = s(j) .
--- eq m(s(i),s(z)) = s(i) .
--- eq m( m(s(i), s(j)), k) = m( s(m(i,j)), k) .
)
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 Term(s(s(q)), lift(s(q),s(z),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
load cic_v2.maude
load /home/gaspi/maude/MFE/src/mfe.maude
(select tool CRC .)
(CRC help .)
(ccr LPM .)
---(show all critical pairs .)
\ No newline at end of file
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