Commit 852beb20 authored by Gaspard Ferey's avatar Gaspard Ferey

WIP: Coq Model with constraints.

parent b4755d77
#NAME cc.
(; Natural numbers ;)
N : Type.
0 : N.
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).
B : Type.
true : B.
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
[i] le i (s i) --> true.
[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))
).
#NAME idic.
def 0 := cc.0.
def 1 := cc.s 0.
def 2 := cc.s 1.
def Sort := cc.N.
def Set := 0.
def sle := i:Sort => j:Sort => cc.le (cc.s i) j.
def and := cc.and.
(;
(* id_example.v *)
Definition id {A : Type} (a : A) := a.
Polymorphic Definition pid {A : Type} (a : A) := a.
Definition pid_id := pid (@id).
Definition pid_id_expl := @pid (forall A:Type,A->A) (@id).
Definition pid_pid := pid (@pid).
Definition pid_pid_expl := @pid (forall A:Type,A->A) (@pid).
Polymorphic Definition p_pid_id := pid (@id).
Polymorphic Definition p_pid_id_expl := @pid (forall A:Type,A->A) (@id).
Polymorphic Definition p_pid_pid := pid (@pid).
Polymorphic Definition p_pid_pid_expl := @pid (forall A:Type,A->A) (@pid).
(*
Top.9 < Top.8
Top.7 < Top.6
Top.5 < Top.4
< Top.3
Top.1 = Top.5
Set < Top.9
< Top.8
< Top.7
< Top.6
< Top.5
< Top.4
< Top.3
< Top.1
Prop < Set
*)
;)
def Top_1 : Sort.
def global : cc.Cstr :=
(and (sle Set Top_1)
cc.true
)
.
(;
id = fun (A : Type@{Top.1}) (a : A) => a
: forall A : Type@{Top.1}, A -> A
(* Top.1 |= *)
;)
def id :
A : cc.U global Top_1 ->
cc.T global Top_1 A ->
cc.T global Top_1 A := A => x => x.
(;
Polymorphic pid@{Top.2} =
fun (A : Type@{Top.2}) (a : A) => a
: forall A : Type@{Top.2}, A -> A
(* Top.2 |= *)
;)
def pid : Top_2 : cc.Sort ->
A : cc.U Top_2 -> cc.T Top_2 A -> cc.T 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 := 2.
def pid_id : A : cc.U Top_1 -> cc.T Top_1 A -> cc.T Top_1 A :=
pid Top_3
(cc.prod
Top_3
Top_1
(cc.u Top_1)
(A => cc.prod Top_1 Top_1 A (x => A)))
id.
(;
pid_id_expl =
pid@{Top.4} (@id)
: forall A : Type@{Top.5}, A -> A
(* Top.4 Top.5 |= Top.1 < Top.4
Top.1 = Top.5
*)
;)
def Top_4 := 2.
def Top_5 := 1.
def pid_id_expl : A : cc.U Top_5 -> cc.T Top_5 A -> cc.T Top_5 A :=
pid Top_4
(cc.prod
Top_4
Top_5
(cc.u Top_5)
(A => cc.prod Top_5 Top_5 A (x => A)))
id.
(;
pid_pid =
pid@{Top.6} (@pid@{Top.7})
: forall A : Type@{Top.7}, A -> A
(* Top.6 Top.7 |= Top.7 < Top.6
*)
;)
def Top_6 := 2.
def Top_7 := 1.
def pid_pid : A : cc.U Top_7 -> cc.T Top_7 A -> cc.T Top_7 A :=
pid Top_6
(cc.prod
Top_6
Top_7
(cc.u Top_7)
(A => cc.prod Top_7 Top_7 A (x => A)))
(pid Top_7).
(; pid_pid_expl is exactly the same as previous
replacing Top.7 with Top.9 and Top.- with Top.8. ;)
(;
Polymorphic p_pid_id@{Top.11} =
pid@{Top.11} (@id)
: forall A : Type@{Top.1}, A -> A
(* Top.11 |= Top.1 < Top.11
*)
;)
(; Somehow translate here that Top.11 >= Top.1 + 1;)
constraints : Type.
prf : constraints -> Type.
eq : cc.Sort -> cc.Sort -> constraints.
refl : i : cc.Sort -> prf (eq i i).
lt : cc.Sort -> cc.Sort -> constraints.
ltp : i : cc.Sort -> j : cc.Sort -> prf (lt i (plus (plus i j) 1)).
le : cc.Sort -> cc.Sort -> constraints.
lep : i : cc.Sort -> j : cc.Sort -> prf (lt i (plus i j)).
and : constraints -> constraints -> constraints.
conj : a : constraints -> b : constraints -> prf a -> prf b -> prf (and a b).
def p_pid_id : Top_11 : cc.Sort ->
p : prf (lt Top_1 Top_11) ->
A : cc.U Top_1 -> cc.T Top_1 A -> cc.T Top_1 A.
(;
[] p_pid_id -->
Top_11 : cc.Sort =>
pid Top_11
(cc.prod
Top_11
Top_1
(cc.lift (plus 1 Top_1) Top_11 (cc.u Top_1))
(A => cc.prod Top_1 Top_1 A (x => A)))
id.
;)
(;
Polymorphic p_pid_id_expl@{Top.12 Top.13} =
pid@{Top.12} (@id)
: forall A : Type@{Top.13}, A -> A
(* Top.12 Top.13 |= Top.1 < Top.12
Top.1 = Top.13
*)
;)
(;
Polymorphic p_pid_pid@{Top.14 Top.15} =
pid@{Top.14} (@pid@{Top.15})
: forall A : Type@{Top.15}, A -> A
(* Top.14 Top.15 |= Top.15 < Top.14
*)
;)
(;
Polymorphic p_pid_pid_expl@{Top.16 Top.17} =
pid@{Top.16} (@pid@{Top.17})
: forall A : Type@{Top.17}, A -> A
(* Top.16 Top.17 |= Top.17 < Top.16
*)
;)
Definition id {A : Type} (a : A) := a.
Polymorphic Definition pid {A : Type} (a : A) := a.
Definition pid_id := pid (@id).
Definition pid_id_expl := @pid (forall A:Type,A->A) (@id).
Definition pid_pid := pid (@pid).
Definition pid_pid_expl := @pid (forall A:Type,A->A) (@pid). (* identical *)
Polymorphic Definition p_pid_id := pid (@id).
Polymorphic Definition p_pid_id_expl := @pid (forall A:Type,A->A) (@id).
Polymorphic Definition p_pid_pid := pid (@pid).
Polymorphic Definition p_pid_pid_expl := @pid (forall A:Type,A->A) (@pid).
Set Printing Universes.
Print Universes.
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