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 (**************************************************************************)
15 include "logic/equality.ma".
18 include "list/list.ma".
20 inductive list_x : Type ≝
22 | cons_x : ∀T:Type.∀x:T.list_x → list_x.
24 let rec mk_prod (l:list_x) ≝
27 | cons_x T x tl ⇒ ∀y0:T.∀p0:x = y0. mk_prod tl ].
29 let rec appl (l:list_x) : mk_prod l → Type ≝
30 match l return λl:list_x.mk_prod l →Type
32 [ nil_x ⇒ λT:mk_prod nil_x.T
33 | cons_x Ty hd tl ⇒ λT:mk_prod (cons_x Ty hd tl).appl tl (T hd (refl_eq Ty hd)) ].
35 inductive list_xyp : list_x → Type ≝
36 | nil_xyp : ∀l.list_xyp l
37 | cons_xyp : ∀l.∀T:mk_prod l.∀x:appl l T.list_xyp (cons_x ? x l) → list_xyp l.
39 (* let rec tau (l:list_x) (w:list_xyp l) on w: Type ≝
42 | cons_xyp l' T' x' w' ⇒
43 ∀y:appl l' T'.∀p:x' = y.
44 tau (cons_x ? y l') w' ].
49 ∀T1:∀x0:T0. a0=x0 → Type.
50 ∀a1:T1 a0 (refl_eq ? a0).
51 tau ? (cons_xyp nil_x T0 a0 (cons_xyp (cons_x T0 a0 nil_x) T1 a1 (nil_xyp ?))) Type).
53 inductive index_list (T: nat → Type): ∀m,n:nat.Type ≝
54 | il_s : ∀n.T n → index_list T n n
55 | il_c : ∀m,n. T m → index_list T (S m) n → index_list T m n.
57 lemma down_il : ∀T:nat → Type.∀m,n.∀l: index_list T m n.∀f:(∀p. T (S p) → T p).
58 ∀m',n'.S m' = m → S n' = n → index_list T m' n'.
60 [destruct;apply il_s;apply f;assumption
62 [apply f;rewrite > H;assumption
64 [rewrite > H;reflexivity
68 definition R1 ≝ eq_rect'.
73 ∀T1:∀x0:T0. a0=x0 → Type.
74 ∀a1:T1 a0 (refl_eq ? a0).
75 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type.
76 ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
80 ∀e1:R1 ??? a1 ? e0 = b1.
83 apply (eq_rect' ????? e1);
84 apply (R1 ?? ? ?? e0);
91 ∀T1:∀x0:T0. a0=x0 → Type.
92 ∀a1:T1 a0 (refl_eq ? a0).
93 ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type.
94 ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
95 ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1.
96 ∀x2:T2 x0 p0 x1 p1.R2 T0 a0 T1 a1 T2 a2 ? p0 ? p1 = x2→ Type.
100 ∀e1:R1 ??? a1 ? e0 = b1.
102 ∀e2:R2 T0 a0 T1 a1 T2 a2 ? e0 ? e1 = b2.
103 ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).T3 b0 e0 b1 e1 b2 e2.
104 intros 12;intros 2 (e2 H);
105 apply (eq_rect' ????? e2);
106 apply (R2 ?? ? ???? e0 ? e1);
110 (*let rec iter_type n (l1 : lista dei nomi fin qui creati) (l2: lista dei tipi dipendenti da applicare) ≝
113 | S p ⇒ match l2 with
114 [ nil ⇒ Type (* dummy *)
115 | cons T tl ⇒ ∀t:app_type_list l1 T.iter_type p (l1@[t]) tl ]].
117 lemma app_type_list : ∀l:list Type.∀T:iter_type l.Type.
121 |simplify in i;apply F;apply i;apply a]
124 definition type_list_cons : ∀l:list Type.iter_type l → list Type ≝
125 λl,T.app_type_list l T :: l.
127 let rec build_dep_type n T acc ≝
131 Type → list Type → Type.
134 inductive II : nat → Type ≝
137 | k3 : ∀n,m. II n → II m → II O.
139 inductive JJ : nat → Type ≝
142 | h3 : ∀n,m. JJ n → JJ m → JJ O.
146 lemma test: h3 ?? h1 h2 = h3 ?? h2 h1 → True.
148 letin f ≝ (λx.S (S x));
149 cut (∃a,b.S a = f b);
150 [decompose;cut (S (S a) = S (f a1))
157 definition IId : ∀n,m.II m → II n → Type ≝
158 λa,b,x,y.match x with
159 [ k1 n ⇒ match y with
160 [ k1 n' ⇒ ∀P:Type.(n = n' → P) → P
162 | k3 m n p' q' ⇒ ∀P:Type.P ]
163 | k2 n ⇒ match y with
165 | k2 n' ⇒ ∀P:Type.(n = n' → P) → P
166 | k3 m' n' p' q' ⇒ ∀P:Type.P ]
167 | k3 m n p q ⇒ match y with
170 | k3 m' n' p' q' ⇒ ∀P:Type.(∀e1:m = m'.∀e2:n = n'. (eq_rect ??? p ? e1) = p'
171 → (eq_rect ??? q ? e2) = q' → P) → P ]].
173 lemma IInc : ∀n,x,y.x = y → IId n n x y.
174 intros;rewrite > H;elim y;simplify;intros;
177 |apply f;reflexivity]
182 lemma IIconflict: ∀c,d.
183 k3 c d (k1 c) (k2 d) = k3 d c (k2 d) (k1 c) → False.
184 intros;apply (IInc ??? H);clear H;intro;
185 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);
186 simplify;intros;apply (IInc ??? H);
188 inductive I1 : nat → Type ≝
191 inductive I2 : ∀n:nat.I1 n → Type ≝
194 inductive I3 : Type ≝
195 | kI3 : ∀x1:nat.∀x2:I1 x1.∀x3:I2 x1 x2.I3.
197 definition I3d: I3 → I3 → Type ≝
199 [ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
200 [ kI3 u1 u2 u3 ⇒ ∀P:Type.
202 ∀e2: R1 ?? (λy1,p1.I1 y1) ?? e1 = u2.
203 ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) ? e1 ? e2 t3 = u3.P) → P]].
205 lemma I3nc : ∀a,b.a = b → I3d a b.
206 intros;rewrite > H;elim b;simplify;intros;apply f;reflexivity;
209 (*lemma R1_r : ΠA:Type.Πx:A.ΠP:Πy:A.y=x→Type.P x (refl_eq A x)→Πy:A.Πp:y=x.P y p.
210 intros;lapply (eq_rect' A x P p y (sym_eq A y x p1));
211 generalize in match Hletin;
212 cut (∀p1:y = x.sym_eq ??? (sym_eq ??? p1) = p1)
213 [rewrite > Hcut;intro;assumption
214 |intro;apply (eq_rect' ????? p2);simplify;reflexivity]
220 ∀T1:∀x0:T0. x0=a0 → Type.
221 ∀a1:T1 a0 (refl_eq ? a0).
222 ∀T2:∀x0:T0. ∀p0:x0=a0. ∀x1:T1 x0 p0. x1 = R1_r ??? a1 ? p0 → Type.
226 ∀e1:b1 = R1_r ??? a1 ? e0.
227 ∀so:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).T2 b0 e0 b1 e1.
228 intros 8;intros 2 (e1 H);
229 apply (R1_r ????? e1);
230 apply (R1_r ?? ? ?? e0);
234 definition I3prova : ∀a,b,c,d,e,f.kI3 a b c = kI3 d e f → ∃P.P d e f.
235 intros;apply (I3nc ?? H);clear H;
237 generalize in match f as f;generalize in match e as e;
238 generalize in match c as c;generalize in match b as b;
240 apply (R1 ????? e1);intros 5;simplify in e2;
241 generalize in match f as f;generalize in match c as c;
243 apply (R1 ????? e2);intros;simplify in H;
248 definition KKd : ∀m,n,p,q.KK m n → KK p q → Type ≝
249 λa,b,c,d,x,y.match x with
250 [ c1 n ⇒ match y with
251 [ c1 n' ⇒ ∀P:Type.(n = n' → P) → P
253 | c3 m' n' p' q' h' i' ⇒ ∀P:Type.P ]
254 | c2 n ⇒ match y with
256 | c2 n' ⇒ ∀P:Type.(n = n' → P) → P
257 | c3 m' n' p' q' h' i' ⇒ ∀P:Type.P ]
258 | c3 m n p q h i ⇒ match y with
261 | c3 m' n' p' q' h' i' ⇒
262 ∀P:Type.(∀e1:m = m'.∀e2:n = n'. ∀e3:p = p'. ∀e4:q = q'.
263 (eq_rect ?? (λm.KK m n') (eq_rect ?? (λn.KK m n) h n' e2) m' e1) = h'
264 → (eq_rect ?? (λp.KK p q') (eq_rect ?? (λq.KK p q) i ? e4) ? e3) = i' → P) → P ]].
266 lemma KKnc : ∀a,b,e,f.e = f → KKd a b a b e f.
267 intros;rewrite > H;elim f;simplify;intros;apply f1;reflexivity;