...
 
Commits (2)
#NAME cc.
(; 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.
Can only lift k levels from 0 or 1 level from universe i.
- 1 + max(i,j) is not convertible with max(1+i, 1+j)
It remains unclear whether this is an issue or not.
......
load cc.maude
load /home/gferey/maude/MFE/src/mfe.maude
(select tool CRC .)
(ccr LPM .)
......@@ -9,7 +9,7 @@ This variant implements :
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.
Can only lift k levels from 0 or 1 level from universe i.
- 1 + max(i,j) is not convertible with max(1+i, 1+j)
It remains unclear whether this is an issue or not.
......
......@@ -13,7 +13,7 @@ This variant implements :
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.
Can only lift k levels from 0 or 1 level from universe i.
;)
......
......@@ -9,7 +9,7 @@ This variant implements :
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.
Can only lift k levels from 0 or 1 level from universe i.
;)
......
#NAME cc.
(; Natural numbers ;)
N : Type.
......@@ -9,7 +7,8 @@ s : N -> N.
def max : N -> N -> N.
[i ] max 0 i --> i
[i ] max i 0 --> i
[i,j] max (s i) (s j) --> s (max i j).
[i,j] max (s i) (s j) --> s (max i j)
[i ] max i i --> i.
B : Type.
......@@ -27,7 +26,8 @@ def le : N -> N -> B.
[i,j] le (s i) (s j) --> le i j
[i] le i i --> true
[i] le (s i) i --> false
[i] le i (s i) --> true.
[i] le i (s i) --> true
[i,j,k] le (max i j) k --> and (le i k) (le j k).
[i,j,k] and (and (le i j) (le j k)) (le i k) --> and (le i j) (le j k)
[i,j,k,c] and (and (and (le i j) (le j k)) (le i k)) c --> and (and (le i j) (le j k)) c.
......@@ -109,6 +109,8 @@ constrain : d : Cstr -> c : Cstr -> i : N -> a : U c i -> U (and d c) i.
(x => constrain (le j k) d j (b x))
).
def u' : c : Cstr -> i : N -> U c (s i) := c => i => constrain c true (s i) (u i).
def u'' : c : Cstr -> i : N -> j : N -> U (and c (le (s i) j)) j :=
......
#NAME idic.
def Cstr := cc.Cstr.
def s := cc.s.
def Sort := cc.N.
......@@ -63,7 +61,7 @@ def g2 : Cstr.
def id :
A : cc.U global Top_1 ->
cc.T global Top_1 A ->
cc.T global Top_1 A := c => A => x => x.
cc.T global Top_1 A := A => a => a.
......@@ -74,39 +72,57 @@ fun (A : Type@{Top.2}) (a : A) => a
(* Top.2 |= *)
;)
def pid :
c : Cstr ->
Top_2 : Sort ->
A : cc.U (and c global) Top_2 ->
cc.T c Top_2 A ->
cc.T c Top_2 A := c => Top_2 => A => x => x.
A : cc.U global Top_2 ->
cc.T global Top_2 A ->
cc.T global Top_2 A
:= Top_2 => A => x => x.
(;
pid_id = pid@{Top.3} (@id) : forall A : Type@{Top.1}, A -> A
(* Top.3 |= Top.1 < Top.3 *)
;)
def Top_3 : Sort.
def g3 : Cstr.
[] g2 -->
(and (sle Set Top_3)
(and (sle Top_1 Top_3)
g3)).
#INFER
(cc.prod
cc.true
(s Top_1)
cc.true
Top_1
(cc.u Top_1)
(A => cc.prod
cc.true
Top_1
cc.true
Top_1
A
(x => A))).
def pid_id :
c : Cstr ->
A : cc.U c Top_1 ->
cc.T c Top_1 A ->
cc.T (and (sle Top_1 Top_3) c) Top_1 A
A : cc.U global Top_1 ->
cc.T global Top_1 A ->
cc.T global Top_1 A
:=
c : Cstr =>
pid (and (sle Top_1 Top_3) c) Top_3
pid Top_3
(cc.lift global
(cc.prod
(and (sle Top_1 Top_3) c)
Top_3
(and (sle Top_1 Top_3) c)
Top_3
(cc.u'' c Top_1 Top_3)
cc.true
(s Top_1)
cc.true
Top_1
(cc.u Top_1)
(A => cc.prod
c
cc.true
Top_1
c
cc.true
Top_1
A
(x => A)))
......
ind : Type.
1 : ind.
2 : ind.
3 : ind.
4 : ind.
5 : ind.
6 : ind.
7 : ind.
8 : ind.
9 : ind.
X : ind.
def P : ind -> ind.
[] P 1 --> X.
[] P 2 --> 1.
[] P 3 --> 2.
[] P 4 --> 3.
[] P 5 --> 4.
[] P 6 --> 5.
[] P 7 --> 6.
[] P 8 --> 7.
[] P 9 --> 8.
def S : ind -> ind.
[] S 1 --> 2.
[] S 2 --> 3.
[] S 3 --> 4.
[] S 4 --> 5.
[] S 5 --> 6.
[] S 6 --> 7.
[] S 7 --> 8.
[] S 8 --> 9.
[] S 9 --> X.
def trunc3 : ind -> ind.
[] trunc3 X --> X.
[] trunc3 1 --> 1.
[] trunc3 4 --> 1.
[] trunc3 7 --> 1.
[i] trunc3 i --> P i.
bool : Type.
T : bool.
F : bool.
def and : bool -> bool -> bool.
[x] and T x --> x
[x] and F x --> F.
def or : bool -> bool -> bool.
[x] or T x --> T
[x] or F x --> x.
def not : bool -> bool.
[] not T --> F
[] not F --> T.
def eq : ind -> ind -> bool.
[x] eq x x --> T
[x,y] eq x y --> F.
def ite : A : Type -> bool -> A -> A -> A.
[A,x] ite A T x _ --> x
[A,x] ite A F _ x --> x.
ind_list : Type.
Empty' : ind_list.
Cons' : ind -> ind_list -> ind_list.
sudo : Type.
Empty : sudo.
Cons : ind_list -> sudo -> sudo.
def E : ind_list :=
Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X Empty')))))))).
def empty_sudo : sudo :=
Cons E (Cons E (Cons E (Cons E (Cons E (Cons E (Cons E (Cons E (Cons E Empty )))))))).
def set' : ind -> ind -> ind_list -> ind_list.
[j,k,a,l] set' j k (Cons' a l) --> ite ind_list (eq j 1) (Cons' k l) (Cons' a (set' (P j) k l)).
def set : ind -> ind -> ind -> sudo -> sudo.
[i,j,k,a,l] set i j k (Cons a l) --> ite sudo (eq i 1) (Cons (set' j k a) l) (Cons a (set (P i) j k l)).
def get' : ind -> ind_list -> ind.
[j,a,l] get' j (Cons' a l) --> ite ind (eq j 1) a (get' (P j) l).
def get : ind -> ind -> sudo -> ind.
[i,j,a,l] get i j (Cons a l) --> ite ind (eq i 1) (get' j a) (get (P i) j l).
def exists' : (ind -> bool) -> ind -> bool.
[f ] exists' f X --> F
[f,i] exists' f i --> or (f i) (exists' f (S i)).
def exists : (ind -> bool) -> bool := f => exists' f 1.
def mem_line : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_line i j k s --> exists (i' => eq (get i' j s) k).
def mem_col : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_col i j k s --> exists (j' => eq (get i j' s) k).
def mem_squ : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_squ i j k s -->
(i':ind =>
j':ind =>
or (or (eq (get i' j' s) k)
(or (eq (get (S i') j' s) k)
(eq (get (S (S i')) j' s) k)))
(or (or (eq (get i' (S j') s) k)
(or (eq (get (S i') (S j') s) k)
(eq (get (S (S i')) (S j') s) k)))
(or (eq (get i' (S (S j')) s) k)
(or (eq (get (S i') (S (S j')) s) k)
(eq (get (S (S i')) (S (S j')) s) k))))
)
(trunc3 i) (trunc3 j).
def check : ind -> ind -> ind -> sudo -> bool :=
i => j => k => s =>
and (not (mem_line i j k s))
( and (not (mem_col i j k s))
(not (mem_squ i j k s))).
solution : Type.
success : sudo -> solution.
fail : solution.
def iffail : solution -> solution -> solution.
[x] iffail (success x) _ --> success x
[d] iffail fail d --> d.
def solve : ind -> ind -> ind -> sudo -> solution.
[i,s] solve i X _ s --> solve (S i) 1 1 s.
[ s] solve X _ _ s --> success s.
[i,j,s] solve i j X s --> fail.
[i,j,k,s] solve i j k s -->
ite solution
(eq (get i j s) X)
(ite solution
(check i j k s)
(iffail
(solve i (S j) 1 (set i j k s))
(solve i j (S k) s)
)
(solve i j (S k) s)
)
(solve i (S j) 1 s).
def solve_sudo : sudo -> solution := s => solve 1 1 1 s.
def extract_sol : solution -> sudo.
[x] extract_sol (success x) --> x.
def sol := solve_sudo empty_sudo.
#EVAL sol.
ind : Type.
1 : ind.
2 : ind.
3 : ind.
4 : ind.
5 : ind.
6 : ind.
7 : ind.
8 : ind.
9 : ind.
X : ind.
def P : ind -> ind.
[] P 1 --> X.
[] P 2 --> 1.
[] P 3 --> 2.
[] P 4 --> 3.
[] P 5 --> 4.
[] P 6 --> 5.
[] P 7 --> 6.
[] P 8 --> 7.
[] P 9 --> 8.
def S : ind -> ind.
[] S 1 --> 2.
[] S 2 --> 3.
[] S 3 --> 4.
[] S 4 --> 5.
[] S 5 --> 6.
[] S 6 --> 7.
[] S 7 --> 8.
[] S 8 --> 9.
[] S 9 --> X.
def trunc3 : ind -> ind.
[] trunc3 1 --> 1
[] trunc3 2 --> 1
[] trunc3 3 --> 1
[] trunc3 4 --> 4
[] trunc3 5 --> 4
[] trunc3 6 --> 4
[] trunc3 7 --> 7
[] trunc3 8 --> 7
[] trunc3 9 --> 7.
bool : Type.
T : bool.
F : bool.
def and : bool -> bool -> bool.
[x] and T x --> x
[x] and F x --> F.
def or : bool -> bool -> bool.
[x] or T x --> T
[x] or F x --> x.
def not : bool -> bool.
[] not T --> F
[] not F --> T.
def eq : ind -> ind -> bool.
[x] eq x x --> T
[x,y] eq x y --> F.
def ite : A : Type -> bool -> A -> A -> A.
[A,x] ite A T x _ --> x
[A,x] ite A F _ x --> x.
list : A : Type -> Type.
l : A : Type -> A -> A -> A -> A -> A -> A -> A -> A -> A -> list A.
def get' : A : Type -> ind -> list A -> A.
[A,x] get' A 1 (l A x _ _ _ _ _ _ _ _) --> x
[A,x] get' A 2 (l A _ x _ _ _ _ _ _ _) --> x
[A,x] get' A 3 (l A _ _ x _ _ _ _ _ _) --> x
[A,x] get' A 4 (l A _ _ _ x _ _ _ _ _) --> x
[A,x] get' A 5 (l A _ _ _ _ x _ _ _ _) --> x
[A,x] get' A 6 (l A _ _ _ _ _ x _ _ _) --> x
[A,x] get' A 7 (l A _ _ _ _ _ _ x _ _) --> x
[A,x] get' A 8 (l A _ _ _ _ _ _ _ x _) --> x
[A,x] get' A 9 (l A _ _ _ _ _ _ _ _ x) --> x.
def set' : A : Type -> ind -> (A -> A) -> list A -> list A.
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 1 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A (k x1) x2 x3 x4 x5 x6 x7 x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 2 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 (k x2) x3 x4 x5 x6 x7 x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 3 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 (k x3) x4 x5 x6 x7 x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 4 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 (k x4) x5 x6 x7 x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 5 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 (k x5) x6 x7 x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 6 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 x5 (k x6) x7 x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 7 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 x5 x6 (k x7) x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 8 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 x5 x6 x7 (k x8) x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 9 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 x5 x6 x7 x8 (k x9) ).
def sudo : Type := list (list ind).
def E : list ind := l ind X X X X X X X X X.
def empty_sudo : sudo := l (list ind) E E E E E E E E E.
def get : ind -> ind -> sudo -> ind.
[i,j,s] get i j s --> (get' ind j (get' (list ind) i s)).
def set : ind -> ind -> ind -> sudo -> sudo.
[i,j,k,s] set i j k s --> set' (list ind) i (set' ind j (x => k)) s.
def exists' : (ind -> bool) -> ind -> bool.
[f ] exists' f X --> F
[f,i] exists' f i --> or (f i) (exists' f (S i)).
def exists : (ind -> bool) -> bool := f => exists' f 1.
def mem_line : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_line i j k s --> exists (i' => eq (get i' j s) k).
def mem_col : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_col i j k s --> exists (j' => eq (get i j' s) k).
def mem_squ : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_squ i j k s --> F.
def mem_squ2 : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_squ2 i j k s -->
(i':ind =>
j':ind =>
(or (eq (get i' j' s) k)
(or (eq (get (S i') j' s) k)
(or (eq (get (S (S i')) j' s) k)
(or (eq (get i' (S j') s) k)
(or (eq (get (S i') (S j') s) k)
(or (eq (get (S (S i')) (S j') s) k)
(or (eq (get i' (S (S j')) s) k)
(or (eq (get (S i') (S (S j')) s) k)
(eq (get (S (S i')) (S (S j')) s) k)))))))))
)
(trunc3 i) (trunc3 j).
def check : ind -> ind -> ind -> sudo -> bool :=
i => j => k => s =>
and (not (mem_line i j k s))
( and (not (mem_col i j k s))
(not (mem_squ i j k s))).
solution : Type.
success : sudo -> solution.
fail : solution.
def iffail : solution -> solution -> solution.
[x] iffail (success x) _ --> success x
[d] iffail fail d --> d.
def solve : ind -> ind -> ind -> sudo -> solution.
[i,s] solve i X _ s --> solve (S i) 1 1 s.
[ s] solve X _ _ s --> success s.
[i,j,s] solve i j X s --> fail.
[i,j,k,s] solve i j k s -->
ite solution
(eq (get i j s) X)
(ite solution
(check i j k s)
(iffail
(solve i (S j) 1 (set i j k s))
(solve i j (S k) s)
)
(solve i j (S k) s)
)
(solve i (S j) 1 s).
def solve_sudo : sudo -> solution := s => solve 1 1 1 s.
def extract_sol : solution -> sudo.
[x] extract_sol (success x) --> x.
def sol := solve_sudo empty_sudo.
#EVAL sol.
#EVAL[SNF,1] get 2 2 (extract_sol sol).
#EVAL[SNF,2] get 2 2 (extract_sol sol).
#EVAL[SNF,3] get 2 2 (extract_sol sol).
#EVAL[WHNF,4] mem_squ2 2 2 3 (extract_sol sol).