Commit 80e6ef1d authored by Gaspard FEREY's avatar Gaspard FEREY

Added project to translate HOAS to DB with AC normalization.

parent 400d0b70
#NAME HOASDB.
N : Type.
0 : N.
S : N -> N.
def plus : N -> N -> N.
def max : N -> N -> N.
def rule : N -> N -> N.
Sort : Type.
poly : N -> Sort.
forall : (N -> Sort) -> Sort.
def U' : Sort -> Type.
[f] U' (forall f) --> x : N -> U' (f x).
(;
#SNF
U' (
forall (i =>
forall (j =>
forall (k => poly (max i (plus j k)))))).
;)
(; ------------- ;)
Term : Type.
0' : Term.
def S' : Term -> Term.
Lam : Term -> Term.
def Ind := N.
db : Ind -> Term.
def max' : Term -> Term -> Term.
def plus' : Term -> Term -> Term.
def rule' : Term -> Term -> Term.
(; ------------- ;)
def V := N.
var : V -> N.
def normalize : Term -> Term.
def normalize2 : Term -> Term.
def minus : V -> V -> Ind.
[n] minus n 0 --> n
[n,m] minus (S n) (S m) --> minus n m.
def U3 : V -> N -> Term.
[k,k'] U3 k (var k') --> db (minus k k')
[k,i,j] U3 k (max i j) --> max' (U3 k i) (U3 k j)
[k,i,j] U3 k (plus i j) --> plus' (U3 k i) (U3 k j)
[k,i,j] U3 k (rule i j) --> rule' (U3 k i) (U3 k j)
[k] U3 k 0 --> 0'
[k,x] U3 k (S x) --> S' (U3 k x).
def U2 : V -> Sort -> Term.
[k,f] U2 k (forall (x => f x)) --> Lam (U2 (S k) (f (var (S k))))
[k,x] U2 k (poly x) --> normalize2 (normalize (U3 k x)).
def U : Sort -> Term := U2 0.
(; -------------- ;)
Bool : Type.
T : Bool.
F : Bool.
def ite : Bool -> Term -> Term -> Term.
[x] ite T x _ --> x
[x] ite F _ x --> x.
def eq : Term -> Term -> Bool.
[x] eq x x --> T
[x,y] eq x y --> F.
def or : Bool -> Bool -> Bool.
[x] or T x --> T
[y] or F y --> y.
def and : Bool -> Bool -> Bool.
[x] and T x --> x
[y] and F y --> F.
def nlt : N -> N -> Bool.
[x] nlt 0 x --> T
[y] nlt (S y) 0 --> F
[x,y] nlt (S x) (S y) --> nlt x y.
def lt : Term -> Term -> Bool.
def lexi_lt : Term -> Term -> Term -> Term -> Bool.
[x,y,z,t] lexi_lt x y z t --> or (lt x z) (and (eq x z) (lt y t)).
(; 0 < S < db < rule < max < plus < ;)
[x] lt 0' x --> T
[x] lt x 0' --> F
[x,y] lt (S' x) (S' y) --> lt x y
[x,y] lt (S' x) y --> T
[x,y] lt x (S' y) --> F
[i,j] lt (db i) (db j) --> nlt i j
[i,y] lt (db i) y --> T (; TODO: y should be any of the 3 cases (max', rule', plus') ;)
[j,x] lt x (db j) --> F (; TODO: x should be any of the 3 cases (max', rule', plus') ;)
[x,y,z,t] lt (max' x y) (max' z t) --> lexi_lt x y z t
[x,y,z,t] lt (plus' x y) (plus' z t) --> lexi_lt x y z t
[x,y,z,t] lt (rule' x y) (rule' z t) --> lexi_lt x y z t
[x,y,z,t] lt (max' x y) (plus' z t) --> T
[x,y,z,t] lt (plus' z t) (max' x y) --> F
[x,y,z,t] lt (rule' x y) (max' z t) --> T
[x,y,z,t] lt (max' z t) (rule' x y) --> F
[x,y,z,t] lt (rule' x y) (plus' z t) --> T
[x,y,z,t] lt (plus' z t) (rule' x y) --> F.
[] normalize 0' --> 0'
[x] normalize (S' x) --> S' (normalize x)
[i] normalize (db i) --> db i
[x,y,z] normalize (max' (max' x y) z) --> normalize (max' x (max' y z))
[x,y,z] normalize (plus' (plus' x y) z) --> normalize (plus' x (plus' y z))
[x,y] normalize (plus' x y) -->
(z : Term => t : Term =>
ite (lt z t)
(plus' z t)
(plus' t z)) (normalize x) (normalize y)
[x,y] normalize (max' x y) -->
(z : Term => t : Term =>
ite (lt z t)
(max' z t)
(max' t z)) (normalize x) (normalize y).
[x] plus' 0' x --> x.
[x,y] plus' (S' x) y --> S' (plus' x y).
[x,y] plus' x (S' y) --> S' (plus' x y).
[x] max' 0' x --> x.
[x,y] S' (max' x y) --> max' (S' x) (S' y).
[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' j i) (plus' k i).
def ltei : Term -> Term -> Bool.
[x] ltei x x --> T.
[a,b,c,d] ltei (plus' a b) (plus' c d) --> or (and (ltei a c) (ltei b d)) (ltei (plus' a b) d).
[x,y,z] ltei x (plus' y z) --> or (ltei x y) (ltei x z).
[x,y,z] ltei x (max' y z) --> or (ltei x y) (ltei x z).
[x,y] ltei (S' x) (S' y) --> ltei x y.
[x,y] ltei x (S' y) --> ltei x y.
[x,y] ltei x y --> F.
[x,z] normalize2 (max' x z) --> ite (ltei x z) (normalize2 z) (max' x (normalize2 z)).
[x] normalize2 (S' x) --> S' (normalize2 x).
[x,y] normalize2 (plus' x y) --> plus' (normalize2 x) (normalize2 y).
[x] normalize2 (db x) --> db x.
def 1 := S 0.
def 2 := S 1.
def 3 := S 2.
def 4 := S 3.
def 5 := S 4.
(; max (a + 2) (a + 3 + b) (a + (max 5 (4 + c))) ;)
#SNF
U (
forall (a =>
forall (b =>
forall (c =>
poly
(max
(max
(plus a 2)
(plus (plus a 3) b))
(plus a (max 5 (plus 4 c)))))))).
(; max SSa SSS(b+a) SSSSSa SSSS(c+a) ;)
(; a + 3 + (max b (1 + (max 1 c))) ;)
#SNF
U (
forall (a =>
forall (b =>
forall (c =>
poly
(plus (plus a 3) (max b (plus 1 (max 1 c)))))))).
(; max SSS(b+a) SSSSSa SSSS(c+a) ;)
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