cic.dk 2.62 KB
Newer Older
Gaspard Ferey's avatar
Gaspard Ferey committed
1 2
(; WIP, constraints ;)

3 4
(;  Code types depend on a universe and associated constraints  ;)

5 6 7 8 9 10 11 12 13
(; Natural numbers ;)

N : Type.
0 : N.
s : N -> N.

def max : N -> N -> N.
[i  ] max 0     i     --> i
[i  ] max i     0     --> i
Gaspard Ferey's avatar
merge  
Gaspard Ferey committed
14 15
[i,j] max (s i) (s j) --> s (max i j)
[i  ] max i     i     --> i.
16 17 18


B : Type.
Gaspard Ferey's avatar
Gaspard Ferey committed
19
true  : B.
20 21 22 23 24 25 26 27 28 29 30 31 32
false : B.

defac and [B].
[x] and true  x --> x
[x] and false x --> false
[x] and x     x  --> x.

def le : N -> N -> B.
[i]   le 0     i     --> true
[i]   le (s i) 0     --> false
[i,j] le (s i) (s j) --> le i j
[i]   le i     i     --> true
[i]   le (s i) i     --> false
Gaspard Ferey's avatar
merge  
Gaspard Ferey committed
33 34
[i]   le i     (s i) --> true
[i,j,k] le (max i j) k --> and (le i k) (le j k).
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114

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

[i,j,k]          and (le i j) (le (max i k) (max j k))  -->        le i j
[i,j,k,c] and c (and (le i j) (le (max i k) (max j k))) --> and c (le i j)
[i,j,k]          and (le i j) (le (max k i) (max k j))  -->        le i j
[i,j,k,c] and c (and (le i j) (le (max k i) (max k j))) --> and c (le i j).

def Cstr := B.


U : c : Cstr -> i : N -> Type.

u : i : N -> U true (s i).

def T : c : Cstr -> i : N -> a : U c i -> Type.

def lift : c : Cstr -> i : N -> j : N -> U c i -> U (and (le i j) c) j.

def prod : c : Cstr ->
       i : N ->
       d : Cstr ->
       j : N ->
       a : U c i ->
       b : (T c i a -> U d j) ->
       U (and c d) (max i j).

constrain : d : Cstr -> c : Cstr -> i : N -> a : U c i -> U (and d c) i.


[c,j,i]   T c j (u i) --> U (and c (le i j)) i.

[i,j,c,a] T _ j (lift c i j a) --> T c i a.

[i,j,c,d,a,b]
  T _ _ (prod c i d j a b) -->
  x : T c i a -> T d j (b x).

[c,d,i,a] T (and c d) i (constrain d    c    i a) --> T c i a.
[d,i,a]   T d         i (constrain d    true i a) --> T true i a.
[c,i,a]   T c         i (constrain true c    i a) --> T c i a.


[c,i,a] lift c i i a --> a.


[k,c,i,j,a]
  lift _ _ k (lift c i j a) -->
  constrain
    (and (le i j) (le j k))
	(and c (le i k))
	k
    (lift c i k a).



[d,k,c,i,j,a,b]
  prod _ _ d k (lift c i j a) b
  -->
  lift
    (and (le i j) (and c d))
	(max i k)
	(max j k)
    (prod
	  (and c (le i j)) i d k
	  (constrain (le i j) c i a) b).

[c,i,a,d,j,k,b]
  prod c i _ _ a (x => lift d j k (b x))
  -->
  lift
    (and (le j k) (and c d))
	(max i j)
	(max i k)
    (prod
	  c i (and d (le j k)) j
	  a
	  (x => constrain (le j k) d j (b x))
	).
Gaspard Ferey's avatar
Gaspard Ferey committed
115

Gaspard Ferey's avatar
merge  
Gaspard Ferey committed
116 117


Gaspard Ferey's avatar
Gaspard Ferey committed
118 119 120 121
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 :=
  c => i => j => lift c (s i) j (u' c i).