Commit 7c71d534 authored by Gaspard Ferey's avatar Gaspard Ferey

Translator from cic.dk to AC.

parent 58d96cdb
(; This is not a CiC implementation : nocic ;)
def Nat : Type := cc.Sort.
def z : Nat := cc.0.
def s : Nat -> Nat := x => cc.plus cc.1 x.
def m : Nat -> Nat -> Nat := cc.max.
(; Sorts ;)
def Sort : Type := cc.Sort.
def prop : Sort := cc.0.
def type : Nat -> Sort := s.
def succ : Sort -> Sort := s.
def next : Sort -> Sort := s.
def rule : Sort -> Sort -> Sort := cc.rule.
def max : Sort -> Sort -> Sort := cc.max.
(; Types and terms ;)
def Univ : s : Sort -> Type := cc.U.
def Term : s : Sort -> a : Univ s -> Type := cc.T.
def univ : s : Sort -> Univ (succ s) := cc.u.
def prod : s1 : Sort ->
s2 : Sort ->
a : Univ s1 ->
b : (Term s1 a -> Univ s2) ->
Univ (rule s1 s2) := cc.prod.
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (cc.max s1 s2).
[i,j,a] lift (cc.plus i j) i a --> a.
[i,j,a] lift i (cc.plus i j) a --> cc.liftnk i j a.
......@@ -8,9 +8,9 @@ def s : Nat -> Nat := x => cc.plus cc.1 x.
def m : Nat -> Nat -> Nat := cc.max.
#CONV i : Nat => m i z , i : Nat => i.
#CONV j : Nat => m z j , j : Nat => j.
#CONV i : Nat => j : Nat => m (s i) (s j) , i : Nat => j : Nat => s (m i j).
#CHECK (i : Nat => m i z ) == (i : Nat => i).
#CHECK (j : Nat => m z j ) == (j : Nat => j).
#CHECK (i : Nat => j : Nat => m (s i) (s j) ) == (i : Nat => j : Nat => s (m i j)).
(; Sorts ;)
......@@ -21,24 +21,24 @@ def type : Nat -> Sort := s.
(; Universe successors ;)
def succ : Sort -> Sort := s.
#CONV succ prop, type z.
#CONV i : Nat => succ (type i), i : Nat => type (s i).
#CHECK succ prop == type z.
#CHECK (i : Nat => succ (type i)) == i : Nat => type (s i).
(; Universe cumulativity ;)
def next : Sort -> Sort := s.
#CONV next prop, type z.
#CONV i : Nat => next (type i), i : Nat => type (s i).
#CHECK next prop == type z.
#CHECK (i : Nat => next (type i) ) == i : Nat => type (s i).
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort := cc.rule.
#CONV s1 : Sort => rule s1 prop, s1 : Sort => prop.
#CONV s2 : Sort => rule prop s2, s2 : Sort => s2.
#CONV i : Nat => j : Nat => rule (type i) (type j), i : Nat => j : Nat => type (m i j).
#CHECK (s1 : Sort => rule s1 prop) == s1 : Sort => prop.
#CHECK (s2 : Sort => rule prop s2) == s2 : Sort => s2.
#CHECK (i : Nat => j : Nat => rule (type i) (type j)) == i : Nat => j : Nat => type (m i j).
def max : Sort -> Sort -> Sort := cc.max.
#CONV s1 : Sort => max s1 prop, s1 : Sort => s1.
#CONV s2 : Sort => max prop s2, s2 : Sort => s2.
#CONV i : Nat => j : Nat => max (type i) (type j), i : Nat => j : Nat => type (m i j).
#CHECK (s1 : Sort => max s1 prop ) == s1 : Sort => s1.
#CHECK (s2 : Sort => max prop s2 ) == s2 : Sort => s2.
#CHECK (i : Nat => j : Nat => max (type i) (type j) ) == i : Nat => j : Nat => type (m i j).
(; Types and terms ;)
......@@ -50,7 +50,9 @@ def univ : s : Sort -> Univ (succ s) := cc.u.
def plus : Sort -> Sort -> Sort := cc.plus.
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (cc.plus s1 s2) := cc.liftnk.
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (cc.max s1 s2).
[i,j,a] lift (cc.plus i j) i a --> a.
[i,j,a] lift i (cc.plus i j) a --> cc.liftnk i j a.
def prod : s1 : Sort ->
s2 : Sort ->
......@@ -58,38 +60,42 @@ def prod : s1 : Sort ->
b : (Term s1 a -> Univ s2) ->
Univ (rule s1 s2) := cc.prod.
#CONV s : Sort => Term (succ s) (univ s), s : Sort => Univ s.
#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.
#CHECK (s : Sort => Term (succ s) (univ s) ) == s : Sort => Univ s.
#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) =>
x : Term s1 a -> Term s2 (b x).
#EVAL[SNF] s1 : Sort => s2 : Sort => a : Univ s1 => Term (max s1 s2) (lift s1 s2 a).
#EVAL[SNF] s1 : Sort => s2 : Sort => a : Univ s1 => Term s1 a.
#CHECK (s1 : Sort => s2 : Sort => a : Univ s1 => Term (max s1 s2) (lift s1 s2 a))
== s1 : Sort => s2 : Sort => a : Univ s1 => Term s1 a.
#CHECK ( 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) =>
x : Term s1 a -> Term s2 (b x).
(; Canonicity rules ;)
#CONV s : Sort => max s s, s : Sort => s.
#CONV s1 : Sort => s2 : Sort => s3 : Sort => max (max s1 s2) s3,
s1 : Sort => s2 : Sort => s3 : Sort => max s1 (max s2 s3).
#CHECK (s : Sort => max s s ) == s : Sort => s.
#CHECK (s1 : Sort => s2 : Sort => s3 : Sort => max (max s1 s2) s3)
== s1 : Sort => s2 : Sort => s3 : Sort => max s1 (max s2 s3).
#CONV s1 : Sort => s2 : Sort => s3 : Sort => rule (max s1 s3) s2,
s1 : Sort => s2 : Sort => s3 : Sort => max (rule s1 s2) (rule s3 s2).
#CONV s1 : Sort => s2 : Sort => s3 : Sort => rule s1 (max s2 s3),
s1 : Sort => s2 : Sort => s3 : Sort => max (rule s1 s2) (rule s1 s3).
#CHECK (s1 : Sort => s2 : Sort => s3 : Sort => rule (max s1 s3) s2)
== s1 : Sort => s2 : Sort => s3 : Sort => max (rule s1 s2) (rule s3 s2).
#CHECK (s1 : Sort => s2 : Sort => s3 : Sort => rule s1 (max s2 s3))
== s1 : Sort => s2 : Sort => s3 : Sort => max (rule s1 s2) (rule s1 s3).
#CONV s : Sort => a : Univ s => lift s s a,
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.
#CHECK (s : Sort => a : Univ s => lift s s a)
== s : Sort => a : Univ s => a.
#CHECK (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).
#CHECK (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)).
#CHECK (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)).
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