Added a bunch of CoqModels, some models to study and two files about arithmetic.

CoqModels/AC/2-test/cc.dk

+(; 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.

CoqModels/AC/2-test/cc.maude

+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

CoqModels/AC/2-test/commands.maude

+load cc.maude
+load /home/gferey/maude/MFE/src/mfe.maude
+(select tool CRC .)
+(ccr LPM .)

CoqModels/Constraints/constrained_interp/cic.dk

+(; 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)).

CoqModels/Constraints/constrained_interp_poly/cic.dk

+(; 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)).

CoqModels/Constraints/cc.dk → CoqModels/Constraints/constrained_types/cic.dk

 (; WIP, constraints ;)
 
+(;  Code types depend on a universe and associated constraints  ;)
+
 (; Natural numbers ;)
 
 N : Type.

CoqModels/README.md

@@ -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

CoqModels/experimenting/liftk/Makefile

+#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

CoqModels/experimenting/liftk/cic.dk

+
+(;-------------------------------;)
+(;  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)).

CoqModels/experimenting/liftk/univ/orig/univ.dk

+(; 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).

CoqModels/experimenting/liftkplus/Makefile

+#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 ./
+

CoqModels/experimenting/liftkplus/cic.dk

+
+(;-------------------------------;)
+(;  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).
+

CoqModels/experimenting/liftkplus/cic.maude

+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

CoqModels/experimenting/liftkplus/commands.maude

+load cic.maude
+load /home/gferey/maude/MFE/src/mfe.maude
+(select tool CRC .)
+(ccr LPM .)
+

CoqModels/experimenting/liftkplus/univ/plusAC/univ.dk

+
+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.
+

CoqModels/experimenting/liftkplus/univ/plusACpred/univ.dk

+
+
+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).
+

CoqModels/experimenting/liftmax/Makefile

+#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: