Experimental scripts for nth-order rewriting principles.

diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma
new file mode 100644 (file)
index 0000000..d3d2aad
--- /dev/null
+++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma
@@ -0,0 +1,82 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+(*
+include "nat/nat.ma".
+include "list/list.ma".
+
+inductive index_list (T: nat → Type): ∀m,n:nat.Type ≝
+| il_s : ∀n.T n → index_list T n n
+| il_c : ∀m,n. T m → index_list T (S m) n → index_list T m n.
+
+lemma down_il : ∀T:nat → Type.∀m,n.∀l: index_list T m n.∀f:(∀p. T (S p) → T p).
+                ∀m',n'.S m' = m → S n' = n → index_list T m' n'.
+intros 5;elim i
+[destruct;apply il_s;apply f;assumption
+|apply il_c
+ [apply f;rewrite > H;assumption
+ |apply f1
+  [rewrite > H;reflexivity
+  |assumption]]]
+qed.
+
+definition r1 : ∀T0,T1,a0,b0,e0.T1 a0 → T1 b0 ≝
+  λT0:Type.λT1:T0 → Type.
+  λa0,b0:T0.
+  λe0:a0 = b0.
+  λso:T1 a0.
+  eq_rect' ?? (λy,p.T1 y) so ? e0.
+  *)
+
+include "logic/equality.ma".
+  
+ndefinition R1 ≝ eq_rect_Type0.
+
+ndefinition R2 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type[0].
+  ∀a1:T1 a0 (refl ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type[0].
+  ∀b0:T0.
+  ∀e0:a0 = b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:R1 ??? a1 ? e0 = b1.
+  ∀so:T2 a0 (refl ? a0) a1 (refl ? a1).T2 b0 e0 b1 e1.
+#T0;#a0;#T1;#a1;#T2;#b0;#e0;#b1;#e1;#H;
+napply (eq_rect_Type0 ????? e1);
+napply (R1 ?? ? ?? e0);
+napply H;
+nqed.
+
+ndefinition R3 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type[0].
+  ∀a1:T1 a0 (refl ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type[0].
+  ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
+  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1.
+      ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 x0 p0 ? p1 a2 = x2 → Type[0].
+  ∀b0:T0.
+  ∀e0:a0 = b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:R1 ??? a1 ? e0 = b1.
+  ∀b2: T2 b0 e0 b1 e1.
+  ∀e2:R2 ???? T2 b0 e0 ? e1 a2 = b2.
+  ∀so:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).T3 b0 e0 b1 e1 b2 e2.
+#T0;#a0;#T1;#a1;#T2;#a2;#T3;#b0;#e0;#b1;#e1;#b2;#e2;#H;
+napply (eq_rect_Type0 ????? e2);
+napply (R2 ?? ? ??? e0 ? e1);
+napply H;
+nqed.
\ No newline at end of file

diff --git a/helm/software/matita/tests/destruct_bb.ma b/helm/software/matita/tests/destruct_bb.ma
new file mode 100644 (file)
index 0000000..a494909
--- /dev/null
+++ b/helm/software/matita/tests/destruct_bb.ma
@@ -0,0 +1,256 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+(*
+include "nat/nat.ma".
+include "list/list.ma".
+
+inductive index_list (T: nat → Type): ∀m,n:nat.Type ≝
+| il_s : ∀n.T n → index_list T n n
+| il_c : ∀m,n. T m → index_list T (S m) n → index_list T m n.
+
+lemma down_il : ∀T:nat → Type.∀m,n.∀l: index_list T m n.∀f:(∀p. T (S p) → T p).
+                ∀m',n'.S m' = m → S n' = n → index_list T m' n'.
+intros 5;elim i
+[destruct;apply il_s;apply f;assumption
+|apply il_c
+ [apply f;rewrite > H;assumption
+ |apply f1
+  [rewrite > H;reflexivity
+  |assumption]]]
+qed.
+
+definition r1 : ∀T0,T1,a0,b0,e0.T1 a0 → T1 b0 ≝
+  λT0:Type.λT1:T0 → Type.
+  λa0,b0:T0.
+  λe0:a0 = b0.
+  λso:T1 a0.
+  eq_rect' ?? (λy,p.T1 y) so ? e0.
+  *)
+  
+definition R1 ≝ eq_rect'.
+
+
+definition R2 :
+  ∀T0:Type.
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type.
+  ∀a1:T1 a0 (refl_eq ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type.
+  ∀b0:T0.
+  ∀e0:a0 = b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:R1 ??? a1 ? e0 = b1.
+  ∀so:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).T2 b0 e0 b1 e1.
+intros 8;intros 2 (e1 H);
+apply (eq_rect' ????? e1);
+apply (R1 ?? ? ?? e0);
+simplify;assumption;
+qed.
+
+definition R3 :
+  ∀T0:Type.
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type.
+  ∀a1:T1 a0 (refl_eq ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type.
+  ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
+  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1.
+      ∀x2:T2 x0 p0 x1 p1.R2 ?????? p0 ? p1 a2 = x2→ Type.
+  ∀b0:T0.
+  ∀e0:a0 = b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:R1 ??? a1 ? e0 = b1.
+  ∀b2: T2 b0 e0 b1 e1.
+  ∀e2:R2 ?????? e0 ? e1 a2 = b2.
+  ∀so:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).T3 b0 e0 b1 e1 b2 e2.
+intros 12;intros 2 (e2 H);
+apply (eq_rect' ????? e2);
+apply (R2 ?? ? ??? e0 ? e1);
+simplify;assumption;
+qed.
+
+
+
+definition r3 : ∀T0:Type.∀T1:T0 → Type.∀T2:∀t0:T0.∀t1:T1 t0.Type.
+                ∀T3:∀t0:T0.∀t1:T1 t0.∀t2:T2 t0 t1.Type.
+                ∀a0,b0:T0.∀e0:a0 = b0.
+                ∀a1:T1 a0.∀b1:T1 b0.∀e1:r1 ?? ?? e0 a1 = b1.
+                ∀a2:T2 a0 a1.∀b2:T2 b0 b1.
+                ∀e2: r2 ????? e0 ?? e1 a2 = b2.
+                T3 a0 a1 a2 → T3 b0 b1 b2.
+intros 12;intro e2;intro H;
+apply (eq_rect' ????? e2);
+apply (R2 ?? ?? (λy0,p0,y1,p1.T3 y0 y1 (r2 T0 T1 T2 a0 y0 p0 a1 y1 p1 a2)) ? e0 ? e1);
+simplify;assumption;
+qed.
+
+
+apply (R2 ?? (λy0,p0,y1,p1.T3 y0 y1 (r2 T0 T1 T2 a0 y0 p0 a1 y1 p1 a2)) ??? e0 e1);
+simplify;
+                
+                
+                
+                
+                
+  λT0:Type.λT1:T0 → Type.λT2:∀t0:T0.∀t1:T1 t0.Type.
+  λT3:∀t0:T0.∀t1:T1 t0.∀t2:T2 t0 t1.Type.
+
+  λa0,b0:T0.
+  λe0:a0 = b0.
+
+  λa1:T1 a0.λb1: T1 b0.
+  λe1:r1 ???? e0 a1 = b1.
+
+  λa2:T2 a0 a1.λb2: T2 b0 b1.
+  λe2:r2 ????? e0 ?? e1 a2 = b2.
+ 
+  λso:T3 a0 a1 a2.
+  eq_rect' ?? (λy,p.T3 b0 b1 y) 
+    (eq_rect' ?? (λy,p.T3 b0 y (r2 ??? ??e0 ??p a2)) 
+       (eq_rect' T0 a0 (λy.λp:a0 = y.T3 y (r1 ?? a0 y p a1) (r2 ??? ??p  a2)) so b0 e0) 
+    ? e1)
+  ? e2.
+
+let rec iter_type n (l1 : lista dei nomi fin qui creati) (l2: lista dei tipi dipendenti da applicare) ≝
+  match n with
+  [ O ⇒ Type
+  | S p ⇒ match l2 with
+    [ nil ⇒ Type (* dummy *)
+    | cons T tl ⇒ ∀t:app_type_list l1 T.iter_type p (l1@[t]) tl ]].
+  
+lemma app_type_list : ∀l:list Type.∀T:iter_type l.Type.
+intro;
+elim l
+[apply i
+|simplify in i;apply F;apply i;apply a]
+qed.
+
+definition type_list_cons : ∀l:list Type.iter_type l → list Type ≝
+  λl,T.app_type_list l T :: l.
+
+let rec build_dep_type n T acc ≝
+  match n with
+  [ O ⇒ acc
+  | S p ⇒ 
+Type → list Type → Type.
+  λta,l.match l
+
+inductive II : nat → Type ≝
+| k1 : ∀n.II n
+| k2 : ∀n.II n
+| k3 : ∀n,m. II n → II m → II O.
+
+inductive JJ : nat → Type ≝
+| h1 : JJ O
+| h2 : JJ (S O)
+| h3 : ∀n,m. JJ n → JJ m → JJ O.
+
+(*
+
+lemma test: h3 ?? h1 h2 = h3 ?? h2 h1 → True.
+intro;
+letin f ≝ (λx.S (S x));
+cut (∃a,b.S a = f b);
+[decompose;cut (S (S a) = S (f a1))
+ [|clear H;destruct;
+cut (∀→ True)
+[elim Hcut;
+qed.
+*)
+
+definition IId : ∀n,m.II m → II n → Type ≝
+ λa,b,x,y.match x with
+ [ k1 n ⇒ match y with
+   [ k1 n' ⇒ ∀P:Type.(n = n' → P) → P
+   | k2 n' ⇒ ∀P:Type.P
+   | k3 m n p' q' ⇒ ∀P:Type.P ] 
+ | k2 n ⇒ match y with
+   [ k1 n' ⇒ ∀P:Type.P
+   | k2 n' ⇒ ∀P:Type.(n = n' → P) → P
+   | k3 m' n' p' q' ⇒ ∀P:Type.P ]
+ | k3 m n p q ⇒ match y with
+   [ k1 n' ⇒ ∀P:Type.P
+   | k2 n' ⇒ ∀P:Type.P
+   | k3 m' n' p' q' ⇒ ∀P:Type.(∀e1:m = m'.∀e2:n = n'. (eq_rect ??? p ? e1) = p' 
+     → (eq_rect ??? q ? e2) = q' → P) → P ]].
+
+lemma IInc : ∀n,x,y.x = y → IId n n x y.
+intros;rewrite > H;elim y;simplify;intros;
+[apply f;reflexivity
+|apply f;reflexivity
+|apply f;reflexivity]
+qed.
+
+inductive I1 : nat → Type ≝
+| kI1 : ∀n.I1 n.
+
+inductive I2 : ∀n:nat.I1 n → Type ≝
+| kI2 : ∀n,i.I2 n i.
+
+inductive I3 : Type ≝
+| kI3 : ∀x1:nat.∀x2:I1 x1.∀x3:I2 x1 x2.I3.
+
+definition I3d: I3 → I3 → Type ≝ 
+λx,y.match x with
+[ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
+  [ kI3 u1 u2 u3 ⇒ ∀P:Type.
+    (∀e1: t1 = u1.
+     ∀e2: (eq_rect ?? (λx.I1 x) t2 ? e1) = u2.
+     ∀e3: (eq_rect' ?? (λy,p.I2 u1 y)
+            (eq_rect' ?? (λy,p.I2 y (eq_rect ?? (λx.I1 x) t2 ? p)) t3 ? e1) 
+            ? e2) = u3.P) → P]].
+
+lemma I3nc : ∀a,b.a = b → I3d a b.
+intros;rewrite > H;elim b;simplify;intros;apply f;reflexivity;
+qed.
+
+definition KKd : ∀m,n,p,q.KK m n → KK p q → Type ≝
+ λa,b,c,d,x,y.match x with
+ [ c1 n ⇒ match y with
+   [ c1 n' ⇒ ∀P:Type.(n = n' → P) → P
+   | c2 n' ⇒ ∀P:Type.P
+   | c3 m' n' p' q' h' i' ⇒ ∀P:Type.P ] 
+ | c2 n ⇒ match y with
+   [ c1 n' ⇒ ∀P:Type.P
+   | c2 n' ⇒ ∀P:Type.(n = n' → P) → P
+   | c3 m' n' p' q' h' i' ⇒ ∀P:Type.P ]
+ | c3 m n p q h i ⇒ match y with
+   [ c1 n' ⇒ ∀P:Type.P
+   | c2 n' ⇒ ∀P:Type.P
+   | c3 m' n' p' q' h' i' ⇒ 
+     ∀P:Type.(∀e1:m = m'.∀e2:n = n'. ∀e3:p = p'. ∀e4:q = q'. 
+     (eq_rect ?? (λm.KK m n') (eq_rect ?? (λn.KK m n) h n' e2) m' e1) = h' 
+     → (eq_rect ?? (λp.KK p q') (eq_rect ?? (λq.KK p q) i ? e4) ? e3) = i' → P) → P ]].
+     
+lemma KKnc : ∀a,b,e,f.e = f → KKd a b a b e f.
+intros;rewrite > H;elim f;simplify;intros;apply f1;reflexivity;
+qed.
+
+lemma IIconflict: ∀c,d.
+  k3 c d (k1 c) (k2 d) = k3 d c (k2 d) (k1 c) → False.
+intros;apply (IInc ??? H);clear H;intro;
+apply (eq_rec ????? e1);
+intro;generalize in match e1;elim
+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);
+simplify;intro;
+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);
+simplify;intro;
+
+generalize in match H1;
+apply (eq_rect' ?? (λx.λp.eq_rect ℕ c II (k1 c) x p=k2 x→False) ?? e1);
+simplify;intro;destruct;
+qed.
+
+elim e1 in H1;
+