1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
16 include "list/list.ma".
18 inductive index_list (T: nat → Type): ∀m,n:nat.Type ≝
19 | il_s : ∀n.T n → index_list T n n
20 | il_c : ∀m,n. T m → index_list T (S m) n → index_list T m n.
22 lemma down_il : ∀T:nat → Type.∀m,n.∀l: index_list T m n.∀f:(∀p. T (S p) → T p).
23 ∀m',n'.S m' = m → S n' = n → index_list T m' n'.
25 [destruct;apply il_s;apply f;assumption
27 [apply f;rewrite > H;assumption
29 [rewrite > H;reflexivity
33 definition r1 : ∀T0,T1,a0,b0,e0.T1 a0 → T1 b0 ≝
34 λT0:Type.λT1:T0 → Type.
38 eq_rect' ?? (λy,p.T1 y) so ? e0.
41 definition R1 ≝ eq_rect'.
47 ∀T1:∀x0:T0. a0=x0 → Type.
48 ∀a1:T1 a0 (refl_eq ? a0).
49 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type.
53 ∀e1:R1 ??? a1 ? e0 = b1.
54 ∀so:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).T2 b0 e0 b1 e1.
55 intros 8;intros 2 (e1 H);
56 apply (eq_rect' ????? e1);
57 apply (R1 ?? ? ?? e0);
64 ∀T1:∀x0:T0. a0=x0 → Type.
65 ∀a1:T1 a0 (refl_eq ? a0).
66 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type.
67 ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
68 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1.
69 ∀x2:T2 x0 p0 x1 p1.R2 ?????? p0 ? p1 a2 = x2→ Type.
73 ∀e1:R1 ??? a1 ? e0 = b1.
75 ∀e2:R2 ?????? e0 ? e1 a2 = b2.
76 ∀so:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).T3 b0 e0 b1 e1 b2 e2.
77 intros 12;intros 2 (e2 H);
78 apply (eq_rect' ????? e2);
79 apply (R2 ?? ? ??? e0 ? e1);
85 definition r3 : ∀T0:Type.∀T1:T0 → Type.∀T2:∀t0:T0.∀t1:T1 t0.Type.
86 ∀T3:∀t0:T0.∀t1:T1 t0.∀t2:T2 t0 t1.Type.
87 ∀a0,b0:T0.∀e0:a0 = b0.
88 ∀a1:T1 a0.∀b1:T1 b0.∀e1:r1 ?? ?? e0 a1 = b1.
89 ∀a2:T2 a0 a1.∀b2:T2 b0 b1.
90 ∀e2: r2 ????? e0 ?? e1 a2 = b2.
91 T3 a0 a1 a2 → T3 b0 b1 b2.
92 intros 12;intro e2;intro H;
93 apply (eq_rect' ????? e2);
94 apply (R2 ?? ?? (λy0,p0,y1,p1.T3 y0 y1 (r2 T0 T1 T2 a0 y0 p0 a1 y1 p1 a2)) ? e0 ? e1);
99 apply (R2 ?? (λy0,p0,y1,p1.T3 y0 y1 (r2 T0 T1 T2 a0 y0 p0 a1 y1 p1 a2)) ??? e0 e1);
106 λT0:Type.λT1:T0 → Type.λT2:∀t0:T0.∀t1:T1 t0.Type.
107 λT3:∀t0:T0.∀t1:T1 t0.∀t2:T2 t0 t1.Type.
112 λa1:T1 a0.λb1: T1 b0.
113 λe1:r1 ???? e0 a1 = b1.
115 λa2:T2 a0 a1.λb2: T2 b0 b1.
116 λe2:r2 ????? e0 ?? e1 a2 = b2.
119 eq_rect' ?? (λy,p.T3 b0 b1 y)
120 (eq_rect' ?? (λy,p.T3 b0 y (r2 ??? ??e0 ??p a2))
121 (eq_rect' T0 a0 (λy.λp:a0 = y.T3 y (r1 ?? a0 y p a1) (r2 ??? ??p a2)) so b0 e0)
125 let rec iter_type n (l1 : lista dei nomi fin qui creati) (l2: lista dei tipi dipendenti da applicare) ≝
128 | S p ⇒ match l2 with
129 [ nil ⇒ Type (* dummy *)
130 | cons T tl ⇒ ∀t:app_type_list l1 T.iter_type p (l1@[t]) tl ]].
132 lemma app_type_list : ∀l:list Type.∀T:iter_type l.Type.
136 |simplify in i;apply F;apply i;apply a]
139 definition type_list_cons : ∀l:list Type.iter_type l → list Type ≝
140 λl,T.app_type_list l T :: l.
142 let rec build_dep_type n T acc ≝
146 Type → list Type → Type.
149 inductive II : nat → Type ≝
152 | k3 : ∀n,m. II n → II m → II O.
154 inductive JJ : nat → Type ≝
157 | h3 : ∀n,m. JJ n → JJ m → JJ O.
161 lemma test: h3 ?? h1 h2 = h3 ?? h2 h1 → True.
163 letin f ≝ (λx.S (S x));
164 cut (∃a,b.S a = f b);
165 [decompose;cut (S (S a) = S (f a1))
172 definition IId : ∀n,m.II m → II n → Type ≝
173 λa,b,x,y.match x with
174 [ k1 n ⇒ match y with
175 [ k1 n' ⇒ ∀P:Type.(n = n' → P) → P
177 | k3 m n p' q' ⇒ ∀P:Type.P ]
178 | k2 n ⇒ match y with
180 | k2 n' ⇒ ∀P:Type.(n = n' → P) → P
181 | k3 m' n' p' q' ⇒ ∀P:Type.P ]
182 | k3 m n p q ⇒ match y with
185 | k3 m' n' p' q' ⇒ ∀P:Type.(∀e1:m = m'.∀e2:n = n'. (eq_rect ??? p ? e1) = p'
186 → (eq_rect ??? q ? e2) = q' → P) → P ]].
188 lemma IInc : ∀n,x,y.x = y → IId n n x y.
189 intros;rewrite > H;elim y;simplify;intros;
192 |apply f;reflexivity]
195 inductive I1 : nat → Type ≝
198 inductive I2 : ∀n:nat.I1 n → Type ≝
201 inductive I3 : Type ≝
202 | kI3 : ∀x1:nat.∀x2:I1 x1.∀x3:I2 x1 x2.I3.
204 definition I3d: I3 → I3 → Type ≝
206 [ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
207 [ kI3 u1 u2 u3 ⇒ ∀P:Type.
209 ∀e2: (eq_rect ?? (λx.I1 x) t2 ? e1) = u2.
210 ∀e3: (eq_rect' ?? (λy,p.I2 u1 y)
211 (eq_rect' ?? (λy,p.I2 y (eq_rect ?? (λx.I1 x) t2 ? p)) t3 ? e1)
214 lemma I3nc : ∀a,b.a = b → I3d a b.
215 intros;rewrite > H;elim b;simplify;intros;apply f;reflexivity;
218 definition KKd : ∀m,n,p,q.KK m n → KK p q → Type ≝
219 λa,b,c,d,x,y.match x with
220 [ c1 n ⇒ match y with
221 [ c1 n' ⇒ ∀P:Type.(n = n' → P) → P
223 | c3 m' n' p' q' h' i' ⇒ ∀P:Type.P ]
224 | c2 n ⇒ match y with
226 | c2 n' ⇒ ∀P:Type.(n = n' → P) → P
227 | c3 m' n' p' q' h' i' ⇒ ∀P:Type.P ]
228 | c3 m n p q h i ⇒ match y with
231 | c3 m' n' p' q' h' i' ⇒
232 ∀P:Type.(∀e1:m = m'.∀e2:n = n'. ∀e3:p = p'. ∀e4:q = q'.
233 (eq_rect ?? (λm.KK m n') (eq_rect ?? (λn.KK m n) h n' e2) m' e1) = h'
234 → (eq_rect ?? (λp.KK p q') (eq_rect ?? (λq.KK p q) i ? e4) ? e3) = i' → P) → P ]].
236 lemma KKnc : ∀a,b,e,f.e = f → KKd a b a b e f.
237 intros;rewrite > H;elim f;simplify;intros;apply f1;reflexivity;
240 lemma IIconflict: ∀c,d.
241 k3 c d (k1 c) (k2 d) = k3 d c (k2 d) (k1 c) → False.
242 intros;apply (IInc ??? H);clear H;intro;
243 apply (eq_rec ????? e1);
244 intro;generalize in match e1;elim
245 apply (eq_rect' ?? (λx.λp.∀e2:x=c.eq_rect ℕ c II (k1 c) x p=k2 x→eq_rect nat x II (k2 x) c e2 = k1 c → False) ?? e1);
247 apply (eq_rect' nat ? (λx.λp:c=x.k1 x = k2 x → eq_rect nat c II (k2 c) x p = k1 x → False) ?? e2);
250 generalize in match H1;
251 apply (eq_rect' ?? (λx.λp.eq_rect ℕ c II (k1 c) x p=k2 x→False) ?? e1);
252 simplify;intro;destruct;